Lean 之父 de Moura：AI 写码时代，验证成新瓶颈
bigdata · x · 2026-10-30
Ben Lorica 采访 Lean 创造者、AWS 杰出科学家 Leo de Moura，主题是 AI 让形式化验证变得可用，可能重塑软件工程。
核心观点
- 代码生成已不是难题，验证才是新瓶颈；AI 生成代码需要机器可检验的证明，而非“信我”式交付。
- 规格说明（specifications）与机器校验证明的重要性上升，软件工程的重心从写代码转向写规格。
- 讨论 AI 辅助数学：Autoformalization、Mathlib 的规模化、Navier-Stokes 等证明错配问题与可编辑证明。
- 延伸话题：验证 AI 自主 agent、沙箱与安全策略，以及“已验证软件栈”的愿景；AI 与形式化方法能否推进理论物理。
对工程师的含义：技能与职业方向将向规格编写与验证能力倾斜，类似突破还可能在其他领域出现。
所属事件:Lean 之父：AI 写码时代验证成关键瓶颈(3 条相关)→
「编程与Agent」频道最新
- Gym-Anything 引入审计 Agent,专门用合法动作破坏环境找错 — wellecks · 2026-10-30
- CMU 用 Agent 自动造 200+ 软件环境,Gym-Anything 拿 GDP 数据选题 — wellecks · 2026-10-30
- Cloudflare 不肯做,开发者自研工具实现 Durable Objects 零停机迁出 — samgoodwin89 · 2026-10-30
- 两分钟面试法：用一条 prompt 让 Grok 帮你搭两个定制 bot — nateliason · 2026-10-30
- Cursor、Harvey 为何自训专用模型：多数细分市场养不起专属大脑 — MartinGTobias · 2026-10-30
- Scenario 开源 3D OS：80 项技能让编码 Agent 直通 Blender 和 Unreal — Scobleizer · 2026-10-30