Claudeがフェルマーの最終定理を11日で形式化｜1,300万行の証明を検証する仕組み

公開日

2026年9月6日

更新日

2026年9月7日

2026年9月4日、Anthropicは、Claudeを使ってフェルマーの最終定理の証明をLeanで形式化し、コンピュータで検査できる成果物として公開したと発表しました。同社が報告した形式化の作業期間は11日間です。これは「未解決だったフェルマーの最終定理をAIが初めて解いた」というニュースではありません。既知の数学的議論を、機械で検査できる証明へ組み立てた成果です。［1］

主要な数値には公式発表の裏付けがあります。ただし、11日間は検証ソフトを動かした時間だけを意味せず、通常のチャットサービスに一度頼むだけで同じ成果を得られたわけでもありません。何を作り、どの条件で検証したのかを分けて読む必要があります。

この記事では、Anthropicの発表、公開リポジトリ、ケビン・バザード教授自身の検証報告、Leanの公式文書を照合し、確認できる事実と仕事への応用上の考察を区別します。

Claudeによるフェルマーの最終定理の形式化を表す図解。11日間、約1,300万行、最終証明に約29,500の補助定理を使用という数値はAnthropicの発表に基づく

図中の数値はAnthropicの発表によるものです。「11日間」は形式化の作業期間であり、検証だけの所要時間ではありません。

この記事の主な内容

何が起きたのか：既存の証明をLeanで形式化した

フェルマーの最終定理は、nが3以上の整数のとき、xⁿ＋yⁿ＝zⁿを満たす正の整数x、y、zは存在しないという定理です。アンドリュー・ワイルズの論文とリチャード・テイラーとの共著論文は、1995年5月の『Annals of Mathematics』に掲載されました。今回の成果は、この定理に初めて証明を与えたものではありません。［7］

形式化とは、数学的な対象、定理の主張、推論を、証明支援系が扱える言語で記述することです。Leanでは、中心となる検査機構「カーネル」が、証明をその論理体系の規則に照らして検査します。文章を一行ずつ翻訳するだけではなく、人間向けの説明で省かれている手順や、前提として使う定理も補う必要があります。［4］

今回の証明は、ワイルズの原論文の逐語的な変換ではなく、ダーモン・ダイアモンド・テイラーによる既知の証明の解説に沿うものです。公開リポジトリの最終定理は、上記の自然数に関する主張を記述し、Mathlibの定理文にも接続しています。［2］［3］

「11日」「1,300万行」は何を数えた数字か

次の数値は、特に断りのない限りAnthropicの発表値です。この記事の編集時に、生成作業の全ログから独自に集計した数値ではありません。［1］

項目	発表内容	読み取る際の注意
作業期間	11日間	複数のエージェントによる形式化の期間。環境開発や既存ライブラリの整備を含む総工数ではありません。
Leanコード	約1,300万行	成果物の規模であり、証明の簡潔さや数学的な新規性を直接表す数値ではありません。
途中で証明した定理	約30,300、そのうち最終証明で約29,500を使用	生成・証明した総数と、最終証明に使った数を区別します。
出力トークン	約60億	出力の量です。この数字だけで総計算量や利用料金は算定できません。
使用モデル	Claude Fable 5.1とおおむね同等と説明された、汎用の社内研究モデル	一般提供モデルを通常のチャット画面で使った実験と同一視できません。

人間からの数学面の助言は、ときどきの高水準の指示に限られていたと説明されています。一方、共同作業基盤の構築や、Lean・Mathlibなどの既存資産までAIがゼロから無人で用意した、という意味ではありません。公開リポジトリにも、インペリアル・カレッジ・ロンドンのFLTプロジェクトやflt-regularなどからのコード利用が明記されています。［1］［2］

「機械検証済み」は何を保証し、何を保証しないか

単にLeanのコードが動いたことと、目的の定理が余分な仮定なしに証明されたことは同じではありません。未証明部分を仮置きするsorryや追加の公理に依存していないか、定理文が意図した内容になっているかまで確認する必要があります。Leanの公式文書も、これらを別の確認項目として扱っています。［4］

1．定理文と、その定義を確認する

今回の公開コードには、正の自然数と3以上の指数を対象にした最終定理があります。READMEでは、検証ツールcomparatorを使い、定理文とそこで使われる定義が基準となるMathlibのものと一致すること、証明全体をカーネルで再検査したことを報告しています。別の弱い命題を証明していないか、という確認です。［2］

2．証明が依存する公理を確認する

FinalCheck.leanでは、最終定理の依存公理がpropext、Classical.choice、Quot.soundの3つであることを確認するコードが公開されています。これらはLeanで通常の数学に使われる公理です。「数学に必要な公理は全部で3つしかない」という意味ではなく、この形式的証明が、未証明の穴や独自に追加した前提に依存していないことを確かめる検査です。［2a］［4］

3．検証機構と外部の確認状況を確認する

READMEは、Leanとは別に実装された検証カーネルnanodaでも検査したと報告しています。ただし、用いたのは進捗表示や高速化のための修正を加えた版です。また、バザード教授は自身のブログで、コードをビルドし、comparatorを実行して確認できたと報告しています。したがって、2026年9月6日時点で「開発企業の発表しかなく、外部の検証報告はまだない」という状況ではありません。［2］［3］

