OmniTools 10月1日消息，Lean 定理证明器创始人 Leonardo de Moura 在近期技术分享中指出，当前 AI 已能辅助完成复杂形式化证明，例如成功通过 C 语言测试并验证 zlib 库全压缩级别与输入的往返正确性。然而，随着 Mathlib 形式化数学库规模突破 240 万行，规模化验证与生态治理面临挑战。目前 Lean 核心采取严格治理，扩展层相对开放，约 20 人的 Lean FRO 团队负责维护核心信任。此外，近期一个疑似由 AI 参与构造的 Collatz 猜想反例，同时暴露了 Lean 内核及 Rust 版 Nanoda 检查器的漏洞，凸显了 AI 辅助证明场景下检查器自身的安全风险。
