有限単純群の分類のLeanによる形式化：Axiomの証明が確かめること、人に残ること

Axiom Mathは、有限単純群の分類（CFSG）について「コンピュータが検査した初めての完全な証明」を作ったとしています。CFSGは、その証明が数学で最も長いとよく言われる定理です。同社の研究記事¹によれば、同社のエンジニアと数学者は24日間にわたって「数十のAIエージェントからなる群れ（swarm）を指揮し」、エージェントたちは約4,310万行のLeanを書きました。Leanは、証明の一歩一歩をコンピュータが検査する言語です。その過程でエージェントは、分類の鍵となる結果の1つに至る1986年の道筋のうち、ある1つのステップに反例を見つけ、Axiomはそのステップのための新しい議論を公開しました。研究記事の日付は2026年10月26日です。10月27日にコード²、論文⁵、Xでの発表が続き、10月28日に57ページの正誤表（errata）⁴が公開されました。

Xでの発表は、「人類史上最大の数学の証明が、コンピュータで検証された」という一文で始まります。⁶これは正確な主張ですが、聞こえるよりも狭い主張です。Leanが検査するのは、証明が形式的な命題と短い公理のリストから一歩ずつ導かれることです。その形式的な命題が、群論の研究者がCFSGと呼ぶものを述べているかどうかや、Axiomが公開した正誤表の96項目が正しいかどうかは検査しません。また10月30日の時点で、Axiomの外の誰かが検査を再実行したという報告は見つかりませんでした。Axiom自身も、命題とビルドについて外部からの確認を呼びかけ、正誤表への訂正を求めています。

以下では、定理が何を述べているか、Axiomが何を公開したか、Leanのファイルが何を立証しているか、Axiomが文献の中に何を見つけたか、文書によって数字がどう違うか、そして何が人に残されているかを順に紹介します。出典はすべて2026年10月30日に確認しました。

有限単純群の分類とは何か#

群とは、組み合わせたり元に戻したりできる対称性の集まりです。Axiomの記事は立方体を例にしています。24通りの回転は立方体の見た目を変えず、そのうち2つを続けて行うと24通りのうちの別の1つになり、どの回転も逆向きに戻せます。¹整数が素数に分解されるように、有限群はそれ以上分解できない部品に分解されます。その部品が有限単純群です。

CFSGは、それらをすべて列挙します。Axiom自身の論文の言葉では、「すべての有限単純群は、素数位数の巡回群、n ≥ 5 の交代群 A_n、リー型の単純群、26個の散在型単純群のいずれかである」。⁵最大の散在型単純群であるモンスター群は、約 8 × 10^53 個の元を持ちます。

難しいのは証明です。Axiomの記事は、それを「約100人の数学者による500本以上の論文、およそ1万5,000ページ」と説明しています。Daniel Gorensteinは1983年に分類の完成を宣言しましたが、1つの場合、つまり準薄群（quasithin groups）の場合は、Michael AschbacherとStephen Smithが2004年に1,221ページの論考を出版するまで未解決のままでした。Gorenstein、Richard Lyons、Ronald Solomon、のちにInna Capdeboscqも加わった第2世代の証明は、今も刊行が続いています。記事によれば2023年までに10巻が出ており、少なくとも12巻になる見込みです。Axiomの発表スレッドは、問題をこう表現しています。「全体を読んだ人は1人もいない。大きすぎるのだ」。⁶

Axiomは何を発表したのか#

10月1日、Axiomはプロジェクトを調整するためのSlackチャンネルを開き、10月2日に最初のエージェントの「群れ」が動き始めました。¹既存のLeanの成果と、文献から組み立てた証明の地図をもとに、プロジェクトは108のマイルストーンと約380の小さなタスクに分けられました。「主導役のエージェントは難しい議論を分解し、形式化される命題を確認した」一方で、ほかのエージェントは既存の結果を探したり、Leanの証明を書いたりしました。10月10日、チャンネルには「モンスター群が単純であることを証明した」という書き込みがありました。すべてが前に進んだわけではありません。いくつかのマイルストーンは、エージェントが「証明せずに仮定していた」前提に依存していたことが分かり、「その仮定の上に築かれた数万行を削除した」とされています。

