Lean 创造者 Leonard 谈 AI 形式化验证：机器证明将重塑软件工程

Lean 创造者、AWS 杰出科学家 Leonard 表示，AI 时代代码生成日益容易，验证正成为软件工程的关键瓶颈，单靠测试不足以建立可信软件。AI 驱动的形式化验证有望从根本上改变软件构建方式，并同时重塑数学研究与软件开发。