Axiom Math、群の分類を証明する4,310万行のLean証明を公開

Axiom Mathは2026年10月27日、有限単純群の分類について、同社が「初の完全なコンピューター検証済み証明」と呼ぶものを公開すると発表した。この証明は、数十のAIエージェントの群れを指揮するエンジニアと数学者が24日間で作成したもので、Lean証明支援系で約4,310万行のコードが書かれた。

同社は発表で、「本日、有限単純群の分類（CFSG）について、初の完全なコンピューター検証済み証明を公開します」と記した。この分類は有限群の基本的な構成要素を特定するもので、元の証明は約100人の数学者による500本を超える論文にまたがり、約15,000ページに及ぶ。その規模から「巨大定理」という異名を持つ。

Axiomが公開したもの

CFSGによると、すべての有限単純群は、素数位数の巡回群、5個以上の文字上の交代群、有限体上に構成されるリー型群の16の無限系列のいずれか、またはちょうど26個ある孤立した散在群のいずれかである。発表によれば、著者によってはティッツ群を27番目の群として数える。最大の散在群であるモンスター群は、196,884次元の代数を用いて、ロバート・グリースが1980年に構成した。

人間による証明の取り組みは数十年に及んだ。1963年、ウォルター・ファイトとジョン・トンプソンは、すべての非可換有限単純群の位数が偶数であることを証明した。その論文は255ページに及び、『Pacific Journal of Mathematics』の一号全体を占めた。ダニエル・ゴレンスタインは1972年、分類を完成させるための16段階の計画を示し、1983年に完成を宣言した。しかし、準薄群の場合はジェフリー・メイソンの未完の原稿に依拠しており、マイケル・アシュバッハーとスティーブン・スミスが2004年に1,221ページの論文を発表して、後に第一世代の証明と呼ばれるものを締めくくった。ゴレンスタインとリチャード・ライオンズが始め、後にロナルド・ソロモンとインナ・カプデボスクが加わった、より体系的な第二世代の証明は、いまも未完成である。そのためAxiomは第一世代の証明を形式化した。

プロジェクトのページでは、この形式化は第一世代の証明に沿っており、すべての論理的なステップがLeanのカーネルで検証されると説明されている。また、Leanのコード4,310万行、宣言205万件、コーパスに収録された論文・書籍715点が記載されている。Axiomによると、証明の見取り図は第二世代の書籍を参考に作成され、形式化には以前のQiuzhen-CFSGプロジェクトのコード約120万行も組み込まれている。また、数百人の貢献者による成果として同社が謝意を示すMathlibを基盤としている。プロジェクトでは、ディーン・キュアトン、ヴァシリー・イリン、バビク・メータ、ニールス・フォスが主要な貢献者として挙げられ、レットン・ホンが主任研究者を務める。

公開GitHubリポジトリでは、この成果を「sorry」を含まないLean4証明と説明している。バージョン4.35.0-rc3に固定され、MathlibとTauCetiプロジェクトを基盤とし、標準公理のClassical.choice、propext、Quot.soundのみを使用しており、native_decideは使っていない。TauCetiから引用した分類の形式的な記述は、「すべての有限単純群は、分類リストに明示的に構成された群のいずれかと同型である」となっている。READMEによると、lake buildで開発全体を検査できる。また、Lakeビルドツールへの公開中の変更と、チームが上流に取り込む予定の最適化によって、ビルド時間は24時間未満になった。コードにはApache-2.0ライセンスが適用されている。

24日間にわたるエージェント群の取り組み

2026年10月1日、Axiomはプロジェクトの調整に向けてSlackチャンネルを開設した。既存のLean関連の成果と、公開文献をもとに作成した社内の証明の見取り図により、取り組みは108のマイルストーンと約380の小規模なタスクに分割された。最初のエージェント群は2026年10月2日に稼働し、エージェントはGitHubのイシューを通じてマイルストーンを引き受け、完了した作業をSlackで報告した。主導するエージェントは難しい論証を分解し、記述を確認する一方、ほかのエージェントは既存の結果を探したり、Leanの証明を書いたりした。また、エージェントは不足している前提となる結果の証明を別のエージェントに委ねることができ、その成果は共有リポジトリに取り込まれた。

