Official Announcement

Stream: CSLib

[Clark Barrett]

The following announcement went out this morning by email to the cslib-announce list as well as to a long list of people who have expressed interest. I wanted to share it also here and encourage folks to join the cslib-announce list if you aren't on it already.

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.  And for concrete suggestions on how to get involved, please see the CONTRIBUTING document in the GitHub repository.

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

[Snir Broshi]

Can you clarify the role of the Google group as opposed to this Zulip channel? Where do you expect the main collaboration to happen?

[Chris Henson]

I do not speak for the Steering Committee, but I don't think it was meant to imply anything about not using Zulip for collaboration. The contributing guidelines link you here to the Zulip.

[Clark Barrett]

The Google group is a low traffic occasional announcements list for people who aren't monitoring Zulip.

[Nadim Farhat]

Congratulations on the launch, just read the paper, exciting!