用数百次 agent 交叉验证替代 Lean,AI 数学证明可信度引争论
DimitrisPapail · x · 2026-09-15
- Dimitris Papail 回应质疑:他没见过 sol/astra 等模型宣称证明正确却被证伪的案例,相关结果已由横跨 3 个模型的数百次 agent 调用交叉验证,许多人已接受这种方式。
- 对话另一方 QuangVDao 认为,缺少 Lean 形式化验证会让纯计算类结果难以取信于人,他自己项目中用 Lean 检查大型证书就很难。
- Papail 反驳:这类证明涉及大量输入、界与数值表,几乎不可压缩,转成 Lean 未必更容易,例如上界证明形如「若这些概率分布与数值表满足所有给定不等式,则容量至多为某值」。
所属事件:AI 智能体协作四周产出数学新成果，3000 美元 GPU 费引热议(10 条相关)→
「编程与Agent」频道最新
- Snapcompact:把上下文渲染成像素图,成本降一半以上 — brandon_galang · 2026-09-15
- Benzi 上线：贴个 GitHub 链接即可在线对话任意代码仓库 — DonkeyTheKing · 2026-09-15
- 蚂蚁 Ling 携手 Hugging Face 与 NVIDIA 办本地 AI 助手实战专场 — heyneighbor · 2026-09-15
- 两周经验浓缩成开源 Skill,一句话让 Codex 开发并上架 Obsidian 插件 — vista8 · 2026-09-15
- 腾讯微信团队开源 WeKnora:企业知识库 RAG 平台斩获 2.3 万 Star — yangyi · 2026-09-15
- 开发者自建本地编排层 Taskuary,给多个编码 agent 共享任务队列 — Appropriate-Path-461 · 2026-09-15