图
颜色
有限单群的分类是数学界最伟大的集体成就之一。其第一代证明横跨数千页期刊篇幅，由约一百位数学家在数十年间写成。它表明每个有限单群要么是素数阶循环群，要么是交错群，要么是李型群，要么是26个散在群之一。
在此我们给出遵循第一代证明的完整 Lean 形式化，每一步逻辑都由 Lean 的内核检查。在此过程中，我们发现了已发表的关于非平衡群定理（Unbalanced Group Theorem）论证中的一个问题。配套论文解释了该问题以及我们证明中采用的替代路线。我们的博客文章讲述了完整经过。
Lean 代码行数
43.1M
声明数
2.05M
里程碑
100
论文与书籍
715
核心贡献者Dean Cureton*†, Vasily Ilin†, Bhavik Mehta*†, Niels Voss†
其他贡献者Rafael Cabral†, Colin Defant*, Erik Gregory†, Aaron Hill†, Letong Hong◇, Qinheping Hu†, Dustin Jamner†, Albert Jiang†, Tadeusz Jordan†, Andranik Kurghinyan†, Kenny Lau*†, Jonathan Laurent†, David Liang†, Jannis Limperg†, Simon Mahns†, Brian Nugent*, Connor Olson†, Ken Ono*, Eric Paul†, Dhruv Rajan†, Karun Ram†, Charlie Ray†, Ho Chung Siu†, Ashvin A. Swaminathan*†, Jesse Thorner*, Aleksey Tsaplin†, Chenkai Wang†
*数学贡献者†工程贡献者◇首席研究员
这是 Agent Blueprint，即我们最初交给智能体的蓝图。关于 Lean 代码本身，请参见Lean 仓库
语料库139 部源作品
18701950197019902026
每个方块代表一篇论文或一本书，其大小由它提供的陈述数量决定。悬停可查看其陈述。