Anthropic、ClaudeがLeanでフェルマーの最終定理の形式化を支援したと発表

Anthropicは、Claudeを使ってフェルマーの最終定理をLeanで形式化する研究を公開した。Leanは数学的議論を一行ずつ検査する証明支援系であり、この発表はモデルが新しい証明を独力で発見したという話ではない。むしろ、人間が圧縮して書いた高度な証明を、機械が検査できる形式コードへ変換するという、AI数学支援の実用的な前線を示している。

フェルマーの最終定理は数学史で最も有名な結果の一つだ。Andrew Wilesが1990年代に証明したが、その証明は数論や代数幾何の深い道具に依存する。これを形式化する作業は、読者向けの説明を書くこととはまったく違う。定義、依存する定理、変形、論理的な一歩一歩を、証明支援系が検査できるほど明示しなければならない。専門家にとっても遅く、細かな作業になる。

Anthropicの記事では、Claudeはこの証明工学の共同作業者として位置づけられている。モデルはLeanコードを提案し、数学的な記述を形式構文へ移し、エラーを修正し、中間補題をつなぐ案を出すことができる。一方で、研究者は方針が数学的に妥当かを判断し、生成コードを読み、証明状態が複雑になったときにシステムを導く必要がある。これは人間の判断を不要にする話ではなく、AI支援の精度が上がっているという話だ。

形式証明は言語モデルにとって厳しい試験でもある。モデルは説得力ある文章を書きながら間違えることがあるが、Leanは論理が通らない証明を受け入れない。そのため誤りは自動的に見つかりやすい。成功の意味も変わる。AIが美しい証明文を書けるかではなく、厳密な形式システムの中で検証可能な成果物を完成に近づけられるかが問われる。

AI業界にとって、この研究は科学技術分野での利用像を示す。モデルは退屈な翻訳、探索、修復のループを担い、専門家チームを速くできる可能性がある。形式数学、プログラム検証、安全が重要な工学では、流暢な文章だけでなく、監査可能な推論と外部ツールで確認できる成果物が必要になる。モデルがその制約内で働けるなら、専門家の検証を残したまま作業速度を上げられる。

Anthropicもこの成果を到達点ではなく一歩として扱っている。大規模な定理形式化はなお難しく、人間の計画と修正は欠かせない。それでも今回の発表は、前線のAIが会話の答えだけでなく、厳しい環境で検証可能な仕事を作れるかによって評価され始めていることを示している。