AI最新情報読了 10 分

「証明の中にカーネルのバグがある方に100ポンド」――Claudeが11日で終えたフェルマー証明に数学者たちがざわついた理由

Shiritomo編集部 @shiritomoAI_jp 2026年9月5日更新

「証明の中にカーネルのバグがある方に100ポンド賭ける」。
Anthropicの発表に対して、ある研究者がこんな軽口をXに投稿しました。
話題になっていたのは、AI「Claude」が専門家なら数年はかかると見込んでいた作業を、わずか11日間で終えたというニュースです。
数学者アンドリュー・ワイルズ氏が1995年に証明した「フェルマーの最終定理」を、コンピューターが一行ずつ検証できる形に書き直す――この一報が、著名な数学者からAI業界の投資家まで巻き込む議論を呼びました。
SNSでAI関連の話題を追っている方にとっても、AIが「検証」という地味だが手間のかかる作業をどこまで肩代わりできるのかを考える材料になりそうです。

先に結論をまとめると：
– Claudeが11日間かけて「フェルマーの最終定理」をLean（コンピューターが検証できるプログラミング言語）向けに書き直し、全行程を機械的に検証できる証明を完成させました
– その過程で1300万行のコードと2万9500個の中間定理を積み上げ、Lean史上最大規模の証明になったとされています
– 専門家からは称賛の声が上がる一方、「本当に穴がないのか」という懐疑や皮肉の反応もXで見られました

何が起きたのか

発端はAnthropic公式アカウントの投稿でした。
「数学の大きな証明が正しいかを確認するには何年もかかることがある。
数式による論証をLeanのようなコンピューター証明支援ツールが検証できる形に変換する『形式化』は、それを助けてくれる」と切り出し、「先月、Claudeがフェルマーの最終定理の最初の形式化された証明を完成させた」と続けています。

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help.

Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of… pic.twitter.com/pdT8zwlV4A
— Anthropic (@AnthropicAI) 2026年9月4日

フェルマーの最終定理そのものは目新しい発見ではありません。
ワイルズ氏が1995年に証明を発表し、数学界ではすでに決着済みの問題です。
それなのになぜ今さら話題になっているのか。
ここに引っかかった人が多かったようで、Xでは「もう証明済みなのになぜ」という戸惑いから始まり、内容を知るにつれて称賛や懐疑に転じていく反応が連鎖していきました。
ただ、投稿の文面だけでは「形式化」が何を指すのか分かりにくく、なぜここまで大きな話題になったのかは実際に一次情報を確認しないと見えてきません。

調べて分かったこと

そもそも「形式化」とは何をしたのか？

ワイルズ氏の証明は129ページに及ぶ論文で、発表後も検証に数ヶ月を要したといわれています。
数学の論文には「自明」「同様に」といった論理の省略がしばしば含まれますが、これは人間の数学者同士なら通じても、コンピューターには通用しません。
今回Claudeが行ったのは、その省略を一切許さない形――Leanという証明支援系言語のコードとして、証明の全ステップを書き下す作業でした。
これを見た日本語圏のユーザーからも、次のような解説投稿がありました。

Anthropicがフェルマーの最終定理の証明したよって言ってて「もう証明済みなのになんでそんな無駄なことを」と思ったけど、最近は「証明」もLeanっていうプログラミング言語で行われることがあって、これは「自明」とか「同様に」とか論理の省略が許されなくて、要するに完全な証明が保証されるみたい… https://t.co/favbQFvWdw
— らけしで / Mizmic Studio (@lakeside529) 2026年9月5日

Anthropicによれば、Leanが標準で持つ3つの公理だけを使い、証明に含まれる推論のすべてがコンピューターによって検証済みだといいます。
つまり「新しい定理を発見した」のではなく、既存の証明に一切の穴がないことを、機械が保証できる形に翻訳した、というのが実態に近いようです。

どうやって11日間で終えたのか？

Anthropicの発表によると、この作業は数十体のClaudeエージェントが協調しながら進め、合計で約60億トークンを生成したとされています。
人間側の関与は「時折、優先すべき数学的な概念について高レベルの指示を与えた程度」にとどまり、ほぼ自律的に作業が進んだそうです。
最終的に採用されたコードのうち、約7%は初期の失敗した試行から得られたものだったとも説明されており、一度で成功したわけではなく、試行錯誤を重ねた末の結果だったことがうかがえます。

専門家はどう評価しているのか？

Anthropicはこの証明を、Imperial College Londonでフェルマーの最終定理の形式化プロジェクトを率いるケビン・バザード氏に共有し、評価を求めています。
バザード氏は「この驚くべき自動形式化の成果は、Anthropicの研究者いわく11日しかかからなかったとのことだが、数学の公理以外の一切の仮定なしにフェルマーの最終定理を証明している。
その過程で代数・調和解析・幾何学・数論の自動形式化を目にすることになり、AIによる自動形式化の成果物はもはや積み上げに耐えるだけ頑健であることを学んだ」と述べています。
この評価がXでも紹介され、反響を後押ししました。

