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

AWS 自动推理组副总裁、Lean 创造者 Leo de Moura 在访谈中表示，AI 已能按形式化规格生成代码并给出机器可检验的 Lean 证明，例如 Kim Morrison 将 zlib 移植到 Lean 并证明压缩解压无损。他认为形式化验证正从人工测试转向以规格和机器检验证明为核心，可用于验证 AI 生成代码与自主智能体。