Remember the last time someone forwarded you a 700-page file and asked you to “just have a quick look.”
Now multiply that feeling by a few thousand mathematicians, and you have roughly what Tuesday evening, October 6, looked like.
At 6 PM Eastern, according to Scientific American, OpenAI put a repository on GitHub. No keynote. A blog post and a folder holding 722 mathematics manuscripts, grouped into 372 families of results and produced by an internal model that OpenAI hasn’t released to anyone outside the company. It landed about a month after OpenAI said another internal model had solved the Navier-Stokes problem, which I went through in my article “10,000 AI Agents Just Solved a Math Problem Humanity Couldn’t Crack for 90 Years.” That one came with a Lean proof too, and with a caveat about Lean that matters even more this time.
First, a correction to the headline number. 722 is not 722 solved problems. A family bundles a major result with variants and consequences, and the major results themselves run from full answers to partial progress to counterexamples that show a long-trusted idea is false. OpenAI stated that it presented around 4,000 problems to the model, with the average outcome requiring the equivalent of three hours of ChatGPT Pro processing time. Three hours for questions some people have chased for decades. I haven’t found a number for what the problems that didn’t pan out cost, and I’d like one.
What OpenAI Released: Results a Child Can Read the Question For
Behind the unreadable titles, a lot of these are questions you can explain at a kitchen table. Take an infinite sheet of paper and colour every point so that no two points exactly one centimetre apart share a colour. How many colours do you need at a minimum?
Seven works: tile the sheet with hexagons like a honeycomb. In 2018, Aubrey de Grey, better known for aging research than for mathematics, showed that four isn’t enough and pushed the floor to five. So the answer was five, six, or seven. OpenAI’s paper says five fails too, which leaves six or seven, and its catalogue marks the proof as checked in Lean. One paper, and the list of candidate answers shrinks by a third.
Pi gets a similar treatment. It has been irrational for over two centuries, but some fractions sit suspiciously close to it. 22/7, already used by Archimedes, is good to two decimals, and 355/113, found in China over 1,500 years ago, is good to six. So mathematicians asked whether pi hides miraculous fractions far out in the numbers, and they measure that with the irrationality exponent. The best bound before this, from 2019, was about 7.1, and almost every number has an exponent of 2. OpenAI’s records state that pi’s exponent equals 2 exactly, suggesting that pi resembles the crowd. No fraction hiding at infinity, no shortcut. It’s not a digits record either; nobody computed more decimals. It’s a statement about what pi is.
Then Riemann, the one with the million-dollar prize. In 1859, Bernhard Riemann tied the distribution of the prime numbers to the zeros of a function and noticed they all seemed to line up on one line, the real part of one half. It’s still unproven, 167 years later. OpenAI hasn’t proven it. The claim is smaller: no zero anywhere with an actual part above 7/8 for the zeta function or any Dirichlet L-function. Mathematicians are already calling it the quasi-Riemann hypothesis. Until now, the known zero-free region got thinner the higher you climbed, and this is a flat wall.
Alex Kontorovich of Rutgers wrote on X that “If a human did this, it would be an instant Fields Medal, no questions asked.”
The list goes on. A paper claims that matrix multiplication, the arithmetic your favourite chatbot’s chips spend most of their time on, needs roughly n to the power 9/4 operations over the complex numbers, against a previous record of 2.37. Another claims Catalan’s constant is irrational. It is also claimed that Hilbert’s tenth problem, the hope for a procedure to decide if any equation possesses whole-number solutions, yields a negative result for fractions, similar to Matiyasevich’s proof for whole numbers in 1970. If that holds, it’s a machine proving that no machine will ever settle everything. I’ll enjoy that irony for exactly as long as the specialists take to read it. The matrix result is theoretical for now, so your chatbot will not run twice as fast tomorrow.
One more, because the surrounding story is the best in the pile. In the late 1970s, Freeman Dyson, Elliott Lieb, and Barry Simon went after a question that sounds silly: why does a magnet stay magnetic? Barry Simon’s own list of fifteen problems in mathematical physics says they announced a solution and made an error. The story I know has a colleague, Jürg Fröhlich, preparing a course on their work and spotting the mistake after the corrected proofs were already sealed in an envelope in the outgoing mail. They went and got the envelope back. Over forty years later, OpenAI’s catalogue lists a paper claiming that, in three or more dimensions, the quantum Heisenberg ferromagnet becomes spontaneously magnetized at every sufficiently low temperature.
How much is verified? Lean Proofs and a Sign Error
Here is the part I keep coming back to. On October 7, less than 24 hours after the release, OpenAI withdrew three manuscripts. A sign mistake invalidated a proof regarding Weil classes and, consequently, the two papers based on it, including one on the rational Hodge conjecture for products of K3 surfaces. Fourteen other manuscripts got repairs. Cornell’s Alex Townsend told Retraction Watch he suspects more errors will turn up. A sign error is something a schoolkid does in algebra. It’s also how real mathematics fails, as the envelope story above shows.
So the question checks the rest. Lean is a proof assistant that verifies every logical step, with no tiredness and no fooling it. According to AI Weekly’s reading of OpenAI’s change log, six new Lean formalizations on October 7 brought the formalized share to roughly 42 percent, 300 of the 719 papers still standing. That’s a lot of certainty, and it’s not all of it. As I explained in the Navier-Stokes piece, Lean guarantees you answered the question as it was written in Lean, not that it was the right question. If the translation is slightly off, Lean will happily certify a perfect answer to a slightly distinct problem, and a human has to catch that.
The rest has no machine check. Kevin Buzzard of Imperial College, one of Lean’s most prominent champions, told The Verge that in his corner, algebraic number theory, only around six results immediately stood out and few if any were formally verified, so “I either have to read possibly-not-correct slop, or wait for others to do the same, or wait for someone to formalise them before I can say for sure that the results are even correct.” Andrew Sutherland of MIT says to treat claims about the model’s one-shot successes as unverified until the model is released, and adds, “We should ask for receipts.” OpenAI told Scientific American it’s working to release the model. You can check the proof. You can’t check the machine.
Terence Tao, Math 2.0 and the Mathematicians Who Say Stop
Terence Tao, who won the Fields Medal at 31 and is often called the greatest living mathematician, wrote a reflection the same day. It wasn’t an alarm against AI. In his telling, here is what happens when a big proof lands: seminars, meetings, junior researchers picking it up, ideas moving into courses and then into textbooks. A proof is the start of a collective life. He worries that hundreds of results arrive with nobody to explain them. In his post, he says the field is leaving what he calls Math 1.0:
“‘Math 1.0’ placed a premium on being the first to solve an open problem, even if the solution was not initially well understood.”
His Math 2.0 values exposition, community building, and opening new directions over raw problem-solving, and he thinks AI can help with those too.
Others are blunter. The Association for Human Mathematics put out a statement the next day, and Retraction Watch quotes it:
“Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. We urge mathematicians to discontinue their work with OpenAI and to return to a vision of science that centers human understanding.”
On the other hand, is Daniel Litt of Toronto, who told Scientific American he sees no reason a company should keep these answers secret from mathematicians. And in between sits the Advisory Group on Mathematics and AI, nine unpaid mathematicians hosted at the Institute for Advanced Study, including Timothy Gowers, Martin Hairer, and Edward Witten, set up in September to advise OpenAI on exactly this kind of release. Their recommendations criticize the use of proprietary internal models, and OpenAI says it takes the guidance seriously but isn’t bound by it. The group gives advice and has no decision-making power at any AI company.
The community is already building plumbing. The same day, Ben Antieau announced Hexagon, a nonprofit archive for AI-generated proofs that arXiv declined to host, and Tao reposted the announcement on his blog.
Here’s where I land. OpenAI made answers cheap and sent mathematicians the bill for checking them, and a sign error inside 24 hours is what that bill looks like. But I don’t think the bleakest reading is right either. For centuries the rarest thing in mathematics was the answer. It’s becoming less rare, not free and not always correct, and what gets valuable instead is choosing which questions deserve an answer, checking, understanding, explaining. Lozano-Robledo of UConn told The Verge, “Research will go on.” Every one of those papers, even a machine-checked one, is still waiting for a human to understand it and do something with it. And it holds well outside mathematics. In your job and in mine, machines will propose more and more answers, and the people who know what to ask and can tell whether the output holds will stay ahead.
If the part about who checks the machines stuck with you, my piece on the Navier-Stokes fight over pace goes into why some people wanted the whole industry to slow down, and what it had to do with a Trump-Xi summit.
If a sign error inside 24 hours made you wince the way it made me, follow us and subscribe for more breakdowns of where AI is actually heading.