1万5000頁の有限単群分類をAIが24日で形式化、Axiomの主張と残る課題

数学史上もっとも長い証明とされる有限単群分類定理（CFSG）を、Axiom MathのマルチエージェントシステムAxiomProverが24日間でLean 4に形式化した。生成したコードは4,310万行で、同社は既存のオープンソースプロジェクトを上回る規模だと主張する。あわせて34箇所の論理的なずれを検出し、その一部は新しい定理の証明で埋めたという。数値はすべて同社の発表に基づく。

1万5000頁の定理とは何か

有限単群は、それ以上分解できない群、つまり対称性の最小単位である。すべての有限群は素数位数の巡回群、5文字以上の交代群、16の無限系列のリー型群、そして26個の散在群のいずれかに分解できる。この分類を宣言したのがCFSGで、1950年代から約100人の数学者が500本超の論文を積み上げ、証明は1万5,000頁に達した。1983年に完成が宣言された後も穴が残り、2004年にAschbacherとSmithが1,221頁の論文で補っている。

人が読んで確認することが現実的でない規模になっていた、という点が重要である。形式化は、その1万5,000頁を機械が一字ずつ検査できる形に翻訳する作業にあたる。

24日間で何が起きたのか

工程は人間とAIの分担で進んだ。数学者が巨大な証明を108の節目と約380の下位課題に割り、AIの群れが手分けしてLeanのコードを書く。前提が足りないと判断すると、その課題を別のAIへ回送する。コードの生成速度が速すぎてLean側の再検査が追いつかず、分散キャッシュを急遽作り直したという記述も残る。

34箇所のずれと、埋め直された穴

もっとも重い指摘は不平衡群定理（UGT）にあった。部分群の構造から群全体の姿を導く、分類の要となる定理である。Axiomのチームは1986年のWalterの論文を土台に選んだが、形式化の途中で、鍵となる閉包の主張が論理的に成立しないとAIが警告を出した。反例としてPSL₂(49)が示されている。

ここで人間が呼び戻された。CFSGの原作業に関わったRichard LyonsとRonald Solomonが議論に加わり、Solomonが1976年に示した理論を手がかりに新しい筋道を立てる。その筋道に沿ってAIが証明したのが「Preservation of simple tops」で、これが穴を塞いだという。定理そのものは揺らいでいないが、証明の一部は人の手を離れたことになる。

形式化は数学を速くするのか

日本の産業界にとっての関心は、数学の話ではなく検証の話だろう。自動車の制御ソフトや医療機器、金融の決済系では、仕様と実装のずれが事故に直結する。形式手法は以前から使われてきたが、人手で記述するコストが導入の壁だった。1万5,000頁を24日で翻訳できるという主張が正しければ、その壁は確実に低くなる。

ただし順序を間違えてはいけない。形式化が保証するのは「書かれた通りの証明が正しい」ことであって、「書かれた内容が意図した対象を捉えている」ことではない。今回34箇所のずれが見つかったのは、まさにその隙間である。仕様の解釈を人が決める工程は残る。

よくある質問

Q. 24日という期間は何を指すのか。
Axiom社の発表では、2026年10月1日に着手し、10月10日に魔群が単群であることの証明まで到達、その後24日間で全体を走らせたという流れである。既存文献の形式化であり、定理を新しく発見した期間ではない。

Q. 第三者による検証は済んでいるのか。
本稿の取材範囲では、独立した研究チームによる再検証の公表は確認できていない。Leanのコードが公開されていれば誰でも機械的に検査できるが、その検査結果そのものを筆者は確認していない。

編集部の見解

派手な数字が並ぶが、読み方は冷静でいい。24日という短さは、AIが賢いからではなく、検査を機械に任せられる形に問題を落とせたから実現している。逆に言えば、形式化できない領域では同じ速度は出ない。

日本の読者にとって現実的なのは、自社の仕様書や設計文書をどこまで機械可読にできるかという問いだ。数学の巨大定理より規模は小さいが、効果は同じ方向に出る。まず検査可能な範囲を決め、そこから広げる。順序を守れば、この発表は他人事ではない。

my-best.ai 編集部

出典：36Kr「AIが人類史上最大の数学証明を補完、数学者がその場で涙した」（寄稿：新智元、2026年10月30日）

あわせて読みたい

• 全モーダルAIが「いつ話すか」に苦戦、リアルタイム対話の349本総説
• GPTも狼人殺で嘘を見抜けない、東大MIDAが示す二値正解率27.6%
• 臨床試験の被験者不足をAI仮想患者が埋める、評価額10億元の挑戦

本日の36Kr AI版の記事を日本語で整理したものです。最新記事の一覧から他のニュースも読めます。