Axiom Mathは2026年10月26日、数学の巨大な定理として知られる「有限単純群の分類」を、証明支援系Leanで検査可能な形式にしたと発表した。数学的な定義や証明を計算機が扱える形式言語で記述する「形式化」に取り組み、同社によると、24日間で約4,310万行のコードを作成したという。その過程では、従来の証明で使われていた中間的な主張に反例も見つかったが、有限単純群の分類そのものを覆すものではない。今回の成果を理解するには、何を機械で検査できるようになったのか、発見された反例がどの推論に影響するのか、そして人間による確認がどこに必要なのかを区別することが重要だ。

AD

有限群を分解すると現れる構成要素

立方体を回転させ、元と同じ見た目になるように重ねる方法は24通りある。こうした回転操作は、どの2つを続けて行っても24通りのいずれかになり、それぞれに元の状態へ戻す逆操作が存在する。このような構造を数学的に扱うのが群論であり、要素の数が有限であるものを有限群と呼ぶ。

有限群を数学的に分解していくと、それ以上同じ方法では分解できない構成要素に行き着く。これが単純群である。厳密には、単位元だけからなる群ではなく、自分自身と単位部分群以外に正規部分群を持たない群を指す。有限単純群の分類は、あらゆる有限群に現れるこうした構成要素が、既知のリストにすべて含まれることを示す定理だ。ただし、構成要素の種類が分かっても、それらをどのように組み合わせれば有限群を構成できるのかが、すべて明らかになるわけではない。

そのリストには、素数個の要素を持つ巡回群と、5次以上の交代群が含まれる。さらに、リー型と呼ばれる群の族があり、これらの系列に属さない26の散在群が存在する。分類の難しさは、こうした群を個別に発見することだけではない。リストに含まれない有限単純群が存在しないと証明して、初めて分類が完成する。

Axiom Mathの公式発表によると、従来の人間による証明は500本以上の論文にまたがり、合計約15,000ページに及ぶ。今回の形式化は、長年の数学研究によって築かれた「第一世代の証明」を対象としている。つまり、有限単純群の分類という結論を新たに発見したわけではない。多数の論文に分散していた議論を整理し、必要な前提から最終的な結論まで、推論の依存関係を機械で検査できる一つの証明としてまとめたという発表である。

24日間の形式化を支えた既存コードと人間の作業

Axiom Mathが公表したコードの規模は約4,310万行で、定義や定理などを含む宣言の数は約205万に達する。ただし、宣言の数がそのまま新しい数学的発見の数を意味するわけではない。大部分は、既存の数学的な知識を計算機で扱える形式に記述したものである。

また、24日間の作業は、何もない状態から始まったわけではない。Leanや数学ライブラリMathlibに加え、Qiuzhen-CFSGの約120万行を含む既存の形式化が基盤となった。Axiom Mathの公式報告によると、同社の数学者と技術者が数十のAIエージェントを稼働させ、数学者が証明上の障害を分析し、技術者がコードの統合やビルドを進めたという。長年蓄積されてきた研究成果と人間の専門的な作業を活用しており、この24日間を、それまでの数学研究に費やされた数十年間と単純に比較することはできない。

証明全体をつなぎ合わせるうえで重要なのは、コードの量よりも、それぞれの推論がどの前提に依存しているかである。同社は、未証明の追加仮定に依存していた数万行のコードを削除し、計画の一部を立て直したと説明している。ある仮定の下で補題が成立するとLeanが確認しても、その仮定自体を証明できなければ、有限単純群の分類を証明したことにはならない。個々の証明が機械検査を通ることと、必要な前提だけから最終的な結論を導けることは別の問題だ。今回の形式化では、従来の数学的な議論に含まれていた推論のつながりにも問題が見つかった。

AD

PSL₂(49)の反例は何を否定したのか

Axiom Math名義の論文『The Unbalanced Group Theorem』は、2026年10月27日にHexagonでプレプリントの第1版が公開された。識別子はhexagon:2610.00575v1で、登録上の寄稿者はColin DefantとKen Onoである。査読済み学術誌への掲載は確認されていない。

