フェルマーの最終定理のLeanによる形式化：1,000のClaudeエージェントと30時間、何が確認されたのか

フェルマーの最終定理は、証明の一歩一歩をコンピュータが検査する言語であるLeanで、完全に形式化されています。最初の完全な形式化は、2026年9月4日にAnthropicが発表しました。8月の11日間に、未公開の研究用モデルがそれを書き上げ、その間、1人の研究者がときどき方向を示しました。コードは公開されており、この定理を形式化する人間のプロジェクトを率いるインペリアル・カレッジ・ロンドンのケヴィン・バザード（Kevin Buzzard）は、それをコンパイルし、「確かに検査を通る」と報告しました。⁷2026年11月9日、Anthropicは、Claude Fable 5.2を動かす約1,000のエージェントからなるチームが「最小限の人の介入で、わずか30時間で定理を完全に形式化した」と述べました。¹その技術解説記事は、実行時間を28.7時間とし、これを「トイ実験」と呼んで、それが「証明を再現した」と書いています。²定理そのものは、1994〜95年にアンドリュー・ワイルズがリチャード・テイラーとともに証明しました。2つの実行はどちらも、その既知の証明を機械で検査したものです。

30時間の実行について確かなことは、はるかに少なくなります。11月12日の時点で、そのLeanのコードは公開されておらず、Anthropicの外の誰かがそれを確認したという報告も見つかりませんでした。時間、トークン数、規模の数字と、Claude Opus 5.5との比較は、Anthropic自身の記事と、モデルごとに1回だけの実行によるものです。どちらの実行についても、Leanの検査を通ったことが示すのは、述べられた定理がLeanの公理から導かれることです。形式的な命題がフェルマーの主張したことを述べているかどうかは示しませんし、証明を読めるものにするわけでもありません。9月の証明については、バザードと別の検査ツールが命題を確認しました。新しい実行については、その確認が行われたかどうかをAnthropicは述べていません。

以下では、何が変わったのか、Leanの検査が何を扱うのか、何が公開されているのか、誰が何を確認したのか、バザードが何を述べたのか、関連する2つの発表、そして短い歴史を順に紹介します。出典はすべて2026年11月12日に確認しました。

主な用語#

• Lean：証明支援系。そのカーネルは、それぞれの証明を言語の規則に照らして検査する小さなプログラムです。
• Mathlib：形式化された数学の、コミュニティによるライブラリ。ほとんどのLeanのプロジェクトがその上に築かれています。
• sorry：未完成の証明でもコンパイルできるようにするプレースホルダー。完全な形式化には1つもありません。
• 公理：証明が出発点にしてよい仮定。Mathlibが依拠しているのは、propext、Classical.choice、Quot.sound の3つです。
• Comparator：Leanプロジェクトのツール。別に書かれた命題と、許された公理のリストに照らして証明を検査し、それをカーネルで再実行します。¹⁶
• nanoda：Rustで書かれた独立のLeanのカーネルで、2つ目のチェッカーとして使われます。

フェルマーの最終定理はLeanで形式化されたのか、それは誰によるものか#

この定理は、nが2より大きいとき、aⁿ + bⁿ = cⁿ を満たす正の整数a、b、cは存在しない、と述べています。Anthropicの公開リポジトリは、これをLeanで theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n と述べています。⁵

Anthropicの最初の実行は、コロンビア大学のTianyi Pengのグループが作った共同形式化のプラットフォームProve2Meの上で、2026年8月7日に始まり、¹⁵最終的な定理は8月17日の夜に証明済みとされました。数十のエージェントが「Claude Fable 5.1におおむね匹敵する、汎用の社内研究用モデル」を動かし、約60億の出力トークンを消費しました。記事によれば、人による数学的な寄与は「Tianyiによる時折の大まかな指示に限られていた」。³付属のタイムラインは、人間は「目標とする定理の1行の命題を除いて、数学もLeanも一切書かなかった」と付け加えています。⁴

