有限単純群の分類がLeanで形式化される
Classification of Finite Simple Groups Formalized in Lean (cfsg.axiommath.ai)
要約
数学における長年の偉業である有限単純群の分類が、Lean証明支援系を用いて完全に形式化されました。このプロジェクトは、数千ページに及ぶ既存の証明を検証し、その過程でUnbalanced Group Theoremに関する公開済みの議論に誤りを発見しました。この成果は、数学的証明の厳密性をコンピュータで検証可能にする重要な一歩です。
全文翻訳
The Classification of Finite Simple Groups, formalized in Lean
有限単純群の分類は、数学における偉大な集団的成果の一つです。その第一世代の証明は、数十年かけて約100人の数学者によって書かれ、数千ページの学術論文に及びます。この分類は、すべての有限単純群が、巡回群（素数位数）、交代群、リー型群、または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 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}}
}
これはエージェントブループリント、すなわちエージェントに与えられた初期ブループリントです。Leanコード自体については、Leanリポジトリを参照してください。
コーパス 139のソースワーク
18701950197019902026
各ブロックは、提供されたステートメントのサイズに応じた論文または書籍です。ステートメントを見つけるにはホバーしてください。