フェルマーの最終定理は、nが2より大きいとき、xⁿ + yⁿ = zⁿには正の整数の解がないというものです。ピエール・ド・フェルマーは1630年代に余白に書き込み、アンドリュー・ワイルズ氏は1990年代に、史上最も難しい数学の一部を使ってそれを証明しました。2026年9月4日、AnthropicはClaudeが11日間でその証明の初めての完全なコンピューター検証済みの版をつくったと発表しました[1]。この記事では、それが何を意味するのか、なぜ数学だけでなくコンピューターサイエンスの話でもあるのか、そして何を意味しないのかを説明します。
年表
- 1630年代フェルマーが「この余白はそれを書くには狭すぎる」証明があると主張。
- 1994〜95年アンドリュー・ワイルズ氏（リチャード・テイラー氏と）が証明を完成。
- 2024年ケビン・バザード氏がインペリアル・カレッジ・ロンドンで、証明をLeanで形式化する人間主導のプロジェクトを開始。
- 2026年8月Claudeのエージェントが11日間でLeanによる完全な形式化を完成。
- 2026年9月4日Anthropicが成果を発表し、バザード氏が確認。
証明支援系がすること
GCSE基礎
人が書いた証明は、小さな段階を読者に任せます。熟練の査読者でさえ穴を見落とすことがあります。Leanのような証明支援系は、その危険をなくします。定義と証明をコードとして書くと、小さく信頼できる検査プログラム（カーネル）が、どの段階も論理とそれまでの結果から導かれることを確かめます。コードがコンパイルできれば、定理は検証されたことになります。正しいと証明できない限りプログラムを実行しないコンパイラーのようなものです。
形式的な証明は木の形をしています。最終定理は大きな中間結果に、それは補題に、補題は定義と基本的な事実に支えられています。Leanはすべてのつながりを検査します。ボタンを押して、土台から木を検査してみましょう。模式図です。実際の木には約2万9500個の定理があります。
Claudeが実際にしたこと
A-Level発展
- ダーモン、ダイアモンド、テイラーによる、ワイルズの証明の簡略版を形式化した[1]。
- 成果は約1300万行のLeanと約3万300個の定理（最終証明に使われたのは約2万9500個）で、Mathlibの5倍以上の大きさ[1]。
- 何十ものClaudeエージェントが11日間並行して働き、社内の研究用モデルの出力トークンを約60億使った[1]。
- 人間の数学的な関与は、Anthropicの研究者ティエンイー・ペン氏によるときどきの大まかな指示に限られた[1]。
- 証明はLeanの3つの標準公理だけに依拠し、比較ツールによって、最終定理がMathlib自身のフェルマーの最終定理の記述とまったく同じことを述べていると確認された[1]。
- インペリアル・カレッジ・ロンドンのケビン・バザード氏のFLTプロジェクトの部品を再利用し、完成した証明はバザード氏が確認した[1]。
クイックチェック
証明がLeanで「コンパイルできる」とはどういう意味ですか？
主張の確認が大切な理由
コンピューター検証済みの証明は、正しい主張を証明している場合にだけ役に立ちます。Leanで定理が少しでも間違って書かれていたら、間違ったことの完璧な証明には価値がありません。だからチームは比較ツールを使って、主張がMathlibで独立に書かれた版と一致することを確かめました。また「余分な公理なし」の検査が大切なのは、何も単に仮定されていないことを示すからです[1]。段階の検証と仕様の妥当性確認は別の仕事で、ソフトウェアテストとまったく同じです。
学習者が見落としがちな違い
正しいことは、美しいこと（や新しいこと）とは違います。
試験形式の問題
フェルマーの最終定理の形式的証明を例にして、検証（verification）と妥当性確認（validation）の違いを説明しなさい。 [4点]
模範解答と採点基準を表示
- 検証とは、製品が正しくつくられていること、つまり仕様を満たしていることを確かめること (1点)
- ここでは、Leanが証明のすべての段階が論理的に正しいことを検証している (1点)
- 妥当性確認とは、正しい製品がつくられたこと、つまり仕様が本当に必要だったものと一致していることを確かめること (1点)
- ここでは、Leanの主張をMathlibの独立したFLTの記述と比べることで、証明が意図した定理を証明していることを確かめている (1点)
採点者が重視する点: 両方の用語を定義し、それぞれを例の特定の部分に結びつけること。
よくある間違い: 2つの言葉を同じ意味として扱うこと。プログラムはすべての検証に合格しても、間違ったことをする可能性があります。
論理、証明、テストはA-Levelの数学とコンピューターサイエンスをつなぎます。AIは本当に数学ができるのか？の記事では全体像を、ミレニアム懸賞問題ではまだ未解決の問いを紹介しています。
出典とさらに詳しく学ぶために
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — 規模、エージェント、公理、人間の関与、バザード氏の確認、注意点
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — ニュース報道
- Lean community: Mathlib — Leanの数学ライブラリ
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — 人間主導のプロジェクト
最終確認日:2026年10月5日。数値は一般に公表されている典型的な値であり、規則は変わる可能性があります。試験の表現は各試験仕様(specification)によって異なるため、ご自身のものを確認してください。
よくある質問
AIがフェルマーの最終定理を証明したのですか？
いいえ。証明したのは1990年代のアンドリュー・ワイルズ氏です。2026年に起きたのは、Claudeのエージェントがその証明の一つの版を、すべての論理の一歩を検査する言語Leanに翻訳したことです。2026年9月4日にAnthropicが発表したこの成果は、定理の初めての完全なコンピューター検証済み証明です。
Leanとは何ですか？
証明支援系です。定義、定理、証明をコードとして書くプログラミング言語です。カーネルと呼ばれる小さな信頼できるプログラムが、各段階が論理の規則とそれまでの結果から導かれることを確かめます。証明がコンパイルできれば、Leanに組み込まれた公理だけを仮定して、定理は検証されたことになります。
証明はどれくらいの大きさですか？
約1300万行のLeanコードと約3万個の定理（最終的な証明に使われたのは約2万9500個）で、Leanの主要なコミュニティ数学ライブラリMathlibの5倍以上の大きさです。かかったのは11日間で、何十ものClaudeエージェントが並行して働き、Anthropicの研究者ティエンイー・ペン氏がときどき大まかな指示を出しました。
AIが書いた証明は良いものですか？
Leanが検査したという意味では正しく、インペリアル・カレッジ・ロンドンで人間主導のFLT形式化プロジェクトを率いるケビン・バザード氏も確認しました。ただしAnthropicは、必要よりずっと長いだろうと述べ、失敗した試みが定型以外の行の約7%を残したとしています。正しいことと美しいことは別物です。
読者からの評価とレビュー
この記事を複数の観点から評価してください — あなたの意見は他の読者の助けになり、私たちの改善にもつながります。
この記事は役に立ちましたか？
ご感想をお聞かせください — 修正点、未解決の疑問、次に取り上げてほしいトピックなど。
直接話したいですか？ ご都合のよい時間に無料のビデオ通話を予約できます。短い質問は15分、その他は30分です。時間はお住まいのタイムゾーンで表示されます。
著者について
Sudershan Soni
Mostak Servicesの創業者兼主任講師 — 数学・理科・情報科学・STEMの修士号を持つ講師であり、20年以上のプロフェッショナルとしての経験を持ちます。11+やGCSEからA-Levelおよびそれ以降まで、世界中の生徒をオンラインで指導しています。
プロフィール全文を読む