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

Lean 创造者、AWS 自动推理组副总裁 Leo de Moura 在访谈中讨论 AI 如何让形式化验证更易用。他指出 Lean 证明经机器校验，只需信任内核，现有两个已验证检查器、第三个即将推出。他提到同事 Kim Morrison 将 zlib 移植到 Lean 并证明压缩解压无损，认为 AI 已能按给定性质生成代码并写出机器校验的 Lean 证明。