20 亿行 Lean 证明却无人能懂？数学家激辩「证明不等于理解」

Singularitarian · x · 2026-09-09

Aram Pell 提出一个尖锐问题：如果黎曼猜想或 Collatz 猜想的 Lean 形式化证明长达 20 亿行，人类究竟学到了什么？费马大定理的 Lean 证明约 1300 万行，但至少有 Wiles/Taylor-Wiles 的人类可读论证骨架可从头到尾跟随；而仅靠内核验证、无法压缩为人类论证的证明，可能是完全不同的对象——「没有理解的证明」。

数学家 Alex Kontorovich 回应：有了 Lean 形式化后，他会与 AI 迭代对话，把自己已理解的部分告诉 AI，再逐个攻克未知环节——他甚至想用这个方法重新研究 FLT 的证明过程。他认为形式化打开了人类理解的新可能。双方分歧在于：机器尺度的证明证书与不存在的最短人类解释之间，数学理解将走向何方。