AIエージェント群が11日間で1300万行のコードを自動生成
350年以上前にフェルマーが書き残した予想の証明が、AIの手でコンピュータ検証可能な形に生まれ変わりました。
米AI企業Anthropicは、自社の対話型AI「Claude」を用いてフェルマーの最終定理の証明を形式検証言語Leanに落とし込み、世界初の完全なコンピュータ検証済み証明を完成させたと発表しました。
Anthropic公式ブログのほか、米SiliconANGLE、米AI Weeklyなども今回の成果を報じています。
フェルマーの最終定理とは何か
フェルマーの最終定理は、17世紀のフランスの数学者ピエール・ド・フェルマーが1637年に書き残した予想です。
「3以上の自然数nについて、aのn乗+bのn乗=cのn乗を満たす正の整数の組a、b、cは存在しない」という一見シンプルな主張です。
フェルマー自身は「驚くべき証明を発見したが、余白が狭すぎて書けない」と書き残しており、その真偽は350年以上にわたって数学者を悩ませてきました。
最終的に証明を成し遂げたのは、英国出身の数学者アンドリュー・ワイルズです。
ワイルズは1995年、楕円曲線とモジュラー形式という高度な現代数学の理論を駆使し、129ページに及ぶ証明を発表しました。
この証明はあまりに複雑で、数学界が正しさを検証し尽くすまでに数カ月を要したといわれています。
Claudeが行ったのは「新証明」ではなく「形式検証」
今回Anthropicが行ったのは、ワイルズによる証明そのものを新たに発見したことではありません。
ワイルズの証明を、Leanと呼ばれる形式検証言語(数式の各論理ステップを省略せず機械的に記述し、コンピュータが公理に照らして正しさを自動判定できるプログラム言語)に落とし込む「形式化」という作業です。
人間が書く通常の証明は、専門家であれば自明な手順を省略して記述しますが、Leanではその一段一段をすべて明示的にコード化する必要があります。
Anthropicの研究チームはこの形式化作業を、複数のClaudeエージェントに自律的に分担させる形で進めました。
作業には、米コロンビア大学のティエンイー・ポン氏らが開発したオープンな共同形式化基盤「Prove2Me」が活用されています。
Prove2Meは証明すべき定理群を有向非巡回グラフ(DAG)として管理し、既存の定理を自然言語で検索・再利用できる仕組みを備えています。
この基盤により、複数のAIエージェントが互いの作業状況を把握しながら並行して作業を進めることが可能になりました。
結果として、わずか11日間で作業は完了しました。
生成されたコードは1300万行に達し、証明の過程で30300個の定理が新たに証明され、うち29500個が最終的な証明に組み込まれました。
この間に消費されたAIの出力トークン数はおよそ60億トークンにのぼるとされています。
専門家も驚いた規模とスピード
今回生成されたコード量は、数学界が共同で構築してきた主要な数学ライブラリ「Mathlib」の実に5倍の規模に達します。
形式化の取り組みを主導してきた英インペリアル・カレッジ・ロンドンの数学者ケビン・バザード氏は、この成果を「特筆すべき快挙」と評価しています。
バザード氏は、自動形式化の技術が「もはや実用に耐えるレベルに達した」ことを示すものだと述べています。
専門家の間では、この規模の形式化には数年単位の歳月がかかると予想されていました。
それがわずか11日間で完了したという事実そのものが、AIによる数学研究支援の到達点を象徴しているといえます。
もっとも、Anthropic自身も今回生成された証明について、人間が書く証明に比べて大幅に冗長になっていると認めています。
これはMathlibに蓄積された定理群の方が簡潔に整理されているためで、AIによる形式化にはまだ改善の余地が残されています。
数学研究をどう変えるのか
形式検証済みの証明が普及すれば、査読者が数式を1行ずつ手作業で追う負担を大幅に軽減できると期待されています。
また、既存の数学論文に潜む誤りを機械的に洗い出すことにも応用できるとみられています。
数学の世界では、複雑な証明ほど誤りが見つかりにくく、査読だけでは限界があることが長年の課題とされてきました。
AIによる自動形式化が普及すれば、新たに発表される証明をコンピュータが即座に検証できる未来も現実味を帯びてきます。
一方でAnthropicの研究チームは、今回の取り組みはあくまで既存の証明を検証したものであり、新しい数学的発見そのものではないとも強調しています。
形式化された証明は、人間が読んで理解できる従来の数学的記述を置き換えるものではなく、それを補完する役割にとどまるという立場です。
関連豆知識：Claudeはリーマン予想でも成果
Anthropicは今回のフェルマーの最終定理に先立ち、同じく未解決の数学最大の難問とされる「リーマン予想」の証明でも一部前進を報告しています。
リーマン予想は素数の分布に関わる160年以上未解決の難問で、解決すれば100万ドルの懸賞金が贈られることでも知られています。
また今回の形式化作業を支えた基盤「Prove2Me」は、Anthropic以外の研究者にも開放されたオープンな仕組みです。
今後は他のAI開発企業や大学の研究チームも、同様の手法で別の難問の形式化に挑む可能性があります。
まとめ
AnthropicのAI「Claude」は、350年以上前にフェルマーが書き残した予想の証明を、わずか11日間でコンピュータ検証可能な形式に変換しました。
1300万行のコードと3万個近い定理という規模は、数学界のベテラン専門家すら驚かせるものでした。
今回の成果は新たな数学的発見ではなく、既存の証明の「検証」である点には注意が必要です。
それでも、AIが人間の専門知を要する高度な数学の世界に本格的に入り込みつつあることを示す象徴的な出来事といえます。
今後、同様の手法が他の難問や現代数学の主要文献にどこまで広がっていくのか、注目が集まります。