用数百次 agent 交叉验证替代 Lean,AI 数学证明可信度引争论
DimitrisPapail · x · 2026-09-15
- Dimitris Papail 回应质疑:他没见过 sol/astra 等模型宣称证明正确却被证伪的案例,相关结果已由横跨 3 个模型的数百次 agent 调用交叉验证,许多人已接受这种方式。
- 对话另一方 QuangVDao 认为,缺少 Lean 形式化验证会让纯计算类结果难以取信于人,他自己项目中用 Lean 检查大型证书就很难。
- Papail 反驳:这类证明涉及大量输入、界与数值表,几乎不可压缩,转成 Lean 未必更容易,例如上界证明形如「若这些概率分布与数值表满足所有给定不等式,则容量至多为某值」。
所属事件:三智能体四周写出数学新结果，3000 美元 GPU 产出 100GB 证书(10 条相关)→
「编程与Agent」频道最新
- 开源 awa-video-reel:用 Claude Code 自动剪辑短视频并录制网站 B-roll — TawohAwa · 2026-11-02
- 经济学博士求职市场数据库上线：900+ 候选人可接入 AI 助手 — aniketapanjwani · 2026-11-02
- 终端能跑 cron 却挂：开发者的 7 条定时任务排查清单 — petrusenko_max · 2026-11-02
- 本地量化模型对决 Claude：9 个真实 bug 修复实测，量化掉分更掉时间 — FeydRowan · 2026-11-02
- 把产品重做一遍给 AI 用：MCP 让 Claude Code 代管全部后台 — gefei55 · 2026-11-02
- 独立开发者发布 31 工具社交排程 MCP server，分享三条实战设计经验 — troyizzle · 2026-11-02