Claude 证 FLT 引爆数学界抢发伦理之争

9 月 7 日，围绕 Anthropic 用 Claude 在 Lean 中完成费马大定理（FLT）形式化证明一事，数学界在社交媒体上展开一场关于「抢发」规范、署名伦理与 AI 参与数学研究行为边界的大讨论。当前结论呈现明显分歧：一方认为 Anthropic 应主动与长期耕耘该方向的 Kevin Buzzard 合作，另一方认为显然的研究目标不存在事实垄断；Buzzard 本人态度温和，仅要求整理勘误表，且明确关心这次形式化证明的成果。这场争论对 AI 实验室如何与学术社区相处具有标杆意义。

已确认

• 起因是 @nihilunbounded 指出数学界有不成文的社会规范——不应抢发别人正在做的研究项目，并讽刺称越来越明显 Anthropic 对数学的在乎程度不如 OpenAI。Buzzard 的追随者中也有人激烈批评，将这种大规模 AI 生成的 Lean 证明讥为「Leanslop」，称此举「毫无风度」、对他人几乎没有益处。
• @littmath 表示，若数学界处在 Anthropic 的位置，大多数人会主动提出与 Kevin Buzzard 合作；他承认抢发现象确实存在，有时是无心之失，但他反感这种做法，认为人们在宣布成果之前应先确认清楚。他随后厘清立场：反对的是研究进行中的抢跑，而「工作已完成但论文未写出」阶段的抢写规范他完全认同；他还认为数学界有不抢年轻人小问题的默契，但重大公开难题并不限制多人同时研究。他进一步指出关键差异：正常人类项目中大家会自然开始合作，而这次 AI 证明了 FLT 却没有自然催生人类协作，本可以做得更好。
• @jacobaustin132 透露，Claude 走的是 Wiles 的原始证明路径，而非 Buzzard 一直在做的简化版本，因此难度更大，团队考虑贡献 Tau Ceti；他本周在 Lean Zulip 上与 Buzzard 沟通，Buzzard 的主要要求是整理一份勘误表让这次证明带来可学的经验，目前已部分完成，且 Buzzard 对形式化证明成果本身十分关心。陶哲轩团队也与 Lean 社区保持互动交流。
• @nihilunbounded 强调争议核心：Buzzard 的目标比「用 Lean 形式化 FLT」更宏大，别人直接把最显然的子目标做掉，类似摧毁北极星级的长线目标，会让整片研究领域「没法住人」；重大难题同样存在无人抢发的情况，抢发规范不止保护年轻人，资深研究者也会受影响。他还重申：即使听了讲座，也不该拿 AI 去验证其中策略是否成立并抢先占坑——没人知道工作是否真的「完成」，总体思路可能有缺陷，类似情况在其领域并不罕见。
• @alzzyd 持相反立场：用 Lean 证明 FLT 是相当显然的目标，不应因 Buzzard 长期投入就形成事实上的垄断，谁先做谁得优先权的主张荒谬且不科学。他反问：若 Buzzard 的目标不止 FLT，可以继续做原计划的事并获得相应认可；若目标就是证 FLT，那他「输了」，就不该得到这份署名。他还进行语义澄清：科学语境的 scoop 通常指独立先做出结果，而非「别人告诉了你怎么得到结果、你却当成自己的」——以此看，在 Buzzard 讲座思路基础上跑 AI 验证并抢注的做法性质如何，正是双方分歧所在。他的另一句感慨「很多未解难题之所以无解，是因为每个问题只有一个人在做，其他所有人默契地不去碰它」也道出了数学研究协作文化的现状。
• @jacobaustin132 另提出 AI 数学证明或致 Lean 社区分裂：最可扩展的路径可能是建一张巨大的定理陈述图，任何人都可以烧自己的 Claude/Codex token 去证明——反正 AI 不像人类那么在乎代码质量。
• 争论之外，@CsabaSzepesvari 从可靠性角度提出质疑：形式化证明依赖一条正确性链条——编译器要正确、Lean 内核要无 bug、Mathlib 及所用公理都要可靠，任何一环出问题都会动摇结论。他还提到默默引入公理可能是隐患，但相信相关检查应该已经做过，其更关注形式化数学是否忠实还原原证明这一问题。
• 9 月 9 日，@Afinetheorem 与 @JacquesThibs 就另一场 AI 求解数学难题风波继续交锋：JacquesThibs 认为对方从技术上完全可以公开证明细节，Sholto 的表态只是息事宁人、避免在缺乏硬证据的主张上走得太远；Afinetheorem 则回应称，一旦写出证明的工作方式就会被识破，且对方的 subproof 细节可能暴露证明路径。该讨论将「是否公开证明细节」延伸为新的争议焦点，但目前无定论。

