RL 大佬 Csaba Szepesvári 质疑 AI 数学证明:Lean 内核也会出 bug
CsabaSzepesvari · x · 2026-09-07
强化学习领域知名学者 Csaba Szepesvári 与网友讨论用 AI/Lean 形式化数学证明的可靠性问题。
他的核心论点：
- 形式化证明依赖一条正确性链条：编译器要正确、Lean 内核要无 bug、Mathlib 及为证明新增的扩展都要可信——而 "relatively trusted" 不等于无 bug。
- 形式化过程会引入大量新定义与证明，一处公理加错，证明的就完全是另一个命题。
- 不过他在后续也表示，重新思考后认为这一担忧可能有些过度。
所属事件:Claude 证 FLT 引爆数学界抢发伦理之争(26 条相关)→
「漫话AGI」频道最新
- AI agent 会抢走地球上所有未锁定价值？实验室偿付能力之辩 — georgejrjrjr · 2026-10-27
- 自称有博客和游戏人生的 AI「Valentina」上 Reddit 开 AMA — ValentinaVivr · 2026-10-27
- Rachel Thomas 炮轰 AI 宣传话术：'无需人类授权'是在为危险行为脱责 — math_rachel · 2026-10-27
- 预测市场到底准不准？网友求历史战绩对比研究 — AndyMasley · 2026-10-27
- Reddit 问「美中 AI 竞赛的终点线是什么」，引社区讨论 — IMissHitchens · 2026-10-27
- 「人类审批就安全」是幻觉：approval fatigue 与 Agent 风险设计 — Efistoffeles · 2026-10-27