数学家 Kevin Buzzard 独立验证 Anthropic 的 FLT Lean 证明:确实成立
AlexKontorovich · x · 2026-09-05
数学家 Alex Kontorovich 转发了 Kevin Buzzard 的博文,后者对 Anthropic 完成的费马大定理 Lean 形式化做了独立核验。
- Buzzard 已编译代码库并运行 comparator,校验通过
- 证明超 1340 万行,在 96 核机器上编译耗时约为 mathlib 的近 20 倍,即便 500G 内存机器浏览仓库也会卡顿
- 该证明完成的是 Wiedijk 100 大形式化挑战的最后一项,采用 Darmon–Diamond–Taylor 1995 年路线
此帖与 Anthropic 官方公告同一事件,Buzzard 的独立验证为可信度提供了数学界背书。
「研究」频道最新
- VeriPhy:用类型化物理义务对世界模型生成视频做可审计验证 — Wenzhuo Xu · 2026-09-05
- Agent 评测框架 TRACES 上线:考察实时执行而非对答案 — SucceededMind · 2026-09-05
- Domingos 反讽：我的「新点子」RNN 做对了能碾压 Transformer — pmddomingos · 2026-09-05
- LoRA 作者发博文详解开源模型后训练与 RL 实操 — iamrobotbear · 2026-09-05
- CoT 监控热议下，一视频带你窥探 LLM 内部思维过程 — kastnerkyle · 2026-09-05
- 多智能体辩论可能越辩越错，ICML 论文揭示讨好型失败模式 — ghadfield · 2026-09-05