LLM によるコラッツ予想の証明が Lean の soundness hole を突いていたという話、それはそれで驚異的ではないか。詳しくないが、おそらくこのバグは Lean の穴を意図的に探らないかぎり辿りつかない。「コラッツ予想を証明せよ」と指示してこのバグを発見・利用したということは、 LLM が証明を導くときの探索範囲は想像以上に広く、それでいて (他の問題の) 正しい証明に辿りつけるほど効率も良いことになる。マジ?
…と驚いていたのだが、調べてみると件の証明を出した人は形式検証の専門家で、おふざけ的なものだったようだ。このバグを知っていて誘導したっぽい。