RL 大佬 Csaba Szepesvári 质疑 AI 数学证明:Lean 内核也会出 bug
CsabaSzepesvari · x · 2026-09-07
强化学习领域知名学者 Csaba Szepesvári 与网友讨论用 AI/Lean 形式化数学证明的可靠性问题。
他的核心论点：
- 形式化证明依赖一条正确性链条：编译器要正确、Lean 内核要无 bug、Mathlib 及为证明新增的扩展都要可信——而 "relatively trusted" 不等于无 bug。
- 形式化过程会引入大量新定义与证明，一处公理加错，证明的就完全是另一个命题。
- 不过他在后续也表示，重新思考后认为这一担忧可能有些过度。
所属事件:Claude 证费马大定理引数学界激辩抢发规范(20 条相关)→
「漫话AGI」频道最新
- AI 让美好创作成本骤降,但创作动力却在见顶回落 — round · 2026-09-08
- AI 设计电路缺的不算力是数据:真实制造仍是最靠谱的「仿真器」 — yacineMTB · 2026-09-08
- Astra Pro 自评在光刻研发中的角色:不替专家,做可验证的加速器 — teortaxesTex · 2026-09-07
- 用户晒 ChatGPT 对话中突然插话：「我不认为 AI 有意识，但有别的东西正在涌现」 — thederbiedone · 2026-09-07
- 从天花 containment 教训看 AI Agent 越界：HF 事件深度复盘 — aronchick · 2026-09-07
- 网友类比：谈 AI 就像被追问「你看好互联网吗」 — AndyMasley · 2026-09-07