20 亿行 Lean 证明引激辩：证明是否等于理解
形式化专家 Aram Pell 提出思想实验：若 AI 产出一份长达 20 亿行的 Lean 形式化证明，证明了黎曼猜想或 Collatz 猜想，人类究竟学到了什么？对比费马大定理约 1300 万行的 Lean 证明，这一「无理解的证明」在数学界引发激辩，探讨形式化验证与人类理解之间的鸿沟。
2026-09-09 ~ 2026-09-09 · 2 条相关
- 20 亿行 Lean 证明意味着什么:形式化专家提出「无理解的证明」 — arampell · 2026-09-09
- 20 亿行 Lean 证明却无人能懂？数学家激辩「证明不等于理解」 — Singularitarian · 2026-09-09