OpenAI Solves Ten Open Math Problems, Mentions It in Paragraph Three

There are many ways to announce that you have resolved ten open problems in mathematics, some of which had resisted every living expert since 1999. You could hold a press conference. You could ring a bell. You could, at minimum, put it in the headline.

OpenAI chose a different path. On August 1, the company published a blog post titled “Ten advances in mathematics and theoretical computer science” — a title with the emotional register of a syllabus — and waited until the third paragraph to mention, almost as an aside, that the work was done by “an internal version of Astra, our next major model.”

Paragraph three. The construction of the first non-sofic group, a question that has been open since Bill Clinton was president, was delivered with the narrative urgency of a parking validation.

The results themselves are, by all accounts, real. Not “real” in the AI-industry sense, where a demo works twice and the second time is the launch video, but real in the annoyingly checkable sense: OpenAI released a 249-page manuscript alongside machine-verifiable Lean 4 proof certificates on GitHub, with — and mathematicians confirmed this with the tone of people who had gone looking — zero sorry statements. In Lean, sorry is the keyword for “trust me.” There were none. The proofs do not ask for trust. They ask for a laptop.

The haul includes the non-sofic group construction, a disproof of Connes’s rigidity conjecture, and three problems from the Erdős catalog, which is the mathematical equivalent of clearing three tickets off a backlog that predates the company, the industry, and in one case the transistor era of several of the reviewers.

Total compute cost: roughly $2,000 at API rates. Two thousand dollars. Eighty years of accumulated human bafflement, resolved for less than the average AI conference badge.

The mathematical community responded with the traditional two-step. Step one: awe. Fields Medalist Timothy Gowers reportedly said he would recommend related work from the model family for publication in the Annals of Mathematics “without hesitation,” which for the Annals is roughly equivalent to a standing ovation with pyrotechnics. Thomas Bloom, curator of the Erdős problems archive, called the results “big news,” and then — step two — immediately clarified that this does not mean AI is replacing mathematicians, in the tone of a man who has answered that question eleven times before breakfast.

Harvard’s Melanie Matchett Wood supplied the necessary asterisk: “This result does not show us all the times AI has claimed to have a proof of something and been wrong.” Which is fair. The graveyard of confident machine proofs is large and well fertilized, and none of the ten results have been through peer review — a process that, unlike Astra, cannot be rushed for any amount of compute.

The timing invites its own conspiracy corkboard. Sam Altman reportedly demonstrated Astra to federal officials in Washington, and press reports suggest the model is expected to be the first to go through the government’s new pre-release review framework, established by executive order in June. That framework is — and officials are very insistent on this word — voluntary. Frontier labs may, if they feel like it, grant the government up to 30 days of early access before launch. Purely optional. In the way that showing your bag to the security guard on the way out of the store is optional.

So the sequencing, as best anyone can reconstruct it: build a model, quietly solve a decade of open mathematics with it, demo it in Washington, volunteer it for inspection, and announce the whole thing in a blog post formatted like homework. Somewhere in San Francisco, a comms professional fought hard for that third paragraph and considers it the restrained option.

The rest of us are left with the actual substance, which is genuinely something: proofs no human found, verified by machines, checkable by anyone, priced like a used couch. The machines did the math. The humans, as ever, are handling the messaging — and on current evidence, only one of those groups is operating at superhuman level.

Sources: