有限单群分类定理在 Lean 中完成形式化

# 有限单群分类定理的 Lean 形式化 来源：https://cfsg.axiommath.ai/ 有限单群的分类是数学史上最伟大的集体成就之一。其第一代证明跨越数千页期刊论文，由约一百位数学家历经数十年完成。该定理表明：每个有限单群要么是素数阶循环群，要么是交错群，要么是李型群，要么属于 26 个散在群之一。 这里我们给出了遵循第一代证明的 Lean 完整形式化，每一个逻辑步骤都由 Lean 的内核校验。在此过程中，我们发现了已发表的 Unbalanced Group Theorem 论证中的一个问题。随附论文（https://cfsg.axiommath.ai/papers）解释了这一问题以及我们在证明中采用的替代路径。我们的博客文章（https://axiommath.ai/research/the-enormous-theorem-formalized/）讲述了完整的故事。 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 \*数学贡献者　†工程贡献者　◇首席研究员 ### 引用本工作 `` @misc{axiom-cfsg, author = {Cureton, Dean and Ilin, Vasily and Mehta, Bhavik and Voss, Niels and Cabral, Rafael and Defant, Colin and Gregory, Erik and Hill, Aaron and Hong, Letong and Hu, Qinheping and Jamner, Dustin and Jiang, Albert and Jordan, Tadeusz and Kurghinyan, Andranik and Lau, Kenny and Laurent, Jonathan and Liang, David and Limperg, Jannis and Mahns, Simon and Nugent, Brian and Olson, Connor and Ono, Ken and Paul, Eric and Rajan, Dhruv and Ram, Karun and Ray, Charlie and Siu, Ho Chung and Swaminathan, Ashvin A. and Thorner, Jesse and Tsaplin, Aleksey and Wang, Chenkai}, title = {Lean formalization of the classification of finite simple groups}, year = {2026}, howpublished = {\url{https://github.com/AxiomMath/CFSG}}, note = {Interactive proof map at \url{https://cfsg.axiommath.ai}} } ``` 这是 Agent Blueprint，即我们最初提供给智能体的蓝图。Lean 代码本身请参见 Lean Repo（https://cfsg.axiommath.ai/#） ### 语料库\*139 个源文献\* 1870　1950　1970　1990　2026 每个方块代表一篇论文或专著，其大小对应它所提供的命题数量。悬停可查看其命题。 ### 里程碑\*108\*