Respect where respect is due: Anthropic says Claude completed the first fully computer-checked proof of Fermat’s Last Theorem in 11 days.

Andrew Wiles proved the theorem in 1995. Claude’s achievement was turning an existing proof into a form where a computer can check every… https://t.co/FcRbJn5GYb pic.twitter.com/OOdfoI2AZD
— Chubby♨️ (@kimmonismus) 2026年9月4日

数論の研究者であるアレックス・コントロヴィッチ氏も、自身のアカウントで「!!!!!!!」とだけ投稿し、驚きを表現しています。
専門家の間でも、それだけ異例の出来事として受け止められたことがうかがえます。

懐疑や皮肉の声もある

一方で、手放しの称賛ばかりではありませんでした。
冒頭で紹介した「証明の中にカーネルのバグがある方に100ポンド賭ける」という投稿は、Leanという検証ツール自体（あるいはその基盤となるカーネル）にバグが潜んでいる可能性を茶化した皮肉です。

£100 says there's a kernel bug used in this proof https://t.co/BRPetvL9jM
— Alex Kavvos (@lambdabetaeta) 2026年9月5日

どれだけ厳密な検証系であっても、検証系自身にバグがあれば「証明が正しいことが証明された」とは言い切れない、という指摘は、形式手法に詳しい人ほど頭をよぎるポイントのようです。
実際、Anthropicの発表文でも「一切の仮定なし」と説明されているのはLeanの公理部分に限られており、Lean自体の実装に不具合がないかどうかは、また別の話として残ります。

Lean（証明支援系言語）とは何か、なぜこれからも注目されるのか？

Leanはもともと数学者やソフトウェア工学の研究者が使う証明支援系言語で、「この論証は本当に正しいか」をコンピューターに検証させるためのツールです。
今回のニュースをきっかけに「Leanとは何か」への関心が高まっているようで、これは一過性の話題では終わらなそうです。
Xの投稿の中にも「これほど重い証明は多くなさそうなので、人類がこれまで出版した全ての数学論文のLean化も近いうちに達成できそうだ」という見立てがありました。
AIが証明支援を担う流れが続く限り、Lean自体への関心は今後もたびたび浮上してくると考えられます。

AI数学ツール市場への波紋

今回の件は、AIと数学を掛け合わせたスタートアップ企業にとっても他人事ではないようです。
ある投稿者は「Axiom MathやHarmonicのようなAI数学スタートアップが15億ドル規模で評価されているのに、Claudeでこれができてしまうなら、その評価額はどう正当化されるのか」という趣旨の疑問を投げかけていました。

Genuine question: How can companies like Axiom Math and Harmonic be valued at $1.5B when you can just do this with Claude? I always felt their valuation was incredibly high, but I don't see how they could ever compete with this. https://t.co/AoKu3D6LN3
— Jasper Dekoninck (@j_dekoninck) 2026年9月4日

AI数学系のスタートアップは専用モデルや専用ツールを強みにしていますが、汎用モデルであるClaudeが数学の形式化で成果を出したことで、投資家や業界関係者の間で「専用性の価値」を問い直す議論が生まれつつあるようです。

Shiritomo編集部の考察

今回の拡散を分析の視点で見ると、伸びた要因は証明の中身そのものよりも「第三者による裏付け」だったと考えられます。
実際の反応を見ると、最も多くの反応を集めたのはAnthropic自身の投稿（いいね9000件超、インプレッション176万件超）で、ケビン・バザード氏の評価を紹介した引用ツイートなどはそれに続く反応でした。
それでも、独立した専門家による裏付けが紹介されたことで、自社発表だけでは伝わりにくい技術的な価値の信頼性が補強され、議論が広がりやすくなったという構造は今回も見て取れます。
SNS運用の観点では、技術的な発表を行う際に「誰が保証してくれるか」を用意できているかどうかが、拡散するかどうかの分かれ目になりやすいといえるでしょう。
また、懐疑的な皮肉のツイートも一定の反応を集めており、称賛一色にならない「ツッコミどころ」があることも、議論を長引かせる要因になっていました。

まとめ

Claudeが11日間で成し遂げたのは、新しい数学的発見ではなく、既に決着していた証明を「機械が検証できる形」に書き直す作業でした。
それでも専門家の評価と皮肉交じりの懐疑の両方を巻き込んで話題になったのは、AIが人間の知的作業をどこまで代替できるのかという、より大きな問いに触れていたからかもしれません。