9月9日、ZME Scienceが「An AI Formalized and Verified Fermat's Last Theorem in 11 Days, a Task Expected to Take Years」と題した記事を公開した。人間の数学者チームが5年かけようとしていた作業を、AnthropicのAIシステムがわずか11日で完遂した——この対比が示す意味は、AI×数学の形式化が「ファンタジー」から現実に転じたことだ。
11日間で13万行、じゃない——1300万行のLeanコード
Anthropicは数十のClaudeエージェントを並列稼働させ、フェルマーの最終定理の証明を1300万行のLeanコードに変換した。過程で証明した中間定理は3万以上、最終的な構成に使われたのはそのうち2万9500本だ。
Leanとは、数学的な論理を一行ずつ機械的にチェックする形式検証言語（GitHub）。人間の証明が「暗黙の前提」や「自明なステップの省略」を許すのに対し、Leanは一切の省略を認めない。どんな自明な補題も明示的に書き下さなければ、コンピュータは受け付けない。
この作業を形式化（formalization）と呼ぶ。AIが新しい定理を発見したわけではない。Andrew WilesとRichard Taylorが1990年代に確立した証明を、機械が追跡検証できる形に「翻訳」した作業だ。
Imperial College Londonの数学者Kevin Buzzardは2024年から人間主導の形式化プロジェクトを率いていた。Claudeの成果を見た後、彼はNature誌にこう語った。
「以前は99.9%正しいと確信していた。今は100%確信している」
フェルマーの最終定理とは
17世紀の数学者ピエール・ド・フェルマーが1637年に書き残した命題——「nが2より大きいとき、aⁿ + bⁿ = cⁿを満たす正の整数a, b, cは存在しない」。フェルマー自身は「真に驚くべき証明を発見したが、余白が狭すぎて書けない」という注記だけを残して死んだ。
以来350年以上、誰も証明できなかった。Andrew Wilesが1993年に発表した証明にも当初欠陥が見つかり、Taylorとの共同作業でさらに1年かけて修正した。その業績でWilesは2016年のアーベル賞を受賞している。
技術的な詰まりどころ——自律的な数学作業の難しさ
Anthropicの実験は順風満帆ではなかった。初期のClaudeエージェント群はプロジェクト全体の把握を失い、協調が崩壊した。研究者たちはその後、Prove2Meというプラットフォームに移行した（元記事では第三者製のタスク管理基盤として紹介されており、Anthropic製ではない）。数千の依存サブ問題をマップ化し、各エージェントが完了済みの作業を把握しながら次に取り組む問題を選べる設計だ。
コスト面では、今回の実行で消費したトークンは約60億出力トークン。Anthropicの公表している商用レートで換算すると約30万ドルになる計算だ（円換算は記事執筆時点の為替レートに依存するため省略）。ただし内部コストはそれより大幅に安いとされる。
「正しい証明」と「使える証明」は別物
今回の形式化には大きな留保がある。
生成された1300万行のLeanコードは、数学者コミュニティが共有するライブラリ「Mathlib」の5倍以上の規模だ。ClaudeはMathlibを活用して再利用可能な形で書いたわけではなく、基本的な数学的機械を一から組み上げている。
Buzzardは自身のXenaブログにこう書いた。
「数学的には、Anthropicのこの作業は本質的に何も新しいことを教えてくれない」
一方でAnthropicの発表文では「現代数学文献の自動形式化への大きな一歩」とも述べている。この一見矛盾した評価は、「証明が機械的に正しい」ことと「数学コミュニティが積み上げられる資産になっている」ことが別問題だからだ。
将来のAIシステムが大量の正しい証明を生成するが、それぞれが独自の膨大な補助数学を抱え、互いに互換性がないという事態をBuzzardは「ナイトメアシナリオ」と呼んでいる。
2年前は「ファンタジー」だった
AI×数学の形式化は今年に入って急加速している。2月には、AIシステム「Gauss」がMaryna Viazovska（フィールズ賞受賞者）による8次元球充填問題の解のLean形式化を補助した。8月にはOpenAIが、内部モデルが数学・理論計算機科学の未解決問題10件で新たな結果を出し、それぞれをLean証明書として形式化したと発表している。
ただし、OpenAIの成果は「新たな数学的発見＋形式化」であり、Claudeの今回の作業（既知の証明の形式化）とは性質が異なる。
今後の本命は、新しい長い証明が正しいかどうかを自動検証する「疲れ知らずの第二の査読者」としての活用だ。カリフォルニア大学サンディエゴ校の数学者Frederick Mannersは「査読はより時間がかかるようになった一方で、質は下がっている」と指摘する。トロント大学の数論学者Daniel Littは「フェルマーの最終定理を形式化できるなら、おそらく何でも形式化できる」と述べ、Buzzardはシンプルにこう総括している——「2年前、これはファンタジーだった」。三者の言葉が重なるところに、今回の達成の重みがある。
詳細はAn AI Formalized and Verified Fermat's Last Theorem in 11 Days, a Task Expected to Take Yearsを参照していただきたい。
