Anthropicによれば、同社のClaude AIはフェルマーの最終定理の完全にコンピュータ検証された証明を、11日間でほぼ自力に近い形で完成させ、史上最長の数学的証明を書き上げたという。

ロンドンの帝国理工大学（Imperial College London）で進められている人間主体のプロジェクトは、まったく同じ作業を2024年から続けており、完成にはほど遠い。Claudeはそれを追い抜いた。この帝国理工大学プロジェクトを率いる数学者Kevin Buzzardは、Claudeの証明をレビューし、数学の最も基本的な論理規則のみに基づいて成り立っていることを確認した。

Anthropicによると、Claudeは史上最長の数学的証明を書き、それを使って数学者を358年間悩ませ続けた問題、フェルマーの最終定理を形式的に証明した。このAIは11日間で、ほぼ自力でそれを成し遂げ、数学者の言葉を信じるのではなく、コンピュータが一行ずつ検証できる1300万行のコードを生成した。

フェルマーの最終定理は、3つの正の整数をそれぞれ2より大きい累乗し、最初の2つの和が3つ目と等しくなることはあり得ないとするものだ。Pierre de Fermatは1637年にこの主張を数学書の余白に書き付け、「真に驚くべき証明」を持っているが余白が狭すぎて書ききれないと付け加えた。その後彼は亡くなり、数学者たちはその後358年間、彼が何を思っていたのかを再構築しようと試み続けた。

証明することと検証することは別の仕事である

数学の証明は論理的步骤の連鎖であり、一つの環が壊れれば全体が崩壊する。数百ページに及ぶ緻密な議論の中に埋もれたその一つの壊れた環を見つけるのに、他の数学家は人生の何年もを費やすことがある。

証明を形式化するとは、コンピュータが自力で各ステップを検証できるほど厳密に字義通りの言語へ翻訳することを意味する。主観が介入する余地はない。

数学者は長い間、検証に苦戦してきた。1908年のドイツの賞（今日の価値で約100万～200万ドルに相当し、この定理の最初の正当な証明に贈られるもの）は、初年度だけで621件の誤った応募を集めた。

AnthropicがXに投稿した内容：

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

本物の証明が現れたのは1995年、イギリスの数学者Andrew Wilesによるもので、そこには波乱があった。Wilesは1993年6月に3回の講演で解を発表したが、後に査読者が穴を発見した。彼は元教え子のRichard Taylorとともにほぼ1年かけて修正し、あきらめかけながらも、最終的に1995年5月に修正済みの129ページの証明を発表した。それはフェルマーの存命中には存在しなかった数学に依存しており、これが数学者たちがフェルマー自身の「驚くべき証明」が実際には機能しなかったと疑う大きな理由となっている。

コンピュータ検証による数学自体は数十年の歴史がある。最初の有名な事例は1976年のコンピュータ支援による四色定理の証明で、人間が手作業で完全に読める証明が有効とみなされるべきかについて継続的な議論を引き起こした。Leanのような形式証明言語は——もともとMicrosoft ResearchにいたLeonardo de Mouraによって作られた——まさにその緊張関係から生まれたもので、ソフトウェアに検証を任せることで人間が結果を信頼できるようにした。

2024年、帝国理工大学の数学者Kevin Buzzardは、Claudeがちょうど成し遂げたことと同じことを目指すプロジェクトを開始した。Wilesの証明を、コンピュータが検証できる言語であるLeanに翻訳するのだ。この種の作業にはボランティア数学者の大軍が必要で——プロジェクト自体の概要は86ページに及び、資金は2029年まで確保されている。Claudeはその全体を11日で完成させた。

Claudeは実際にどのように成し遂げたのか

Anthropicはより詳しい記事の中で、コロンビア大学のチームとともにAI形式化ツールを開発しているTianyi Pengが、Claudeがどこまで自力で到達できるか試してみようと決めたと説明している。数十のClaudeエージェントが並行して動き、定義を書き、小さな結果を証明し、それらをより大きな結果へと積み上げた。人間の介入は「次はこの定理を優先せよ」のような時折の指示程度だった。

最初は順調には進まなかった。序盤、エージェントたちはすでに証明した内容を見失い、協力をやめてしまい、それらの失敗は最終的な証明の行数の約7%を占めている。

これを解決したのは、同じくPengのチームが開発したProve2Meというツールだった。このツールは、まだ必要とされる小さな証明のライブのToDoリストをすべてのエージェントに共有し、誰も作業を重複したり脱線したりしないようにした。また、Leanがすべてを高速に検証できるようファイルを整理し、各結果に関する平易な英語のメモを保管して、エージェントが互いの成果を再発明ではなく再利用できるようにした。

完了時点で、Claudeは3万を超える補助定理を証明し、数十億のトークンを消費した。Anthropicによれば、使用されたのは後に一般公開されたClaude Fable 5.1とほぼ同等の研究モデルだという。完成した証明は1300万行に及び——数学者がすでにこの種の作業に使っている共有ライブラリMathlibの5倍以上のサイズだ。

一般的な小説は8万語程度である。Claudeの証明は、純粋な論理的議論にして160冊の小説に相当する。

では、これは実際に重要なのか？

自身のプロジェクトの資金が2029年まで確保されているBuzzardは、Claudeの証明をレビューし、「数学の公理以外にいかなる仮定もなく」定理を証明しているとして承認した。

これはClaudeがまったく新しい数学を発見したこととは異なる。Anthropicは今年初め、暗号研究で新規数学の発見も主張している。Wilesは30年以上前にフェルマーの定理を証明しており、Claudeはその機械検証可能な領収書を作ったにすぎない。それが重要なのは、検証されていない証明（AIが書いたものを含む）が人間が手作業で確認できる速度を上回って押し寄せ、数学者がますます対応に追われているからだ。また、この種の形式化された証明は決定論的であり、人為的ミスの影響を受けにくい。これは数学において非常に重要である。

これは新しい問題ではない。ケプラー予想のコンピュータ支援証明には4年かかり、それでも審査パネルは「99%確実」としか断言できなかった。Grigori Perelmanによるポアンカレ予想の証明が完全に受け入れられるまでにも同程度の時間がかかった。

Anthropicの言葉を鵜呑みにしたくない人は、そうする必要はない。1300万行の完全な証明は現在GitHubで公開されており、時間のある数学者なら誰でも一行ずつ吟味できる。