Ben Lorica 与 Lean 作者、AWS 自动化推理组副总裁 Leo de Moura 的长访谈。出发点是一个判断：生成已经变容易了（但不见得便宜），于是瓶颈转移到验证。两人讨论了 AI 生成的代码为什么需要机器可检验的证明、自动形式化与 Mathlib 的规模化、AI 生成的证明能否被信任、以及“从写代码转向写规格”之后软件工程会变成什么样子。
🔑 核心要点
核心命题：生成容易之后，验证成为新的稀缺资源。
话题覆盖 Rust 验证、自动形式化、Mathlib 扩展与证明检查器本身的信任问题。
把形式化验证推向 AI agent、沙箱与安全策略——不只是数学与算法。
展望部分延伸到金融、化学、会计与法律：凡有明确规格的领域都可能被覆盖。
💡 金句
We’re in an era where generation has become easy. Not necessarily cheap, as people who use Claude Code will attest, but easy. And so, one of the key challenges is verification.