成果物には、2万9,511の定理と約1,300万行のLeanがあります。ワイルズの議論についての、Darmon、Diamond、Taylorによる1995年の解説に従っており、マズールの定理やラングランズ–タネルの定理といった深い前提を、議論が必要とする特別な場合について証明しています。また、バザードのインペリアル・カレッジのプロジェクトと、正則素数についてこの定理を形式化した先行プロジェクトflt-regularから、106のファイルを、出典を明記したうえで手直しして使っています。⁴

フェルマーの最終定理は、Freek Wiedijkの100の定理のリストの中で、最後まで形式化されていなかった項目でした。バザードは、この成果が「20年来のこのベンチマークを締めくくる」と書き、⁷2026年11月1日に最終更新されたWiedijkのページは、いまや100%と表示し、この定理を「Lean, Anthropic」の功績としています。¹³

30時間の実行は、9月と比べて何が新しいのか#

最も詳しい説明は、Barry Zhang、Tianyi Peng、Elle Najt、Keller Scholl、Lance Martinが書いた、Anthropicの開発者向けブログの記事です。²目的は、「Prove2Meも、作業を方向づける研究者もなしに、汎用のツールで組み立てたハーネスを使って」結果をやり直すことでした。

主導役のエージェント1つと補助役のエージェント999は、それぞれ、ネットワークにつながらない仮想マシン、LeanとMathlib、Gitのブランチ、共有データベースを持っていました。出発点となる材料も渡されていました。「エージェントには、60の命題のリスト、古典的な道筋の1文の概略、それらの命題が使う定義、そして以前の形式化で証明済みの47の補題を与え、主導役と補助役の役割を割り当てた」。

開始から約27分の時点で、すでに3つの命題が証明されていました。主導役は、補助役の多くが予算内では実現できないと判断した47の命題をいったん脇に置き、ほぼすべての補助役を残りの10の命題に回しました。この10の命題は約70分以内に証明されました。チームはその後、47の命題に戻りました。最も難しい部分はラングランズ–タネルの定理で、その担当のキャプテンは「時間内に終わる見込みは1%未満」と見積もっていました。チームはそれを2,418のタスクからなる木に分割し、開始から28.4時間の時点で証明しました。続いて28.7時間の時点で最終的な定理が証明され、主導役はこう書きました。「みんな、ありがとう。フェルマーの最終定理はmainに入った。公式のチェッカーでカーネル検査済みだ」。

記録されている介入は2つです。ハーネスが主導役に、残り時間を知らせる自動のリマインダーを19回送ったこと、そして開始から約18時間の時点で、Anthropicが「最後に保存した状態から実行を再開し、エージェントにさらに12時間を与えた」ことです。

発表記事は、これを単純化しています。28.7時間を30時間とし、技術解説記事が出力トークンと書くところを「アクショントークン」と呼び、技術解説記事がFable 5.2の初期バージョンと書くところで、モデルをFable 5.2としています。11月9日にアーカイブされた最初の文面は、Fable 5.2が「数学の参考文献を一切使わず、進捗を採点するための中間定理の命題のリストだけを使った」とも述べていました。²³11月11日、Anthropicはその一節を削除し、上の出発点の材料を引用した脚注を加えて、「モデルに提供した情報をより正確に説明するため」に段落を修正したと記しました。¹

	最初の形式化	30時間の実行
発表	2026年9月4日	2026年11月9日。11月11日に修正
モデル（Anthropicの報告による）	「Claude Fable 5.1におおむね匹敵する」社内の研究用モデル	「Claude Fable 5.2の初期バージョン」
期間	11日間（8月7日〜17日）	28.7時間。開始から約18時間の時点で、最後に保存した状態から再開
エージェント	数十	約1,000：主導役1、補助役999
人の関与（説明による）	1人の研究者による時折の大まかな指示。目標の1行の命題は人が書いた	研究者による舵取りはなし。命題、概略、定義、最初の証明からの47の補題を提供。自動のリマインダー19回
調整	Prove2Meのプラットフォーム	Git、共有データベース、隔離されたサンドボックス
出力トークン	約60億	3分の1。具体的な数字はなし
証明の規模	2万9,511の定理、約1,300万行	長さは7分の1。行数はなし
公開されているもの	Leanのコード、ビルドと検査のスクリプト、閲覧用のページ、17ページのタイムライン	2本のブログ記事とその図