正確には、意図した命題が形式的に記述され、採用する論理体系と検証機構を信頼するという前提のもとで、証明が成立すると確認されたと説明できます。検証ソフトの実装まで無条件に正しいと保証したわけではなく、数学的な意味の理解や、人間が読みやすい解説の価値もなくなりません。［4］

本記事は公開資料、最終定理、検査コードの照合に基づく解説です。編集時に約1,300万行の全証明を独自にビルドし直したり、検証ツールを再実行したりしたものではありません。

人間が進めていたプロジェクトが、そのまま不要になったわけではない

バザード教授のプロジェクトと今回の成果には、フェルマーの最終定理を形式化するという共通点があります。しかし、証明の経路と成果物の目的は一致しません。教授側は後年の発展を取り入れた現代的な証明を扱い、再利用できる数学的な定義や結果をMathlibへ追加すること、人間が証明をたどれる文書を作ることも目指しています。［3］［5］

このため、「人間が数年かけていた同じ仕事をAIが11日で終えた」と単純比較すると、目的の違いと先行研究の蓄積を落としてしまいます。大規模な形式化を短期間で達成したことは評価できても、人間のプロジェクトの全目標を置き換えたとは言えません。

長い作業を支えたのは、検証と共同作業の仕組み

今回使われたProve2Meは、複数のAIエージェントが証明を持ち寄り、ほかのエージェントの成果を再利用するための共同作業基盤です。定理同士の依存関係を管理する、定理文と証明を分けて扱う、必要な結果を検索できるようにする、といった仕組みが用意されています。［6］

Anthropicは、初期の試行ではエージェント間の連携が崩れ、Prove2Meへ切り替えた後に完成へ進めたと説明しています。最終コードの定型部分を除く行数の約7％は初期試行に由来するという記載もありますが、これは初期試行の成果を再利用したという話であり、未証明の穴を残したまま完成扱いにしたという意味ではありません。［1］［2a］

ここから「Leanさえあれば長時間の仕事が必ず成功する」と結論づけることはできません。検証器に加え、モデルの能力、作業の分担、状態の管理、利用できる計算資源が組み合わさった事例として捉える必要があります。

マスログの視点：行数は、質や持続力そのものを測る指標ではない

「約1,300万行」という数値は成果物の大きさを示します。しかし、その数字だけでは、必要最小限の長さ、再利用のしやすさ、運用コスト、同じ実験を繰り返したときの成功率は分かりません。行数をそのまま「AIの持続力の指標」とするのも飛躍があります。

量を評価するときには、何を達成したか、どの条件で検証したか、どれだけの資源を使ったか、ほかの人が再利用できるかを分けて考えます。今回なら、形式化された最終定理と検証条件は確認できる一方、一般の仕事での成功率や費用対効果までは、この結果から求められません。

仕事への応用はここからの考察：AIの出力と、確認する仕組みを分ける

ここからは、発表された実験結果そのものではなく、和からとしての業務・研修への応用上の考察です。参考になるのは、AIが「できました」と言うことと、外部の基準で「できた」と確認することを分けるという設計です。

ただし、数学の証明と一般業務では、検証できる範囲が違います。テストやチェックリストは、そこで指定した条件の確認には使えますが、条件に含めていない誤りや、現実の目的への適合性まで保証するものではありません。

まとめ：成果の大きさと、主張できる範囲を分けて読む

今回の発表の中心は、既知の数学的議論を大規模に形式化し、機械検証できる形で公開したことです。企業の発表に加えて、公開コードと外部の数学者による検証報告もあります。一方で、生成までの期間、完成後の検証、利用した研究モデル、人間の先行成果、一般業務への適用可能性は、それぞれ区別する必要があります。

仕事に持ち帰るなら、「長くAIに任せればよい」という話より、何を達成したら完了なのか、その達成を何で確認するのかを具体化する題材として扱うのが適切です。和からの研修・関連解説については、以下のページをご覧ください。

出典・確認資料

［1］Anthropic「Formalizing Fermat’s Last Theorem」（2026年9月4日）。期間、行数、定理数、使用モデル、人間の関与に関する発表。
［2］Anthropic「Fermat’s Last Theorem in Lean 4」。READMEに定理文、検証方法、再実行手順、先行コードの出典を記載。
［2a］公開コード「FinalCheck.lean」。最終定理の公理依存の検査とMathlibの定理文への接続。
［3］Kevin Buzzard「FLT: Anthropic has beaten me to it」（2026年9月4日）。本人によるビルド・comparatorの実行報告と、自身のプロジェクトとの違い。
［4］Lean公式文書「Validating a Lean Proof」「Axioms」。証明の検査、公理の確認、信頼の前提。
［5］Lean公式サイト「Formalizing Fermat’s Last Theorem in Lean: A Landmark Mathematical Project」。人間側の形式化プロジェクトの方針。
［6］Chenほか「Prove2Me: An Open Collaborative Platform for Scaling Math Formalization」（2026年8月、プレプリント）。共同形式化基盤の説明。
［7］Annals of Mathematics、1995年141巻3号：Wiles「Modular elliptic curves and Fermat’s Last Theorem」、Taylor・Wiles「Ring-theoretic properties of certain Hecke algebras」。