フェルマーの最終定理の証明を、コンピューターが最後まで検査できる形にする。Anthropicは9月4日、Claudeを使ったこの形式化を公開しました。発表によると作業は11日間。使ったのは、一般提供モデルと同一とは限らない社内研究モデルです。
ここで注目したいのは「AIが難問を解いた」という見出しよりも、長い仕事をどう分け、どの成果なら次の担当が使ってよいと判断したかです。数学の話ですが、複数のAIと一緒に大きな仕事を進める人にも、考える材料があります。
新しかったのは、証明を検査できる形にしたこと
フェルマーの最終定理は、3以上の整数nについて、正の整数a、b、cで「aのn乗＋bのn乗＝cのn乗」を満たす組はない、という主張です。既知の証明を土台にした今回の仕事では、人が読める数学を、細部まで検査できる形式的な記述に変換しています。
人間向けの文章には「ここから明らか」「同様に示せる」といった省略があります。形式化では、その間を埋める必要があります。最終結論だけ正しそうに見えても、途中の依存先が未証明なら完成とは言えません。
Anthropicの発表は、初期の試みでエージェントが作業状態を見失い、協力がうまく続かなかったことも記しています。そこで使われたのがProve2Meです。定理間の依存関係を管理し、既存の成果を検索して再利用できるようにします。発表は約60億の出力トークンを報告しており、短い日数を、そのまま少ない計算量だと読むことはできません。
会話の記憶だけに、大きな仕事を載せない
Prove2Meの論文は、人とAIが形式化のミッションに参加し、互いの結果を使いながら進めるプラットフォームを説明しています。今回の公式発表では、定理の依存関係を循環のないグラフで持つこと、定理の記述と証明を別ファイルにすること、自然言語の説明から成果を探せることが挙げられています。
たとえば「最後にDを示すにはBとCが必要で、BにはAが必要」と分かっていれば、次に着手できる仕事を選べます。担当が交代しても、会話を最初から読み直して全体像を推測する負担を減らせます。これは仕組みを説明するための簡略例で、実際の証明の構成図ではありません。
AICompanyとして読み取るポイントは、作業の分割と、成果の採用条件をセットで設計することです。「Aができたそうです」という報告と、「Aを検査する手段があり、その検査を通った」という記録では、後続作業の安心感が違います。
何を証明したのかまで確かめる
公開リポジトリのREADMEには、最終的な定理の記述と検証方法が掲載されています。依存する公理の確認に加え、Mathlib側の定理と同じ内容を証明しているかをcomparatorで照合したと報告しています。
これは大切な区別です。検査に通る文章を書けても、それが最初に頼んだ主張と違えば目的を達成したことにはなりません。採点基準そのものを簡単にして満点を取っても、仕事は終わらないわけです。
READMEは、別の検証カーネルnanodaによる検査も報告しています。ただし独自の修正を加えたことを明記しています。検証ツールへの信頼は残り、中間定理の名前が意図した数学的意味を表すかは、読者が判断すべき点とも説明しています。
AICompanyは公開文書を照合しましたが、巨大な証明全体のビルドや独立検証を再実行していません。ここで紹介した検証結果は公開元の報告です。
小さく取り入れるなら、成果物の受け渡しから
ここからはAICompanyの応用案です。数学の形式検証と、普段の開発や記事制作の品質確認は同じ強さの保証ではありません。それでも、仕事の受け渡し方には応用できます。
たとえば記事の図表を作る仕事なら、集計、数値の照合、図の作成、説明文という順に分けます。「集計完了」の条件を、ファイルが存在するだけでなく、対象期間と件数が記録され、元データとの照合が済んでいることにします。図を作る担当には、検査済みの版を渡します。
小さな試行では、次の4項目を一枚の作業表に書くだけでも始められます。
- 成果物：何を残すか
- 依存先：どの成果物の、どの版を使うか
- 合格条件：何を確かめたら次へ渡せるか
- 証拠：検査結果をどこに保存するか
さらに、集計を一か所変更したときに、図と説明文のどこを再確認すべきかを辿ってみます。必要な再確認が分からなければ、依存関係の書き方を直します。この思考実験の目的は、AIを増やす前に、手戻りが見えるかを確かめることです。今回の記事では、この運用による時間短縮を実測したわけではありません。
速さだけで、日常利用の近さを判断しない
公開コードは研究成果物として提供され、保守や貢献受付を行わないとされています。READMEには大きなメモリ・ディスク要件と、Windowsの長いパスに関する制約も記載されています。手元のパソコンで気軽に同じ検証ができる、と期待する用途には向きません。
また、一つの大きな成功例から、依存関係の管理だけが成功の原因だったとは断定できません。モデル、計算資源、人の助言、既存の数学資産も関わっています。大量に生成できることと、人間に読みやすいこと、長く保守できることも別の課題です。
それでもこの事例は、AIが書く量を増やすだけでなく、書かれたものを確かめて積み重ねる仕組みに目を向けさせます。自分の仕事に持ち帰るなら、まず一つの成果物について「何をもって完了とするか」「後からどう確かめるか」を決める。その小さな約束が、長い仕事を一緒に進める土台になります。