「形式化された」とはどういう意味か、Leanの検査は何を立証するのか#

証明を形式化するとは、Leanが公理から始めてすべてのステップを検査できるように、それを書き直すことです。9月のリポジトリのビルドが通ったということは、カーネルがその中のすべての宣言を受理したということです。ビルドは、fermat_last_theorem がちょうど3つの標準的な公理に依存していなければ失敗するようにも設定されており、これによって、その下のどこかに sorry や追加された公理がある可能性は排除されます。⁵

これは、証明については強い証拠ですが、命題については限られた証拠にすぎません。バザードの11月12日の投稿は、2行の例を挙げています。a、b、cが正であるという条件を省いた、フェルマーの最終定理のLeanでの定義は偽です。Leanの自然数には0が含まれるからです。「だからといって、命題がコンパイルできなくなるわけではない！」と彼は書いています。コンパイルできなくなるのは、その命題の証明のほうだけです。⁸誰かが命題を読み、それが正しい命題であることを確かめなければなりません。

さらに3つの限界があります。リポジトリのREADMEは、「どのツールにも検査できないのは、それぞれの中間定理が、その名前が示唆するとおりの意味を持っているかどうかだ」と記しています。⁵Leanの証明は何も説明しません。同じREADMEは、ソースが「読まれるためではなく、検査されるために書かれている」としています。そして、カーネルは信頼するしかありません。バザードは、見つかってから4時間後に修正された、Leanのカーネルの健全性に関わるバグを振り返り、独立した複数のカーネルで検査すればそうしたバグに備えられると論じています。⁸

彼の投稿は、AIが生成したLeanのコードに問うべき4つの問いを示しています。公開されている情報をもとに、2つの実行に当てはめると次のようになります。

バザードの問い	最初の形式化	30時間の実行
Leanの命題は、非形式的な命題と一致しているか	Leanの自然数と、Mathlibのべき乗の関数を使っている。バザードは読んだと述べている。comparatorが、Mathlibだけをインポートするファイルとこれを照合した	記載なし。エージェントには命題と定義が渡されていた
コードはコンパイルできるか	はい。Anthropicのゼロからのビルドと、Anthropicが貸したマシンでのバザードのビルドで	主導役のエージェントは「公式のチェッカーでカーネル検査済み」と報告。外部でのビルドはできない
述べられたとおりの定理を証明しているか	comparatorを通過。Anthropicとバザードがそれぞれ実行	報告なし
Leanのカーネルのバグを突いていないか	Anthropicの実行で、nanodaがすべての宣言を受理。nanodaは4つの小さなパッチを当ててビルドされており、Anthropicによれば型付けの規則は一切変えていない	報告なし

新しいLeanのコードは公開されているのか、誰でも再ビルドできるのか#

いいえ。11月12日の時点では公開されていません。発表記事も技術解説記事も、コードへのリンクを載せていません。GitHubにあるAnthropicのフェルマーのリポジトリは9月24日が最終更新で、置かれているのは、Lean 4.33.1とMathlib v4.33.0による9月の証明だけです。⁵Anthropicのもう1つの公開Leanリポジトリであるformal-mathにあるのは、関係のない3つのプロジェクトです。¹⁷実行のプロンプト、ログ、採点器、ハーネスが公開された形跡も見つかりませんでした。

最終的な命題、LeanとMathlibのバージョン、行数で見た規模、そしてcomparatorや2つ目のカーネルがそれに対して実行されたかどうかは、いずれも分かっていません。

9月の証明は、十分なハードウェアがあれば誰でも再ビルドできます。Anthropicのビルドは、96の並列ジョブで5時間32分かかり、メモリの使用量は最大で153 GBでした。READMEは、約15時間かかるcomparatorの検査には300 GBを見込むよう勧めています。バザードは最初に自分のコンピュータで試しましたが、「あっという間にメモリが足りなくなった」ため、Anthropicが96コアのマシンを一時的に使えるようにしました。⁸READMEは、このリポジトリを「研究の成果物。保守されておらず、貢献も受け付けていない」としています。⁵

