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

Lean 创始人、AWS 副总裁兼杰出科学家 Leo de Moura 在访谈中表示，AI 已能根据形式化规格生成代码并写出可机器校验的 Lean 证明，其同事 Kim Morrison 已将压缩库 zlib 移植到 Lean 并证明压缩后解压可无损还原数据。他指出形式化验证只需信任极小的内核，Lean 现有两个经过验证的检查器、第三个即将推出。