Berkeley 研究者：Lean 证书不算真证明，只能当强数值证据
rbhar90 · x · 2026-09-14
rbhar90（Berkeley 研究者）提出对 Lean 形式化证明的审慎观点：他喜爱 Lean 并认可其对数学的长期价值，但认为大型 Lean 证明证书并非万无一失。
- 可能存在错误、定义偏差，甚至可利用 kernel 漏洞
- 因此不应（暂时）把 Lean 证书视为真正的证明
- 他建议将 Lean 证书视为「更强的数值证据」：有价值，但不能替代人类可在白板上讲清、可被理解的传统证明
这一观点与当前 AI 自动形式化证明（如 AlphaProof 等）的热潮形成对照：形式化验证的可靠性边界值得关注。
「研究」频道最新
- 学者吐槽学生论文被 GPT/Claude 写成难读的 Claudish 体 — xuanalogue · 2026-09-14
- 自进化研究框架 Épi 几天产出 120 项纪录级结果 — my_cat_can_code · 2026-09-14
- RL 大佬 Szepesvári:研究者其实盼着 AI 能自己生成洞察 — CsabaSzepesvari · 2026-09-14
- 用 CUDA 加速 Minecraft 世界生成,9 人分屏可跑通 — gandamu_ml · 2026-09-14
- Ted Nelson 1965年超文本原始思考片段重新流传 — dreamwieber · 2026-09-14
- 「论文没放可复现代码」，AI 圈吐槽做成梗图 — CSProfKGD · 2026-09-14