AI can now produce maths faster than mathematicians can check it

722 papers in one GitHub push

On 6 October, OpenAI put a repository called openai/math on GitHub. It holds 722 mathematical manuscripts, grouped into 372 "families" of related results, almost all written by a model the company has not released. Over the evaluation, the model was given about 4,000 problems. Each result used, on average, three hours of what OpenAI calls ChatGPT Pro thinking compute.

The subjects are not modest. One family is about the irrationality exponent of π. Others take on Kaplansky's direct-finiteness conjecture, the Mahler conjectures, spin glasses and the Riemann zeta function. People have worked on some of these for decades.

Now read the fourth paragraph of the repository's own README: "Some of the unformalized results could have issues."

That sentence is the real story.

The hard part used to be finding the proof

For most of history, the bottleneck in mathematics was producing a proof. Checking one could take experts months, sometimes years, but there was never much to check, because people could only produce so much.

That ratio has flipped. One lab has just released 722 papers in a single push. Each one needs a specialist in its own corner of mathematics to judge it, and there are only so many of those. The scarce resource is no longer the proof. It is the checking.

Here is where the 722 actually stand. The repository includes a catalogue of formal proofs written in Lean, a programming language whose software checks every logical step mechanically. It lists 162 papers whose main result has been formalised. The other 560 rest on the model's own write-up.

The catalogue is candid about itself. It describes its scope as "Partial progress", records that the formalisations were produced by an agent, and lists its review status as "unchecked". A Lean proof shows that the formal statement follows, step by checked step, from the definitions. Someone still has to confirm that the formal statement says what the paper's headline claims. That is a human job, and it has not been done yet.

A year from embarrassment to this

It moved fast, and it did not start well.

| When | What was claimed | What happened | |---|---|---| | Oct 2025 | OpenAI's then vice-president Kevin Weil posted that GPT-5 had found solutions to 10 previously unsolved Erdős problems | The solutions already existed in the published literature. The post was deleted. | | 20 May 2026 | An OpenAI model disproved a geometry conjecture Paul Erdős made in 1946, on how many pairs of points can sit exactly one unit apart | Mathematicians including Noga Alon, Melanie Wood and Thomas Bloom endorsed it in remarks published alongside | | Sep 2026 | OpenAI said about 10,000 AI agents, working for roughly 88 hours, showed that a fluid described by the 3D Navier–Stokes equations can blow up in finite time under an external force | A Lean proof was released. Mathematicians dispute whether it answers the question they care about. | | 6 Oct 2026 | 722 manuscripts across 372 families | 162 come with a machine-checked main result; the rest are unverified |

The May result is the one Quanta Magazine called "the first historically significant proof to come from an AI model." The model found a family of constructions that beats the square-grid patterns people had assumed were close to best for 80 years. Mathematicians reviewed it and published supporting remarks alongside the announcement, which is exactly what the October 2025 claim had skipped. It was not the last word, either: Quanta notes that human mathematicians improved on it substantially within weeks.

Noga Alon, one of the endorsers, told Quanta that once AI started solving the Erdős problems, "there is no point anymore" in pursuing them himself. That is a strange thing for a mathematician of his standing to say, and it is the most honest description of the mood I have read.

Notice that "solved" is doing three different jobs in these headlines. A lab claiming something, a machine confirming the logic, and mathematicians agreeing it matters are separate events. Only one of the four has clearly reached the third column, and even for that one, a machine check is not reported.

Navier–Stokes: solved, depending on which problem you meant

The Navier–Stokes problem is one of the seven Millennium Prize Problems the Clay Mathematics Institute set in 2000, each worth $1 million. It asks whether the equations that describe how fluids move always behave, or whether a smooth flow can suddenly develop a point where the velocity becomes infinite.

OpenAI says its system showed that such a blow-up can happen when the fluid is pushed by a smooth external force, and it released a Lean proof. The outlets disagree on how settled that is. Scientific American says it "unambiguously" solves the problem as the Clay Institute originally wrote it, which allows a forced version as one acceptable answer. IEEE Spectrum still describes the claim as awaiting verification. Either way, most researchers had been chasing a blow-up that comes from the fluid's own motion, with no outside push.

Luis Silvestre of the University of Chicago put the split precisely to Scientific American: "The most important problem is unsolved. The Clay problem is settled, but the main problem for the Navier-Stokes equations is not."

Not everyone thinks the force is a cheat. Diego Córdoba, quoted in the same article, pointed out that "all fluids we know of are under some kind of external force. So to have the force makes complete sense." OpenAI has said it does not intend to claim the prize.

The mathematicians' case against this, and where it lands

On 11 September, 25 Fields Medal winners, Terence Tao of UCLA among them, signed an open letter against AI labs racing to solve famous problems. Their complaint is not that the maths is fake. It is that results are "announced in a rush, leaving no time for a proper writeup", and that this raises "severe attribution and plagiarism questions".

Tao put the deeper worry well to The Brighter Side of News, talking about AI jumping straight to answers: "It's a little like going to watch a movie and jumping straight from the first ten minutes to the last ten minutes. Technically, all the plot lines are resolved, but most of the value of the experience was lost."

Peter Scholze of the University of Bonn, one of the 25, went further on a panel reported by IEEE Spectrum: "They're really just solving these difficult mathematical problems as benchmarks, as some kind of PR stunt." Geordie Williamson of the University of Sydney, on the same panel, named the underlying problem: "What we want as a mathematical community is understanding, but we measure this against unsolved problems, and the problem is that these two measurements are very, very quickly becoming uncorrelated."

The checking problem is not only the labs' doing. Thomas Bloom, who runs the database that tracks the Erdős problems and endorsed OpenAI's May result, told Quanta about a different flood: people who are not mathematicians posting 100- to 200-page papers that an AI wrote and checked. "But no human has read it, and no human is going to read it."

They are right about most of it. A proof nobody understands teaches nobody anything; mathematics has always been as much about the ideas a proof forces you to build as the yes-or-no answer at the end. Credit matters to people whose careers depend on it. And 560 unverified papers dropped on a field in one night are not a gift if nobody has the hours to read them.

Where I would push back is on "stunt". The May disproof found something humans had missed for 80 years, and mathematicians' supporting remarks were published alongside it. And formal checking, for all that its review is still marked unchecked, is the one form of checking that can grow as fast as the output does. The argument is really about who checks, how fast, and who gets the credit. Whether the machines can do the mathematics now looks settled.

Why this matters outside mathematics

Mathematics is the cleanest test case because, in principle, an answer can be checked to the last step. Most fields do not have that. Contracts, medical guidance, software and policy drafts are increasingly written with AI, and there is no Lean for a legal argument.

The same question will reach all of them. When producing a plausible answer costs almost nothing, the value moves to whoever can tell a right one from a wrong one, at the speed the answers arrive.

We do not know yet how many of the 722 will survive. By its own README, neither does OpenAI. And nobody has yet said who is going to read the other 560.

---

Idea Infotech builds AI systems for companies and governments, and puts as much engineering into checking what they produce as into producing it. Some of that work is here.