Frontiers of Artificial Intelligence Seminar: CSLib: The Lean Computer Science Library

Abstract: Following Mathlib's success in building a shared foundation for formalized mathematics, CSLib is a community-oriented effort to build a similar infrastructure for computer science and software in the Lean theorem prover.

In this talk, I will present CSLib's current state, including its architecture, governance, organization, and how to contribute. Rather than giving only a high-level overview, I will use minimal working examples to illustrate the library's current API. I will showcase abstractions and definitions already available, ranging from computational paradigms to modeling and programming languages, logics, algorithms, and infrastructure to verify their properties.

I will also introduce the CSLib Initiative, supported by Renaissance Philanthropy, which aims to coordinate and accelerate the development of the library and its surrounding ecosystem. I will discuss the CSLib Initiative roadmap

Finally, I will show how CSLib is already being used beyond the library itself, through community projects, textbooks, courses, and large-scale verification efforts. These include Software Foundations in Lean, the Functional Algorithms Design and Computational Semantics with Lean, and the port of Amazon's s2n-bignum formal proofs to Lean.

Bio: Alexandre Rademaker is the Director of the CSLib Initiative at Renaissance Philanthropy. CSLib is a global open-source effort to build a library of formalized computer science in Lean. He also cooperates with NYU in DARPA's ExpMath program, which aims to accelerate mathematics research with AI.

Alexandre is also a professor at EMAp/FGV (Applied Mathematics School, Getulio Vargas Foundation), where he has been teaching for about 20 years. He worked at IBM Research for 12 years until April 2025, when he left to lead the Specification IDE project at Atlas Computing, part of the Formal Verification of Software initiative funded by Schmidt Sciences under their Science of Trustworthy AI program.

During his PhD, he held research fellowships at Microsoft Research, working with the Z3 SMT solver team, and at SRI International. He has published more than 100 papers and spent much of his career leading open-source research collaborations with international communities, working with computational linguistics and building language resources. He was publication chair of the Language Resources and Evaluation Conference (LREC) and has served on the boards of research associations in Brazil and internationally.

Alexandre received a PhD in Computer Science from PUC-Rio, where his thesis on proof theory for description logics was published by Springer, and is based in Rio de Janeiro.