AxiomProverとは？有限単群分類のLean形式化を解説

何を検証したのか

人類史上最大の数学証明が、いま計算機で検証された。

Axiomが発表したのは、有限単群分類定理（Classification of Finite Simple Groups）のLeanによる完全な自動形式化です。同社はこの定理を「対称性の周期表」と呼び、約1万5000ページにわたり、世代をまたぐ100人超の数学者が築いてきた巨大な証明だと説明しています。

形式化に使ったのは、AI証明器のクラスタAxiomProverです。人間が書いた証明をLeanの機械検証可能なコードへ落とし、証明全体をコンピュータがチェックできる形にした、というのが発表の芯です。

わかっている規模

編集情報では、Lean上の成果物は約5000万行、構築に要した時間は24日とされています。Axiomはこれを、計算機で検証された数学証明として史上最大だと位置づけています。元の論文規模（約1万5000ページ）と、生成された形式化コードの行数は別の単位なので、そのまま読み替えることはできません。

関連名として cfsg.axiommath.ai が挙げられています。ただし公開ビルド、ダウンロード、公式ページはまだ出ておらず、現時点で示されているのは短い予告映像と発表です。

• 24日

  クラスタによる形式化に要したとされる期間です。

• 約5000万行

  Lean上のコード規模として伝えられている数字です。

• 約1万5000ページ

  元になった人間の証明の分量です。

使える範囲と残る問い

アーキテクチャの詳細、重みの公開、API、料金、利用上限は発表からは読み取れません。比較対象となる他の証明器との数値対決も、この時点の材料には含まれていません。したがって、研究者が同じ手順を手元で再現したり、部分証明だけをAPIで呼び出す段階には至っていません。

開いている問いは、5000万行の検証が第三者の手元で追えるか、24日という期間に人間のレビューがどこまで入っているか、そして予告の先にソースやビルドが公開されるかです。定理そのものの数学的な意義は長年の蓄積にあり、今回の新規性はAxiomProverによる完全形式化の主張にあります。