数学家发文质疑 OpenAI 88小时万Agent证明：只有证书没有理解
_onionesque · x · 2026-10-13
数学家 Alexander Gamburd 在 arXiv 发表文章《The Siren Call of Silicon Leviathan》，针对 OpenAI 用约 1 万个软件 Agent 在 88 小时内生成 166 页、61.6 万行 Lean 代码的证明成果提出哲学反思。
- 历史上证明有双重意义：真理证书 + 让他人理解为何为真的演示；OpenAI 只交付了前者，全文至今无人完整读过。
- 作者认为接受「无演示的证书」等于接受霍布斯式契约：权威而非真理决定规则。
- 文章将这种趋势称为「倒退的中世纪」，警示数学等学科在 AI 时代面临的认知权威危机。
所属事件:数学家发文质疑 OpenAI 万 Agent 证明：只有证书没有理解(2 条相关)→
「漫话AGI」频道最新
- Fleuret 批「模型预测被 Lean 验证」说法:形式化验证给不了那种保证 — francoisfleuret · 2026-10-13
- 数学家的新焦虑:几个月内 AI 已解出多个重大数学难题 — stevenstrogatz · 2026-10-13
- 数学难题接连被 AI 攻破,数学家反应分化引《银河系漫游指南》式担忧 — LostBetsRed · 2026-10-13
- 研究估算：约五分之一图书由 AI 显著参与撰写，销售额占比从 0 涨到 20% — TuhinChakr · 2026-10-13
- 研究：Amazon 自出版小说已泛滥 AI 文本并挤占人类作者收入 — TuhinChakr · 2026-10-13
- 小模型验证不可靠?Langford 谈规模阈值效应并引 NextLat 论文 — JohnCLangford · 2026-10-13