A firehose of AI-generated mathematics

On October 6, OpenAI published 722 mathematical manuscripts produced by an internal frontier model. On October 8, it retracted three of them because of a sign error.

Between those two dates, the math community had to decide what a 719-paper corpus means. The scale is hard to absorb. 719 manuscripts is more papers than most mathematics departments publish in a decade, and they attack open problems in algebraic geometry, complex geometry, statistical physics, and theoretical computer science. OpenAI framed the release as sharing progress: new results on open problems, Lean proof formalizations, and research details, all in the openai/math GitHub repo.

Here is the number that matters. 300 of the 719 main results, about 42%, now come with proofs checked by the Lean proof assistant. The other 419 papers are pure prose. No machine check. No peer review. Just a model's confident writeup.

That split, 42% machine-checked and 58% not, is where the story lives. Everything that happened after the release follows from it.

The sign error that sank three papers

The first update log in the openai/math repo explains what went wrong. All three retracted papers belong to family 032, the Hodge conjecture cluster. The root cause sits in the paper "Algebraicity of Weil classes on split abelian eightfolds," dated September 18, one of the earliest manuscripts in the repo.

Somewhere in a key argument, the sign of a geometric operation is written as +1. The paper's own convention says it should be -1. One sign flip turns a cancellation into a nonzero count. The argument leans on a classical theorem whose precondition requires that count to be exactly zero. Precondition broken, the construction above it loses its support.

Two companion papers borrowed that construction. One covers Kuga-Satake correspondences for K3 surfaces, the other the rational Hodge conjecture for products of K3 surfaces. Both were retracted with the source paper.

OpenAI's note on all three is consistent: the proofs are withdrawn, but the mathematical statements themselves are not declared false. Original manuscripts stay available through archive links. Family 032 was renamed from "Hodge and Kuga-Satake results for all projective K3 surfaces" to "rational Hodge conjecture for CM abelian varieties." The K3 claims are off the table. The core claim about CM abelian varieties survives in revised form, with updated citations.

Three weeks passed between that manuscript's date and its public release. It survived one or two days of public scrutiny.

Quick Take: The bottleneck is no longer generating mathematical arguments. It is verifying them fast enough to trust anything.

Where Lean was, and where it wasn't

Notice where the failures cluster: the non-formalized part of the corpus. The retracted papers and nearly all of the substantively revised ones sit outside the Lean-checked set.

The 14 revised manuscripts cover Lipschitz height and Ashkin-Teller models in statistical physics (4 papers), the Kähler minimal model program and abundance in complex geometry (6), symplectic geometry (2), Navier-Stokes universal computation (1), and a BSD paper with an outdated citation removed (1). The fixes range from patched proofs to narrowed claims to clarified dependencies.

The most instructive case is family 342, which claims a proof of Simon Donaldson's "tame pushout compatibility" conjecture. The main theorem survived, and it has a Lean formalization. But a stronger side claim was overstated. The revision narrows it to specific cases and adds a counterexample showing it fails in general.

Read that twice. Lean-verified main theorem, overstated side claim. Formalization checks the proof you wrote, not the statement you meant to prove. It is a floor under correctness, not a force field around it.

The update added 6 new Lean formalizations and 5 auxiliary results. The heavyweight: family 103, claiming that logspace computation fully derandomizes (L = RL = BPL), now has its main result machine-checked.

Key numbers:

• 722 manuscripts released October 6; 719 after retractions
• 3 retracted, 14 revised, 13 citation updates in the first errata
• 300 of 719 main results formalized in Lean (~42%)
• 419 papers with no machine-checked proof
• 48 hours between public release and first retraction

One clarification on the formalization rate. Earlier coverage cited "about 60%," but that used family-level counting: a family counts if any paper in it has formalization. OpenAI's 42% counts main results per manuscript. Different denominators, different story. The stricter number is the honest one.

The community pushes back

Fields Medalist Terence Tao reposted a statement from the Association for Human Mathematics urging mathematicians to stop working with OpenAI. The association's position: the lab pressed ahead with solving open problems against the group's stated recommendations, and the mass release changes the norms of credit, verification labor, and what counts as publishable.

When I saw Tao's repost, the replies were already split. One camp read it as protecting the field's social contract: open problems get attacked carefully, one at a time, with the community following every step. A 719-paper dump inverts that, and referees now face a backlog generated in a week. The other camp read it as rearguard action. The capability exists, the papers are public, and refusing to collaborate with one lab does not unbake the bread. Build verification tooling instead of boycotts.

The loudest online arguments were about the retraction, not the ethics. The sign error became a Rorschach test. For skeptics, it proved AI proofs are worthless. For the other camp, it proved the release process works: the error was caught, documented, and the manuscripts preserved. I land closer to the second group, with a caveat. The process caught it fast because people actually read the papers, and because the ones they could check were checkable.

The open-source counterpunch

Days after the release, researchers posted improvements to some of the results, verified in Lean, on GitHub. The integer-mult-bounds repo takes bounds OpenAI's model produced and tightens them, with a machine check on every bound.

The sentiment on Reddit was blunt: the output people dismissed as slop proofs contained usable mathematics that could be improved the moment it was made precise. I spent part of an afternoon in that repo. It is small, concrete, readable. That is the point. Because the original claims were stated precisely enough to formalize, an outsider tightened them within days, between the release and the first errata.

That is the workflow the field should be building toward. AI proposes. Lean disposes. Humans aim.

