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.

翻译：我们介绍CSLib，这是一个在Lean证明助手中用于证明计算机科学相关定理及编写形式化验证代码的开源框架。CSLib旨在成为计算机科学领域的"Mathlib"，正如Lean的Mathlib之于数学。Mathlib已产生巨大影响：它是Lean在数学研究社区广受欢迎的关键原因，并在数学推理AI系统的训练中发挥了关键作用。然而，当前Lean中的计算机科学知识基础仍相当有限。CSLib将极大扩展这一知识库，并为在实际验证项目中运用这些知识提供基础设施。通过这一举措，CSLib将（1）推动Lean在计算机科学教育与研究中的广泛应用，（2）促进大规模形式化验证系统的人工及AI辅助工程。