AIの側について、記事は「エージェントは入れ替わる複数のモデルを組み合わせて使い、調整のためのツールがその作業を支えた」としか述べていません。モデルの名前は挙げていません。人の側については、「人間の数学者は数学的な障害を調べ、エンジニアは拡大していくシステムが成果を出し続けられるようにした」とあります。プロジェクトのサイトには31人の貢献者が載っており、そのうち4人が中心的な貢献者とされています。³

形式化は、Leanの主要な数学ライブラリであるMathlibと、後で説明するもう1つのライブラリTau Cetiの上に築かれています。記事によれば、先行する公開プロジェクトQiuzhen-CFSGの約120万行も取り込まれています。Qiuzhen-CFSGのREADMEは、Feit–Thompsonの定理、Bender–Suzukiの定理、Gorenstein–Walterの定理を完成済みとしています。¹⁴

公開は、いくつかに分かれていました。

公開物	日付	内容
研究記事1「Formalizing the Enormous Theorem」	10月26日付	経緯、数字、文献で見つかったこと
Xのスレッド6、@axiommathai	10月27日 14:34（UTC）	発表と、確認の呼びかけ
GitHubリポジトリ2 AxiomMath/CFSG	10月27日。コミットは1つ、15:07（UTC）	Leanのコード、Apache-2.0ライセンス
The Unbalanced Group Theorem5、Hexagon 2610.00575v1	10月27日	新しい議論についての35ページの論文
Selected Departures from Published Arguments4	10月28日	正誤表：57ページ、96項目

Leanのファイルは実際に何を立証しているのか#

命題と、その出どころ

リポジトリの看板となる定理、Comparator/Solution.lean の CFSGComparator.classification は、TauCeti.ClassificationStatement を証明します。README²は、この命題を次のように引用しています。

def ClassificationStatement : Prop :=
  ∀ (G : Type u) [Group G] [Finite G] [IsSimpleGroup G],
    ∃ i : CFSGIndex, Nonempty (G ≃* i.Group)

言葉にすると、すべての有限単純群 G について、リストのある項目 i があり、G はその項目が定義する群と同型である、ということです。リスト CFSGIndex の項目は4種類あります。素数位数の巡回群、次数5以上の交代群、明示的な代数的データから作られるリー型の群、そして26個の散在型単純群です。散在型単純群はそれぞれ、有限表示（生成元と、それらの間の関係式）で与えられています。

この命題を書いたのはAxiomではありません。出どころはTau Ceti¹¹で、「Lean FROとMathlib Initiativeがインキュベートした」Leanのライブラリです。そこでは「ロードマップは人間が受け持ち」、「コードはAIが受け持つ」とされています。この命題についてのTau Cetiのロードマップは2026年8月8日に追加され、¹³命題そのものは9月25日にマージされました。¹²AxiomのリポジトリはTau Cetiを10月2日のコミットに固定しています。つまりこの命題は別のプロジェクトのために書かれたもので、10月1日にAxiomのプロジェクトが始まる前から公開されていました。

この命題は一方向です。すべての有限単純群がリストに載っている、と述べるだけです。Tau Cetiのファイル¹²は、何を扱わないかを明記しています。「列挙された台（carrier）の有限性や単純性は、ここでは何も主張しない」。Tau Cetiのロードマップは、列挙された群の「有限性、単純性、位数」を「下流の作業」に委ねています。Axiomのリポジトリは、Axiom自身の定義を使った、より広い2つ目の定理も証明しており、そちらはリストの群が有限かつ単純であることも加えています。²その定理を読むには、Axiomの定義も読む必要があります。

公理、そしてnative_decideを使わないこと

READMEによれば、証明は「標準的な公理 Classical.choice、propext、Quot.sound（native_decide は使わない）」を使っています。それぞれ選択公理、命題外延性、商の健全性です。Leanはどの定理についても、それが依存する公理を一覧にできるので、余分な隠れた仮定があれば表に出ます。

