Anthropic Claudeがフェルマーの最終定理を形式化。証明を発見したわけではない

Anthropic Claudeは、11日間でフェルマーの最終定理を形式化した。しかし、定理を発見したわけでも、Andrew Wilesの証明に取って代わったわけでもない。この違いは重要だ。今回の成果が関わるのは、検証、規模、そして研究自動化である。これまで未解決だった問題への新たな解答ではない。

Anthropicは2026年9月4日にこの結果を発表した。同社によれば、数十のClaudeエージェントが1,300万行のLeanコードを生成し、3万300件の中間定理を証明した。このうち2万9,500件が最終証明に含まれている。

Leanは証明支援系であり、各形式的なステップが明示的な定義、公理、先行定理から導かれるかを検査する。形式化とは、専門家向けに書かれた数学を、Leanの論理カーネルが検証できるほど精密な指示へと変換する作業だ。

証明が現代数論、代数幾何学、調和解析、表現論にまたがる場合、このプロセスは単なる事務作業では済まない。人間の著者は、よく知られた手順を日常的に省略する。Leanはそうした近道を一切認めない。

したがって、Claudeによるフェルマーの証明は、AI対数学者という構図よりも明確な対比を生み出す。重要なのは、機械規模の形式化と、慎重に維持される人間可読な形式数学との比較だ。

この緊張関係により、Kevin BuzzardがImperial College Londonで進めるプロジェクトが物語の中心に置かれる。Anthropicのシステムは短期間でエンドツーエンドの検証済み結果に到達した一方、コミュニティプロジェクトは再利用可能なライブラリ、読みやすい抽象化、査読済みの貢献を重視してきた。

どちらの道筋でも有効な形式数学を生み出せる。最適化している成果が異なるのであり、Anthropicの結果は、カーネルが「正しい」と判断した後にどの性質を重視すべきか、研究者に決断を迫る。

Anthropic Claudeが実際に完了したこと

Anthropic Claudeは、確立済みの数学的議論を完全な機械検証済み成果物へと翻訳した。これは証明を発明することとは異なる。

フェルマーの最終定理は、nが2より大きいとき、aⁿ + bⁿ = cⁿを満たす正の整数は存在しないと述べる。Pierre de Fermatは1637年ごろにこの主張を書き残したが、受け入れられた一般的証明が現れるまでには3世紀以上を要した。

Andrew Wilesは1993年に証明を発表した。その後、査読者が重大な欠落を発見し、WilesはRichard Taylorとともに修正したうえで、1995年に訂正済みの研究成果を発表した。この経緯は、通常の数学的査読がいかに困難になり得るかを示す点で重要だ。

ClaudeはWilesとは別の道筋を見つけたわけではない。Anthropicの形式化に関する説明によれば、このシステムはHenri Darmon、Fred Diamond、Richard Taylorによる簡略化された解説に従った。

この議論は依然として、Gerhard Frey、Jean-Pierre Serre、Ken Ribet、Wiles、Taylorら、多くの研究者が築いた数学的連鎖に基づいている。Claudeの役割は、専門家の読者が不足部分を補うことに頼らず、その連鎖をLeanで表現することだった。

Anthropicはこの成果を、フェルマーの最終定理に対する初の完全なコンピュータ検証済み証明と表現している。「証明」が完成した形式的成果物を指すなら、この表現は擁護できる。だが、読者がそれを新たな数学的発見と受け取れば、誤解を招く。

形式的証明と非形式的証明は関連しているが、異なる役割を果たす。数学論文は資格を持つ人間にアイデアを説明する一方、形式的証明は論理カーネルがすべての依存関係を検証できるだけの詳細を与える。

Leanは、専門家が標準的だと認識するからという理由だけで文章を受理しない。すべての定義が存在しなければならない。すべての型が一致しなければならない。すべてのインポート済み結果が、有効な項の明示的な列を通じて最終命題につながらなければならない。

Anthropicによると、この取り組みは研究者のTianyi Pengが、Claudeが形式化を前進させられるかを試したことから始まった。Pengは、AI支援形式数学のツールを開発するColumbia Universityのグループと協力している。

システムは当初、苦戦した。Anthropicは、初期のエージェントがプロジェクトの全体像を見失い、効果的な連携を止めたと報告している。こうした失敗した試行も、最終証明に含まれる定型文以外の行の約7%に寄与した。

