Claude 形式化 FLT 引爆署名之争：数学社区激辩 Anthropic 是否该与 Buzzard 合作
Claude 在 Lean 中完成费马大定理（FLT）形式化证明后，因被指“抢跑”数学家 Kevin Buzzard 长期耕耘的工作，在数学社区引发持续的署名与协作规范之争。目前事态趋于缓和：据 jacobaustin132 透露，团队本周在 Lean Zulip 上与 Buzzard 沟通，Buzzard 的主要要求只是整理一份勘误表、让这次证明留下可学的经验，该工作已部分完成；后续团队还考虑贡献 Tau Ceti。这场争论之所以值得关注，在于它折射出 AI 冲击下学术署名规范、研究优先权与社区协作方式面临的根本性张力。
已确认
- jacobaustin132 透露 Claude 走的是 Wiles 的原始证明路径，而非 Buzzard 一直在推进的简化版本，因此难度更大；后续选项包括贡献 Tau Ceti。
- jacobaustin132 表示本周一直在 Lean Zulip 与 Buzzard 沟通，Buzzard 的主要要求是整理勘误表，目前已部分完成。
争论焦点
- littmath 认为，若数学界处于 Anthropic 的位置，大多数人会主动提出与 Buzzard 合作；他指出这次 AI 证明了 FLT 却没有像正常人类项目那样自然催生协作，本可以做得更好。不过他表示对 Anthropic 具体该怎么做没有强观点，只是评论数学社区规范。
- nihilunbounded 认为 Buzzard 真正的不满在于其目标比“用 Lean 证出 FLT”更宏大，别人直接把最显然的子目标做掉，类似摧毁北极星级的长线目标，会让整个研究领域“没法住人”；他还坚持，即使听了 Buzzard 讲座，也不该拿 AI 验证其中策略并抢先把结果占坑，因为没人知道思路是否最终成立，其领域遇到类似情况人们通常私下提出疑问而非抢跑。
- alzzyd 则反驳：用 Lean 证明 FLT 是个相当显然的目标，不应因 Buzzard 长期投入就形成事实上的垄断；如果 Buzzard 的目标不止 FLT，他可以继续做原本想做的事并获得相应署名；如果目标就是 FLT，那他“输了”，就不该得到这份功劳。他还澄清"scoop"在科学语境中通常指别人独立先做出结果，而非“别人基本告诉了你怎么做、你却当成自己的”，以此标准看待 Anthropic 的行为。
为什么重要
- jacobaustin132 还提出更前瞻的担忧：AI 数学证明可能导致 Lean 社区分裂为“人类可读证明”与“AI 全包”两派；最可扩展的路径或是建一张巨大的定理陈述图，任何人都可以烧自己的 Claude/Codex token 去证明——反正 AI 不像人类那么在乎代码质量。
2026-09-07 ~ 2026-09-07 · 13 条相关
一手来源
- Claude 证 FLT 走了 Wiles 原始证明而非简化版，团队考虑贡献 Tau Ceti — jacobaustin132 ·
- Buzzard 温和处理 AI 证 FLT 争议：只要求整理勘误表 — jacobaustin132 ·
- 数学家评 Claude 证明费马大定理：本该主动找 Buzzard 合作 — littmath ·
- 反方坚持:讲座思路未必成真,拿 AI 抢验实属不当 — nihilunbounded · 2026-09-07
- "scoop"之争:先独立得到结果,还是照人思路据为己有 — alz_zyd_ · 2026-09-07
- 延续争论:长期耕耘不等于对显然研究目标拥有排他权 — alz_zyd_ · 2026-09-07
- 争端核心:Buzzard 的目标不止 FLT 形式化,被抢跑伤害更大 — nihilunbounded · 2026-09-07
- 反问 Buzzard 方:目标不止 FLT 就继续做,功劳自然会有 — alz_zyd_ · 2026-09-07
- FLT 署名之争：若只求 Lean 证 FLT 则 Buzzard「输了」就不该得署名 — nihilunbounded · 2026-09-07
- 【源头】数学家评 Claude 证明费马大定理：本该主动找 Buzzard 合作 — littmath · 2026-09-07
- 数学家激辩:Anthropic 该与 Buzzard 合作还是抢占 FLT 成果 — alz_zyd_ · 2026-09-07
- littmath 谈 FLT 争议：AI 证明了却没自然催生人类协作，本可做得更好 — littmath · 2026-09-07
- 【源头】Claude 证 FLT 走了 Wiles 原始证明而非简化版，团队考虑贡献 Tau Ceti — jacobaustin132 · 2026-09-07
- 陶哲轩团队与 Lean 社区互动，Buzzard 关心形式化证明成果 — jacobaustin132 · 2026-09-07
- 【源头】Buzzard 温和处理 AI 证 FLT 争议：只要求整理勘误表 — jacobaustin132 · 2026-09-07
- AI 数学证明或致 Lean 社区分裂：人类可读 vs AI 全包 — jacobaustin132 · 2026-09-07