論文が扱う「Unbalanced Group Theorem（UGT）」は、単純群の内部にある部分群の性質から、群全体の種類を絞り込むための定理だ。対象となるのは非可換単純群であり、その真部分群に現れる非可換単純群の構成要素が、既知の分類に含まれるという帰納的な前提を置く。論文では、この条件を「K-proper」と呼んでいる。未知の有限単純群が存在すると仮定した場合に、その中で最も要素数の少ないものを調べるための条件である。

ここで、群の中に2回掛けると単位元に戻る「位数2の元」があるとする。この元と掛ける順序を入れ替えても結果が変わらない元をすべて集めると、中心化群と呼ばれる部分群が得られる。その中心化群に、単位元だけではない奇数位数の正規部分群が存在する場合、UGTは元の群が奇標数のリー型、または次数が4a＋3の交代群に属することを示す。ここでaは正の整数であり、UGTはあくまで所定の前提を満たす非可換単純群についての定理である。

今回見つかった反例は、UGT自体を否定するものではない。論文が問題としているのは、John Walterによる1986年の論証で、命題II.5.9(ii)を証明する際に使われた「閉性」の主張である。閉性とは、ある集合に属する群に特定の操作を施しても、そこから得られる単純成分が同じ集合に属し続けるという性質を指す。この性質が成り立つことを前提に推論を進めていたが、実際には集合の外に出てしまう例が存在した。

具体的な反例は、PSL₂(49)という群である。PSL₂やPGL₂は群の種類を表す記号で、括弧内の数は構成に用いる有限体の大きさを示している。まず、PSL₂(49)は論文で指定された集合L0に属する。次に、有限体の構造に由来する位数2の自己同型、すなわち群の演算構造を保ったまま要素を入れ替える変換を考え、その変換によって不変となる元を集めると、PGL₂(7)に同型な群が得られる。その単純成分はPSL₂(7)である。

しかし、PSL₂(7)は集合L0に含まれない。7がメルセンヌ素数であり、L0の定義では除外されているためだ。つまり、集合L0に属するPSL₂(49)から出発しても、指定された操作によって集合外の単純成分が現れる。これにより、従来の推論で必要とされた閉性が一般には成立しないことが分かる。ただし、この操作で用いる自己同型はPSL₂(49)の内部にある元ではなく、UGTの条件に登場する「群内の位数2の元」とは異なる。

すべての場合に成立するはずの数学的な主張は、反例が一つ見つかるだけで否定される。しかし、今回の反例が否定するのは、Walterの証明で使われた閉性の主張であって、命題II.5.9(ii)そのものの結論ではない。論文もRemark 1.8で、この反例は当該命題やUGTに対する反例ではなく、証明の途中にある推論の不備を示すものだと明記している。したがって、必要なのは分類の結論を変更することではなく、問題のある推論を正当な議論に置き換えることである。

必要な条件を明示した別の証明経路

問題となった閉性に頼らず、必要な結論を導くことはできるのか。論文では、Ronald Solomonが1976年に発表した理論に基づき、別の証明経路を構築している。その中心となるのが、定理2.3「Preservation of simple tops」である。ただし、これはあらゆる群や操作について単純商の型が保たれるという一般原理ではなく、対象となる群と比較操作に厳密な条件を設けた結果だ。

まず、対象の群Gは非可換単純群で、前述のK-properという条件を満たす必要がある。比較の基準となる単純群Tも、7次の交代群A₇か、qが5以上の奇素数冪であるPSL₂(q)に限定される。さらに、比較対象となる部分群の選び方には、論文で定義された極大性の条件が課される。任意の部分群を自由に比較できるわけではない。

