数学家回应 AI 数学证明争议：自然语言与 Lean 证明不一致只是漏了校对步骤
AlexKontorovich · x · 2026-10-09
数学家 Alex Kontorovich 回应关于 AI 数学证明「自然语言论文与 Lean 形式化证明不对应」的质疑，认为这不是大事。
他解释：该证明的最终命题已经过语义对齐检查（属于 DeepMind 的 Formal Statements 项目），且在标准公理下无 sorry。问题只是流程中漏掉了第三步：
- 步骤 1（很难）：让 AI 解决问题并写出自然语言论文
- 步骤 2（极难）：让 AI 将论文形式化为 Lean 证明，需修正论证中的笔误甚至所引文献的错误
- 步骤 3（简单）：让 AI 回头比对自然语言与形式化版本，修复暴露的问题并标注文献修正
像「某个中间引理在自然语言里用 m+4 正则性、形式化证明里用 m+5」这种不一致，只是流程瑕疵，不影响结论的可信度。引用者 Joel Watson 则认为，社区尚未就「有了 Lean 认证后什么才算证明」达成共识，若散文证明与 Lean 证明不能紧密对应，仍是值得重视的问题。
「研究」频道最新
- aimotive 自动驾驶数据集训练标签靠「事后诸葛」追踪器生成 — RexDouglass · 2026-10-09
- Yale 研究发现 LLM 内部表征存在符号结构 — tallinzen · 2026-10-09
- COLM 2026 离散扩散 meetup:10 月 8 日 4-5 点 Grand Ballroom — yuntiandeng · 2026-10-09
- Astra 机器人控制实测:Johns Hopkins 深度评测其运动与控制理解 — jmin__cho · 2026-10-09
- Tavily 智能体可见性报告遭质疑：提问带域名才 93% 实时检索 — edwin · 2026-10-09
- 独立研究者发布 AI 加速相变模型，6 个预注册预测窗口全部命中 — sadeyeprophet · 2026-10-09