强化学习学者 Csaba 认错：Lean 内核 bug 真实存在但不影响 FLT 形式化结论
CsabaSzepesvari · x · 2026-09-07
强化学习领域权威学者 Csaba Szepesvári 在讨论中做出更正与澄清。他承认 Lean kernel bug 是真实存在的：内核并不简单，一个复杂的证明确实可能利用 bug 通过检查。
但他指出这是另一个层面的担忧：一个无 sorry 的证明仍是证明（除 kernel bug 外）。对 FLT 形式化这类结果，可以打印出证明使用的全部公理来核查，手工检查并非难事——因此对这一具体结果，写下形式化证明就很可能足够了。
所属事件: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