ハクソク

世界を動かす技術を、日本語で。

フェルマーの最終定理の形式化

2026年9月5日原文(anthropic.com)

概要

  • Claudeによる Fermat’s Last Theorem（FLT） の初の完全なコンピュータ検証済み証明の達成
  • Leanプログラミング言語 を用いた自律的な形式化作業
  • 証明過程で 13百万行のLeanコード と 29,500個の中間定理 を自動生成
  • Prove2Meプラットフォームによる 多エージェント協働 の成功
  • 今後の数学研究とAI活用への 意義と展望

ClaudeによるFLT自動形式化の概要

  • 2024年、AnthropicのAI Claudeが Fermat’s Last Theorem（FLT） の完全自動形式化証明に成功
  • Lean証明支援系 を使用し、11日間で証明を完了
  • Claudeはほぼ自律的に 13百万行のLeanコード と 30,300個の定理証明 を生成
  • 最終証明では 29,500個の中間定理 を活用
  • この成果は、 Kevin Buzzard（Imperial College London） らによる長年のコミュニティ活動を基盤とする

FLT証明自動形式化の背景

  • Pierre de Fermat が1637年に命題を記述：aⁿ + bⁿ = cⁿ（n > 2）を満たす正の整数は存在しない
  • Andrew Wiles が1995年に初めて証明を発表、129ページに及ぶ複雑な内容
  • Wilesの証明 を自動形式化する試みは長年困難とされてきた
  • 証明支援系 Lean と Mathlib を基盤とした形式化プロジェクトが進行

証明自動化の意義と課題

  • 証明支援系 は論理的正当性を機械的に検証
  • 人間向け証明は多くの省略や既知の知識に依存しているが、 Lean は全てのステップを明示的に記述する必要
  • 複雑な証明の形式化は、 人的コストや時間 が非常に大きい
  • Claude は多エージェント協働と Prove2Me プラットフォームの活用でこの課題を克服

Prove2Meと協働自動化

  • Prove2Me は定理間の依存関係をDAG（有向非巡回グラフ）で管理
    • 各エージェントが次に証明すべき定理を効率的に選択
    • 複数エージェントの並列作業を実現
  • Leanの証明文と定理文を分離し、 コンパイルやリソース消費を最適化
  • 各定理に 自然言語による説明 を付与し、検索・再利用性を向上

証明過程と成果

  • Claudeは Wilesの証明の簡略版（Darmon, Diamond, Taylorによる解説） に基づき形式化
  • 最初の試行は協働の失敗もあったが、 Prove2Me 導入で大規模協働証明が実現
  • Leanの標準3公理 のみを用い、証明の正当性を完全に検証
  • 完成した証明は Mathlib のFLT定式化と一致

数学研究への影響と今後の展望

  • 巨大な証明の自動形式化により、 数学的知識の信頼性向上 と 査読負担の軽減 が期待
  • Kevin Buzzard によると、現代数学文献の自動形式化への大きな一歩
  • AI生成証明 の検証コスト削減、 人間による検証の補助 としてのAI活用
  • 今後は 主要定理の協働形式化 が消費者向けAIサブスクリプションでも可能になる見通し

謝辞と関連プロジェクト

  • 本証明は Andrew Wiles らによるFLT証明の歴史と、 Kevin Buzzard 率いるImperial College Londonのプロジェクト、 Lean/Mathlibコミュニティ の貢献を基盤とする
  • Henri Darmon, Fred Diamond, Richard Taylor の解説を参考
  • Anthropic および他研究機関による外部研究者支援プログラムも拡充中

詳細・全文証明は下記参照： https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...

Hackerたちの意見

ケビン・バザードのブログ記事もぜひ読んでみてほしいな。最近投稿されたばかりだよ：https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... この成果についての素晴らしい背景や、その意味、そして意味しないことについても触れてる。

└

数学はあんまり得意じゃないけど、ケビンは全ての数学者のために彼女をもっと旅行に連れて行くべきだと思うな。

└

「私のプロジェクトを5年間で運営するために100万ポンドもらったけど、Anthropicはたった11日で終わらせた。でも、もっとお金を使ったのかな…」って、スケール感がわかるよね。

└

ありがとう！そのリンクをトップテキストに追加したよ。できればそれをトップリンクにしたいんだけど（https://www.anthropic.com/research/formalizing-fermats-last-...をトップテキストに relegated したい）、HNはずっとhttps://news.ycombinator.com/user?id=kevinbuzzardの作業を追ってきてるし、私たちも大ファンだからね。でも、それはやりすぎかもしれないね。

その過程で、1300万行のLeanを作成し、29,500の中間定理を証明したんだ。すごいよね。これで、正しいと証明できることはモデルによって実現できるって考えがさらに強まると思う。

└

フェルマーがあのマージンに収められたとは思えない。絶対に正当化されたね。

└

既存の129ページの人間による証明と比べると特にね。

AIツールが進化するにつれて、こういった発表がどんどん増えていくと思う。エージェントによるコーディングはすごいけど、医療や数学、物理学の研究の価値にはかなわないよね。AIの力で、私の生きているうちに世界的な「万能薬」が登場することを楽観的に期待してる。コスト効率の良い大規模な遺伝子工学、すべての病気の治療法、さらには老化の治療法まで。未来は美しくも恐ろしい。

└

それは起こらないと思う。AIモデルは制約があるからね。こういうツールを使える人はほんの一握りなんだ。

└

老化を治すべきものだと思うと、なんだかすごいよね。自然な人間の経験の一部じゃないってことだし。神の役割を演じようとする人たちや、こういうことを応援する人たちには本当に疲れたよ。

この証明を作成するのにかかったスピードは、数学の大部分を形式化することが可能になったことを示している。これにより、一般的な数学の証明の中のエラーを見つけたり、新しい研究の審査の負担を軽減できるかもしれない。^ この部分は最初の数段落に入れるべきだったと思う。なぜこれが重要なのかを説明するのは、もっと早くにすべきだよね。

└

記事の著者が読者が最後まで読むと思ってたのは許してあげて。

Hacker Newsで議論の続きを見る