数学

1995年に証明された定理を、Claude が11日で Lean に書き直した。約1,300万行・29,511定理。すでに正しいはずの証明を、なぜ機械で検証し直すのか——その意味と限界を一次情報で整理します。

Anthropicが8月10日、研究版Claudeが「リーマン予想を満たすと証明された零点の割合」の下限を41.6%から67.2%へ引き上げたと発表。約60のサブエージェントが約1日半で650の失敗を積んで突破し、Lean形式証明も公開済み。証明ではなく未査読だが、AIが数学の前線を押した記録だ。

Anthropic の Levent Alpöge 氏が Claude Fable 5 で得たヤコビアン予想の反例。Lean 形式化は CI を通過したが、査読論文もプレプリントもない。反例は3変数の多項式写像で、2変数の場合は未解決。何が機械的に検証され何が未確認かを一次情報だけで整理する。