Axiom、数学史上最長の証明とされる有限単純群の分類をLeanで検証したと発表

スタートアップのAxiomは、「巨大定理」とも呼ばれる有限単純群の分類（CFSGと略されることが多い）の証明をコンピュータで検証可能にしたと主張している。これは約15,000ページに及び、数十年にわたって約100人の数学者によって500以上の論文に分散して書かれた証明である。発表は10月27日火曜日の15時34分（パリ時間）にXで行われ、前日付の長いブログ記事、インタラクティブな証明マップ、コードリポジトリが添えられた。

何についての話か

群は、立方体を変えない24の回転のように、対称性を記述する。有限群は、整数が素数に分解されるのと同じように、それ以上分解できない「ブロック」である単純群に分解される。分類は、これらのブロックのリストが完全であることを述べている。すなわち、素数位数の巡回群、5次以上の交代群、「リー型」群の16の無限族、そしてちょうど26の散在群、その中で最大のものはモンスター群である。この結果は多くの分野（代数、数論、組合せ論）で使われるが、その全体を検証できる人はほとんどいない。

Axiomはこの証明を、証明支援系のLeanで書き直した。Leanとは、すべての定義と論理的ステップが、プログラムがそれらを検査できるほど正確に書かれた言語である。プロジェクトのサイトにはLean 4310万行と205万の宣言が表示されている。

AIエージェントがどのように活用されたか

Axiomの物語は、何よりも組織の物語である。プロジェクトは2026年10月1日に、文献と既存のLeanコードから引き出された証明マップで始まり、108のマイルストーンと約380のタスクに分割された。10月2日には早くも、AxiomProverエージェントの数十の群が、変化するモデルの組み合わせを使用し、GitHubチケットを通じてタスクを要求し、Slackで報告を行った。「リーダー」エージェントは難しい論証を分解し、記述を検証した。他のエージェントは既存の結果を探したり、証明を書いたりした。

Axiomは失敗を隠さない。一見単純なマイルストーンが、エージェントが証明する代わりに仮定していた莫大な前提を隠していた。数万行が削除された。再コンパイル時間もボトルネックとなり、マシン間で共有されるキャッシュシステムで解決された。人間は中心にいた。根本的な障害には数学者、システムを動かすためにはエンジニア。

機械が発見したもの

形式化することは、人間の読者が自分で埋めるものを明示することを義務づける。Axiomによると、発見された問題のほとんどは軽微なもの（誤字、誤った表、忘れられた仮定）だったが、34件の顕著な相違が文献との間で解決されなければならなかった。最も深刻なものは、John Walterの1986年の版における非平衡群定理に関わるものだ。エージェントは推論の一段階に対する反例を発見したが、定理自体を反証したわけではない。分類の歴史的専門家であるRichard LyonsとRonald Solomonの助けを借りて、Solomonの1976年の研究から別の経路が構築された。Axiomはこれを群論の新しい結果として提示しており、発表に付随する論文に記載されている。

Axiomは専門家委員会とともに完全な誤り訂正リストを公開することを約束している。それがオンラインになるまでは、発見された誤りの総数は検証不可能のままである。

留意すべき限界

Leanは推論を検査するが、記述の意味は検査しない。最終的な定理とその定義が分類が述べていることを本当に述べているかどうかは、まだ人間が検証しなければならない。Axiomはその文章の中でこれを認めている。執筆時点で、完全な独立検証は公開されておらず、私たち自身もリポジトリを再コンパイルしていない。形式化はゼロから始まるわけでもない。Qiuzhen-CFSGプロジェクトの約120万行を統合し、Mathlibライブラリに依拠している。

この発表は、OpenAIが主張した数学的成果の翌日に届いた。それについてはこちらで紹介した。アプローチは異なる。OpenAIは新しい結果を発見したと述べ、Axiomは既知の結果を機械的に検証し、その一部を修正したと述べている。