何が自己申告で、Anthropicの外の誰が何を確認したのか#

30時間の実行についての情報は、すべてAnthropicから出ています。4つの点は、もう少し詳しく見る必要があります。

• モデル。 エージェントが動かしたのは、Fable 5.2の「初期バージョン」でした。²それが公開されたモデルと同じように振る舞うかどうかは、書かれていません。
• Opus 5.5との比較。 発表記事によれば、同じ設定でOpus 5.5は「18時間で形式化の26%しか完了せず、30時間を過ぎてもほとんど進まなかった」。¹図は完了度を「証明された命題の重み付きの割合」として測っていますが、重みは示されておらず、図の説明文には「モデルごとに1回の実行」とあります。1回の実行では、結果がどれだけばらつくかは分かりません。
• トークンと規模。 絶対的な数字は示されておらず、どちらの記事も、長さをどう測ったかを述べていません。これが重要なのは、Anthropicのタイムラインに引用されている、9月の証明についてのClaude自身の評価が、「証明ファイルの全行の約5分の1は、ツリー内のほかの場所にある宣言の逐語的なコピーだ」と指摘しているからです。⁴
• 出発点。 47の補題と定義は、9月4日から公開されている9月の形式化から来ています。モデルが訓練の中でそのコードを見ていたかどうかを、Anthropicは述べていません。

9月の証明には、外部の読み手がいます。バザードはそれをコンパイルし、comparatorを実行し、さらにコメント欄で読者に語ったところによれば、「（Claudeによれば）数学的な定義でも定理の証明でもない、コードベースのすべての行を手作業で調べた」。⁷別の読者には、証明は機械が検査するが、命題は誰かが読んで「正しい定理に対応していることを確かめなければならない。だが、それは私がやった」と説明しています。Anthropicは、「証明をレビューし、コメントをくれたこと」について彼に謝意を述べています。³リポジトリ自身のメタデータは、今もレビューの状態を「self-assessed」（自己評価）と記録しており、レビュアーの一覧は空です。⁶

30時間の実行については、外部の確認は見つかりませんでした。バザードの11月12日の投稿は、9月の証明を論じていますが、新しい実行には触れていません。⁸XenaブログのBlueskyアカウントは2025年12月から投稿しておらず、MathstodonのLeanとフェルマーに関する2つのハッシュタグにもこの件についての投稿はなく、Leanコミュニティのチャットの公開アーカイブは2026年2月28日が最終更新だったため、そこでの議論は読めませんでした。²²数学者が運営するサイトProofs and Promptsは、11月10日に発表を取り上げ、Anthropicについて「1,000のClaudeエージェントのチームがフェルマーの最終定理の証明をわずか30時間で形式化したと自慢している」と書きました。¹⁸サイトは、Anthropicが以前にもこの定理を形式化していたことを読者に思い出させ、エージェントがどこで答えを見つけたのかについての冗談を、サイトの公式見解ではないと断ったうえで付け加えています。

ケヴィン・バザードは何を述べたのか、人間によるFLTプロジェクトはどうなるのか#

バザードのインペリアル・カレッジのプロジェクトは、リチャード・テイラーが計画し、KhareとWintenbergerの研究を取り入れた、定理への現代的な道筋をたどっています。¹¹英国工学・物理科学研究会議（EPSRC）が、助成番号EP/Y022904/1により、2024年10月から2029年9月まで資金を出しており、掲げられた最初の目標は、定理を1980年代末までに知られていた結果に帰着させることです。¹²

9月4日の投稿「FLT: Anthropic has beaten me to it」（FLT：Anthropicに先を越された）で、彼はAnthropicを祝福し、この結果が何を意味するかを率直に述べました。⁷「数学的には、Anthropicのこの仕事は本質的に何も教えてくれないことに注意してほしい」と彼は書いています。証明が正しいことはすでに99.9%確信しており、「形式化は、証明についての初期の文献に忠実に従っているだけで、何も付け加えていない」からです。しかし、「この仕事がたしかに教えてくれるのは、自動形式化の分野で何が可能かということだ」。彼は、機械による検査が「私の分野のさまざまな重要な結果の証明で、正確に何が仮定されているのか」を示すことを期待しています。1か月後、彼は、専門家にしか知られず、公開された記述もない、自分の分野の議論があったことが、好奇心にもとづく研究を離れて形式化に移った理由だと説明しました。「Leanはごまかせない。これは、ごく早い段階で学ぶことだ」。⁹

