Mathematicians Accuse OpenAI's Astra Proofs of Plagiarism
Steven Miller says the sphere-packing proof copies the central argument of his 2016 paper; Fournier-Facio says it stitches 2016 and 2019 results.
Within days of OpenAI’s July 30 presentation of ten machine-verified mathematics results — including the celebrated sphere-packing proof and a non-sofic group construction — two mathematicians have publicly charged that the work reproduces prior published arguments without attribution.
Steven Miller (Yeshiva University) says the sphere-packing proof OpenAI showcased pastes in the central argument from his own 2016 paper without credit, describing the pattern as deliberate. Francesco Fournier-Facio (Cambridge) says the soficity “breakthrough” stitches together ideas from 2016 and 2019 papers.
Key facts
- The claim: OpenAI’s Astra-generated proofs reuse central arguments from earlier published mathematics without citation — characterized by two named mathematicians as improper credit or plagiarism.
- Who: Steven Miller (Yeshiva), sphere-packing; Francesco Fournier-Facio (Cambridge), soficity.
- Follows: the July 30 drop of 10 Astra proofs (previously covered on this site as an unqualified research breakthrough — this story is the credibility counterweight).
- The twist: the proofs are machine-verified in Lean 4 — the correctness check and the novelty/attribution check are different problems, and this dispute targets the second one.
- OpenAI’s response: at time of writing, no substantive public response to the specific attribution charges.
Why it matters
- Verification ≠ authorship. A legitimate proof can still be non-novel. If the accused arguments are genuinely prior work, the “breakthrough” framing misrepresents what Astra did — and the research-community damage is real.
- The economy of AI research credit is broken. Models are trained on the full public record of mathematics; attribution requirements for AI-generated proofs remain undefined, so disputes like this will multiply until norms are set.
- It cuts both ways for OpenAI’s positioning. Machine-verified proofs were the lab’s credibility play; a credible plagiarism charge around them is more damaging than a failed theorem.
What to watch
- OpenAI’s formal response — rebuttal, correction, or amended citation list changes the story materially.
- Journals’ handling: any formal misconduct review of AI-generated proofs with disputed novelty sets a precedent for the entire field.
- Whether other mathematicians file additional prior-art claims — ten proofs, one week, two challenges, more likely.
Official source
- Scientific American: OpenAI’s latest math breakthroughs commit research misconduct, experts say
- Our earlier coverage: OpenAI’s Astra Proves Ten Math Problems
Updated August 10, 2026.