Claudeがフェルマーの最終定理を形式化。11日間で何を成し遂げたのか

Claudeがフェルマーの最終定理の証明を、コンピューターで検証できる形に書き上げました。Anthropicの発表によると、かかった時間は約11日間。数十のAIエージェントが協力して完成させた研究成果です。Anthropicの発表

もとになったのは、Wilesらによる既知の証明です。数学者が読めば省略を補える議論も、機械に確かめさせるには、定義や前提を一つずつ書き起こさなければなりません。その膨大な作業をClaudeが担いました。

公開されたコードを実際に検査した数学者からも、成果を認める報告が出ています。証明の中身と検証の手順をたどると、今回の研究が評価される理由も、まだ残っている課題も見えてきます。

9月4日付の発表を、9月6日分の未掲載重要ニュースとして取り上げます。調査の基本期間は日本時間9月5日8時〜9月6日8時、資料の確認日は9月6日です。発表の正確な時刻は確認できていません。

人が読める証明を、機械も確かめられるようにする

フェルマーの最終定理は、3以上の整数nについて、正の整数a・b・cが「aⁿ＋bⁿ＝cⁿ」を満たすことはない、という主張です。今回のコードにはこの命題が記され、数学のライブラリMathlibにある定理の表現にも結びつけられています。定理の宣言と最終チェック

証明を書くために使われたのが、Leanです。Leanでは、定義や前提から結論を導く過程を厳密な規則に沿って記述します。出来上がった証明を検査するのは、「カーネル」と呼ばれる中核部分。証明を探す処理が複雑でも、最後にはその結果を検査できる形にする仕組みです。Leanの公式解説

人向けの説明なら「先ほどの結果から明らかです」で済む場面でも、機械にはそのまま通じません。どの結果を使ったのか、その結果を使うための条件は満たされているのか。こうした細部までつながって、初めて全体の証明になります。大きな定理では、最後の結論に至るまでに必要な定義や補助的な定理も膨大です。

今回Claudeが成し遂げたのは、既知の証明をこの粒度で記述する「形式化」でした。未知の難問に新しい解法を見つけた成果とは異なりますが、既に分かっている数学を、どこまで細かく確かめられるかという課題を大きく進めています。

11日間を支えたのは、ClaudeとProve2Me

初めから順調だったわけではありません。Anthropicによると、初期の試みではエージェントが進捗を見失ってうまく協力できなくなり、共同作業基盤のProve2Meを導入してから完成に至りました。使用したのはClaude Fable 5.1におおむね相当する内部研究モデルで、出力トークンは約60億に上ります。研究の実行条件

Prove2Meには、証明すべき命題と、その証明を別々に管理する仕組みがあります。同じ命題に複数の証明を提出でき、他のエージェントもその成果を再利用できます。難しい証明を小さな課題へ分け、どの課題がどれに依存しているかを扱えるようにした設計です。Prove2Me論文・第3〜4節

誰かが途中まで書いた長いファイルを、別の担当が読み解いて続きを書く。その方法では、人数を増やすほど調整も増えます。命題ごとに成果を受け渡せれば、何を使えるか、何がまだ解けていないかを共有しやすくなる。モデルの推論能力だけでなく、こうした作業の組み立て方も成功を支えていました。

なお、公開版のFable 5.1に同じ作業を頼んだ試験ではありません。GPTなどの競合や旧モデルと条件をそろえた比較もないため、この結果からモデル間の優劣や改善率までは判断できません。

正しい証明でも、違う命題を証明していたら意味がない

機械の検証を通っていても、最初に書いた命題が本来の問題より簡単なものに置き換わっていれば、その証明が正しいことと、目的の定理を証明したことは一致しません。何を証明したのかも確かめる必要があります。

この取り違えを確認するのが、Leanの開発側が公開するComparatorです。用意した課題と提出された証明を照合し、同じ命題を証明しているか、認められた公理だけを使っているか、カーネルが受理するかを確かめます。公理とは、証明の出発点として認める前提のこと。照合の基準になる課題や実行環境、検証器を信頼できることも必要です。Comparatorの仕様

Anthropicの公開資料には、次の検査を通したと記されています。

出典：証明リポジトリの検証記録。nanodaは別の実装ですが、この実行結果を報告しているのもAnthropicです。第三者機関の監査として紹介された記録ではありません。

成果物と検査手順が公開されているので、第三者も報告を確かめられます。今回、実際にそれを行った数学者がいます。

自分でも確かめた数学者は、どう評価したか

Imperial College LondonのKevin Buzzard氏は、自身もフェルマーの最終定理の形式化に取り組んできた数学者です。公式発表への推薦文に加え、自分のブログでも評価を公表しました。コードをコンパイルし、Comparatorも実行して確認できたという報告です。検証にはAnthropicから計算機へのアクセス提供を受けたことも記しています。Buzzard氏による検証と評価

同氏は、自動形式化がこれほど大きな数学を扱えるようになったことを高く評価しています。一方、数学的には既存の議論をたどっており、新しい内容を加えたものではないとも述べています。

同氏は、Mathlibへ再利用可能な成果を取り込むことや、人が現代的な証明を探索しながら理解できる資料を作ることを、自分のプロジェクトで続ける仕事として挙げています。証明が検査を通っても、それだけでは終わりません。

機械が確かめられる証明を作るところまでは到達した。次は、人が理解し、使いやすい形に整える。 専門家の評価からは、成果の大きさと、その先にある仕事の両方が伝わってきます。

検証だけでも、相応の計算資源がいる

証明の検証にも、相応の時間とメモリが必要です。リポジトリにある実行記録では、ビルドに96並列で5時間32分、Comparatorに約15時間かかっています。後者のピークメモリは230GB。実行する際は300GBを確保するよう案内されています。いずれも公開元の環境での値で、Link AIの実測ではありません。必要な資源と検証手順

また、このコードは既存のオープンソースの成果を利用しています。研究成果物として公開されていますが、継続保守や外部からの変更の受け入れは行わない方針です。

「11日間」という数字から分かるのは、作業が終わるまでの経過時間です。並列に使った計算量、試行錯誤の費用、土台となった数学やライブラリを整えた労力は、それぞれ別にかかっています。内部研究モデルの総費用も、今回確認した資料では分かりません。

そのため、人間の何年分の仕事を何分の一の費用で置き換えた、という換算はできません。公開APIの単価を掛けても、この研究の実費にはならない。短期間で完遂した成果は評価しつつ、費用については追加の情報を待つのが妥当でしょう。

「できた」という報告の先までたどれる

今回の発表は、巨大な証明を作ったという報告だけで終わっていません。コードがあり、検査の手順があり、自分でも確かめた数学者の報告があります。何を根拠に成果を認めればよいのか、読者もそこまでたどれます。

数学と同じ確かめ方を、あらゆる業務に使えるわけではありません。市場調査には入力情報そのものの真偽が、経営判断には問いの立て方や将来の不確実性が関わるため、数学で証明を検査できたことから、こうした判断の正しさまで保証できるとは言えません。

AIの成果を知ったとき、何を作り、どの条件で合格とし、誰が確かめたのかをたどってみる。今回のClaudeの研究は、そこまで読める材料がそろった事例です。検証の裏づけがある成果を評価し、まだ分からない費用や使い勝手は保留する。そんな読み方が、次の発表を見るときにも役立ちます。

Link AIでは、AIの能力と制約を踏まえた導入判断・アセスメントを支援しています。自社でAIに任せる範囲や、成果をどう確かめるかを整理したい方は、お問い合わせください。