native_decide は、大きな計算のための近道です。Leanのリファレンス¹⁶は、それが「Leanのコンパイラ全体を信頼される部分に加え、#print axioms に新しい公理が現れる」と警告しています。これを使わなければ、信頼される部分は、すべての証明を検査するLeanのカーネルと3つの公理だけにとどまります。Axiomによれば、コストの高い有限の計算は「別に検査できる証明書（certificate）」に移しました。私たちが開いた証明書のファイルは decide +kernel を使っており、これは計算そのものをカーネルに行わせるものです。

sorryがないこと、Leanのバージョン

Leanでは、sorry は「未完成のタクティク証明のための一時的なプレースホルダー」です。¹⁶sorry を含むファイルも警告付きでコンパイルされ、それに依存するすべての定理に公理 sorryAx が付きます。「sorry-free（sorryがない）」とは、どのステップもプレースホルダーのまま残されていないということで、上の公理のリストがその確認になります。そこに sorryAx はありません。リポジトリのメタデータのファイルには sorry_count: 0 と記録されています。

意図的な sorry は1つだけで、Comparator/Challenge.lean にあります。このファイルは、目標とする命題を証明なしで述べるものです。設定ファイルがLeanのコンパレータ（comparator）ツールに、解答がまさにその命題を、許された3つの公理だけを使って証明していること、そしてカーネルがそれを受理することを確認させます。ツールのREADME¹⁵によれば、Lean 4.35.0以降、この確認は lake comparator としてLeanに同梱されています。

プロジェクトはリリース候補版のLean v4.35.0-rc3でビルドされ、MathlibとTau Cetiを特定のコミットに固定しているので、再ビルドでも同じツールチェーン、ライブラリ、命題を使えます。

同じメタデータのファイルには、作業がどう確認されたかも書かれています。status: self-assessed（自己評価）、reviewers: ["Axiom Math"]、自動化については method: autonomous、framework: "AxiomProver" です。

Leanのカーネルが検査すること	人がまだ確かめなければならないこと
最終的な定理から3つの公理までさかのぼる、すべての推論	ClassificationStatement とそのリストの定義がCFSGを意味していること
どのステップも sorry のまま残されていないこと	公開されたファイルから、ほかの人のマシンでビルドが成功すること
証明書のファイルの中の有限の計算	正誤表の96項目がそれぞれ正しいか、新しいものか
	形式化が歴史的な証明を一歩ずつたどっているか

最後の行について、記事自身がこう書いています。「形式的な展開が特定の歴史的な議論の各ステップを再現しているかどうかは、別の問題である」。¹

Axiomは文献の中に何を見つけたのか#

エージェントは、作業を進めながら問題の疑いを記録していきました。記事によれば、その大半は「無害だと分かった。誤植、表の誤り、抜け落ちた仮定、文脈から明らかなステップなどだ。いくつかは本当の数学を必要とした」。¹AschbacherとSmithの準薄群の巻にある1つの補題では、群 SL₂(5) について、「主張された等式では2であるべきところで、ある量が1だった」とされています。

非平衡群定理

最も大きな事例は、非平衡群定理（Unbalanced Group Theorem、UGT）に関するものです。Axiomの論文は、それをこう要約しています。分類の帰納法の仮定のもとで、「対合の中心化群において正規な、奇数位数の非自明な部分群があると、それを含む単純群は、奇標数のリー型の群か、特定の次数の交代群のいずれかでなければならない」。⁵対合とは、位数2の元のことです。論文の言葉では、「したがってUGTは、残りの分類問題からすべての非平衡群を取り除く」。

Axiomは第1世代の証明に従うことを選んだため、UGTに至る公刊された道筋の1つである、John Walterの1986年の長編論文（memoir）を読み進めました。Walterは、q が奇数で、9、フェルマー素数、メルセンヌ素数を除く、群 PSL₂(q) の族を定義しています。彼の議論は、ある操作、つまり対合の中心化群の成分を取る操作をしても、その族の中にとどまると主張しています。エージェントは、対合が体の自己同型である場合にはそうならないことを見つけました。

