Claudeがフェルマーの最終定理で担った「形式化」とはどんな仕事か

Claudeがフェルマーの最終定理を11日で形式化した。そんなニュースを見ても、数学の難問を新しく解いたのか、すでにある証明を扱ったのかで、成果の意味はまるで変わる。

Anthropicが2026年9月4日に報告したのは、既存の数学的な証明の流れを使い、コンピューターが検査できる証明を作る仕事だ。新しい定理を発見したのではなく、大規模な証明を検査可能な形へ書き直したことが今回の中心にある。 数学の専門知識がなくても違いを追えるよう、形式化という言葉の意味から見ていく。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以上のすべてまで扱ったことにはならない。だから、検査に通ったかどうかとは別に、何を証明したのかを見る必要がある。

確かめたいこと	見るもの
元の問題と同じか	正整数や指数の条件を含む定理の記述と、その照合方法
認めた前提から論理が通るか	公理の一覧と、Leanによる検査の結果
人が道筋を理解できるか	各段階の説明と、実際に証明した命題

公開成果物の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/ が公開されている。成果物は研究用で、保守しないとも記載されている。公開リポジトリ

今回、こちらでLeanやComparatorを再実行していないため、検査に通ったという結果は発表元の報告として扱う。それでも、問題文、証明、検査方法が公開されている以上、11日という日数だけを手がかりにせず、何を作り、どう確かめたのかを自分で追える。

まとめ

• 今回の成果は、既存の証明の流れを使い、省略された推論を補って、コンピューターが検査できる形へ書き直したこと。新しい定理を見つけた話ではない。
• 11日は、人が節目で方向を示し、内部の研究モデルによる複数のエージェントが書き下ろしを分担した期間。普段のClaudeの会話画面で再現する結果ではない。
• 成果を見るときは、検査に通ったかに加えて、元の問題と同じ命題か、どの公理を認めたか、人が道筋を理解できるかを分けて確かめる。