Amazon（亚马逊）；Stanford University（斯坦福大学）；Google DeepMind（谷歌DeepMind）；The University of Texas at Austin（德克萨斯大学奥斯汀分校）；FORM, University of Southern Denmark（南丹麦大学FORM）；Lean FRO；Atlas Computing（阿特拉斯计算）；Getulio Vargas Foundation（热图利奥·瓦加斯基金会）；Institute for Theoretical Studies, ETH Zürich（苏黎世联邦理工学院理论研究所）
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai
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.
New York University（纽约大学）；Aarhus University（奥胡斯大学）；ETH Zurich（苏黎世联邦理工学院）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究所）；Chalmers（查尔姆斯理工大学）
Université Paris Cité and Sorbonne Université, CNRS, IMJ-PRG（巴黎西岱大学与索邦大学，法国国家科学研究中心，数学与计算机研究所）；Université Paris Cité, CNRS, Institut de recherche en informatique fondamentale（巴黎西岱大学，法国国家科学研究中心，基础信息学研究所）
LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
Yau Mathematical Sciences Center, Tsinghua University（清华大学尤洋数学科学中心）；Iluvatar CoreX；Department of Mathematics, Southern University of Science and Technology（南方科技大学数学系）；Westlake Institute for Advanced Study, Westlake University（西湖研究学院）；Qiuzhen College, Tsinghua University（清华大学齐臻学院）；Department of Physics, The Chinese University of Hong Kong（香港中文大学物理系）；Yanqi Lake Beijing Institute of Mathematical Sciences and Applications (BIMSA)（燕琦湖北京应用数学研究所（BIMSA））
MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
Department of Computer Science, University of Virginia（弗吉尼亚大学计算机科学系）；Astronomy , California Institute of Technology（加州理工学院天文学系）；Purdue University（普渡大学）；Massachusetts Institute of Technology（麻省理工学院）
A Machine-Verified Proof of a Quantum-Optimization Conjecture
Center of Mathematical Sciences and Applications, Harvard University（哈佛大学数学科学中心）；MIT Center for Theoretical Physics - a Leinweber Institute（麻省理工学院理论物理中心 - 莱因韦伯研究所）；Research Laboratory of Electronics, Massachusetts Institute of Technology（麻省理工学院电子研究实验室）
