Math: OpenAI's AI has solved 372 problems, and nobody understands its proofs

Tuesday, October 6, six in the evening in New York. OpenAI deposits a folder containing 719 mathematics papers on GitHub, the huge repository where developers share their code. Not high school exercises: 372 results on problems that researchers had been unable to solve for years, sometimes decades. All written by an in-house AI that OpenAI has not even named yet. The next day, Scott Aaronson, one of the best-known computer scientists in the United States, writes on his blog that this is “surely one of the greatest days in the history of mathematics”. Just that!

And the worst part is that he adds that almost no human has understood these proofs yet.

Delivery of 719 papers. Sign here, and good luck with the proofreading

The conjecture of a lifetime, settled in one night

A conjecture is a statement that everyone believes to be true, but that nobody has managed to prove. As long as there is no proof, it remains a bet, even if the entire profession is betting the same way.

In OpenAI's batch, there is a proof of the “unique games conjecture”, put forward in 2002 by researcher Subhash Khot. Basically, it says that for an entire family of problems, even finding a roughly correct answer is as hard as finding the perfect answer. It sounds abstract, but it has been one of the big questions in theoretical computer science for twenty-four years. And Aaronson's wife, Dana Moshkovitz, also a researcher, has worked on it throughout her career.

Her reaction, as reported by her husband: the proof is “so horribly written that it is impossible to read without the help of an AI”, and it gives the impression of having been written “by someone on psychedelics”. Imagine spending twenty years of your life on a question, thinking about it in the shower, on vacation, during family meals, and getting the answer on a Tuesday evening, in a jumble, in gibberish that you have to get another machine to translate so you can understand what was taken from you. Ouch.

How do you verify a proof that nobody knows how to read?

Some of the proofs come with a verification written in Lean, software that rereads a mathematical argument step by step and refuses to move forward if there is the slightest gap. A bit like a spellchecker, but for logic: it does not understand the idea, it just checks that each step of the staircase is properly resting on the previous one.

But according to the specialist site Implicator, as of October 7, only 300 manuscripts out of 719 had their Lean verification. Barely more than four out of ten. And there is a trap that mathematicians immediately pointed out: Lean verifies that the proof is correct for the statement as it was typed into the machine. If someone copied the statement incorrectly, the proof can be perfect and answer a different question from the one we were asking. In short, a “verified” stamp on a paper that nobody has read.

Verified. Understood, that's another matter

And it didn't take long: as early as October 7, OpenAI withdrew three manuscripts because of a sign error, a plus that should have been a minus, and corrected fourteen others. That's exactly the kind of thing a proper review catches, and it's reassuring to see that someone is checking the work. As someone who reviews code written by Claude Code every day, I know that feeling very well: something that works, and you still don't know why.

372 problems solved, but out of how many?

The figure of 372 is impressive, but it needs to be put in perspective. According to Aaronson, the AI was run on around 8,000 problems, with roughly three hours of computation each, and it solved around 5%. Ninety-five percent failures, then. That's still huge, because those 5% are problems that humans had not solved, but this isn't a machine that solves everything you give it. And none of these results solves the biggest questions in the field. Researcher Lance Fortnow is the one who points that out. He, of all people, found a question in the list that he had asked in his own thesis, in 1989. Thirty-seven years of waiting!

Andrew Sutherland, a mathematician at MIT, puts it bluntly: as long as OpenAI doesn't publish its model and nobody can repeat the experiment, these announcements have to be treated as unverified. And he's right about one specific point: OpenAI has published neither its instructions nor its model, even though a group of mathematicians advising it had asked for them at the end of September. In the meantime, an association of mathematicians is flat-out calling for a boycott of OpenAI, talking about a “demonstration of force”.

Aaronson, for his part, found the comparison that really hurts: mathematicians are like a hunter-gatherer who has spent his life learning to survive in a hostile forest, and who one morning sees a huge luxury hotel spring up right next to his hut, complete with helipad and heated pools.

Thirty years learning to make fire with two sticks. And the hotel across the way has underfloor heating

And what use is it to you?

Tomorrow morning? No use at all. But look at one of the results on the list: a faster way to multiply two large arrays of numbers together, what mathematicians call matrices. It's the operation your PC's graphics card repeats billions of times per second to run a game, a photo filter or an AI. So the AI found a way to do its own calculation faster. It's tinkering with its own engine!

On the other hand, let's calm down. Since the 1990s, records of this kind have almost all remained on paper: they only become faster for arrays so gigantic that no computer in the world will ever manipulate them. Nothing says this one will be an exception. It could take ten years, twenty years, or never make it out of the journals.

The real change for you is elsewhere, and it's slower: math is the foundation on which everything else is built, from weather forecasts to calculating the strength of a bridge, including the little padlock in your browser that protects your bank card. If a machine moves this foundation forward faster than generations of researchers, everything built on top of it will eventually benefit. But not this year.

We've actually already been through this. In 1976, two researchers demonstrated with the help of a computer that four colors are enough to color any map without two neighboring countries having the same color. More than a thousand hours of computation, impossible to check by hand. Mathematicians grumbled for years, some refused to call it a proof. In 2005, it was entirely rechecked by software of the same kind as Lean, and nobody disputes it anymore today.

1976: four colors, a thousand hours of computation, and twenty years of bad temper

Four days ago, I was wondering whether Meta's AI had really solved five unprecedented problems. Five! The next day, OpenAI announced 372.

My opinion

I find it fascinating, and at the same time I perfectly understand the mathematicians' anger. Fascinating because questions that had resisted for twenty years have just fallen, and we are going to learn things by taking them apart. But dumping 719 articles all at once, unreadable, without the model or the instructions, and leaving researchers all over the world to sort through them, that's not how you do science. You put the boxes in front of the door, and you walk away!

So to the maths students wondering this morning whether they chose the right career: you chose it! Someone is going to have to read all this, and the machine isn't going to do it!

Sources

• OpenAI, 6 October 2026: announcement of the publication of the mathematical results
• OpenAI on GitHub: the folder of the 719 manuscripts
• Scott Aaronson, 7 October 2026: "The Mathocalypse" (8,000 problems, 5%, reaction from Dana Moshkovitz)
• Lance Fortnow, 7 October 2026: "Open No More"
• Implicator: Lean verification, withdrawn manuscripts, reaction from Andrew Sutherland
• The Decoder: mathematicians call for an OpenAI boycott

Article written with the help of Claude Code, proofread and corrected by me.