# Claudeが11日でフェルマーの最終定理を証明。評価：SHIP IT。

Published: 2026-09-07

Claudeは11日間で約60億トークンを費やし、フェルマーの最終定理の1300万行にわたるLeanによる証明（最初のエンドツーエンドのコンピューターチェック済み）を記述しました。2024年からこの形式化に取り組んできた数学者は、「数学的には本質的に何も教えてくれない」と言いながらも、感激しています。同日、囲碁世界ランキング1位の申眞諝（シン・ジンソ）が、コミ2子でKataGoを2勝1敗で破りました。評価：SHIP IT。

Canonical: https://thedailydiff.dev/ja/video/2026-09-04-fermat-lean/

## この動画の要点

- Claudeがフェルマーの最終定理をLean 4で形式化
- ChromiumサンドボックスRCE (CVE-2026-85046)、実際に悪用され、報奨金1,000ドル
- 申眞諝がコミ2子でKataGoを破る

## 翻訳されたトランスクリプト

オリジナルの英語ナレーションから翻訳されています。利用可能なオーディオとキャプションはYouTubeによって管理されています。

0:00 フェルマーは、自身の素晴らしい証明は余白に収まらないと述べましたが、 今日、Anthropicはその余白を公開しました。1300万行のLeanコードです。 これはMathlibの5倍のサイズで、すべての数学者がすでに 信じていた定理を証明しています。Anthropicが投稿したとき、トビリシでは10時から11時だったので、 当然、私は起きていました。 昨日、GoogleはChrome 152をリリースし、12個のセキュリティ修正が含まれていました。 そのうちの1つは、すでに実際に悪用されていたV8のバグで、報告者には 1,000ドルが支払われましたが、これは後で話すセダンよりも少ない額です。

0:26 また昨日、Mullvadは11月2日に公開暗号化DNSを停止し、 代わりにQuad9に支払うと述べました。今朝、Rust React CompilerはViteでネイティブになり、Hacker NewsはIBM Bobという AIコーディングエージェントを発見しました。 その後、Claudeがフェルマーの最終定理を形式化し、同じトップページで 韓国のグランドマスターが地球上で最強の囲碁エンジンを破り、 今日、人類は2分の1の成果を出しました。 このビデオでは、Claudeが実際に何を証明したか、その費用、

0:52 この研究にキャリアを費やした数学者がなぜ何も変わらないと言いながらも 喜んでいるのか、そして人間がいかにして囲碁で機械に勝ったのかを説明します。 9月4日金曜日、The Daily Diffです。 フェルマーの最終定理：2より大きい任意のnに対して、正の整数a, b, cは aのn乗＋bのn乗＝cのn乗を満たさない。 フェルマーは1637年頃に余白にこれを書き込み、その過程を示すことなく亡くなりました。 これにより、彼は「works on my machine」（私の環境では動く）でチケットをクローズした最初の開発者となりました。 1908年の10万金マルクの賞金には、最初の1年間で621件の誤った

1:25 証明が集まり、アンドリュー・ワイルズが最終的に1995年にそれを解決しました。 それは129ページに及び、査読者が検証するのに数ヶ月かかりました。 形式化とは、その証明をLeanという証明支援システムが 各ステップを機械的にチェックできるように書き換えることを意味します。インペリアル大学のケビン・バザードは、 2024年からまさにそれを行う人間による取り組みを主導してきました。設計図だけで86 ページにわたります。代わりに、Anthropicの研究者であるTianyi Pengは、数十台のClaudeエージェントを Prove2Meというプラットフォーム上でこれに投入しました。このプラットフォームは定理のDAGを維持しているため、 エージェントは次に何を証明すべきかを知ることができます。これがなければ、最初の

2:00 群れは誰が何を証明しているのか分からなくなり、それはオーケストレーション層がマーケティング予算付きの正規表現である場合に 起こることです。 11日後、ルートノードは「PROVED」と表示されました。1300万行のLeanコード、 29,500の中間定理、そしてClaude Fable 5.1にほぼ匹敵する内部モデルからの約60億の出力トークンです。 内部モデルはおおよそClaude Fable 5.1に匹敵するものです。 証明がLeanの3つの標準公理のみに基づいている場合にのみビルドは成功します。 つまり、ごめんなさい、ネイティブのdecideは使えず、ごまかしはできません。 チェックも安くはありません。

