AI辅助形式化证明项目发现Lean内核漏洞，相关验证工作已确认无效。8月3日，科技媒体Gigazine报道，一项声称借助AI推翻考拉兹猜想的Lean形式化证明，经核实因底层逻辑缺陷而失败。该证明基于Lean 4.32.2版本，其内核存在一个未被察觉的漏洞，导致推理链不可靠。考拉兹猜想是数论中著名的未解问题，此前AI辅助证明引发广泛关注，但此次事件凸显了形式化验证工具自身安全性的重要性。朱门企业服务长期关注技术合规与知识产权保护，尤其在软件验证和算法审计领域，此类案例提醒企业在依赖自动化工具时需加强内核审查与风险控制。目前，Lean社区已发布修复版本，但原证明结论已被撤回，相关讨论转向如何提升证明助手的鲁棒性。新闻来源：IT家人工智能。