もう一つ重要なのが、比較対象となる族のすべての成員について「2-rankが2」であるという仮定だ。これは、互いに可換な位数2の元から構成される基本可換2-部分群の最大位数が4であることを意味する。こうした条件をすべて満たす場合、論文で定められた比較操作を繰り返しても、対応する単純商の型が保たれることを定理2.3は示している。ここでいう単純商とは、対象となる群から奇数位数の正規部分群を取り除き、さらに中心で割ることで得られる非可換単純群を指す。つまり、条件を満たす特定の比較操作に限って群の型を維持できるという結果であり、あらゆる操作に適用できるわけではない。

論文では、この定理をGilmanとSolomonによる還元や、FooteとHarrisによる群の型を特定するための結果と組み合わせ、単純群に関するUGTの証明へと進んでいる。一方、Remark 9.5には、定理2.3を使わずにUGTを導く、より短い証明経路も記載されている。したがって、定理2.3がUGTを支える唯一の手段というわけではない。論文が長い証明を残しているのは、AxiomProverが実際に形式化した経路であることに加え、定理2.3自体がUGTの証明に必要な範囲を超える結果を含んでいるためだ。

この一連の作業は、数学の形式化で何が問われるのかを具体的に示している。重要なのは、最終的な結論が正しいと思われるかどうかだけではない。どの中間的な主張が成立せず、それをどのような条件を満たす別の議論で置き換えたのかを、明確にしなければならない。今回の反例の発見と証明経路の変更は、その過程を示す事例といえる。ただし、形式的な証明が構築されたことと、命題の意味や論文全体に対する学術的な評価が確定することは、分けて考える必要がある。

AD

機械による検査と人間による検証の違い

Axiom Mathの公式発表では、形式化された命題や定義が意図した有限単純群の分類を正しく表現しているかは人間が確認し、そこから結論に至る形式的な推論をLeanが検査すると説明している。また、公開されたGitHubリポジトリのREADMEでは、標準公理を使用し、未証明の部分を仮置きするsorryを含まず、計算をネイティブコードで実行して真偽を判定するnative_decideにも依存していないと説明している。再検査のためのビルド手順としては、lake buildが示されている。公表資料を基に、検証の対象と役割を整理すると次のようになる。

確認の種類 検証対象 公表内容と残る確認事項
Leanによる機械検査 記述された定義と前提から命題を導く形式的な推論 標準公理を使用し、sorryやnative_decideに依存しないと説明。公開コードを第三者が再ビルドし、検査結果を再現できるかが確認事項となる。
人間による意味の確認 命題と定義が、意図した有限単純群の分類を正しく表現しているか Axiom Mathが人間の役割として明示。形式的な推論が正しくても、命題の意味が意図と一致しているかは別途確認が必要となる。
UGT論文の学術的な検討 反例が否定する主張の範囲と、代替となる証明の数学的妥当性 2026年10月27日公開の第1版プレプリントで、DOIは未付与。査読済み誌への掲載や、独立した第三者による全体再検証の完了は確認されていない。

これらは、それぞれ異なる問題を検証する作業である。機械検査が保証するのは、形式化された前提と推論規則に従って、記述された命題を導けるという点だ。仮に人間が意図したものとは異なる命題を形式化していた場合、Leanによる検査が成功しても、それだけでは本来の数学的な主張を証明したことにはならない。また、公開コードの再ビルドに成功することと、UGT論文に示された数学的な議論が学術的に検証されることも、同じではない。

Axiom Mathは有限単純群の分類の形式化が完了したと報告しているが、独立した第三者による公開コード全体の再検証が完了したとの報告は、現時点では確認されていない。今後は、外部の数学者や開発者が形式化された定義と最終命題を精査し、公開コードの検査結果を再現できるかが重要になる。さらに、UGTの証明で見つかった問題と代替経路についても、専門家による学術的な検討が必要だ。

今回の成果の意義は、膨大な数学的議論を計算機で検査できる形式にまとめ、証明の途中で見つかった問題とその解決方法を明示した点にある。従来は多数の論文に分散していた前提や推論のつながりを、第三者が具体的に確認できるようになった。今後の独立した検証を通じて、公開された形式化の信頼性と、そこから得られた数学的な成果の評価がさらに明確になるだろう。