Lean 中有限單純群分類的形式化
Classification of Finite Simple Groups Formalized in Lean
本研究將有限單純群分類的原始證明完整地在 Lean 中形式化，並檢驗每一步的邏輯正確性。
- Lean 宣告量：43.1M，里程碑：2.05M，涵蓋 100 篇論文與書籍。
完整 Lean formalization 讓數學證明可機械驗證，對數學與自動化推理領域皆具重要意義，並提供 43.1M 宣告與 2.05M 里程碑的完整證明路徑。
有限簡單群的分類是數學領域最偉大的集體成就之一。其第一代證明跨越數千頁期刊文章，由約一百位數學家在數十年內完成。它證明每個有限簡單群都是質數階的迴圈群、交替群、李群型或 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†
*數學貢獻者†工程貢獻者◇首席研究員
引用此工作
@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 正式化有限簡單群分類},
year = {2026},
howpublished = {\url{https://github.com/AxiomMath/CFSG}},
note = {Interactive proof map at \url{https://cfsg.axiommath.ai}}
}
這是 Agent Blueprint，給代理的最初藍圖。若要檢視 Lean 程式碼本身，請參閱 Lean Repo
引理或定義是一個單一結果，裡面不包含任何內容。
語料庫 _139 個來源作品_
1870 1950 1970 1990 2026
每個區塊都是一篇論文或書籍，其大小取決於其提供的陳述。將滑鼠懸停即可檢視其陳述。