AIニュース 2026年10月29日

今週 · 研究ページ 10 月 26 日

Axiom の自己申告で証明を24日でLeanに書き直し

AI 数学企業 Axiom は、15,000 ページの証明を 24 日で機械が検査できる Lean のコードに書き直したと述べ、推論の検査は機械、定理が正しく書かれたかの確認は人が担う

なぜ重要か： 本紙の推論：既存の証明を Lean に移す作業は速くなり、人が確かめるのは定理そのものが正しく書かれているかになる。

AI で数学の証明を扱う企業 Axiom は 10 月 26 日、研究ページで、AI エージェント群を使って有限単純群の分類定理の第一世代の証明を Lean で形式化し終えたと発表した。

有限単純群の分類定理は、有限単純群をすべて一覧にした定理である。Axiom がしたのは既存の証明を機械で検査できる形に移す作業で、新しい証明ではない。元の証明は約 15,000 ページで、約 100 人の数学者が何世代もかけて仕上げた。Axiom はこの証明を、定理証明支援系 Lean が一歩ずつ機械で検査できるコードに書き直し、コードは約 4,310 万行になった。10 月 2 日に最初のエージェント群が動き出してから 24 日かかり、同社のエンジニアと数学者が数十のエージェント群を指揮した。どのモデルを使ったか、人と機械がそれぞれ何行書いたかは、研究ページに書かれていない（Axiom 研究ページ、2026-10-26）。

Lean が保証するのは、前提から結論まで一歩ずつ誤りなく推論できていることで、前提と結論が元の定理の言いたいことを表しているかは、今も人が読む必要がある。研究ページによれば、主定理の記述と主定理が使う定義は人が確かめ、記述が意図した分類を表していることを確認した。主定理を導く形式的な推論は Lean が検査した。作業の中で既発表の文献との食い違いが 34 か所見つかり、別ページに正誤表を載せた。それぞれが誤植か証明の穴かは、研究ページに書かれていない。コードは公開されている。説明ファイルによれば、未完成の仮置きは残っておらず、使う公理も標準的な三つだけである（GitHub AxiomMath/CFSG）。

まだ言えないこと： すべて Axiom 自身の説明で、独立チームのビルド成功報告はない どう確かめたか →

次に注目するのは、Lean のコミュニティか Mathlib の保守担当者がビルドの結果を公表するかどうかだ。独立したチームのどれかがビルドに失敗するか、未完成の仮置きを見つけるか、主定理の記述が標準の定義と合わないと指摘すれば、「完成」は撤回となる。