成功した実行では、形式化プロジェクトを有向非巡回グラフとして表現するオープンな協働プラットフォーム、Prove2Meが使われた。各ノードは定理の命題を表し、依存関係は、どの結果を先に完了させる必要があるかをエージェントに示す。

Claudeエージェントはこの構造を用い、作業を分割し、既存の結果を探索し、中間命題を証明し、完了済みのコンポーネントを再利用した。Anthropicはこのプラットフォームを、Claude Codeのマルチエージェント・ハーネスと組み合わせた。

同社によれば、最終キャンペーンでは、社内の汎用研究モデルから約60億出力トークンを消費した。Anthropicはこのモデルを、Claude Fable 5.1とおおむね同等のものと説明している。

これらの数字が示すのは計算の規模であって、Claudeの一般的な信頼性ではない。Anthropicは、同等の形式化プロジェクト全体における成功率や、失敗したキャンペーンの完全な母数を示していない。

それでも完成した成果物は具体的だ。公開されたLeanリポジトリでは、正の自然数と3以上のすべての指数について定理を述べている。

このリポジトリには、証明への経路、ソースファイル、検証資料、閲覧可能な生成ページも含まれる。そのため、スクリーンショットや選別された記録だけで示されるデモンストレーションよりも、中心となる数学的主張を詳しく検証できる。

公開日は、元のホットリスト項目にあった時期の空白も解消する。Anthropicはこの記事の公開日の2日前、2026年9月4日に発表を公開した。

ClaudeによるLean 4の成果が重要な理由

本質的な変化は、汎用AIシステムが、確立済み数学の大規模な体系を形式化するための規模の壁を越えたことにある。

今回の発表以前から、フェルマーの最終定理の形式化は活発な国際プロジェクトだった。Kevin BuzzardはImperial College Londonで公開の取り組みを率いており、支援助成金は2029年9月まで続く予定だ。

その形式化プロジェクトは、単一の最終定理を追求するだけではない。貢献者は、数論、幾何学、関連分野における再利用可能な基盤を構築しながら、それらをMathlibにどう取り込むべきかを検討している。

Mathlibは、Leanコミュニティが維持する数学ライブラリだ。形式化を行う人々に共有の定義と検証済み定理を提供しており、ソフトウェア開発者がすべての関数を作り直すのではなく、確立済みのライブラリに依存するのと同じような役割を果たす。

このライブラリは、公開済み数学をまだ部分的にしか符号化していない。人間による証明は、数十年にわたる文献を引用し、広範な専門知識を前提にできる。Leanプロジェクトは、各前提条件をMathlib内で見つけるか、自ら形式化する必要がある。

この不足しているインフラが、Anthropicの出力規模を説明する。同社によれば、1,300万行はMathlibの5倍以上の規模だが、生成された証明はおそらく必要以上に長いことも認めている。

コード量は数学的深さを測る明確な指標ではない。生成ファイルには、繰り返された構成、冗長な証明項、人間の形式化者なら再利用可能な抽象化に置き換える成果物が含まれ得る。

それでも、この規模を単なる通常のオートコンプリートとして片付けることはできない。システムは依存グラフ全体で数万の検証済み命題を接続し、それらを厳密な最終定理へ導く必要があった。

以前の形式化の取り組みでは、重要な部分集合が完成していた。2024年のプロジェクトは、Kummerのアプローチを用いて、相当数のケース群をカバーする正則素数に関する証明を作成した。この研究は、Leanに有用な代数的数論も加えた。

完全な現代的証明には、より広範なインフラが必要となる。フェルマー方程式の仮想的な解をFrey楕円曲線へ結び付け、モジュラー性に関する結果とRibetの定理を組み合わせて矛盾を導く。

この要約の各フレーズの背後には、大規模な形式ライブラリが隠れている。楕円曲線、モジュラー形式、ガロア表現、変形理論、解析的評価にはすべて、厳密な定義と補助定理が必要だ。

Anthropicの成果は、言語モデルがこのインフラの構築を、はるかに高い速度で支援できるようになったことを示唆している。これこそが、数学、ソフトウェア検証、その他の形式的推論を基盤とする分野にとっての真の転換点だ。

変化はプロジェクト管理にも関わる。単一のチャットボット・セッションでは、数百万行と数千の依存目標の状態を保持するのは難しい。成功したシステムは、その状態をProve2Meに外部化した。

このプラットフォームの定理グラフは、エージェントに共有地図を与えた。自然言語の説明によって命題を検索可能にし、ファイルを分けることでコンパイルのオーバーヘッドとリソース使用量を抑えた。

