AIはフェルマーの最終定理を「解いた」のか？ 11日で完成した1300万行の証明が変える数学

AIはフェルマーの最終定理を「解いた」のか？ 11日で完成した1300万行の証明が変える数学

11日で「証明済み」になった、350年の難問

数学史上もっとも有名な難問の一つが、再び世界の注目を集めている。

Anthropicは2026年9月、同社のAI「Claude」がフェルマーの最終定理について、最初から最後までコンピューターで検証できる完全な形式証明を作成したと発表した。作業にかかったのは11日。生成されたLeanコードは約1300万行に達し、作業の途中では3万300件の定理が証明され、そのうち2万9500件が最終的な証明に使われた。

この数字だけを見ると、AIが人類を何世紀も悩ませた難問を、わずか11日で解いたように思える。しかし、ここには重要な区別がある。Claudeが行ったのは、未知の解法を発見することではない。アンドリュー・ワイルズとリチャード・テイラーによって1990年代に完成され、数学界で正しいと認められてきた証明を、コンピューターが一つずつ論理確認できる言語へ翻訳し、不足する膨大な中間部分を埋めたのである。

「新しい証明の発見」ではなく「既存証明の完全な機械検証」。この違いを押さえなければ成果を過大評価することになる。一方で、形式化を単なる翻訳作業と考えると、その難しさと今回の衝撃を過小評価してしまう。


フェルマーが余白に残した一行

フェルマーの最終定理は、正の整数a、b、cと、2より大きい整数nについて、「aのn乗＋bのn乗＝cのn乗」を満たす組は存在しない、という主張だ。

ピエール・ド・フェルマーは1637年ごろ、古代ギリシャの数学書『算術』の余白にこの主張を書き込み、驚くべき証明を見つけたが、この余白はそれを書くには狭すぎる、という趣旨の言葉を残した。しかし、その証明は発見されなかった。

以後、数世代にわたる数学者が挑戦し、個別の指数については次々と証明が進んだものの、一般の場合は350年以上も未解決のままだった。転機は1993年。ワイルズが長年の秘密研究を経て証明を発表したが、検証中に重大な欠陥が見つかった。ワイルズはテイラーとともに修正に取り組み、1994年に問題を克服。論文は1995年に発表された。

この物語は、数学における「証明済み」が、誰かが答えを書いた瞬間に成立するものではないことを示している。証明は他の専門家に読まれ、前提や引用された定理を含めて検討され、論理の鎖が切れていないことを確かめられなければならない。ワイルズほどの数学者の証明でさえ、最初の発表後に穴が見つかった事実は、その難しさを象徴している。


「人間には明らか」が、コンピューターには通じない

通常の数学論文は、人間の専門家が読むことを前提に書かれている。著者は常識的な変形を省略し、既知の結果を参照し、文脈から理解できる部分を明記しない。読み手も背景知識を使って、行間を補いながら論理を追う。

ところが、コンピューターは「ここは明らかだろう」と推測してくれない。定義、前提、型、使用する定理、そこから導かれる結論を厳密に指定し、各段階がルールに従っていることを示す必要がある。この作業に使われたのが、定理証明支援系のLeanだ。

Leanでは、証明はプログラムに近い形式で記述される。入力された証明が論理規則に従っているかを小さなカーネルが確認し、途中に飛躍があれば受理しない。その意味で形式証明は、数学的主張に対する非常に厳格な自動テストに近い。

難しいのは、ワイルズの論文だけを機械語に置き換えれば終わるわけではない点だ。人間向けの証明は、代数、幾何、調和解析、数論などの巨大な知識体系の上に立っている。必要な概念や補助定理がLeanの共有ライブラリに存在しなければ、それらも新たに定義し、証明しなければならない。今回の1300万行という規模は、この「見えない土台」を一つずつ築いた結果でもある。


複数のAIが、巨大な証明を分業した

Anthropicの実験では、数十のClaudeエージェントが並行して作業した。あるエージェントが概念を定義し、別のエージェントが補助定理を証明し、さらに別のエージェントがそれらを組み合わせ、より上位の定理へ進む。人間が共同研究を行うような分業を、AI群が大規模に実行した格好だ。

