Claude、11日間でフェルマーの最終定理を完全形式化か

何が起きたのか

フェルマーの最終定理は、3より大きい整数nについて、正の整数a、b、cがaⁿ+bⁿ=cⁿを満たすことはない、という命題です。数学者アンドリュー・ワイルズによる証明は1990年代に完成しました。しかし、人間向けの論文をコンピューターが一行ずつ検証できる形式へ変換する作業は、別の大規模な工学課題です。

Anthropicによれば、Claudeを使ったチームは約11日でLeanによるエンドツーエンドの形式化を完成させました。これはClaudeが新しい証明を発見したという意味ではありません。人間の証明に含まれる「明らかである」といった省略をなくし、定義、型、補題、依存関係をすべて明示したということです。Leanは、各推論が既存の公理や定理から正しく導かれるかを機械的に確認します。

規模と検証

発表された数字では、約1300万行のLeanコードと3万件を超える中間定理が作られ、最終証明では約2万9500件が使われました。コード量はLeanの数学ライブラリMathlibの5倍以上に相当するとされています。また、3つの標準公理だけに依存し、定理の主張がMathlibのフェルマーの最終定理と一致することをプログラムで比較したと説明されています。これらはプロジェクト側の報告であり、AIが新理論を発見したことを示すものではありません。

成否を分けたHarness

初期のマルチエージェント構成では、個々のAgentが成果を出しても、全体の状態を見失い、作業の重複や統合作業の難しさが生じました。転機になったのが、Prove2MeとClaude Codeベースのmulti-agent Harnessです。

この仕組みは証明を定理ノードの有向非巡回グラフとして管理します。前提条件、完成状況、再利用できる補題を記録し、定理の主張と証明を分離しながら、自然言語の説明も検索に使います。定義、中間補題、上位定理、最終統合を複数のAgentに分担させ、人間は主に優先順位を示しました。報告された出力トークンは約60億です。

意味と限界

重要なのは、AIが数学の答えを出したことだけではありません。タスクを分解し、依存関係を管理し、コンパイラーのエラーを修正し、成果を再利用するという、形式数学の工程全体をAIが扱える可能性を示した点です。

一方、Leanが保証するのは、与えられた基礎と定式化の上で導出が正しいことです。モデル化が適切か、定理の主張が意図に合っているかを自動で判断するわけではありません。今後の数学AIでは、推論能力だけでなく、記憶、依存関係グラフ、検証器、協調Harnessの品質が重要になります。

出典：量子位