フェルマーの最終定理の証明を、AIが11日で「機械が読める形」にした

この記事には広告（Amazon アソシエイトのリンク）を含みます。

フェルマーの最終定理の証明が、コンピュータで自動検証できる形に書き直された、という話です。Anthropic が2026年9月4日に発表したもので、書き直しをやったのは同社のAI「Claude」。かかった日数は11日、出てきたコードは1,300万行でした。9月7日には Nature のニュース欄も取り上げています。

はじめに断っておくと、このブログの記事は Claude を使って書いています。つまり今回の記事は、当事者側のAIが自分の会社の成果について書いている格好になります。数字や発言は Anthropic の発表文と Nature の記事から拾い、数学者のコメントは外部の人のものだけを使いましたが、その点は頭に置いて読んでください。

Anthropic が公開した「機械が読める証明」

発表の中身をひとことで言うと、「フェルマーの最終定理の証明を、Lean という証明支援システムのコードに全部書き下ろし、最後まで機械に通した」というものです。発表によれば、Claude は約11日間、ほぼ自律的に作業を続け、1,300万行の Lean コードを書き、途中で2万9,500個の補助的な定理を証明しました。完成したコードは GitHub で公開されています。

Nature の記事では、ラトガース大学の Alex Kontorovich 氏が「完全に度肝を抜かれた」と語り、当初は人間がやれば10年はかかると見込まれていた作業だったと伝えています。

ここで大事なのは、「フェルマーの最終定理が証明された」というニュースではないことです。定理はとっくに証明されています。今回起きたのは、その証明を別の形に「翻訳」する作業が終わった、という出来事です。何が翻訳されたのか、なぜそれが10年の仕事と見積もられていたのかを、順番に見ていきます。

350年の難問と、1994年の決着

フェルマーの最終定理は、「n が3以上のとき、xⁿ + yⁿ = zⁿ を満たす正の整数 x, y, z は存在しない」という主張です。n が2なら 3² + 4² = 5² のように解がいくらでもあるのに、3以上になったとたんひとつもなくなる、という話ですね。

1637年ごろ、フランスの数学者ピエール・ド・フェルマーが本の余白にこの主張を書きつけ、「驚くべき証明を見つけたが、余白が狭すぎて書けない」と添えました。証明は残されず、それから350年以上、数学者たちがこの問題に挑み続けます。Anthropic の発表文によれば、1908年に懸賞金がかけられたときは、最初の1年だけで621件の間違った証明が送られてきたそうです。

決着をつけたのはイギリスの数学者 Andrew Wiles でした。1993年に証明を発表したものの、検証の過程で穴が見つかり、元の学生だった Richard Taylor と1年かけて修正。1994年に証明が完成し、1995年に論文として出版されました。論文は129ページで、正しいと確認するだけで数か月がかかっています。Wiles はこの功績で2016年にアーベル賞を受けました。

この時点で、数学の世界では「証明済み」です。では、何が残っていたのでしょうか。

形式化という、もうひとつの作業

数学の証明は、人間が読むために書かれています。129ページの論文は、読み手が同じ分野の専門家であることを前提に、当たり前の手順は飛ばし、過去の膨大な論文の結果を「既知」として引用します。だから人間の専門家が読めば正しさを確かめられる一方、機械には読めません。

これを機械が読める形に書き直すのが「形式化（formalization）」です。Lean のような証明支援システムに向けて、証明の一歩一歩を、どんなに自明な手順も省かずにコードとして書く。書き終えれば、Lean が論理の筋道を機械的にチェックし、一か所でも飛躍があれば通してくれません。通ったなら、その証明は「数学の公理から出発して、隙間なくつながっている」と保証されます。

問題は、それがとんでもなく手間のかかる作業だということです。人間の証明が数百年分の既知の結果の上に立っているのに対し、形式化は「すでに形式化されているごく一部の数学」からしか出発できません。Wiles の証明が使う道具は現代数学の広い範囲にまたがっていて、その土台から作らなければならないわけです。

Wiles の証明を形式化しようという提案自体は2000年代からありました。2024年からはインペリアル・カレッジ・ロンドンの Kevin Buzzard 氏が、Lean で形式化する数年がかりの共同プロジェクトを始めています。その計画書だけで86ページ。「全部終わるまで10年」という見積もりは、この規模感から来ています。

形式化でAIが成果を出した例はすでにあって、今年2月には、球をもっとも効率よく詰める方法に関する Maryna Viazovska 氏の仕事（フィールズ賞の対象になった研究）がAIの助けで形式化されました。ただ Buzzard 氏によれば、フェルマーの最終定理はそれと比べて「一桁むずかしい」仕事だったそうです。

11日間と1,300万行の中身