ただし、最初から順調だったわけではない。初期の試行では、エージェントがプロジェクト全体の進捗を見失い、互いの成果をうまく利用できなくなった。長期作業では、個々のAIの推論力だけでなく、どの課題が終わり、次に何を証明すべきかを管理する仕組みが決定的に重要だった。

そこで使われたのが、定理同士の依存関係を有向非巡回グラフとして管理する共同形式化基盤Prove2Meである。証明すべき項目を地図のように配置し、各エージェントが未解決の作業を選び、完成した結果をほかのエージェントが再利用できるようにした。Leanのコンパイル負荷を抑え、自然言語による説明を検索に利用できる設計も、大規模な分業を支えた。

最終的にAI群は約60億の出力トークンを消費し、11日弱で証明の根に到達した。Anthropicによれば、Leanによる検査に加え、定理の最終的な記述が既存ライブラリMathlibのフェルマーの最終定理と一致することも比較ツールで確認した。つまり、似た名前の別問題を証明して終わったのではなく、狙った主張に到達していることを確認したわけだ。


人間の5年計画と、AIの11日は単純比較できない

今回しばしば対比されるのが、インペリアル・カレッジ・ロンドンの数学者ケビン・バザードが率いる人間中心の形式化プロジェクトだ。このプロジェクトは2024年に始まり、複数年をかけてフェルマーの最終定理をLeanで形式化することを目指している。

「人間が5年かける仕事をAIが11日で終えた」という説明は強烈だが、両者の目的は完全には同じでない。Anthropicの成果は、定理を端から端まで機械検証可能にすることを最優先した。一方、バザードらは共有ライブラリに組み込める基礎理論を整備し、人間が現代的な証明を探索しながら学べる動的文書を作ることも目標にしている。

短期間で「通る」巨大コードを作ることと、数学者が理解し、再利用し、次の研究へ接続できる形に整理することは別の課題だ。Anthropic自身も、人間のプロジェクトや既存のMathlibが築いた土台を利用したと説明している。今回の競争を、AI対数学者の単純な速度勝負として描くのは正確ではない。

それでも、端から端までの形式化が年単位ではなく日単位で可能になった事実は重い。バザードは自身のブログで、この成果から数学的に新しいことはほぼ何も分からないとしつつ、数千ページ相当の文献をAI群が11日で形式化できたことは、自動形式化の可能性を示すと評価した。従来99.9％正しいと考えていた証明について、形式化後は100％確信すると述べたことも、この成果の象徴として受け止められている。


SNSは「驚嘆」と「それは新発見ではない」に二分

発表後、X、Reddit、Hacker Newsなどでは大きな反響が起きた。Lean公式アカウントは、最初の完全なコンピューター検証済み証明として成果を紹介。Hacker Newsでは関連投稿に数百件のコメントが集まり、Redditでも「数年前には考えられなかった」「1300万行という規模に圧倒される」「2万9000件以上の中間定理まで必要なのか」と驚く声が相次いだ。

 

一方、もっとも繰り返されたのは、見出しの受け取り方への警告だった。「AIがフェルマーの最終定理を解いた」という表現に対し、「解いたのはワイルズとテイラーで、Claudeは既存証明をLeanに形式化した」「新しい数学的発見ではない」という訂正が多数投稿された。反応の中には、形式化を単なる書式変換のように軽く見る意見もあったが、それに対しては、長大な証明の欠けた土台を補い、数万件の中間定理を機械検証可能にすること自体が大きな研究上の成果だ、との反論も見られた。

さらに議論は、研究者の役割や資金配分にも及んだ。巨額の助成と数年の計画で進めてきた仕事にAIが短期間で到達したことを、研究生産性の飛躍と歓迎する声がある。その一方で、若手研究者のテーマがAIに先取りされる可能性や、数学を手で考える動機が失われるのではないかという不安も表明された。バザードのブログのコメント欄でも、「数学の悲しい終わり」と見る意見と、「数学的内容は変わっておらず、検証手段が進歩したのだ」とする応答が交わされている。