初期の進展によって、弱点が明らかになった。一見すると取り組みやすそうなマイルストーンの中に、エージェントが証明せずに仮定していた膨大な前提が隠れていることがあり、チームはそうした仮定に基づく数万行のコードを削除し、より確かな計画でやり直した。初期のマイルストーンの一つはシグナライザー関手定理に関するもので、その証明案は、なお正当化が必要な構造上の仮定に依存していた。エージェントがLeanの再検証能力を上回る速度で証明を作成したため、ビルド時間もボトルネックになった。Axiomによると、エンジニアはキャッシュ済みのビルド結果を複数のワーカーに分散し、独立した検査を並行して実行するとともに、負荷の大きい有限計算を、個別に検証できる証明書として外部化した。同社は、こうした変更により検証速度が桁違いに向上したとしている。

同社によると、2026年10月10日、チャンネルに投稿されたメッセージで、エージェントがモンスター群の単純性を証明したと発表された。エージェントはさらに、グリース代数を通じてモンスター群の存在を形式化し、モンスター型の群をモンスター群と同定する定理も形式化した。2026年10月13日に完了したマイルストーンは一つだけだったため、エンジニアは計画の見直しに着手し、未完了のマイルストーンを、より小さく厳密に記述された定理に分割した。各分割では、短いLeanの証明を通じて、分割した各部分から元のマイルストーンをどのように導けるかを示すことが求められた。

公刊済みの証明で見つかった欠落

証明をLeanに翻訳する過程で、公表済みの論証に問題が見つかったとAxiomは報告している。その大半は、誤植、表の誤り、仮定の脱落など軽微なものだったが、同社は公表記録との重要な相違を34件数え、そのうち最も重大なものは「不均衡群定理（UGT）」に関するものだった。

一例は、AschbacherとSmithの準薄群に関する巻に見つかった。そこでは、ある補題が2つの数値は等しいと主張していた。エージェントは群SL₂(5)に関する反例を発見した。この群では、一方の数値が1であり、主張された等式が要求する2とは異なっていた。等式を不等式に置き換えることで補題は修正されたが、後続の論証では等式を使って特定のケースを除外していたため、チームはそれらの配置も扱えるよう、先行する論証の適用範囲を広げた。

UGTは、部分群に関する情報から群全体を特定するのに役立つ。付随する論文の要旨によると、分類の帰納法の仮定のもとでは、対合の中心化群の中で正規となる非自明な奇数位数の部分群が存在すれば、その全体群である単純群は、奇標数のリー型か、特定の次数の交代群であることが導かれる。AxiomはJohn Walterの1986年の回顧録を通じてUGTに取り組み、その論証を形式化する過程で、そこで用いられていた閉包性の主張に明示的な反例を発見した。すなわち、関連する単純群を所定の族にとどめると仮定されていた操作によって、その族から明確に除外される群が生じる場合があった。

同社の説明によると、出発点となるのはPSL₂(49)であり、その体の対合の中心化群はPGL₂(7)である。この操作によって単純成分PSL₂(7)が得られるが、7はメルセンヌ素数であるため、この群は当該族から除外される。Axiomによれば、これらの反例はUGTそのものを否定するものではなく、Walterの命題II.5.9(ii)の結論さえも否定するものではなかった。

この修正には、Solomonが1976年に提唱した極大2成分の理論が活用された。Axiomによると、この理論が、同社のAxiomProverシステムが生み出し、形式化した代替論証の中心的な着想を提供した。論文で定理2.3（単純トップの保存）として述べられている重要な段階について、Axiomは、AxiomProverが証明した群論の新たな結果だと説明している。この結果は、GilmanとSolomonによる簡約、およびFooteとHarrisによる認識定理と組み合わせることで、分類に必要なUGTの単純群版を与える。形式化の後、Axiomの数学者たちは、定理2.3を使わずに同じ結論に至る、より短い第一世代の手法による導出を見つけた。この導出は注9.5に記録されている。

Colin DefantとKen Onoが寄稿したこの論文『The Unbalanced Group Theorem』は、CC BY 4.0ライセンスのもと、2026年10月27日にプレプリントサーバーHexagonでバージョン1として公開された。プロジェクトページによると、全35ページである。Axiomは、文献で見つかった正誤情報を集約するために群論研究者と協力しており、プロジェクトの正誤表ページで公開する予定だという。分類の基盤となった研究を行ったLyonsとSolomonは、UGTの修正について意見を求められた。同社は、両氏を含む諮問委員会とともに、正誤情報の整理と解決を今後も続けるとしている。外部アドバイザーのDan Nakanoも同委員会に加わっている。Axiomは、自社の貢献を、証明を機械的に検証できるようにし、直面した障害を記録するとともに、それらを解決する形式化された論証を提示することだと位置づけている。一方で、この分類は、群を発見し論証を構築した数学者たちの功績であることに変わりはないとしている。