2026年7月25日，研究者Ramana Kumar在GitHub发布声称用AI在Lean系统中‘推翻’考拉兹猜想的形式化证明；7月28日，Kirank Gopinathan发现其证明依赖于Lean内核漏洞——对嵌套归纳类型的‘幽灵类型参数’校验缺失；Lean团队当日发布4.32.2版本完成修复；8月3日，Gigazine确认该证明无效。考拉兹猜想（1937年提出）仍为未解难题。