自身のプロジェクトについては、こう書いています。「上のニュースへの素朴な反応は、私にはもうやるべき仕事がない、というものだろう。そうではない」。Anthropicの証明は、彼がEPSRCに約束した内容よりも先まで進んでいます。しかし彼は、Mathlibへの貢献も約束しており、それは続いています。さらに「人間が現代的な証明を探索できる動的な文書」も約束しており、これはAnthropicが作るとは考えていません。彼は、自分には5年間で100万ポンドが与えられたと記し、Anthropicはそれ以上を費やしたのだろうかと問いかけています。

10月には、Jeremy Avigad、バザード、ほか5人の形式化の研究者が彼のブログに寄せたゲスト投稿が、より鋭く述べました。「成果は見事だが、このAIが生成したコードには、おそらく継続的な価値はほとんどない」。¹⁰彼らの懸念は再利用で、Anthropic自身のタイムラインも、その証明は「まだMathlibが受け入れる形にはなっていない」と述べています。⁴インペリアル・カレッジのリポジトリは今も活動しており、mainブランチでは10月22日までMathlibの更新が続いています。¹¹

11月12日の時点で、30時間の実行についてのバザードの公開のコメントは見つかりませんでした。最新の投稿は、こう締めくくられています。「『Leanで検査されているから正しい』という言い方に、意味を持たせることはできる。だが、それには『Leanのコードがコンパイルできる』ことを超える作業が必要だ」。⁸

AxiomはStacks Projectで何を形式化したのか#

数学のためのAIに取り組むスタートアップのAxiomは、2026年11月4日付で発表を出しました。¹⁹Proofs and Promptsは、11月7日にこれを掲載しました。¹⁸Stacks Projectは、代数幾何学についてのオープンソースのリファレンスで、2005年にコロンビア大学のJohan de Jongが始めました。Axiomは、「Stacks Projectの全体」を「約1,600万行のコード」で形式化したとし、その成果を「これまでに作られた中で最大の、統合された再利用可能な形式化数学のライブラリ」と呼んでいます。これはAxiom自身による説明です。

リポジトリのREADMEは、sorry も native_decide もないこと、証明は3つの標準的な公理だけを使っていること、ライブラリには約6万3,000のLeanのモジュールがあることを述べています。²⁰ライブラリは2層からなります。人がStacks Projectと照らし合わせて確認したコードであるStacksCoreと、「AIエージェントが書いた」コードであるStacksFrontierで、READMEによれば、後者こそ「レビューが最も必要とされる」部分です。Axiomは、命題の忠実さが「マルチエージェントによる監査を通じて、大規模かつ自動的に担保されている」とし、ほかの相互確認も挙げています。¹⁹また、エージェントが元の文献の中に、局所的な修正が必要な命題を数十個見つけたとしています。外部のレビューは、まだ見つかっていません。

これは新しい証明にインポートして使うためのライブラリで、Axiomによるヴェイユ予想の形式化は、すでにこれを土台にしています。Axiomは、de Jongが10月21日に、当面はAIが生成したコメントやプルリクエストを上流のStacks Projectに送らないよう求めたことにも触れています。¹⁹9月にバザードは読者に、Stacksの形式化は「おそらく現時点でも実現可能だが、今日では高くつく」一方で、それをMathlibに取り込むのは「また別の話」だと語っていました。⁷Axiomによる有限単純群の分類の形式化については、以前有限単純群の分類のLeanによる形式化で取り上げました。

インペリアル・カレッジのLanglands Labとは何か#

