An OpenAI model claims to have solved ten mathematical problems left unsolved for decades

OpenAI has announced that an internal version of its next-generation model, called Astra, has produced proofs for ten open problems in mathematics and theoretical computer science. The proofs were published in Lean format, a language that allows automatic verification of logical steps, and are available on GitHub.

Among the results indicated by the company are a construction that would demonstrate the existence of non-sofic groups, an object of study in group theory, and new bounds on the sphere packing problem, a geometric question that has occupied mathematicians for centuries. According to OpenAI, the entire computational process needed to reach these results would have cost around two thousand dollars.

The most discussed figure is not so much the economic cost as the ratio between cost and result: if confirmed, problems that required decades of human work would have been tackled with a relatively modest computational expense. It is precisely this gap that makes the announcement significant, but also demands caution.

Mathematician Timothy Gowers, a Fields Medal winner, commented on one of the proofs produced by the model, saying he would consider it publishable “without hesitation” in a top-tier journal. This is an authoritative but isolated judgment, referring to only one of the ten proofs, and does not amount to a full peer review of the entire set of results.

Astra, the model that reportedly produced these results, has not yet been made available to the public. The published proofs therefore remain at the stage where the mathematical community can freely examine them, but independent and systematic verification — the kind that would establish whether the ten problems are truly solved according to the discipline’s standards — has not yet been completed.

A limitation of this story should be noted: at the moment it stems from a single source, a statement by OpenAI itself picked up by a trade publication; there is as yet no independent confirmation of the scope of the results nor any published peer review. The availability of the code and proofs on an open platform theoretically allows for external scrutiny, but verifying a formal proof in an advanced research field requires time, specific expertise and, typically, publication in specialized journals.

The episode fits into a broader debate on the role of language models in mathematical research, a field in which formalization through languages like Lean is gaining ground precisely because it allows a plausible claim to be distinguished from a proof verifiable step by step. For now, the ten problems remain open in the fullest sense of the term: the proofs exist, they are public, but the scientific community has not yet validated them definitively.