有限単純群の分類（CFSG）は、数学の歴史における最も重要な共同成果の一つと見なされています。この定理は、有限群論の基本的な構成要素であるすべての有限単純群が、いくつかのカテゴリーのいずれかに分類されることを示しています。それらは、素数位の巡回群、交代群、リー型群、または26の「散発的」群のいずれかです。元の証明は、数十年にもわたり、数千ページに及ぶ学術論文を通じて約100人の数学者が関与した巨大な事業であったため、その絶対的な論理的完全性を保証するための形式的検証の候補として長年注目されてきました。
この画像は、定理証明機Leanを用いて有限単純群の分類を形式化する包括的なプロジェクトを表しています。
AxiomMathの研究チームは、数学的証明を検証するために使用される関数型プログラミング言語および対話型定理証明機であるLeanを用いて、CFSGの完全な形式化を達成しました。このプロジェクトは、CFSGの「第一世代」の証明に従っており、すべての論理的ステップがLeanのカーネルによってチェックされることを保証します。この形式化は「sorry-free」であり、未証明のステップに対するプレースホルダーに依存していません。チームはTauCetiプロジェクトのCFSGの記述をベースラインとして利用し、MathlibおよびTauCetiの上に証明を構築し、`Classical.choice`、`propext`、`Quot.sound`などの標準的な公理を使用しました。
この形式化プロジェクトの最も重要な成果の一つは、既存の文献における技術的な誤りの発見でした。第一世代の証明を検証する過程で、チームはUnbalanced Group Theoremに至る公開されたルートで使用されている閉包の主張に対する反例を特定しました。これを解決するために、チームはSolomonの1976年の最大2-成分理論に基づく単純群のケースのための代替的な議論を開発しました。この発見は、形式的検証の有用性を浮き彫りにしています。人間が書いた証明を機械でチェック可能なコードに変換することで、研究者は、複雑で複数の著者による数学的著作において、さもなければ何年も発見されないかもしれない微妙なギャップを明らかにすることができるのです。このプロジェクトは現在、4,300万行以上のLeanコードで構成されており、コーパス内のさまざまな論文や書籍の間の依存関係を視覚化する対話型証明マップも含まれています。
この画像は、プロジェクトの巨大な規模と、形式化がホストされているリポジトリに関連しています。