付随する協働に関する論文は、このアーキテクチャを、人間とAIの貢献者にまたがって数学の形式化を拡張する方法として提示している。Anthropicの実験は、この考え方に対する注目度の高いストレステストとなった。

この仕組みは大規模なソフトウェア工学プロジェクトに似ている。作業者には小さなタスク、明示的なインターフェース、依存関係のシステム、共有状態、自動検査が必要だ。知性だけではプロジェクトの一貫性を保てない。

AI開発者にとって、これは重要な教訓だ。周囲のシステムが状態を保存し、各作業単位を絞り込むと、モデルは長期的なタスクでより有用になる。

数学者にとって、この結果は形式化の予想コストを変える。かつては何年もの協調作業が必要に見えた定理が、AI中心のワークフローによって2週間未満で符号化された。

これは人間の仕事を不要にするものではない。人間の努力がどこで希少になるかを変える。表現の選択、再利用可能なライブラリの設計、結果の解釈、プロジェクト品質の監査は、コード生成が加速するほど重要になる。

主な競争は速度と再利用性の間にある

主な対抗者は別のAI研究所ではなく、永続的な共有インフラとして形式数学を構築する、人間がキュレーションするアプローチである。

Anthropicの成果物は、最終定理への到達に最適化されている。Buzzardのコミュニティプロジェクトもフェルマーの最終定理の証明を目指すが、その道筋をMathlibを慎重に拡張する機会として捉えている。

こうした優先事項は重なり合うが、同一ではない。大規模な生成成果物は、対象となる命題を証明できても、読み取り、保守、再利用が難しいままであり得る。

Anthropicは自らのリポジトリを研究成果物と呼んでいる。プロジェクトは保守されず、貢献も受け付けないと明記している。これは、この公開をMathlibの洗練された拡張と取り違えるべきではないことを示している。

この違いは、本番ソフトウェアに似ている。プログラムはテストに合格しても、重複、不明確なインターフェース、後の変更を高コストにする設計を含み得る。

形式数学には、さらに別の層が加わる。Leanは宣言が論理的に有効かを検査するが、定義が概念を優雅に捉えているかは判断しない。また、中間定理が最も有用な一般性を持つかも決められない。

人間の形式化者は、多くの将来の証明を支える抽象化を選ぶために何日も費やすかもしれない。1つの根定理を目標とする自律的なキャンペーンは、現在の目標をより速く閉じる局所的な構成を選び得る。

それは局所的な構成が誤りであることを意味しない。生み出される価値が変わるだけだ。一方の道筋は検証済みの到達点を提供し、もう一方は査読済みの数学ライブラリを目指す。

Anthropicによると、初期の失敗した試行で生み出されたコードも最終実行に寄与したという。その成果を再利用したことは柔軟性を示す一方、異なる戦略の下で作られたレイヤー間の一貫性には疑問も残る。

証明は膨大な規模であり、手作業での行単位レビューは現実的ではない。研究者には代わりに、アーキテクチャの要約、依存関係マップ、独立して実行できる検証手段が必要となる。

Anthropicは、数学上の節目とLeanの宣言を結び付けるPROOF-PATH.md文書を提供している。これは、機械による受理と人間による理解をつなぐ重要な橋渡しだ。

Kevin Buzzardはこの成果物をレビューし、異例なほど強い支持を表明した。Anthropicの発表で彼は、この達成はAIによる自動形式化の成果物が、追加の作業レイヤーを支えられるほど十分に信頼できることを示していると述べた。

彼の支持が重要なのは、同じ形式化目標を追う大規模な人間の共同プロジェクトを率いているためだ。ただし、それは両プロジェクトの目標が同一になったことを意味しない。

コミュニティプロジェクトは、整理された定義、より小規模な証明、ドキュメント、再利用可能なコンポーネントを引き続き提供できる。Anthropicの成果は、統合すべき不足領域を特定する助けにもなり得る。

これはもっともらしい役割分担を生み出す。AIエージェントが広範な形式的足場を構築し、専門家が有用な部分を圧縮、再編し、上流の共有資産へ取り込む。

もっとも、クリーンアップが慎重な構築より自動的に安価になるわけではない。生成コードは、その内部的な選択を理解しにくい場合、レビュー負荷を増やしかねない。

したがって重要な指標は、1日に生成された行数ではない。専門家レビューを通過し、共有ライブラリに入り、将来のプロジェクトで必要な労力を減らす検証済みコードがどれだけあるかを測るべきだ。

