2026年9月、AIのClaudeが、数学史上最も有名な問題の一つである「フェルマーの最終定理」について、初めて完全にコンピューターで検証可能な形式証明を完成させたとAnthropicが発表しました。Natureも、この成果を数学における重要なマイルストーンとして報じています。

　フェルマーの最終定理は、1637年ごろにピエール・ド・フェルマーが提唱した問題で、「nが2より大きいとき、aⁿ＋bⁿ＝cⁿを満たす正の整数a、b、cは存在しない」というものです。350年以上にわたり数学者を悩ませ、1990年代に数学者アンドリュー・ワイルズらによって証明されました。今回AIが行ったのは、フェルマーの最終定理を新たに解いたことではありません。 人間が築き上げた証明を、数学用の証明支援システム「Lean」が一つ一つ論理的に検証できる形へ変換する「形式化」です。

　Claudeは複数のAIエージェントを用いてほぼ自律的に作業し、わずか11日間で約1,300万行のLeanコードを作成。最終的な証明では約29,500の中間定理を利用しました。人間によるプロジェクトでは長期間を要すると考えられていた規模の作業です。

【GAME-Fからのコメント】

生成AIというと、文章を書いたり、質問に答えたり、画像を作ったりするものを思い浮かべる人が多いかもしれません。しかし今回の成果は、AIが人間の知識を整理し、その論理を一つずつ検証する研究の道具になることを示しています。

　ポイントは、AIがフェルマーの最終定理を「発見した」「初めて解いた」わけではないことです。人間が長い年月をかけて築いた数学的知識をもとに、AIが膨大な証明過程をコンピューターで検証可能な形にしました。

　これは子どもの教育にも重要な問いを投げかけます。AIが答えを出せる時代に、子どもたちは何を学ぶべきなのでしょうか。 答えそのものを覚えるだけでなく、「なぜそうなるのか」を考え、AIが示した結果が正しいのかを確かめ、別の考え方を探す力は、むしろこれまで以上に重要になると考えられます。

　AI時代の教育では、AIに答えを求める力だけではなく、AIの答えを検証する力を育てることが必要になってくるでしょう。

【参考】

Anthropic — Formalizing Fermat's Last Theorem

Nature — Anthropic AI ‘formalizes’ proof of Fermat’s last theorem — a milestone for mathematics