Anthropic、Claudeがフェルマーの最終定理で初の完全なコンピューター検証済み証明を作成したと発表

Anthropicは、フェルマーの最終定理について初の完全なコンピューター検証済み証明を作成したと発表した。Claudeが11日間にわたり、ほぼ自律的に作業して、その成果をLeanで形式化したという。確認され、広く再現されれば、この取り組みは数学とAI支援研究の双方にとって重要な道標となるだろう。

フェルマーの最終定理は、数学で最も有名な命題の一つだ。2より大きい任意の整数nについて、aⁿ + bⁿ = cⁿを満たす正の整数a、b、cは存在しない。アンドリュー・ワイルズは1995年に初めてこの定理を証明したが、その証明は依然として非形式的な人間による論証であり、専門家の検証を必要としていた。Anthropicが説明する長期プロジェクトが目指したのは、それとは異なるものだった。通常の意味での新たな証明ではなく、既存の数学的な論理の連鎖を機械で検証できる形に形式化することだ。

この違いは重要だ。形式証明はコンピューターのカーネルによって独立に検証できるため、曖昧さが減り、見落としやすい誤りの発見にも役立つ。Lean証明支援系は、そのエコシステムにおける主要ツールの一つだ。Anthropicによると、Claudeは膨大な数学的推論をLeanコードに変換し、完全に検証を通過し、形式ライブラリ内の定理の記述と一致すると同社が説明するバージョンに到達した。

この主張は二つの面で注目に値する。第一に、最先端モデルが高度に構造化された技術分野で長時間にわたる作業を遂行できるようになりつつあることを示唆している。第二に、AIシステムが近く、アイデアを提案するだけでなく、人間が精査して信頼できる大規模かつ検証可能な成果物を組み立てるためにも役立つ可能性を示している。Anthropicによると、このプロジェクトでは過程で数千件の定理が生み出され、一つの巧妙な飛躍ではなく、大規模な証明開発作業が行われた。

Leanコミュニティーは何年にもわたり、フェルマーの最終定理の形式化に取り組んでおり、ケビン・バザードのプロジェクトが中心的な役割を果たしてきた。その取り組みの目的は、数学を自動化で置き換えることでは決してない。そうではなく、難解な成果をより監査しやすくし、将来の研究に使われる基盤を改善することを目指している。Anthropicの発表は、この文脈の中で行われたものであり、その外部から現れたものではない。

独立したLeanコミュニティーのページとプロジェクトのリポジトリは、フェルマーの最終定理の形式化が現在進行中の複数著者による取り組みであることを裏付けている。これらの資料だけではClaudeの貢献の正確な範囲を検証できないものの、より広範な研究計画の存在は確認できる。Anthropicの発表と併せて考えると、これは思いつきのデモではなく、活発に進行する数学プロジェクトに組み込まれた成果であることが分かる。

このニュースはまだ初期段階にある。企業による発表は、詳細な査読済み数学論文と同じではなく、研究コミュニティーは証明、ツール、前提条件を慎重に精査したいと考えるだろう。しかし、そうした慎重さを踏まえても、その重要性は失われない。汎用モデルがこの規模の形式証明に取り組めるのであれば、それは数学におけるAIの新たな段階を示唆する。出力が説得力のある文章にとどまらず、機械が検証できる再現可能な成果物となる段階だ。

その可能性は、フェルマーの最終定理をはるかに超える重要性を持つ。同じ手法は最終的に、大規模な数学ライブラリ、ソフトウェアの形式検証、そして信頼性が厳密な記号的推論に依存するあらゆる分野に応用できるかもしれない。Anthropicの発表は、終着点ではなく、その道程における節目として理解するのが最も適切だ。モデルに単に定理を説明させるのではなく、コンピューターが独立して認証できる証明を構築するよう求めたとき、何が起こり得るかを示している。