AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明 - GIGAZINE https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

まさに昨日、Z3のお勉強をしてた時にGoogleAI検索さん(Gemini)と「SMTソルバをベースに分解して検証する方が網羅的で穴がないんじゃないの？＞＜」って議論をして、
AI検索さん曰く「SMTソルバは一階述語論理専用だから、その分解処理を人間が書き下す場面で検証にバグが生じる可能性があるし、なにより、SMTソルバは複雑だからそれ自体のバグの可能性が高いし、Leanのカーネルは高階に対応してるけど手動でシンプルだからバグがある可能性が低い」(意訳)
っていってたのに、バグあったじゃん！＞＜；