定理証明支援系

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