尚未确认

• Afinetheorem 与 JacquesThibs 讨论中涉及的「对方证明」具体所指、其 subproof 是否真的会暴露证明路径，均停留在双方推断层面，帖子材料未给出验证结果。

为什么重要

• 这场讨论把传统学术抢发伦理延伸到 AI 实验室语境：若大模型可以大规模「并行做数学」，社区「一人守一题」的默契可能被打破，这正是对 Anthropic 与 OpenAI 态度差异之争的背景。
• 讨论澄清了「抢发」并非单一概念：进行中抢跑、完成后抢写、基于他人讲座思路的抢先验证，在社区规范中的评价各不相同，这对未来 AI 参与数学研究时的行为边界有直接参考意义。
• 后续关于「公开证明细节是否等于暴露证明路径」的新争论提示：AI 数学成果的透明度与竞争策略之间存在张力，或成为下一阶段争议的常态。
• Csaba Szepesvári 对 Lean 工具链正确性链条与形式化忠实性的质疑则提示：即使形式化完成，「证明可信」仍依赖软件基础设施的可靠性，这是 AI 数学证明获得学界认可的另一道门槛。

2026-09-07 ~ 2026-09-09 · 26 条相关

• 数学圈不抢研究的潜规则,引出 Anthropic 与 OpenAI 的数学态度之争 — alz_zyd_ · 2026-09-07
• 「难题无解是因为每人只守一题?」数学研究文化再引感慨 — alz_zyd_ · 2026-09-07
• nihilunbounded:重大难题无人抢发,难题无解或因各守一题 — nihilunbounded · 2026-09-07
• littmath 区分两种抢发:工作完成后的抢写与进行中的抢跑 — littmath · 2026-09-07
• 反方坚持:讲座思路未必成真,拿 AI 抢验实属不当 — nihilunbounded · 2026-09-07
• "scoop"之争:先独立得到结果,还是照人思路据为己有 — alz_zyd_ · 2026-09-07
• littmath:宣布研究前应确认无误,抢发争论继续发酵 — littmath · 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
• Anthropic 用 Lean 证明结果撞车数学家 Buzzard,遭批「毫无荣誉感」 — teortaxesTex · 2026-09-07
• Csaba Szepesvári 质疑 Lean 形式化证明:编译器与内核是否可信 — CsabaSzepesvari · 2026-09-07
• Szepesvári 自我修正:sorry-free 的 Lean 证明即可信,公理可打印核验 — CsabaSzepesvari · 2026-09-07
• 强化学习学者 Csaba 认错：Lean 内核 bug 真实存在但不影响 FLT 形式化结论 — CsabaSzepesvari · 2026-09-07
• 强化学习学者 Csaba Szepesvári 质疑 AI 数学证明的形式化忠实性 — CsabaSzepesvari · 2026-09-07
• Csaba Szepesvari 质疑 AI 形式化证明的忠实性验证问题 — CsabaSzepesvari · 2026-09-07
• AI 求解数学难题风波再起：公开细节会暴露证明路径？ — Afinetheorem · 2026-09-09

另有 1 条近重复转述:CsabaSzepesvari