Lean形式化验证信任

Lean定理证明器作为数学与代码正确性的“真理机器”，其核心价值在于通过极小的可信内核实现逻辑验证，但近期暴露的信任危机揭示了自动化证明的深层局限。2026年9月，创始人Leonardo de Moura披露Collatz猜想证明事件中，两个独立检查器分别被不同漏洞欺骗，凸显了单一内核实现的脆弱性；同年7月，Lean 4.32版本亦修复了两个可导致证明False的内核漏洞。与此同时，随着AlphaProof等AI系统介入，新的风险浮现：类型检查器仅保证逻辑推导无误，却无法验证命题是否忠实表达人类意图，导致“语义幻觉”。尽管Lean4Lean等外部验证器和Lean Atlas等人工介入工具试图缩小信任范围，但在AI大规模生成证明的背景下，如何确保“陈述的正确性”而非仅仅是“推导的有效性”，仍是该领域尚未解决的根本分歧。