论文与 Lean 证明对不上？开发者点破 AI 数学研究的流水线缺陷
burny_tech · x · 2026-10-09
thomasahle 评论 AI 数学研究成果时指出：模型通常是先用文本解题，再由另一个 agent 将解法形式化为 Lean 证明。后一个 agent 可能发现并修复了证明中的问题，但没有把修复「回移」到论文文本，导致论文与 Lean 代码不一致。他建议直接让模型对照 Lean 中问题是如何修复的来看，因为论文与形式化证明对不上的情况并非第一次发生。
所属事件:剑桥论文质疑 Lean 验证背书，直指 OpenAI Navier-Stokes 证明疑点(18 条相关)→
「编程与Agent」频道最新
- 给 Opus 加 Minecraft 世界记忆后进度提升 133%,WorldBox 沙盒发布 — Lianhuiq · 2026-10-09
- GPT-6 生成式 UI 走红后,下一代 Agent 缺的是生成式工作流层 — Over_Accountant_2311 · 2026-10-09
- Next Token 播客第 5 期:Personal Agent 大战与 AI 复刻软件影响 — op7418 · 2026-10-09
- mattyp 的 build a bot 支持语音反馈,每条反馈进队列交给 agent 修复 — mattyp · 2026-10-09
- 10 分钟用 Claude 逆向复刻 3D 像素 emoji 动画风格,做成可玩 artifact — justin_hart · 2026-10-09
- Delphi 讲解 Predict Anything 原理:LLM 报赔率+LMSR 市场结算 — benfielding · 2026-10-09