AI最新情報読了 7 分

100人・数十年がかりの「巨大定理」、AIはわずか24日で検証完了――見つかった34件の綻び

Shiritomo編集部 @shiritomoAI_jp 2026年10月29日更新

15,000ページ、500本以上の論文、100人を超える数学者が数十年を費やした証明。
それをAIが24日間で読み切り、4,310万行のコードに置き換えて「正しい」と確かめ終えました。
対象は群論（対称性を分類する数学の一分野）で最も巨大な証明とされる「有限単純群の分類（CFSG）」です。
AIで業務を回している読者にとっても、「人間の専門知識をAIが丸ごと検証できるのか」を測る実例として見ておく価値があります。
この記事では、何がどこまで確かめられたのかを一次情報で追いました。

先に結論をまとめると：
– 米AIスタートアップAxiom Mathが、CFSG（有限単純群の分類）の全証明をLean 4（証明を機械的に検証できるプログラミング言語）で形式化し、エラーなしで検証を完了しました
– AIエージェントの集団が24日間で約4,310万行のコードを生成し、元の論文群にあった34件の見過ごされていた問題点を発見・修正しました
– 定理そのものの結論は正しかったものの、1986年発表の一部の証明には穴があり、Axiomは新しい証明を書いて埋めました

何が起きたのか（Xでの盛り上がり）

CFSGは、あらゆる有限単純群（それ以上分解できない対称性の最小単位）を、既知の系列か26種の「散在型」のどれかに分類する定理です。
数学者が「対称性の周期表」と呼ぶほど基礎的な存在で、証明自体は1980年代までに人力でほぼ完成していましたが、全体が正しく積み重なっているかを1人の人間が通読して確認するのはほぼ不可能な規模でした。

この証明をAIが完全に機械検証したというニュースは、X（旧Twitter）でも取り上げられています。
日本時間10月28日昼ごろに投稿されたある投稿は「人類史上もっとも巨大な数学の証明（15,000ページ）が、AIによって完全攻略されてTLが大パニックに」という書き出しでこの出来事を紹介し、投稿者本人の感想として2,879件のいいねを集めました。

【速報】人類史上もっとも巨大な数学の証明（15,000ページ）が、AIによって完全攻略されてTLが大パニックに。

定理：『有限単純群の分類（CFSG）』「対称性の周期表」と呼ばれる群論の最高峰。これをAIエージェント（AxiomProver）がLean…
— black（黔騎士) (@blackright0) 2026年10月28日

100人超の数学者が数十年がけで積み上げた証明を、AIが24日で読み通して検証し終えたというギャップの大きさが、この投稿が注目された理由だと見られます。
ただ、投稿の文面だけでは「本当に全部正しかったのか」「どこにミスが見つかったのか」までは分かりません。
そこで公式発表や海外メディアの報道を確認しました。

調べて分かったこと

CFSG（有限単純群の分類）とはどんな定理なのか

元の証明は、約100人の数学者が複数世代にわたって書き継いだ500本以上の論文・書籍からなり、総量は約15,000ページに達します。
あまりの規模から英語では「Enormous Theorem（巨大定理）」という通称がついています。
Axiom Mathの公式研究ページによれば、プロジェクトは2026年10月1日に始まり、翌2日にAI エージェントの集団（スワーム）が稼働を開始、108個のマイルストーンと約380個の小タスクに証明を分解して進めました。
既存のオープンソースのコードを約120万行引き継ぎつつ、最終的に約4,310万行・205万件の定義や命題（宣言）からなるLean 4のコードベースが出来上がっています。
これは、これまでに書かれたLeanのコードとしては最大規模だということです。
開発元のコア開発メンバーであるヴァシリー・イリン氏は、現地時間10月27日に形式化が完了したとXで明らかにしました。

本当に34件の不備が見つかったのか、何が直されたのか

この点は、Axiom Mathの公式発表と技術メディアの報道の双方で確認できました。
既存の715本の論文・書籍をLeanのコードに翻訳する過程で、タイプミスや表の誤記、前提条件の見落としといった小さな誤りが多数見つかった一方、きちんと修復作業が必要だった「深刻な逸脱」は34件だったとされています。

もっとも重大だったのが「不均衡群定理（Unbalanced Group Theorem、UGT）」と呼ばれる定理に関するものです。
UGTは、ある有限群を、その部分群に関する情報から特定するための柱となる定理で、1986年に発表された証明が使われてきました。
Axiom Mathのチームがこの証明をLeanに落とし込む過程で、証明が前提としていた命題（ウォルターの命題II.5.9(ii)）に対する明示的な反例が見つかったといいます。
UGT自体の結論は正しかったのですが、既存の証明の説明では筋が通らない箇所があったため、Axiomのチームは新しい証明を書き起こして置き換えました。
元のCFSGを手がけた数学者であるリチャード・ライオンズ氏やロナルド・ソロモン氏にも、この修正内容が本来の分類のどこに位置づけられるかを相談したとされています。

人間の役割が消えたわけではない点も、公式ページがはっきり書いています。
公式研究ページは「この分類は、群を発見し議論を組み立てた数学者たちの功績であることに変わりはない」としており、AIが担ったのは発見そのものではなく、既存の証明を1行ずつ機械的に検証し、綻びを洗い出す作業だという位置づけです。
実際、不均衡群定理の新しい証明を書いた数学者の1人は、米国の大学教授職を離れてAxiom Mathの専属数学者になった人物で、今回の最終マイルストーン完了を知って感情が動いたと海外メディアに伝えています。
人間の数学者にとっても、思い入れの大きい出来事だったことがうかがえます。

数学AIはどこまで信頼できるのか

今回の件で気になるのは、「AIが検証した」と言われても、それがどこまで信頼できるのかという点ではないでしょうか。
Lean 4は証明を1行ずつ厳密な論理のルールに沿って検証する仕組みのため、人間が目視で読むより抜け漏れに強いという利点があります。
一方で、AIが自然言語の証明をLeanのコードに「翻訳」する段階で誤訳が起きれば、別の形の見落としが生まれる可能性は残ります。
だからこそAxiomは、翻訳元の数学者本人に重要な修正箇所を確認してもらう工程を残しているのだと考えられます。
AIによる数学研究の信頼性は、今後も検証の仕組みごとに個別に見ていく必要がありそうです。

Shiritomo編集部の考察

今回の件で注目したいのは、AIの役割が「新しい定理を発見すること」ではなく「既存の巨大な証明を検証し、小さな綻びを拾い上げること」だったという点です。
SNS運用やデータ分析の現場でも、AIに期待する役割をこの2つに分けて考えると整理しやすくなります。
たとえば大量の投稿データから新しい仮説を立てる作業は依然として人間の勝負所ですが、「このキャンペーン施策は本当に矛盾なく運用できているか」を1件ずつ機械的にチェックする作業は、AIに任せた方が精度も速度も上がる領域です。
CFSGの形式化は、AIを「検証係」として割り切って使うほど成果が出やすいことを示す、分かりやすい事例だったのではないでしょうか。