これは純粋数学を超えて重要である。形式手法は、コンパイラの正しさ、ハードウェア検証、暗号プロトコル、安全性が重要なソフトウェアを支えている。

組織は近いうちに、人間のレビュアーの処理能力を上回る規模で機械検証済みの成果物を生成するかもしれない。主張を仕様、ソース資料、テスト、承認判断へ結び付ける記録が必要になる。

検索可能なAI knowledge baseは、長期プロジェクト全体でそうしたつながりを維持できる。証明を認定することはできないが、証拠とレビュー履歴をアクセス可能な状態に保てる。

最も強力な結果は、両方のアプローチを組み合わせることだろう。AIがスピードと網羅性を担い、維持されたコミュニティライブラリが理解可能性、再利用性、ガバナンスを担う。

Anthropic Claudeは、前者が驚くべき規模で機能し得ることを示した。より難しい問いは、その出力のどれだけが永続的な数学インフラになり得るかだ。

Leanは証明を検証したが、信頼にはなお複数の層がある

カーネルチェックの成功は論理的妥当性に関する非常に強い証拠をもたらすが、プロセス、品質、解釈に関するすべての問いに答えるものではない。

Anthropicのリポジトリには、よくある近道を防ぐための複数の対策が含まれている。最終ビルドでは、未完了の義務を一時的に受理された状態で残すLeanの仕組みであるsorryに依存する証明を拒否する。

このプロジェクトはまた、望む結果を作り出すために新たな公理が挿入されていないことも確認している。最終定理は、命題外延性、古典的選択、公理的商の健全性という3つの標準Lean公理に依存する。

比較器は、Anthropicの定理文がMathlibにおけるフェルマーの最終定理の定式化と一致することを検証する。この手順は、有名な名前を付けながら弱い命題を証明してしまうという基本的な仕様リスクに対処するものだ。

リポジトリによると、全60,475モジュールがLean 4.33.1の下でソースからビルドされた。すべての宣言はLeanカーネルを通過した。

Anthropicは、Rustで書かれた独立したLeanカーネルであるnanodaによるエクスポートもテストした。第2のチェッカーは、1,052,234件の宣言をエラーなく受理した。

これらの検証により、数学的結論は通常の企業発表よりはるかに強固なものとなる。公開成果物は、独立した研究者がダウンロード、再ビルド、検査できる。

ただし、証明支援系が保証するのは、形式的な命題がその論理環境内で導かれることだけだ。信頼には、カーネル実装、コンパイラ環境、ハードウェア、ビルドプロセス、そして記号と意図された数学の対応関係も含まれる。

2つのカーネルを用いることで、このリスクの一部は低減される。しかし、Anthropicがnanodaに性能関連のパッチを4件適用しているため、実装上のあらゆる問題が解消されるわけではない。

リポジトリは、これらのパッチが型付け規則を変更しないとしている。コードとパッチは公開されているため、独立した専門家はこの主張を検査できる。

より重要な制約は意味に関わる。Leanは、「Mazur」という名前の定理が数学者の想定する版に対応しているかどうかを気にしない。正確にエンコードされた命題と、その命題が最終結果をどのように支えるかを検査する。

フェルマーの最終定理では、最終表現は異例なほど単純だ。3以上の指数について、正の自然数がよく知られた方程式を満たすことはできないと述べている。

この単純さは、出発点における解釈上の隔たりを狭める。中間経路は依然として、人間にははるかに理解しにくい。

証明を検証することと、Anthropicの自律性に関する説明を検証することにも違いがある。ビルドの成功は、Claudeがどの手順を選んだか、人間がどの程度介入したか、公開実行までにどれほど多くの失敗した試行があったかを立証しない。

Anthropicによると、Pengが与えたのは時折の高水準な指示のみだった。例としては、ヤコビ多様体を優先することや、Mazurの定理に関する作業を推進することが挙げられる。

読者は、証明オブジェクトからこの運用履歴を導き出すことはできない。それはAnthropicの記録と報告に依存する。

内部モデルには別の制約もある。同社が一般公開されていない研究システムを使用したため、外部チームは正確な生成プロセスを再現できない。

検証結果は再現できる。しかし、同じ構成が他の大規模形式化プロジェクトをどれほど信頼性高く完遂できるかは、まだ判断できない。

この区別は見出しレベルの評価にも反映されるべきだ。証明成果物には強力な機械検証可能な裏付けがあると言うのは妥当である。一方で、Claudeが数日以内にあらゆる主要な数学的作業を日常的に形式化できると推論するには早すぎる。

