Lean 创始人 Leo de Moura 谈 AI、Lean 与形式化验证的未来

Lean 创始人 Leo de Moura 在访谈中表示，AI 正通过自动形式化生成 Lean 证明，显著降低代码形式化验证的成本。人类编写的 Mathlib 有 2.5 million 行，而已发布的 AI 生成 Lean 证明达到 50 million 行，其中 Anthropic 的费马大定理证明为 13 million 行。