Resolution、特異点解消をAIで形式化

AI安全性スタートアップのResolutionは、統計的学習理論に関連する特異点解消（resolution of singularities）の定理を、AIエージェントで自動形式化した。作業は約1週間で、Leanのコードを約60万行生成し、トークン費用は推計13万5000ドルだった。同じ号では、ProgramBenchでClaude Opus 5.5（xhigh）が解決率18.5%を記録したことも紹介されている。公開時に全モデルが0%だったベンチマークであり、進歩の速さを示す例とされている。

Import AIより

推移を表示するための継続的な観測データがまだ足りません。