今回 Claude がやったのは、つまり「129ページの論文を、1,300万行のコードに翻訳する」作業です。新しい数学を発見したわけではありません。証明の筋道は Wiles のものを、正確には Darmon・Diamond・Taylor による整理版に沿っていて、Buzzard 氏のプロジェクトなど既存の形式化の成果も部品として取り込んでいます。

それでも、この翻訳のほうが、人間には10年と見積もられた仕事でした。数字を並べると、途中で証明した補助定理が3万300個（最終的に使ったのは2万9,500個）。1,300万行というコード量は、Lean で数学を形式化するときの共通ライブラリ「Mathlib」の5倍以上にあたります。Mathlib は世界中の数学者が何年もかけて積み上げてきたものなので、その5倍を11日で書いた、ということになります。

やり方は、数十の Claude エージェントを同時に走らせる形でした。あるエージェントが概念を定義し、別のエージェントが中間の定理を証明し、それを使ってさらに難しい主張を証明する、という分業です。人間からの数学的な指示は、Anthropic の研究者 Tianyi Peng 氏が時おり出した「この定理を優先して」程度の大まかなものだったとされています。

ただ、最初からうまくいったわけではありません。発表文によれば、初期の試みはいくつも失敗しています。エージェントたちは途中から「プロジェクト全体がいまどこまで進んでいるか」を見失い、協力して動けなくなったそうです。成功の鍵になったのは、Peng 氏らがコロンビア大学で作った「Prove2Me」という共同作業プラットフォームでした。証明すべき定理どうしの依存関係をグラフとして管理し、各エージェントが「次に何を証明すべきか」をそこから読める仕組みで、記憶があいまいになる問題を補い、並列作業を可能にしています。作業にはおよそ60億トークンの出力を消費しました。

できあがった証明は Lean が検証済みで、使っている前提は Lean の標準的な3つの公理だけ。証明した命題が Mathlib 側のフェルマーの最終定理の記述と一致することも、別のツールで確認されています。

数学者たちの受け止め

Nature の記事には、外部の数学者3人の反応が載っています。Kontorovich 氏は、機械が人間の数学者の仕事を1,300万行の鉄壁の証明に変えたことに驚いたと語っています。Buzzard 氏は「2年前ならこれは空想だった」と述べ、Anthropic に寄せたコメントでは、代数・調和解析・幾何・数論にまたがる自動形式化がひとつの証明の中で層をなしていて、AIが作った形式化の成果物はもう「その上に積み上げられる」水準にあると評価しています。

トロント大学の Daniel Litt 氏は、フェルマーの最終定理が形式化できるなら、たぶん何でも形式化できる、と言い切っています。

この評価の背景には、数学界が長年かかえてきた「検証の重さ」があります。Wiles の証明が正しいと確認されるまでには数か月、ポアンカレ予想の Perelman の証明は受け入れられるまで約4年。ときには、間違った結果が何年も正しいものとして扱われ、その上に別の理論が築かれてしまうこともあります。形式化の手間がAIで一気に軽くなるなら、査読の負担が減るだけでなく、過去の数学の蓄積そのものを機械で総点検する道も見えてきます。Nature の記事は、有名な結果のいくつかが実は間違っていたと分かる可能性にも触れています。

分かったことと、まだ残ること

今回はっきりしたのは、「証明する」と「証明を機械が確かめられる形にする」は別の仕事で、後者が人間にとって途方もなく重く、しかしAIにとってはそうでもなかった、ということです。Anthropic 自身も、今回の新しさは数学ではなく検証の側にある、と発表文で明言しています。

割り引いて見るべき点もいくつかあります。まず、これは査読された論文ではなく、企業の発表です。使われたモデルは社内の研究用モデルで、Anthropic は「Claude Fable 5.1 におおむね相当する」と説明していますが、一般に使えるものとは違います。1,300万行という長さについても、Anthropic は脚注で「必要以上に長い可能性が高い」と認めていて、Mathlib のように簡潔で吟味されたコードとは性格が違います。

それと、形式化された証明があれば人間の解説がいらなくなる、という話でもありません。Anthropic も、形式的な証明が人間向けの説明に取って代わるべきだとは考えていない、と書いています。機械が「正しい」と言ってくれても、なぜ正しいのかを人間が理解するには、やはり人間が読める形の証明が要ります。

AIが数学に入ってくることには、数学者の側にも戸惑いや議論があります。ただ、形式化については比較的話が単純で、正しさの確認を機械に任せる方向そのものに反対する人はあまりいません。AIが生み出す証明がこれから増えていくなら、それを人間が一つひとつ読んで確かめるのは間に合わなくなります。今回の結果は、その確認作業もAIで回せるかもしれない、という見通しを示した形です。フェルマーの定理の「余白」に何が書かれていたのかは、相変わらず分からないままですが。