OpenAI's 722 maths papers are a sales pitch until it publishes the 4,000 attempts

In October 2025 Kevin Weil, an OpenAI vice-president, posted that GPT-5 had found solutions to 10 previously unsolved Erdős problems and made progress on 11 more. Thomas Bloom, who maintains the Erdős Problems website, called this a dramatic misrepresentation. The model had found existing papers that already contained the answers. Sébastien Bubeck deleted his post and said only solutions already in the literature had been found. Mark Sellke, the OpenAI researcher behind the claim, had described the answers as arriving “after thousands of queries with GPT-5.”

A year later OpenAI is back with a much bigger number. Reports on the README of its openai/math repository put the release at 722 manuscripts in 372 result families. The model was given about 4,000 problems, and the average result used roughly three hours of ChatGPT Pro thinking. 162 of the 722 papers come with a Lean formalisation of their main result. I expected the Lean files to settle my doubts, and for those 162 they mostly do. I was surprised by how little the release tells us about what went wrong last time, which was the process rather than the proofs.

OpenAI calls this progress. In my view that is a claim about a process, and it turns on how much the model did unaided, how much humans steered it, and how many attempts were discarded before the winners were picked. On the first two, the disclosure is 10 abridged summaries of the model’s reasoning, chosen and trimmed by the company that benefits from them. On the third, it gives problem counts and compute estimates. Set 372 result families against about 4,000 problems and you get a hit rate that may be impressive or may be ordinary. Nobody outside OpenAI can tell, because nobody outside can see what the problems were, how hard they were or what the failures looked like.

There is a reason to care. The database run by Paata Ivanisvili and Mehmet Mars Seven, which tracks AI attempts at Erdős problems, puts the real success rate at one to two per cent, mostly on the easier ones. Terence Tao has pointed out that failures rarely get published while wins go viral. He then built a tracker that sorts AI-assisted solutions by how much human help was used, what prior literature existed and whether the proof was formalised in Lean. By his account, misleading claims from tech companies dropped noticeably afterwards, which suggests that making labs show their working changed how they behaved.

The best defence of OpenAI goes like this. The Decoder reports that most results came from a single prompt to a single agent, and that formal verification exists to make review practical. A Lean-checked proof is correct whether a human nudged it many times or never. I accept that for the 162. It does not cover the papers without a Lean proof, which include the claimed isomorphism of the free group factors, and the README itself reportedly concedes that some results without Lean proofs could have issues. Lean also checks that a proof establishes the formal statement someone wrote down. It does not check that the formal statement matches the headline in the paper, or that the result was not already in a journal. That second failure is exactly what happened with Erdős in 2025. And the single-prompt claim is precisely the kind that logs could confirm. If it is true, publishing the transcripts would cost OpenAI very little and would answer the critics directly.

Timothy Gowers, a member of the Institute for Advanced Study’s advisory group, says results should be posted as quickly as possible once minimum standards are met. I agree, and logs do not slow anything down. They already sit on OpenAI’s servers. The advisory group published its guidelines on 29 September 2026 after more than 600 survey responses, and it says itself that it has no decision-making power at any AI company. Its advice only has force if mathematicians refuse to review results that don’t meet it. Their time is limited, and 25 Fields Medal winners have warned that mass-producing results could ruin the ground mathematics grows in. OpenAI is now funding workshops to help people understand these results, which means mathematicians’ time going into reviewing output whose cost of production they cannot see.

Anyone invited to one of those workshops has a cheap lever. Open the formalisation catalogue in openai/math and search for the free group factors. If there is still no Lean file, ask for the complete, unabridged transcript of that single result, prompts and dead ends included, as the price of turning up. If OpenAI cannot hand over one transcript for its biggest claim, I would not count the rest of the 722 papers as progress either.

Prompted by Sharing AI progress in mathematics, openai.com.