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

科学 フェルマーの最終定理の形式化 2026年9月4日 私たちは、フェルマーの最終定理に対する初の完全なコンピュータチェック済み証明を共有します。Claudeは、Leanプログラミング言語で証明を記述するために、11日間にわたりほぼ自律的に作業しました。以下に、形式化がどのように行われたかを説明し、この作業が研究数学にとって何を意味する可能性があるかについての考察を共有します。 1637年頃、ピエール・ド・フェルマーはディオファントスの『算術』の余白に、史上最も有名な数学的予想の一つとなる主張を書き込みました。それは、n > 2 の任意の整数 n に対して、正の整数 a, b, c は aⁿ + bⁿ = cⁿ を満たさないというものです。フェルマーの最終定理（FLT）として知られるようになったこの予想は、証明が信じられないほど困難であることが判明しました。1995年のアンドリュー・ワイルズ卿による最初の証明は129ページに及び、検証には数ヶ月の painstaking な作業が必要でした。 10年後、オランダのコンピュータ科学者ヤン・ベルストラは、ワイルズの証明を「形式化」することを提案しました。これは、数学的推論をコンピュータが自動的にチェックできる形式に変換することです。それ以来、数学者たちは、このような複雑な証明をエンコードするために必要な方法論を開発してきました。これには、2024年にロンドン・インペリアル・カレッジのケビン・バザードが開始した、Lean証明支援システムを使用して形式化を完了するための数年がかりのコミュニティの取り組みが含まれます。 最近、コロンビア大学のAI形式化ツール開発グループに所属するAnthropicの研究者、ティアンイー・ペンは、ClaudeがFLTの形式化で進歩できるかどうかをテストすることにしました。1 その結果は彼の予想を上回るものでした。11日間、ほぼ自律的に作業したClaudeは、FLTの初のend-to-endのコンピュータチェック済み証明を生成しました。その過程で、1300万行のLeanコードを書き、29,500の中間定理を証明しました。 私たちは、この結果の証明をケビン・バザードと共有しました。彼は次のように述べています。 Anthropicの研究者によると、わずか11日で達成されたこの並外れた自動形式化の成果は、数学の公理以外のいかなる仮定もなしにフェルマーの最終定理を証明するものです。その過程で、代数、調和解析、幾何学、数論の自動形式化を目にし、AIの自動形式化アーティファクトが構築可能なほど堅牢になったことがわかります。この証明は多層的です。 FLTほど複雑な証明を自動的に形式化することは、数学のすべての成果が容易にチェックできるようになる未来に向けた重要な一歩です。AIがますます多くの証明を生み出すにつれて、新しい結果を評価する負担（数年かかるプロセス）を軽減するために、作業を容易に形式化する能力は役立つでしょう。私たちは、数学の基盤となる知識体系を信頼することが、より困難になるのではなく、容易になることを願っています。 数学的証明の検証という課題 リーマン予想に関する最近のAI主導の研究が新しい数学を生み出したのとは異なり、ここでの新しい点は検証です。これは、計算機で数学的計算をチェックするのと同じように、数学的証明をチェックすることです。数学の定理を証明するには複雑な論理連鎖を組み立てる必要があり、単一のリンクが壊れると、それに続くすべてが偽である可能性があります。新しい結果をその正しさに確信を持てるほど深く理解するには、数ヶ月、あるいは数年かかることがあります。 フェルマーの最終定理は、それを例示する良い例です。2 フェルマーは、この定理の記述を本の余白に、「この余白には収まりきらないほど素晴らしい証明を発見した」という魅力的な注釈とともに書き込みました。 350年以上にわたり、何世代もの数学者が、素晴らしいかどうかは別として、FLTの証明を探し求めました。1908年には、正しい証明を提示した人に10万ドイツ金マルク（現在の1〜2百万ドルに相当）の賞金が発表され、最初の1年間だけで621件の誤った試みが提出されました。 1993年6月、ワイルズは3日間にわたる一連の講義で、FLTの最初の正しい証明だと信じているものを発表しました。数人の数学者による集中的な検証作業が2ヶ月に入った頃、ある査読者がワイルズに質問し、重大な欠陥が露呈しました。ワイルズは、当初は一人で、後に元教え子のリチャード・テイラーと協力して、その欠陥を修正するために1年を費やしました。彼はプロジェクトを断念寸前でしたが、以前に却下したアプローチが証明を修正できることに最終的に気づきました。ワイルズは1995年5月にFLTの最初の正しい証明を発表しました。それは、1637年のフェルマーが知っていたであろう知識をはるかに超える、現代の数学的手法に依存していました。数世紀にわたる試みの後で初等的な証明が見つかっていないため、数学界は現在、フェルマー自身の元の「素晴らしい証明」は誤っていたと考えています。 フェルマーの最終定理の形式化 証明の正しさをチェックする一つの方法は、コンピュータにそれを実行させることです。Leanのような証明支援システムは、アルゴリズム的に証明の論理を検証し、疑いの余地なくその正しさを証明します。人間にとって難しいのは、Leanが理解できるように証明を書き直すことです。人間向けの証明では多くの自明なステップが省略されますが、Leanはどんなに些細なステップでもすべてを見る必要があります。人間の証明は、何世紀にもわたる出版された研究成果を基盤としていますが、形式化は、すでに形式化されている数学のほんの一部から始まります。 FLTの場合、形式化プロセスには数年かかると予想されていました。プロジェクトの初期段階を説明するために数学界が使用している青写真だけでも、86ページに及びます。 Claudeは11日間で証明を完了し、その過程で30,300の定理のコンピュータ検証可能な証明を生成しました（最終証明では29,500を使用）。数十のClaudeエージェントが協力して概念を定義し、中間定理を証明し、それらの定理を使用してさらに難しい命題を証明しました。1300万行のLeanコードというClaudeの証明は、この定理が構築されている主要なコミュニティライブラリであるMathlibのサイズの5倍以上です。3 FLT形式化の時間経過 Claudeの証明は、Darmon、Diamond、Taylorによるワイルズの証明の簡略化されたバージョンに従っています。人間からの数学的入力は、ティアンイーからの時折の高レベルな指示に限られていました。「Jacobian as a scheme sounds high priority」、「push [the] Mazur [theorem] to be done soon。」Claudeの思考の抜粋はここで見つけることができます。「THE FLT root reads Proved on the site. Historic moment (modulo re-check).」「!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me.」「🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.」Claudeが成し遂げたことを認識した際の思考の抜粋。 Claudeの初期の試みのいくつかは失敗しました。エージェントは初期の成功を収めましたが、プロジェクトの状態を見失い、効果的な協力を停止しました。それらの失敗した努力は、最終証明における非定型行の約7％を占めました。 Prove2Me、すなわちティアンイー・ペンとコロンビア大学の協力者たちが設計した数学形式化のためのオープンな共同プラットフォームを使用するように切り替えたときに、この取り組みは成功しました。Prove2Meは以下の点で役立ちました。 エージェントが次にどの証明を試みるべきかを決定するために使用する定理命題の有向非巡回グラフ（DAG）を維持しました。これは、メモリ劣化を軽減し、複数のエージェントが並列で作業できるようにするのに特に役立ちました。 定理命題と証明を別々のファイルに分離し、それらの間のリンクを独立して維持することにより、Leanのコンパイルを高速化し、リソース消費を最小限に抑えました。 各定理命題の自然言語による説明を維持することにより、検索と再利用を可能にし、より単純な証明パスをもたらしました。 Prove2Me計画の主要なマイルストーン。Claudeはフェルマーの最終定理を形式化するためにこれらを使用しました。3つの色付きのセクションは、最終目標に向けてClaudeが証明する必要があった3つの主要なサブ定理に対応しています。このグラフはワイルズの元の証明に密接に従っています。 Prove2MeとClaude Codeベースのマルチエージェントハーネスを使用することで、エージェントチームは2週間弱で証明を完了し、Claudeに匹敵する汎用的な内部研究モデルから約60億の出力トークンを消費しました。