About

Lean CS Library

We propose to build CSLib, an open-source library of computer-science-related formalizations for the Lean 4 proof assistant. CSLib aims to be for computer science what Lean’s Mathlib is for mathematics. Mathlib has been tremendously impactful: it is a key reason for Lean's popularity within the mathematics research community, and it was also critical for AI-for-math projects such as AlphaProof. However, the base of computer science knowledge in Lean is currently quite limited. By enhancing this knowledge base, CSLib will help human computer scientists design algorithms and software systems with strong correctness and security guarantees, and also simplify the creation of AI systems that automate such design.