インペリアル・カレッジ・ロンドンは、2026年10月27日にLanglands Lab（ラングランズ・ラボ）を発表しました。²¹Proofs and Promptsは、11月4日にこれを掲載しました。¹⁸ラボは、XTX Marketsからの500万ポンドの助成金で運営され、バザードが率います。対象はラングランズ・プログラムで、インペリアル・カレッジはこれを、分野と分野、特に数論と解析学のあいだのつながりを明らかにしようとする取り組みだと説明しています。ラボは、Leanで検証された新しい結果、それを理解しやすくする論文、そして証明をたどるための無料の対話型ツールを生み出すことを目指しています。

助成金は、2027年から4年間、5人の博士課程の学生と3人のポスドク研究者を支援します。学生は、「研究成果に責任を負う前に、取り組んでいる数学を深く理解し、AIの助けなしに自分の結果を説明し、擁護することを求められる」とされています。発表には、バザードの次の言葉が引用されています。「AIは、数学の研究をすることの意味を変えつつある。次の世代の数学者をどう育てるかを、考え直す必要がある」。

検証が難しいAI生成の証明にとって、なぜこれが重要なのか#

理由はAnthropic自身が挙げています。形式化は、数学者が結果に確信を持つ助けになり、「AIモデルが、人間には検証しにくい結果を生み出す場合には、これはいっそう重要になる」。¹フェルマーの最終定理は、誰もそれを疑っていなかったからこそ、きれいなテストになります。正しい命題は短く、よく知られているので、間違った命題であればすぐに気づけます。

AIが生み出した新しい結果は、もっと難しくなります。バザードは、Leanのコードが付いていたOpenAIの290の定理のうち、「約38では、Leanのコードが論文の主定理を証明するどころか、述べてさえいない」と報告しています。⁸Axiomによる有限単純群の分類では、命題はAIが書いたライブラリの約5,600行の定義の上に成り立っており、散在型単純群の定義を注意深く確認したと言う人に、彼はまだ会ったことがありません。同じ問いは、AIはアーロンソン＝アンバイニス予想を証明したのかとOpenAIのヤン–ミルズの証明の記事でも取り上げました。

形式化が速くなるということは、形式的な証明が付いた、AIによる主張がもっと増えるということです。その後に続く確認には、今も人が必要で、この規模になると大きなマシンも必要です。

短い歴史：ワイルズから、Wiedijkのリストの最後の定理まで#

日付	出来事
1637年ごろ	フェルマーが、ディオファントスの『算術』の自分の写本の余白に、この主張を書き込む3
1993年6月	ワイルズが、ニュートン研究所での3回の講義で証明を発表。確認が始まって2か月後に、証明に隙間が見つかる
1993〜94年	ワイルズが約1年をかけて修復する。最初は1人で、のちにリチャード・テイラーとともに
1995年5月	ワイルズの論文と、テイラー–ワイルズの論文が、Annals of Mathematics第141巻に掲載される14
1999年	Wiedijkが形式化の状況を追っている定理の「トップ100」のリストは、この年のもの13
2023年11月	バザードが、GitHubでインペリアル・カレッジのFLTリポジトリを開設11
2024年10月	彼のEPSRCの助成が始まる（2029年9月まで）12
2026年8月7日〜17日	Prove2Me上での、Anthropicの最初の実行
2026年9月4日	Anthropicが最初の完全な形式化を発表。バザード：「Anthropicに先を越された」
2026年10月27日	インペリアル・カレッジがLanglands Labを発表
2026年11月4日	AxiomがStacks Projectの形式化を公開
2026年11月9日	Anthropicが、1,000のエージェントによる30時間の実行を報告

研究の記録にとって何を意味するのか#

AIが書いた形式的な証明を信頼する前に、読者には次の詳細が必要です。誰が形式的な命題を書き、誰がそれを非形式的な命題と照らし合わせたのか。チームの報告によればどのモデルが使われ、人がそれに何を与えたのか。コードのどの版が、どのバージョンのLeanとMathlibで検査されたのか。そして、どの検査が、いつ、誰によって実行されたのか。9月の証明については、Anthropicのリポジトリと記事がその大半に答えています。30時間の実行については、大半がまだ答えられていません。

