AI 辅助推翻考拉兹猜想的证明被确认无效，Lean 4.32.2 修复内核漏洞

一项借助 AI 完成、声称推翻考拉兹猜想的 Lean 形式化证明被确认无效。该项目由形式化验证专家 Ramana Kumar 于 7 月 25 日在 GitHub 发布，没有给出具体反例整数，审查后他发现相关方法甚至能让 Lean 无条件接受 False。