20 亿行 Lean 证明意味着什么:形式化专家提出「无理解的证明」
arampell · x · 2026-09-09
arampell 提出一个思想实验:假如 AI 产出一份 20 亿行代码的 Lean 形式化证明,证明了黎曼猜想或 Collatz 猜想,我们究竟学到了什么?对比之下,费马大定理的 Lean 形式化约 1300 万行,但背后有人类可读的数学主线(Wiles/Taylor-Wiles),可以端到端跟随论证。而一份只有内核验证、没有人类可压缩论证的证明,可能是真正不同的对象——「没有理解的证明」。他追问:当最短的已知证明证书是机器尺度的、而最短的已知解释根本不存在时,数学意味着什么?
「漫话AGI」频道最新
- 技术作者撞见自己的文章被「搬运」成瑞典语，本人毫不知情 — DavidLinthicum · 2026-09-09
- 图灵奖得主 Barak：AI 证明定理受益于人类辅助， soon 会像深蓝质疑一样可笑 — soumitrashukla9 · 2026-09-09
- 「还有什么更难的?」网友推演万级智能体群将重塑软件与安全 — teortaxesTex · 2026-09-09
- AI 或已解开百万美元数学难题,一个领域将被永久改变 — Gari_305 · 2026-09-09
- 网友推测：既然 agent 能解 Navier-Stokes，OpenAI 或已用它加速算法研究 — teortaxesTex · 2026-09-09
- 谷歌研究员自嘲「温水煮蛙」：AI 解千禧年难题已不再震惊 — AlexIrpan · 2026-09-09