Walterの族の群	中心化群の成分	族の外にある理由
PSL₂(49)	PSL₂(7)	7はメルセンヌ素数
PSL₂(81)	PSL₂(9)	9は明示的に除かれている
PSL₂(289)	PSL₂(17)	17はフェルマー素数

論文は範囲に慎重です。「すなわち、私たちが特定したのはこの推論の隙間であって、命題そのものやUGTへの反例ではない」。また「この困難はCFSGを妨げない」とし、UGTへのほかの道筋を挙げています。Morton Harrisの議論に従った、Gorensteinの1983年の巻での説明と、Gorenstein、Lyons、Solomonの第2世代の研究からの導出です。

Hexagonに置かれた新しい議論

Axiomには、組み立てていた第1世代の証明に合う代わりの議論が必要でした。その成果がThe Unbalanced Group Theorem⁵で、表紙に「Axiom Math」とある35ページの論文です。10月27日に、数学研究のリポジトリであるHexagonに登録されました。HexagonはColin DefantとKen Onoを投稿者（contributor）として挙げており、2人ともAxiomの数学面の貢献者に名前があります。登録ページには2つの申告があります。「主に人間が書いた文章」と「人間の理解：すべての部分」です。

主結果は定理2.3「単純な頂部の保存（Preservation of simple tops）」です。Axiomの記事は、これを「AxiomProverが証明した群論の新しい結果」と呼んでいます。論文は注意9.5で、同じ帰着を使えば、定理2.3を必要としない、より短いUGTの導出ができることも記しています。記事によれば、Axiomの数学者がこの近道を見つけたのは形式化の後でした。論文は「AxiomProverがこの道筋を形式化したので」、長いほうの議論を残しています。

LyonsとSolomonの役割

LyonsとSolomonは、どちらも元の分類に取り組んだ数学者です。Axiomの記事によれば、2人は議論について相談を受け、UGTの修復は「LyonsおよびSolomonとのやり取りから恩恵を受けた」。記事はさらにこう書いています。「Lyonsは、利用できる証明の道筋を明確にし、障害を歴史的な文脈の中に位置づけるのを助けた。Solomonの1976年の極大2-成分の理論は、AxiomProverが生成し形式化した代わりの議論に、中心となる発想を与えた」。論文は謝辞でLyons、Dan Nakano、Solomonに感謝しており、Axiomは「Richard LyonsとRonald Solomonを含む群論の研究者による諮問委員会」とともに、正誤表の整備を続けるとしています。

これらの記述はAxiomによるものです。LyonsやSolomonが形式化について公に述べたものは見つかりませんでした。

Axiomはいくつの訂正を報告したのか#

文書によって、示されている数字が違います。

出典	日付	内容
研究記事1	10月26日付	「解決が必要だった、公刊された記録からの注目すべき逸脱34件」。問題の大半は「軽微」
@axiommathaiのスレッド6	10月27日	「数百の重大な誤りも修正した。詳細は追って発表」
@andrew_v102097、公開の告知（「今朝、公開します」）	10月27日	「文献への実質的な修正100件」
正誤表4	10月28日	96項目：パートAに34、パートBに62

コードの規模も一定しません。記事とプロジェクトのサイトはLeanで4,310万行としており、^1,3Xのスレッドは「5,000万行のLean」としています。⁶

何を数えているかを述べているのは、正誤表だけです。その1ページ目にはこうあります。「96の項目は、選ばれた数学上の逸脱と補足を記録したものである。96件の誤りや新しい発見を数えたものではない。これは網羅的な正誤表ではない」。⁴型どおりの誤植の訂正、記法の変更、そして「容易に直せる誤りは省いている」とされています。パートAには「構造上の変更と別証明」についての34項目があり、研究記事の数と同じです。パートBには「追加の議論と局所的な訂正」についての62項目があります。正誤表は、これらの分類が「誤りの大きさや数学的な重要性の尺度ではなく、議論への変更の程度を表す」としています。

