15000ページ 数学の史上最大の巨大定理を、AIエージェントが24日間で形式証明化

数学史上最大「有限単純群の分類定理」をAIエージェント群が24日で形式証明化

　有限単純群の分類定理は、すべての有限群を構成するこれ以上分割できない基本的な要素を分類したものであり、その膨大な規模から「数学史上最大の巨大定理」と呼ばれてきた。1960年代から約100人の数学者が500以上の論文を執筆し、総ページ数は約1万5000ページに達する。これまで全体を一人で読み通し検証した人間は存在せず、その証明の正確性については長らく議論の的となっていた。

　2026年10月26日、AIによる数学的推論の開発を行うAxiom社は、この巨大定理の第1世代証明全体をインタラクティブ証明支援言語Leanに翻訳し、コンピュータによる厳密な機械検証を完了したと発表した。プロジェクトは10月1日に開始され、同社のエンジニアや数学者の指揮のもと、数十のAIエージェントによる群れが分散協調して作業を進めた。結果としてわずか24日間で約4310万行のLeanコードと205万の宣言からなる巨大なリポジトリが構築された。作業にあたっては既存のMathlibなどのライブラリに加え、過去の形式化プロジェクトのコードも活用されている。

　AIを用いた厳密な形式化の過程では、過去数十年にわたり査読を通過し正当とみなされてきた人間の論文に複数の論理的な飛躍や誤謬が存在することが判明した。同社の報告によると、無視できない重大な逸脱が34件確認されている。大半は誤植や前提条件の抜け落ちであったが、中には深刻な論理の欠落も含まれていた。