Claude's FLT Formalization Sparks Attribution Feud Over Whether Anthropic Should Have Collaborated with Buzzard

After Claude completed a formal proof of Fermat's Last Theorem (FLT) in Lean, it sparked an ongoing dispute over attribution and collaboration norms in the math community, with critics saying it "scooped" work that mathematician Kevin Buzzard had long cultivated. The situation is now calming down: according to jacobaustin132, the team communicated with Buzzard on Lean Zulip this week, and Buzzard's main request was simply to compile an errata list and let this proof leave behind learnable lessons—work that is already partially done; the team is also considering contributing to Tau Ceti going forward. The debate matters because it reflects the fundamental tensions that AI impact places on academic attribution norms, research priority, and community collaboration.

Confirmed

• jacobaustin132 revealed that Claude followed Wiles's original proof path rather than the simplified version Buzzard had been advancing, making it harder; future options include contributing to Tau Ceti.
• jacobaustin132 said they had been communicating with Buzzard on Lean Zulip all week, and Buzzard's main request was to compile an errata list, which is now partially complete.

Points of Contention

• littmath argued that if the math community were in Anthropic's position, most people would have proactively offered to collaborate with Buzzard; he noted that this time AI proved FLT without naturally spawning collaboration the way a normal human project would, which could have been handled better. That said, he has no strong opinion on exactly what Anthropic should have done and was merely commenting on math community norms.
• nihilunbounded believes Buzzard's real frustration is that his goal was far bigger than "prove FLT in Lean"—having someone directly knock out the most obvious subgoal is like destroying a North Star–style long-term objective, rendering the whole research area "uninhabitable"; they also insist that even after attending Buzzard's talks, one shouldn't use AI to verify the strategies therein and rush to stake a claim on the results, because nobody knows whether the ideas would ultimately hold up, and in their field when similar things happen people usually raise concerns privately rather than scooping.
• alzzyd countered: proving FLT in Lean is a fairly obvious goal, and Buzzard's long-term investment shouldn't create a de facto monopoly; if Buzzard's goals extend beyond FLT, he can continue doing what he originally intended and receive the corresponding credit; if his goal was just FLT, then he "lost" and shouldn't get the credit. They also clarified that "scoop" in scientific contexts usually means someone else independently produces the result first, not "someone basically told you how to do it and you took it as your own"—by that standard, view Anthropic's actions accordingly.

Why It Matters

• jacobaustin132 raised a more forward-looking concern: AI mathematical proofs could split the Lean community into "human-readable proofs" and "AI does everything" factions; the most scalable path may be building a giant graph of theorem statements that anyone can burn their own Claude/Codex tokens to prove—after all, AI doesn't care about code quality the way humans do.

2026-09-07 ~ 2026-09-07 · 13 related posts

• Counterpoint: you don't know the talk's outline is sound, so don't race to plug it — nihilunbounded · 2026-09-07
• Defining "scoop": independent priority vs. building on someone's outlined strategy — alz_zyd_ · 2026-09-07
• Debate continues: long prior work confers no dibs on an obvious research goal — alz_zyd_ · 2026-09-07
• Core of the dispute: Buzzard's goal went beyond formalizing FLT in Lean — nihilunbounded · 2026-09-07
• If Buzzard's goal was broader, he can keep working and get due credit, argues critic — alz_zyd_ · 2026-09-07
• FLT credit fight: if the goal was just proving it in Lean, Buzzard lost and gets no credit — nihilunbounded · 2026-09-07
• [source] Mathematicians weigh in on Claude's FLT proof: most would have collaborated with Buzzard — littmath · 2026-09-07
• Mathematicians debate: Anthropic should have offered Buzzard collaboration over FLT-in-Lean — alz_zyd_ · 2026-09-07
• littmath: Claude's FLT proof bypassed the natural collaboration a human project would have had — littmath · 2026-09-07
• [source] Claude's FLT proof followed Wiles' original path, not Buzzard's simplified version — jacobaustin132 · 2026-09-07
• Terence Tao's team talks with Kevin Buzzard over Lean formalization — jacobaustin132 · 2026-09-07
• [source] Buzzard responds kindly to Claude's FLT proof, asking mainly for an errata list — jacobaustin132 · 2026-09-07
• Predicting a Lean community schism: human-readable proofs vs AI-generated slop — jacobaustin132 · 2026-09-07