正誤表は、それがどう作られたかも述べています。「この文書はAIシステムAxiomProverが生成した」。さらに、「ここに記述したすべての訂正、補足の議論、別証明は、AxiomProverが自律的に作成した」こと、そして「一部の訂正はすでに知られていたもので、それらを載せることは先取権を主張するものではない」ことも付け加えています。

まだ人の仕事として残っているものは何か#

命題を読む

Axiomの記事は、仕事をこう分けています。「人間は、その命題とそれが使う定義を調べ、意図した分類を表していることを確かめる。Leanは、それを立証する形式的な演繹を検査する」。¹AxiomはXで、まさにそれを求めました。「群論の研究者とLeanのコミュニティに検証をお願いしたい。証明の検査を再実行し、Leanの命題がCFSGと同じことを述べていることを確かめてほしい」。⁶

なぜそれが重要なのか。この形の命題は、そのリスト以上のものにはなりません。リストの定義の1つが意図とは違う群を記述していたら、定理はCFSGとは別のことを述べることになり、それでもLeanは証明を受理します。Tau Cetiのロードマップ¹³も、自身の定義について同じことを述べています。「これらの要件は機械的にではなく、レビューによって守られる」。Leanの公理の検査は「誠実な構成と、目標の存在定理から台を選び出す構成とを区別できない」ので、「各作業項目のレビュアーは定義を読み、台を明示的なデータまでさかのぼってたどらなければならない」と説明しています。10月25日に生成されたTau Ceti自身の状況のページ¹³は、その作業の一部がまだ途中であることを示しています。リー型の群の構成を標準的な群スキームと対応させる作業は、一部の族では終わっていますが、ほかの族ではまだです。

再ビルドする

READMEが示すコマンドは lake build の1つだけで、次の注記が付いています。「このプロジェクトのビルド時間を24時間未満にするため、Lakeに対する未マージの変更をいくつかと、近く上流に取り込む予定の最適化をいくつか使った」。²10月27日、ニュースサイトのRuntimeWire¹⁰が、Axiomの外の誰かが証明をビルドして確認したかを尋ねると、AxiomのCEOのCarina Hongは広報担当者を通じてメールでこう答えました。「まだです。外部の方々が独立に再現するのを助け、促すために、ビルド成果物を公開しています」。10月30日までに、外部で完全に再ビルドしたという公開の報告は見つかりませんでした。私たちはリポジトリのissueとプルリクエストを確認し、ウェブを検索しました。

正誤表と新しい定理を検討する

正誤表の96項目はAIシステムが生成したもので、数十年分の文献にわたります。各項目が正しいか、もっと簡単な修正があるか、すでに知られていたかは、群論の研究者が答えるべき問いです。正誤表はその助けを求めています。「訂正、以前の扱いへの参照、より簡単な議論やさらなる数学的研究の提案を歓迎する」。⁴UGTの論文はプレプリントです。その新しい定理を数学として読むことは、Leanがそれを受理することとは別のことです。

数学者はこれまでに何を述べたのか#

ティモシー・ガワーズは10月27日、Xにこう書きました⁸。「CFSGの証明が100%正しいのかどうか不確かだった歴史を考えれば、たとえ形式化そのものがひどい代物だとしても、これは素晴らしいニュースに思える（実際にひどいのかどうかは知らないが、私の推測ではそうだ）」。

自身のブログで数学について書いているJohn D. Cookは、10月28日にこう書きました⁹。「UGTと、それに依存するCFSGは正しいが、証明には欠陥があった」。これはAxiomの資料についての論評であって、確認ではありません。Axiomの論文は、見つかったことをもっと狭く表現しています。公刊された1つの道筋にある隙間であり、Walterの命題の結論もUGTそのものも否定されていない、というものです。⁵

このような結果を、ほかの人が確かめられるように記録するには#