2:29 ゼロからのビルドには5時間半かかりました。 96コアと153ギガバイトのRAMを使い、定理名は 機械生成されているため、リポジトリ自体は「読むため」ではなく「チェックされるため」に書かれたと説明されており、 これは私がエンタープライズJavaを説明する際にも使う表現です。 さて、矛盾点です。 Anthropicの投稿では、Leanが疑いなく正しさを証明していると述べられています。 これに先を越されたケビン・バザードは、Anthropicが貸与した500ギガバイトの マシンでリポジトリをコンパイルし、チェックアウトを確認した後、次のように書きました。

2:56 引用するなら、「数学的には、この研究は本質的に何も教えてくれない」と。 彼はすでにその定理が真実であると99.9%確信しており、 この証明は新しい数学を加えていません。それが示しているのは、自動形式化が現在何ができるかということであり、 その点については彼は本当に興奮しています。 彼は5年間で100万ポンドを与えられましたが、Anthropicは11日間で、 あるコメント投稿者の手計算によると、60億の出力トークンは定価で 約30万ドルなので、機械の方が安かったです。 機械のトレーニングを含めなければの話ですが、そんなことをする人はいません。

3:24 最高の詳細：彼がウェールズの音楽フェスティバルにいて、 4Gの電波が1本しかないときに、聞いたことのない名前からメールが届いたので、彼はそれをいたずらだと片付け、 1週間後に読みました。これは、「end-to-end formalization」を含む件名に対する正しい対応です。 end-to-end formalization」を含む件名への正しい対応です。 一方、人間は1勝しました。 囲碁の世界ナンバーワンである申眞諝が、 最強のオープンソース囲碁エンジンであるKataGoを、ソウルで2子局で2勝1敗で破りました。 これはトッププロとルーキープロの間の差にほぼ相当します。

3:50 最終局は221手で11.5目勝ちし、 中盤以降99%の勝率を維持し、2億5千万ウォン（約17万ドル）とジェネシスG90を獲得しました。つまり、 つまり、超人的なAIを倒すための賞金は、GoogleのChromeサンドボックスエスケープに対する賞金の170倍です。 サンドボックスエスケープに対するGoogleの賞金の170倍です。彼の説明によると、彼は当初AIの手を真似て負けましたが、 彼自身のスタイルで盤面を構築することで勝利しました。これは私が今年聞いたAIに関する最も有用なアドバイスであり、 ボードゲームから得られたものです。 ボードゲームから得られたものです。 差分にもう2行。

4:22 oxcのRust React CompilerがViteで1つのフラグの背後でネイティブになりました。1,036ファイルのコードベースは、 コンパイルステップで14.3秒から0.81秒に短縮されました。 主にpackage.jsonからBabelを削除したことで、これは私のスキンケアルーチンでもあります。 package.jsonからBabelを削除したことによります。これは私のスキンケアルーチンでもあります。 そしてIBMは、Hi, I'm Bobと挨拶し、サブエージェントを生成し、メインフレームコードを最新化し、 メインフレームコードを最新化し、 Bobalyticsという分析製品を出荷するAIコーディングパートナーBobを立ち上げました。どこかの銀行は非常に 興奮しており、誰もライセンスを読んでいません。

4:51 金曜日1日のマージンとしてはこれだけたくさんあります。もし、私が話すのを聞くよりもこれを読みたいのなら、 The Daily Diffが毎朝あなたの受信トレイに届きます — daily diff dot devで無料で、リンクは下にあります。 dev、リンクは下にあります。 さて、今日の評決は、SHIP ITです。 カーネルはイエス、Buzzardはイエス、数学は変わっていません。 しかし、数学のチェック方法は変わりました。 それが今日の差分です。 AxrisiのNikoです。

5:09 責任を持ってマージしてください。

## 情報源

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com