これらは無作為抽出された世論調査ではなく、各SNS上で確認できた投稿の傾向にすぎない。それでも、今回の成果がなぜ誤解されやすく、同時に強い感情を呼ぶのかをよく示している。人々が反応しているのは一つの定理だけではなく、「知的労働のどこまでが自動化されるのか」という、より大きな問いだからだ。


正しい証明と、役に立つ証明は同じではない

今回の成果には明確な弱点もある。1300万行という規模は、主要な数学ライブラリMathlib全体の5倍を超える。機械が正しさを確認できても、人間が全体像を把握し、必要な部分を見つけ、別の証明に再利用するのは簡単ではない。

数学の発展には、正しい結論だけでなく、なぜそうなるのかを理解できる説明、概念を整理する適切な抽象化、別分野でも使える補題が必要だ。同じ基礎理論を毎回巨大な専用コードとして作り直せば、形式証明は増えても知識体系は育ちにくい。検証可能な証明が大量生産される一方で、それぞれが互換性の乏しい孤島になる可能性がある。

したがって次の課題は、AIが作ったコードを短く整理し、Mathlibへ還元し、人間が読める解説と対応づけることだろう。AIが荒々しく道を切り開き、人間とAIがその道を地図にする。今回の成果はゴールというより、この新しい分業の出発点と見るほうがよい。


査読の限界を補う「疲れない第二の読者」

最大の意義は、有名な定理をもう一度証明したことではなく、これまで費用と時間のために現実的でなかった機械検証を、大規模に実行できる可能性を示した点にある。

数学論文の検証には、専門家の長い時間が必要だ。とくに新しい理論が何百ページにも及び、多数の先行研究に依存する場合、査読者がすべてを再構成するのは難しい。AIが形式化を補助できれば、人間向け論文とともに、Leanなどで検査できる証明書を提出する習慣が広がるかもしれない。

これは、AIが数学的成果を大量に生み始めた時代にはさらに重要になる。人間が読む速度を上回ってAIが論文候補を生成すれば、従来型の査読だけでは追いつけない。生成するAIと、形式化するAIと、最終的に小さな検証カーネルが論理を確認する仕組みを組み合わせることで、少なくとも「論理的に結論が導かれているか」を効率よく確認できる。

もちろん、形式証明は論文の価値をすべて判定するものではない。定義が現実の問題を適切に表しているか、研究課題が重要か、証明が新しい洞察を与えるか、説明が教育的かといった判断は残る。また、検証ソフトウェアや基盤ライブラリへの信頼、巨大コードの監査、計算資源の偏在といった問題も避けられない。

それでも、疲れず、権威に遠慮せず、論理の抜けを見逃さない「第二の読者」を数学が手に入れる意味は大きい。


AIは数学者を置き換えるのか

今回の出来事は、AIが数学者の仕事を一括して代替したという話ではない。証明の原型を生んだ人間、何十年も理論を整備した研究者、MathlibとLeanを育てたコミュニティ、証明を分割する基盤を設計した開発者がいて、初めてClaudeの11日間が成立した。

しかし、「だからAIは単なる道具だ」と片づけるのも早い。複数のエージェントが失敗から立て直し、依存関係を追いながら数万の定理を積み上げ、巨大な目標を完遂したことは、従来の自動化とは質が違う。人間が細かく一手ずつ命令するのではなく、ゴールと作業環境を与えられたAI群が、長期プロジェクトのかなりの部分を遂行したからだ。

今後、数学者の価値は「証明コードを手で書く速さ」よりも、どの問題を選ぶか、どの概念で整理するか、結果が何を意味するかを説明する力へ、さらに重心を移す可能性がある。AIは検証を高速化できるが、数学を人間の知識として編集する仕事まで自動的に終わらせるわけではない。

フェルマーの最終定理そのものについて、新しい結論はない。ワイルズとテイラーの証明は正しかった。だが、その正しさを機械が端から端まで確かめられる形にする仕事が、11日で完了したという事実は、数学の作り方、読み方、信じ方を変える。

余白に収まらなかったフェルマーの証明は、約360年後、今度は1300万行にまで膨らんだ。そして次の挑戦は、その巨大な証明を、再び人間が理解できる知識へと圧縮することなのかもしれない。


出典URL

関連記事