CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai
cs.LO
Feb 4, 2026 · v1
TL;DR
Introduces CSLib, an open-source Lean computer-science library aiming to be the CS counterpart of Mathlib.
Abstract
We introduce CSLib, an open-source framework for proving computer-science-related theorems and writing formally verified code in the Lean 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 has also played a critical role in the training of AI systems for mathematical reasoning. However, the base of computer science knowledge in Lean is currently quite limited. CSLib will vastly enhance this knowledge base and provide infrastructure for using this knowledge in real-world verification projects. By doing so, CSLib will (1) enable the broad use of Lean in computer science education and research, and (2) facilitate the manual and AI-aided engineering of large-scale formally verified systems.
Problem
Lean's Mathlib has been transformative for mathematics formalization, but the base of computer science knowledge in Lean is quite limited, lacking a unified library for CS theory and verified algorithms.
Approach
CSLib is an open-source framework for proving computer-science-related theorems and writing formally verified code in Lean. It aims to be for computer science what Mathlib is for mathematics, covering algorithms, complexity theory, programming languages, and other CS foundations. The project incorporates AI assistance for proof generation and community-driven contributions.
Results
The project establishes a governance model, roadmap, and initial library covering several CS domains. It is designed to serve both as a knowledge base for CS formalization and as training data for AI systems reasoning about computer science.
