Csaba Szepesvári 质疑 Lean 形式化证明:编译器与内核是否可信
CsabaSzepesvari · x · 2026-09-07
RL 领域学者 Csaba Szepesvári 在讨论 Anthropic 相关的 Lean 形式化证明（疑似费马大定理 FLT）时提出核心疑问：把数学证明编译成 Lean 语言需要正确的编译器，Lean 内核虽然小且相对可信，但真的无 bug 吗？为支持证明而引入的 Mathlib 及其扩展同样需要审视。
在后续推文中他表示重新思考后认为自己的担忧可能被夸大了：可以打印出证明使用的全部公理，无需 sorry 的证明即是证明（除 Lean 自身 bug 外），人工核查并非不可行。这是一场关于 AI 辅助形式化证明可信边界的严肃讨论。
所属事件:Claude 证 FLT 引爆数学界抢发伦理之争(26 条相关)→
「研究」频道最新
- DONIC 双手机器人追踪成功率 86.79%，远超此前 SOTA 的 9.43% — liuziwei7 · 2026-10-27
- 研究者吐槽:论文里 PSNR 低于 15dB 基本是用错了指标 — kwangmoo_yi · 2026-10-27
- Ortet 首批医疗评测:34 个开源模型 50 项任务,通用排名不够用 — thegautamkamath · 2026-10-27
- Scaling 拟合之争:Uncheatable 计入输出头 FLOPs,Paloma 剔除,最小档差距高达 65% — dlwh · 2026-10-27
- Marin 作者详解 scaling law 公式：难点在小模型阶段估渐近线 — dlwh · 2026-10-27
- Marin 开源 scaling law 外推 300 倍，预测大模型 loss 误差仅 0.2% — dlwh · 2026-10-27