Gold medals: Nemotron at IMO and IOI

Competition math is the other front. NVIDIA published results showing the Nemotron 3 family reaching gold-medal level at both IMO 2026 and IOI 2026 with an open recipe.

The IMO system scored 30/42, above the official gold threshold of 29. Full credit on four of the six problems means it produced complete, human-grade solutions on most of the exam, not partial credit scraped together. The proofs were graded by official IMO graders, and the system worked entirely in natural language: no formal prover, no external tools, no internet. It combined a strong MoE base with two specialists, one SFT-trained and one RL-trained, inside a generate-verify-refine loop.

The IOI system scored 535.4/600. The gold threshold was 361.12, and the top human scored 498.27. That run was live and prospective, under the same time and submission constraints as human contestants, but it was unofficial and unsupervised, so it does not appear in the official ranking.

Competition	System	Score	Bar to clear	Grading
IMO 2026	Nemotron 3 Ultra, SFT + RL checkpoints in generate-verify-refine	30/42	Gold at 29	Official IMO graders, natural language proofs
IOI 2026	Nemotron-3-Ultra-CC, SFT + GenCorrect	535.4/600	Gold at 361.12; top human 498.27	Live but unofficial, unsupervised

The details that matter for reproducibility: the IMO SFT corpus is 414,890 quality-filtered examples across 15,818 unique proof problems, roughly 26 examples per problem covering proof generation, refinement, verification, and meta-verification. The RL model trained on 9,597 problems selected near the model's capability frontier. For competitive programming, the team curated 22,000 problems and generated synthetic reasoning traces.

The base model is a 550B-parameter MoE with 55B active parameters. The sparse activation is what makes multi-round search feasible: each token touches only a tenth of the network, so running dozens of candidate proofs per problem stays affordable.

The IOI numbers show where the gains come from. The Nano model (30B total, 3B active) went from 130 points before post-training to 280 after SFT and 291 after RL. Small steps. GenCorrect, the iterative generate-evaluate-refine strategy, is what jumped it to 468 points, across the gold threshold of 438.3. The larger Ultra model hit 502 with the same test-time strategy.

The broader lesson: the medals did not come from fine-tuning alone, nor from brute-force sampling alone. They came from co-designing the model, the data, and the inference loop. NVIDIA released the checkpoints, training data, and a new 200-problem IMO benchmark on Hugging Face.

Competition math and research math are different games. IMO gold in natural language is impressive, but those proofs are short and well-scoped, with a known answer and a human grader. OpenAI's corpus shoots at problems where nobody knows the answer, the proofs run dozens of pages, and the graders are overworked referees. The verification burden is not comparable.

The quiet ML win: knot invariants

Not all machine learning for math is about generating proofs. A paper posted on arXiv this month uses reinforcement learning and Bayesian optimization to compute link invariants: the slice genus and the unknotting number of links, plus the strong slice genus for algebraically split links.

These invariants are not known to be algorithmically computable. No known algorithm is guaranteed to terminate with the correct answer, so search plus bounds is the only game in town. The authors use RL agents to find upper bounds through explicit constructions, and classical invariants for lower bounds. When the two meet, you get an exact value. The agents also reproduced the non-additivity of the unknotting number for several Brittenham-Hermiller counterexamples, and in some cases found entirely new unknotting trajectories.

This is a different standard of correctness, and a healthy one. The paper does not claim the agents proved theorems. It claims they found constructions and bounds, checked against known invariants. If you need exact values and no algorithm is known, search plus bounds beats a confident language model every time.

What trips people up

• Treating "not retracted" as "verified." Only 42% of OpenAI's main results are Lean-checked. The other 419 papers are claims. The first batch of errors surfaced within 48 hours. Assume the second batch exists.

• Assuming Lean coverage means full correctness. The Donaldson case had a verified main theorem and an overstated side claim that had to be narrowed with a counterexample. Formalization covers exactly what is formalized. Ask what the check actually covers before citing it.

• Ignoring sign and orientation conventions in generated algebra. The retraction was a single sign flip in a geometric operation. When you audit AI-generated mathematics, check intersection numbers, character sums, and orientation-dependent constructions first. That is where these models bleed.

• Reading competition scores without the fine print. IMO 30/42 was graded by official graders, which is strong evidence. IOI 535.4 was an unofficial, unsupervised run, so it tells you capability, not contest standing. The same number means different things depending on the supervision.

• Using only one bound when computing invariants. The knot paper gets exact values only by pairing RL upper bounds with lower bounds from classical invariants. An upper bound alone is a conjecture. A lower bound alone is a guess. You need both sides before you can write "equals."

One thing to remember: the formalization rate is the news, not the paper count. A lab machine-checked 300 research manuscripts, and the first failures appeared exactly where the machine was not looking. Verification is the product. Generation is the raw material.

The Bottom Line

If you are a working mathematician, start with the 300 Lean-checked manuscripts and treat the other 419 as searchable leads, not citable proofs. The retractions show what happens when you build on unchecked claims.

If you are building a reasoning system, put a verifier in the inference loop, not just in the release pipeline. The integer-mult-bounds result shows what happens when claims are precise enough to check: outsiders improve them in days.

One thing to watch: formalization rate is becoming the headline metric for mathematical AI. Within six months, expect verifier-integrated training and formalization-first benchmarks to be standard, and expect the 42% figure to look embarrassing to any lab that ships without it.