AIの助けを借りた結果を公開する研究者は、同じ詳細を、日付と署名を付け、コードへのリンクとともに書き残すことができます。Papexでは、AIアプリがそうした下書きを準備でき、研究者がそれを確認して署名します（AIアプリがPapexとどう連携するか、英語）。そうした記録は、数学が正しいかどうかについては何も述べません。それはLeanと、命題を読む人々の役割のままです。

未解決の点に決着をつけるのは、次のものです。30時間の実行のコードの公開、それに対するcomparatorと2つ目のカーネルによる検査、Anthropicの外の誰かによる命題の確認、そして完了度の数字の背後にある重みです。

利害関係について：この記事はAnthropicのClaudeモデルについて報じており、Claudeを使って下書きされました。読者は、この点を念頭に置いて本記事を評価し、下記の出典を確認してください。

出典#

1. Introducing Claude Fable 5.2 and Claude Mythos 5.2（Anthropic、2026年11月9日、11月11日に編集）、2026年11月12日確認 ↩ a b c d
2. Safely scaling multi-agent teams with Claude Fable 5.2（Barry Zhang、Tianyi Peng、Elle Najt、Keller Scholl、Lance Martin、claude.dev、2026年11月9日）、2026年11月12日確認 ↩ a b c
3. Formalizing Fermat's Last Theorem（Anthropic、2026年9月4日）、2026年11月12日確認 ↩ a b c
4. Formalizing Fermat's Last Theorem in Lean: a timeline and selected excerpts from Claude's reasoning（Anthropic、17ページ）、2026年11月12日確認 ↩ a b c d
5. anthropics/fermats-last-theorem：README、FinalCheck.lean、コミットaa2d8b34（GitHub、2026年9月24日最終更新）、2026年11月12日確認 ↩ a b c d e
6. anthropics/fermats-last-theorem、formalization.yaml（GitHub）、2026年11月12日確認 ↩
7. FLT: Anthropic has beaten me to it とコメント（Kevin Buzzard、Xena、2026年9月4日）、2026年11月12日確認 ↩ a b c d e
8. 「…and the proof is checked in Lean」（Kevin Buzzard、Xena、2026年11月12日）、2026年11月12日確認 ↩ a b c d e f
9. To grieve, or not to grieve?（Kevin Buzzard、Xena、2026年10月1日）、2026年11月12日確認 ↩
10. How to Formalize All of Mathematics（Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash、Adam Topaz、Xena、2026年10月16日）、2026年11月12日確認 ↩
11. ImperialCollegeLondon/FLT：READMEとコミット履歴（GitHub）、2026年11月12日確認 ↩ a b c
12. ImperialCollegeLondon/FLT、GENERAL.md（GitHub）、2026年11月12日確認 ↩ a b
13. Formalizing 100 Theorems（Freek Wiedijk、ラドバウド大学、2026年11月1日最終更新）、2026年11月12日確認 ↩ a b
14. Modular elliptic curves and Fermat's Last Theorem（Andrew Wiles、Annals of Mathematics第141巻、1995年、第3号）、2026年11月12日確認 ↩
15. Prove2Me: An Open Collaborative Platform for Scaling Math Formalization（Shuze Chenほか共著者4人、arXiv:2608.28433）、2026年11月12日確認 ↩
16. leanprover/comparator：README（GitHub）、2026年11月12日確認 ↩
17. anthropics/formal-math：README（GitHub）、2026年11月12日確認 ↩
18. Newsfeed、2026年11月4日・7日・10日の項目（Proofs and Prompts）、2026年11月12日確認 ↩ a b c
19. The Stacks Project, formalized in Lean（Axiom、2026年11月4日）、2026年11月12日確認 ↩ a b c
20. AxiomMath/Stacks：README（GitHub）、2026年11月12日確認 ↩
21. £5 million grant to establish new laboratory for AI-assisted mathematics at Imperial（インペリアル・カレッジ・ロンドン、2026年10月27日）、2026年11月12日確認 ↩
22. LeanコミュニティのZulipアーカイブ、索引ページ（2026年2月28日最終更新）、2026年11月12日確認 ↩
23. Introducing Claude Fable 5.2 and Claude Mythos 5.2、最初に公開された版（インターネットアーカイブの保存版、2026年11月9日 18:57 UTC）、2026年11月12日確認 ↩