Lean 之父 Leo de Moura：AI 写代码时代，机器验证的证明将取代信任
bigdata · x · 2026-11-01
The Data Exchange 播客访谈 Lean 之父、AWS 杰出科学家 Leo de Moura，主题是 AI 让形式化验证变得触手可及，可能重塑软件工程：
- AI 使代码生成空前容易，「验证」成为关键瓶颈；机器检查的证明（machine-checked proofs）而非传统测试，可能是构建可信软件的必经之路。
- 讨论话题覆盖：规范（specification）的重要性、如何信任 AI 生成的代码与自主智能体、可验证软件栈的愿景、Rust 验证与 autoformalization、Mathlib 的规模化、AI 辅助数学、Navier-Stokes 与证明错配、验证 AI agent 的沙箱与安全策略，以及对工程师/数学家技能与职业的影响。
- 访谈还展望了形式化方法向理论物理等领域的延伸。
「编程与Agent」频道最新
- 用 Qwen3-0.6B 手把手训练你自己的决策模型 — dl_weekly · 2026-11-01
- 143k 星 ui-ux-pro-max 等 7 个设计仓库,帮 AI 网页设计去「AI 味」 — GCWebDesigner · 2026-11-01
- 语音输入工具 Hex 发布稳定版：本地运行，为 AI Agent 对话设计 — madeofAjala · 2026-11-01
- 个人 AI Agent 大混战：一段 prompt 让你的配置在智能体间无缝搬家 — EXM7777 · 2026-11-01
- Nous Research Hermes 移动端开启测试，iOS/Android 双端 Beta 上线 — testingcatalog · 2026-11-01
- 生产级 AI Agent 指南：从模型到结果之间的七层工程 — blaizedsouza · 2026-11-01