Lean 之父 Leo de Moura 访谈：AI 写代码时代，机器验证的证明将取代信任

The Data Exchange 播客中，Lean 之父 Leo de Moura 表示，AI 让代码生成空前容易，机器检查的证明而非传统测试，可能成为构建可信软件的必经之路。讨论涵盖规范、信任AI生成代码与自主智能体、可验证软件栈、Rust验证、autoformalization、Mathlib、AI辅助数学及验证AI agent的沙箱与安全策略。