Lean 之父对谈:AI 写代码时代,谁来证明它是对的?
bigdata · x · 2026-10-29
The Data Exchange 播客邀请 Lean 创造者、AWS 杰出科学家 Leo de Moura,讨论 AI 如何让形式化验证走向实用,并可能重塑软件工程。
核心话题:
- AI 生成代码激增,使规格说明与机器可检证明(specification + machine-checked proofs)变得前所未有的重要——「信我」式代码走到尽头
- 用形式化方法验证 Rust 代码、AI 辅助的 autoformalization 与 Mathlib 的规模化
- 如何信任 AI 生成的形式化模型:需求缺口、模型缺口,以及对证明检查器本身的信任
- 形式化验证 vs 传统软件测试;可编辑证明与 Navier-Stokes 证明核对的案例
- 验证 AI agent、沙箱与安全策略的愿景:一个「被验证的软件栈」
- AI 与形式化方法对数学家、工程师技能与职业的影响,以及能否革命数学与理论物理
主持人 Ben Lorica 同时引申:当 AI 能做大部分数学工作时,学术声望可能转向 AI 做不到的事——提出正确的问题。
所属事件:Lean 创造者：AI 时代验证成软件工程瓶颈(2 条相关)→
「编程与Agent」频道最新
- 独立开发者把美国政府差旅补贴表做成 MCP Server，40 个工具直连 agent — allowancesapiteam · 2026-10-30
- Deepgram 收购 Daily：开源语音框架 Pipecat 将保持开源并成立基金会 — schwentker · 2026-10-30
- 自己写 MCP 值不值？开发者征集踩坑与放弃原因 — AaGho_ · 2026-10-30
- Serro 推出「Agentic TPM」：一个 agent 盯住所有编码 agent 防跑偏 — Scobleizer · 2026-10-30
- Grok 疑似已接入 Suno 的 MCP，账号关联因早期访问受限 — koltregaskes · 2026-10-30
- 医疗软件公司 CTO 自述:AI Agent 签保险登记为何演示容易落地难 — alex_verem · 2026-10-30