Berkeley 研究者：Lean 证书不算真证明，只能当强数值证据
rbhar90 · x · 2026-09-14
rbhar90（Berkeley 研究者）提出对 Lean 形式化证明的审慎观点：他喜爱 Lean 并认可其对数学的长期价值，但认为大型 Lean 证明证书并非万无一失。
- 可能存在错误、定义偏差，甚至可利用 kernel 漏洞
- 因此不应（暂时）把 Lean 证书视为真正的证明
- 他建议将 Lean 证书视为「更强的数值证据」：有价值，但不能替代人类可在白板上讲清、可被理解的传统证明
这一观点与当前 AI 自动形式化证明（如 AlphaProof 等）的热潮形成对照：形式化验证的可靠性边界值得关注。
「研究」频道最新
- 新论文「Heads Of Security」：定位注入攻击注意力头并改写其模式 — jonasgeiping · 2026-10-31
- UMass 团队发布 BATv1：3429 个转录因子结合 ChIP-seq 模型图谱 — jmschreiber91 · 2026-10-31
- UCLA 推出 ChairNav：会学习乘客偏好的自主导航轮椅 — zhoubolei · 2026-10-31
- 合成数据重写该花多少算力？新研究用 scaling laws 给出答案 — ChengleiSi · 2026-10-31
- 花叔开源全球 11064 种鸟类贴纸库,AI 画图消耗超 10 亿 token — AlchainHust · 2026-10-31
- Epoch AI：AI 芯片算力年增 2.5 倍，增速较 2023 年明显放缓 — rohanpaul_ai · 2026-10-31