確認する人に必要なものの多くは、すでに公開されています。正確なツールチェーン、ビルドファイルで固定されたライブラリのコミット、プロジェクトの外から持ってきた命題、コンパレータの設定、そして日付の入った正誤表です。見えにくいのは経緯です。公開のリポジトリには、10月27日に作られた「Initial commit」というコミットが1つあるだけです。²記事が描く24日間の作業はSlackとGitHubのissueで調整されましたが、コードとともに公開されたのではなく記事の中で語られており、モデルの名前も挙げられていません。

ほかの人が確かめられる記録であれば、正確なコミットとツールチェーン、命題とその出どころのコミット、使われた公理、それぞれが公開された日付、誰が何をしたか（人とAIの両方。モデル名も含めて）、そして誰が何を確認し、それぞれの確認の結果がどうだったかを、ひとつに結び付けるでしょう。CFSGの場合、そうした確認は何か月もかけて、さまざまな人から、さまざまな場所で届くかもしれません。

Papexは、その一部のために作られています。仮説、発見、論文を、その背後にある人、ツール、版と結び付け、責任を負う本人が署名し、日付を付けるものです。Papexは証明を検査しません。それを行うのはLeanで、命題を確かめるのは人です。CFSGは未解決問題ではなく定理なので、私たちの問題の一覧にも、未解決問題についてのAIを使った主張を載せているページ（英語）にも載っていません。

出典#

1. Formalizing the Enormous Theorem（Axiom Math、2026年10月26日付の研究記事）、2026年10月30日確認 ↩ a b c d e f g h i
2. AxiomMath/CFSG：README、lean-toolchain、lake-manifest.json、comparator.json、formalization.yaml、Comparator/Challenge.lean、Comparator/Solution.lean、Certificates/Certificate1.lean、CFSG/Milestones/CFSG_classification.lean（GitHub、コミット69cb972f、2026年10月27日）、2026年10月30日確認 ↩ a b c d e f
3. CFSG in Lean、プロジェクトのサイト（Axiom Math）、2026年10月30日確認 ↩ a b
4. Selected Departures from Published Arguments: Notes on the formalization of the classification of finite simple groups（Axiom Math、2026年10月28日）、正誤表のページとPDF、2026年10月30日確認 ↩ a b c d e
5. The Unbalanced Group Theorem, hexagon:2610.00575v1（Axiom Math、投稿者Colin DefantとKen Ono、2026年10月27日）、2026年10月30日確認 ↩ a b c d e f
6. Axiom（@axiommathai）のXでの発表スレッド、2026年10月27日。Leanの行数、証明の規模、UGTと正誤表、確認の呼びかけについての投稿を含む。2026年10月30日確認 ↩ a b c d e f
7. @andrew_v10209のXへの投稿、2026年10月27日、2026年10月30日確認 ↩
8. Timothy Gowers（@wtgowers）のXへの投稿、2026年10月27日、2026年10月30日確認 ↩
9. John D. Cook, The Unbalanced Group Theorem（2026年10月28日）、2026年10月30日確認 ↩
10. Emerson Redding, Axiom publishes Lean proof artifacts to support independent reproduction（RuntimeWire、2026年10月27日）、ニュース記事。Carina Hongのメールでの回答に使用。2026年10月30日確認 ↩
11. Tau CetiのREADME（GitHub）、2026年10月30日確認 ↩
12. Tau Ceti、コミット6e0c6ac時点のCFSG/Classification.lean（2026年10月2日）とその履歴、プルリクエスト#8792（2026年9月25日マージ）、2026年10月30日確認 ↩ a b
13. Tau Cetiのロードマップ、CFSGStatementのREADME（2026年8月8日追加）とSTATUS（2026年10月25日生成）、2026年10月30日確認 ↩ a b c
14. Qiuzhen-CFSGのREADME（GitHub）、2026年10月30日確認 ↩
15. leanprover/comparatorのREADME（GitHub）、2026年10月30日確認 ↩
16. Tactic Reference: decide, native_decide and sorry（Lean Language Reference）、2026年10月30日確認 ↩ a b