CSLib launch

[CSLib Announce]

Dear colleagues,

We are pleased to announce the official launch of CSLib, an open-source effort to formalize computer science in the Lean 4 theorem prover. CSLib is inspired by the impact of the Mathlib project in mathematics and aims to do something similar for computer science. CSLib is broadly organized into two pillars. Pillar one involves formalizing essential computer science concepts in Lean, and pillar two involves building infrastructure in Lean for reasoning about real-world code. We expect the two pillars to inform and build off of each other. We also hope that CSLib will play an important role in advancing neurosymbolic approaches that connect modern AI with formal and symbolic reasoning.

We invite computer science researchers, practitioners, and enthusiasts to learn more and consider getting involved. The main CSLib website is: cslib.io.  To learn more about the big picture and vision of the project, you can read the CSLib white paper: https://arxiv.org/abs/2602.04846.  And for concrete suggestions on how to get involved, please see the CONTRIBUTING document in the GitHub repository: https://github.com/leanprover/cslib/blob/main/CONTRIBUTING.md

We are excited about the possibilities that this project will provide for building infrastructure, collaborations and community. We also appreciate your patience with the inevitable growing pains that a big new project like this faces. We look forward to working together with many of you to make this vision a reality.

Best Regards,

The CSLib Steering Committee

Clark Barrett, Stanford University and Amazon Scholar

Swarat Chaudhuri, Google DeepMind and UT Austin

Fabrizio Montesi, FORM and DIAS, University of Southern Denmark

Jim Grundy, Amazon

Pushmeet Kohli, Google DeepMind

Leo deMoura, Amazon and Lean FRO