Claudeがフェルマーの最終定理を11日で機械検査できる証明にした

Claudeがフェルマーの最終定理を11日で形式化した。形式化という言葉が何を指すのかをつかむと、この11日で何が起きたのかが見えてくる。

Anthropicが2026年9月4日に報告したのは、既存の数学的な証明の流れを使い、コンピューターが検査できる証明を作る仕事だ。数学でも大規模な部類に入る証明を、機械が1段ずつ検査できる形へ書き直したのが今回の成果だ。数学の専門知識がなくても追えるよう、形式化という言葉の意味から見ていく。Anthropicの発表

形式化は証明を機械が検査できる形にする

フェルマーの最終定理は、指数nが3以上の整数のとき、正整数a、b、cで aⁿ + bⁿ = cⁿ を満たす組はない、という主張だ。正整数とは1、2、3……のような0より大きい整数のこと。公開された成果物でも、この条件を定理として記述している。公開コードの「The statement」

指数が2なら 3² + 4² = 5² は成り立つ。9と16を足すと25になるからだ。この形の組は他にもあり、5² + 12² = 13² も成り立つ。25と144を足すと169になる。指数が2のうちは、探せば組が見つかる。

ところが指数を3以上にすると、どの正整数を選んでも式を満たせない、というのが定理の内容になる。指数を1つ増やしただけで、見つかっていたものが1つもなくなる。しかも、なくなるのは指数3のときだけではなく、4でも5でも、その先のすべての整数についてだ、と言っている。大きな数まで順に試して解が見つからなくても、その先にも候補は続くので、すべての正整数について言い切ったことにはならない。候補を一つずつ数え上げずに全体で成り立つ理由を示すのが、証明だ。

形式化とは、こうした数学の定義や推論を、コンピューターが論理を検査できる記述へ書き直すことをいう。今回使われたLeanは、その記述と検査のための言語・システムだ。人向けの証明では「明らかに」と省略される推論も、検査できる形で補う必要がある。Anthropicの「Formalizing Fermat’s Last Theorem」

単純な例で考えてみる。偶数aと偶数bの和も偶数だと示すには、aを2k、bを2mと書き、和が2(k+m)になると説明すればよい。人向けにはこれで通じる。形式化では、ここに含まれている前提まで書く。偶数とは2をかけた整数として表せる数だという定義、kとmが整数ならk+mも整数だという性質、そして最後に得た2(k+m)がふたたび偶数の定義を満たすという確認。どれも人が読むときは飛ばして構わない段階だが、検査する側は飛ばせない。

つまり形式化とは、証明の結論を書き写す作業ではなく、結論に至る道筋を、省略なしで組み直す作業だ。人向けの証明が大きく、省略も多いほど、書き下ろす量は増える。フェルマーの最終定理の証明は数学の中でも大規模なものにあたる。これは考え方を示す例で、今回の証明の中身を再現したものではない。

書く側と検査する側が分かれているところが、この成果の形になる。作業の分担はAnthropicの発表、検査の対象は公開成果物のREADMEによる。人が用意した証明の道筋と節目の指示は、一番上の箱に含まれる。

役割で見ると、Claudeは証明を書く側、Leanは書かれた推論を検査する側を担う。検査に通るというのは、認めた前提と使ってよい規則の範囲で、書かれた推論に飛躍がないという意味になる。AIが自分で正しいと言って終わりにせず、別の仕組みで確かめられるところに、この形の成果の意味がある。

人が道筋を示しClaudeが書き下ろす

Anthropicによると、今回の作業は既存の証明の流れを使い、人から時折大まかな指示を受けながら進んだ。内部の研究モデルによる複数のエージェントが作業を分担している。エージェントは、ツールを使いながら担当の仕事を進めるAIの実行単位と考えるとよい。発表の作業条件

11日という数字は、この分担のもとで出たものだ。証明の道筋は既存のものがあり、人が節目で方向を示す。その条件で、省略された推論を検査できる形へ書き下ろす作業を、複数のエージェントが分担した。

前の節で見たとおり、大規模な証明の形式化では、書き下ろすべき段階が膨大になる。人手では進みにくかったその作業量を、11日でこなしたところに今回の成果の大きさがある。

使われたのは内部の研究モデルで、人の指示と作業環境も込みの結果だ。普段のClaudeの会話画面で同じことを試す話とは分けて読むとよい。

元の問題と同じ命題かも確かめる

論理が正しくても、途中で問題を簡単なものへ入れ替えてしまえば、元の問題に答えたことにはならない。フェルマーの最終定理なら、指数を3だけに限定した証明があっても、4以上のすべてまで扱ったことにはならない。だから、検査に通ったかどうかとは別に、何を証明したのかを見る必要がある。

公開成果物のREADMEには、検査する定理と、証明が依存する公理を確認する FinalCheck.lean がある。公理は、証明の出発点として認める前提のことだ。何を前提として認めたかによって、証明できる範囲は変わる。だから、論理が通っているかを見るときは、どの公理を使ってよいことにしたのかまで一緒に見る。

さらにComparatorという照合ツールを使ったと報告している。このツールが確かめるのは3点で、指定した命題やその定義が一致するか、許された公理の範囲に収まっているか、Leanの検査に通るかだ。1点目が表の1行目に、残りの2点が2行目に対応する。ツール自体にも、実行環境を信頼するといった前提がある。成果物の検査範囲、Comparatorの検査仕様

表の3行目だけは、検査の合格では済まない。定理に付けた名前が内容と合っているかは、機械が判定する対象ではないからだ。READMEも、中間の定理名がその内容を正しく表しているかは読み手が判断する点として挙げている。

読んでみたい場合、専門外なら、まずREADMEの The statement と How it was verified を開くと、何を完成したと報告しているかがつかめる。前者が何を証明したのか、後者がどう確かめたのかにあたるので、この2つだけでも表の1行目と2行目は自分で確認できる。証明の道筋まで追いたい人向けには PROOF-PATH.md と閲覧用の html/ が公開されている。成果物は研究用で、保守しないとも記載されている。公開リポジトリ

問題文、証明、検査方法がそろって公開されているので、何を作り、どう確かめたのかを誰でも自分で追える。

まとめ

• 今回の成果は、フェルマーの最終定理という大規模な証明の省略を補い、コンピューターが検査できる形へ書き直したこと。
• 11日は、人が節目で方向を示し、内部の研究モデルによる複数のエージェントが書き下ろしを分担した期間。人手では進みにくかった作業量をこなした。
• 定理の記述、証明、検査方法が公開されており、READMEの The statement と How it was verified から、何を証明しどう確かめたかを自分で追える。