単一の成功は、好都合な定理、豊富な既存文献、有用な先行Leanプロジェクト、効果的な足場、大量の計算によってもたらされ得る。

フェルマーの最終定理には、よく理解された到達点もある。このシステムが形式化していたのは既知の数学であり、提案された新結果が重要かどうかを判断していたわけではない。

新規研究には追加の不確実性が伴う。モデルは適切な問いを見つけ、新規性を確立し、有用な定義を選び、他の研究者が関心を持つべき理由を説明しなければならない。

Anthropic自身も、このプロジェクトをリーマン予想に関して報告した作業と区別している。フェルマーの成果は、主として新たな数学定理ではなく、検証における進歩である。

このより限定的な説明は、作業の価値を下げるものではない。Claude Lean 4の成果物がなぜ重要であり、証拠がどの結論を支えるのかを正確に示している。

Anthropic ClaudeはAI数学競争を検証へと向ける

この成果は、AI研究所に対し、数学的主張と独立系システムが検査できる成果物を組み合わせるよう圧力をかける。

OpenAI、Google DeepMind、Anthropicはいずれも、推論能力の向上を示すために数学を用いてきた。競技問題は、採点者がすでに答えを知っているため、便利なスコアを提供する。

研究数学は、より難しい評価問題を提示する。流暢な証明には、隠れた穴があったり、定理を誤用したり、前提をひそかに変更したりする可能性がある。

モデルが数千件の候補論証を生成できる場合、人間のレビューは容易にスケールしない。アイデアの生成は安価になる一方、専門家の注意力は依然として限られる。

形式化はこの均衡を変える。Leanカーネルは、疲労したり自信に満ちた言葉に説得されたりすることなく、無効な形式的ステップを拒否できる。

独創性や関連性を判断することはできないが、専門家がより深い評価に時間を使う前に、大きな種類の論理エラーを除去できる。

Anthropicは、将来の数学論文には人間が読める解説とともに形式的証明が日常的に含まれるようになるかもしれないと主張する。同社のフェルマー公開は、この予測の信憑性を高める。

この考えには歴史的な裏付けがある。Thomas Halesによるケプラー予想の証明は長年のレビューを招き、その後彼は最終的に結果を形式化したFlyspeckプロジェクトを率いた。

そのプロセスには大規模な人間の努力が必要だった。AIがエンコードの負担を軽減できれば、形式検証はより幅広い研究で実用的になる。

したがって競争圧力は明白だ。数学上の進歩を発表する研究所は、Lean、Rocq、Isabelle、または同等の成果物を公開するよう、より強く求められるだろう。

同じシステムが機械検証可能な版も生成できる場合、自然言語の論文だけでは十分な証拠にならなくなるかもしれない。形式的成果物を伴わない主張は、より強い懐疑を受ける可能性がある。

ただし、すべての分野がこの変化に備えられているわけではない。形式ライブラリには依然として偏りがあり、現在の研究を明確に記述するために必要な定義が欠けている分野もある。

形式化が可能な場合でも、創造的な証明を保守可能なコードに変換するには大きな判断が必要になり得る。システムは、コンパクトで汎用的なツールに貢献する代わりに、巨大なローカルライブラリを生成するかもしれない。

計算負荷も重要だ。60億出力トークンと数十の協働エージェントは、商業的コストを論じなくとも大規模な実験を意味する。

Anthropicはより小規模な反例も提示している。Prove2Meを通じて連携した3つのコンシューマー向けサブスクリプションが、Vinogradovの三素数定理を3日で形式化したとしている。

この内部実験には、フェルマーのリポジトリほどの公開証拠はない。それでも、モデルと足場が改善すれば、このワークフローが小規模化する可能性を示唆している。

業界比較では、モデル名ではなく完全なシステムに注目すべきだ。検索、状態管理、コンパイル、定理探索、タスク割り当て、検証はいずれもこの成果に寄与した。

孤立したLean問題で優れた性能を示すモデルでも、数百万行規模のキャンペーンでは失敗する可能性がある。別のモデルは、ワンショットのスコアが低くても、より優れたオーケストレーションによって成功できる。

したがってAnthropic Claudeは、2つの点で基準を引き上げる。規模を実証し、他者が中心的な主張に異議を唱えられるだけの完成成果物を公開している。

