AIエージェント群、1万5000ページの有限単純群分類を24日で検証

AI数学スタートアップのアクシオム(Axiom)は、人間による証明が約1万5000ページに及ぶ「有限単純群の分類定理」について、AIエージェント群を使って初めて完全なコンピューター検証を終えたと発表した。2026年10月26日付の研究記事によると、エージェントは24日間で証明支援系Leanのコードを約4310万行書き、同社はコードをGitHubで公開した。

要点

• アクシオムは第1世代の証明全体をLeanで形式化したとし、規模は約4310万行、宣言数は205万に上る。
• GitHubのリポジトリは、証明に未証明の箇所を示す「sorry」がなく、Leanの標準公理3つだけに依拠すると記している。
• 作業の過程で既存文献との重要な食い違いが34件見つかり、1986年の論文にあった誤った主張も含まれる。

有限単純群の分類定理とは

有限単純群は有限の対称性を形づくる基本単位で、対称性の「周期表」とも呼ばれる。分類定理は、すべての有限単純群が素数位数の巡回群、交代群、16系列のリー型群、26個の散在型単純群のいずれかであると述べる。散在型で最大のものが「モンスター群」である。

アクシオムによると、この証明は約100人の数学者による500本超の論文に分散している。ダニエル・ゴーレンスタインは1983年に分類の完了を宣言したが、時期尚早だった。残る穴は2004年、マイケル・アッシュバッハーとスティーブン・スミスが準薄(quasithin)群に関する1221ページの証明を発表して埋まった。より簡潔な「第2世代の証明」はまだ完成していない。

AIエージェントはLean証明をどう組み上げたか

アクシオムは作業を108のマイルストーンと約380の小タスクに分割した。10月1日にSlackチャンネルを開設し、10月2日に最初のエージェント群を稼働させた。エージェントは10月10日にモンスター群が単純群であることを証明した。ただ10月13日時点で完了したマイルストーンは1つだけで、計画を立て直す必要に迫られた。

同社はエージェントが「入れ替わる複数のモデルの組み合わせ」を使ったと説明するにとどめ、モデル名や計算資源、費用は明らかにしていない。作業は数学ライブラリMathlibを土台とし、先行するQiuzhen-CFSGプロジェクトのコード約120万行を取り込んだ。

GitHubのリポジトリはLean v4.35.0-rc3に固定され、Classical.choice、propext、Quot.soundの3公理のみを使い、native_decideは使わない。ライセンスはApache 2.0である。同社はフルビルドを24時間以内に収めることを目指すとしている。

既存の証明で見つかった誤り

最も大きな問題は「アンバランス群定理(UGT)」の部分で見つかった。アクシオムによると、アッシュバッハーとスミスの研究にある補題がSL₂(5)で成り立たず、ウォルターの1986年の論文にある閉包に関する主張がPSL₂(49)で破綻する。ただし、いずれの反例も定理そのものを覆すものではなく、別の経路で論証を修正し、そのために新たな結果も証明したという。

分類プログラムに携わった群論研究者のリチャード・ライオンズ氏とロン・ソロモン氏が、ダン・ナカノ氏とともにこの修正に助言した。

ファイト・トンプソンからエージェント群へ

これまでの代表例はファイト・トンプソンの定理である。255ページに及ぶこの証明は、ジョルジュ・ゴンティエ氏のチームが6年をかけ、2012年にCoqで検証した。アクシオムの主張は規模がはるかに大きく、期間はわずか数週間だ。AIによる数学成果の発表が相次ぐなかでの発表となる。

今後の焦点

現時点で主張はすべてアクシオム側の発表であり、外部の研究グループが証明を再ビルドして確認したという報告はまだない。同社自身も、形式化された命題が意図した定理を正しく表しているかは人間が確認する必要があるとしている。誤り一覧の整理は諮問委員会の下で続ける方針だ。

よくある質問

AIが分類定理を新たに発見したのか
そうではない。アクシオムは、定理はそれを証明した数学者たちの業績だとしている。エージェントは既存の証明を機械で検査できるコードに置き換えた。

証明は独立に検証されたのか
アクシオムによれば、Leanのカーネルがすべての手順を検査し、コードも公開されている。形式化された命題が正しいかについての外部確認は、まだ報告されていない。

参考資料

• Formalizing the Enormous Theorem — Axiom(2026年10月26日)
• The Classification of Finite Simple Groups, formalized in Lean — Axiom
• AxiomMath/CFSG — GitHub
• Axiom Math Releases 43.1M-Line Lean Proof of Group Classification — Unite.AI(2026年10月27日)
• Classification of finite simple groups — Wikipedia