競合他社は、より短い証明、より強力な自動化、よりクリーンなライブラリ統合、あるいは多数のプロジェクトにわたる前向き評価で応じることができる。

この競争が、劇的だが裏付けのない主張ではなく検証可能性を報いるなら、数学は恩恵を受ける。技術的にはコンパイルできても、依然としてナビゲート不可能な巨大な成果物で研究所が専門家を圧倒するなら、数学は損なわれるだろう。

次の標準には、機械による受理と人間による使いやすさの両方が含まれるべきだ。形式的真理は不可欠だが、研究は説明、抽象化、共有された理解にも依存している。

これが数学を変えるかどうかを示す3つの試験

フェルマーの形式化が永続的な転換となるのは、外部者が再現し、専門家が再利用し、その手法が1つの有名な目標を超えて成功する場合に限られる。

最初のシグナルは独立した再構築である。研究者は公開リポジトリをクローンし、すべてのモジュールをソースから再ビルドし、比較器を再実行し、第2カーネルによる検証を調査すべきだ。

再現が成功すれば、成果物が文書化された通りに機能するという確信は強まる。隠れた依存関係、非現実的なリソース要件、不整合なビルドに関する報告があれば、その結論は弱まる。

独立したレビュアーは、最終定理が禁止された抜け道なしに期待された命題へ到達しているかも検査すべきだ。リポジトリはすでに検査手段を提供しているが、第三者による実行のほうがより強い試験となる。

二つ目の指標は再利用性だ。Mathlibのメンテナーと形式数学の研究者は、どの定義や中間結果を保守対象のライブラリへ取り込めるかを見極めるべきである。

大きな構成要素が受け入れられたインフラとなれば、Anthropicの1,300万行は、単一の最終定理を超える価値を生み出したことになる。ほとんどがレビューを通過しなければ、この成果物は高価な証明書に近いものに見えるだろう。

この検証は、Imperial College Londonで進行中のプロジェクトとの関係も明らかにする。コミュニティ主導の取り組みは、自らの抽象化をAnthropicのアプローチと比較し、生成された成果がロードマップを加速させるかどうかを判断できる。

より短く再構成された証明が現れても、Claudeの成果が無効になるわけではない。それは、機械による生成と人間によるキュレーションが補完的な役割を果たすことを示すだろう。

三つ目の指標は、新規プロジェクトに対する将来的な性能である。Anthropicはシステムを実行する前に形式化の目標を定め、成功例と同様に失敗例も報告すべきだ。

有用な指標には、完了率、トークン使用量、人間の介入、ビルド成功率、再利用されたライブラリコード、専門家レビューに要する時間が含まれる。こうした分母がなければ、一つの称賛された成果だけで信頼性を立証することはできない。

今後の対象は、数学的構造において多様であるべきだ。ある数論の証明で成功するシステムでも、位相幾何学、確率論、圏論、解析学では苦戦する可能性がある。

研究者は、既知の証明の形式化と新規定理の発見も比較すべきである。後者では、出発点に信頼できる非形式的な議論が存在しないため、異なる安全策が必要になる。

こうした検証は、数学者だけに関係するものではない。長期間稼働するエージェントを構築する開発者も、状態の喪失、作業の重複、隠れた前提、高コストな検証という同じ課題に直面している。

Anthropicにとって最も強力なアイデアは、定理そのものではなくアーキテクチャかもしれない。外部化されたタスクグラフ、小さく検証可能な単位、独立したチェックによって、大規模なエージェントプロジェクトは監査しやすくなる。

ナレッジワーカーも、より小さな規模で同じ原則を適用すべきだ。洗練された最終回答をただ信頼するのではなく、情報源、中間的な主張、却下した代替案、レビュー上の判断を保存する。

Claudeによるフェルマーの証明は、AIが数学で最も有名な成果の一つを再発見したことを意味しない。AI中心のシステムが、膨大な既存の論証を、二つの論理カーネルが受理できる形式へ変換したことを意味する。

これは「Claudeがフェルマーの最終定理を解いた」という表現より限定的な成果だが、より有用である可能性がある。急速に生成されるAI研究が生む検証負担に対処する道筋を示している。

次の問いは実務的だ。独立したチームはこの成果物を再利用可能な数学へと変えるのか、それとも並外れた一度きりの実演にとどまるのか。再構築、Mathlibへの貢献、そして次に事前計画・記録された取り組みに注目すべきである。それらの指標が、anthropic claudeが形式数学を変えたのか、それとも最も目立つストレステストを完了しただけなのかを明らかにする。