If OpenAI's new publication survives scrutiny from the mathematical community, it may turn out to be one of the most interesting AI events of the year. Not because of another benchmark, but because of a possible shift in the research process itself.
On 1 August 2026 OpenAI made an unusual claim: an internal version of Astra, its next large model, produced new results on ten open problems in mathematics and theoretical computer science.
According to the company, these are problems where no significant progress on the main result had been recorded for at least a decade, and in several cases far longer. The areas include high-dimensional geometry, coding theory, group theory, operator algebras, quantum complexity, lattice-based cryptography and extremal combinatorics.
What OpenAI claims happened
The important part is not only the list of results but the way the work was done. OpenAI says the model found the key ideas behind the proofs. People then prepared paper drafts with the help of the same model, and finally the model formalised the proofs in Lean.
Lean is a proof assistant. Instead of mathematical prose that humans read and interpret, the proof is written so that a machine can formally verify it.
That does not mean the scientific community should accept every claim automatically. It does change how seriously the publication has to be taken: there is a paper, an open repository, and certificates anyone can check.
Among the published results
- New bounds on sphere packing density in high dimensions.
- Improved bounds for binary and spherical codes.
- Construction of a non-sofic group.
- A counterexample to the Connes rigidity conjecture.
- New bounds in arithmetic circuit complexity.
- A quantum parallel repetition theorem for two-player games.
- A hardness-of-approximation result for the closest vector problem in lattices.
- A result on the Ehrhart volume conjecture.
- A superexponential lower bound for multicolour Ramsey numbers.
- Extremal combinatorics results around compactness and degeneracy conjectures.
Why this matters outside mathematics
For years the conversation about AI centred on models that summarise, write, translate or help with code. The claim here is different: a model proposing a new mathematical argument for an open problem.
The line between a system that organises existing knowledge and a system that opens a new research direction is becoming less clear.
If the results hold, the research process may change. The human researcher does not disappear, but the role shifts: less manual enumeration of cases, more choosing questions, testing directions, interpreting, criticising and deciding what actually matters.
Where caution is needed
The publication comes from OpenAI itself, and the community still has to check the correctness, novelty and significance of each result in depth.
Lean certificates help with formal verification, but scientific trust is not only a technical question. It includes understanding the context, the contribution, the relation to earlier work, and whether other researchers can build on the result.
So the precise wording is not "AI solved mathematics" but this: OpenAI published formal results for public verification, and if they hold, it is a turning point in how AI enters scientific research.
The bigger question
If AI starts producing formal proofs for open problems, what will research look like in three to five years?
Probably not a world where the computer replaces the scientist. More likely a world where the scientist works with a system that proposes directions, builds arguments and formally verifies large parts of the work, leaving judgement, responsibility and meaning to the human.
Sources: OpenAI, repository with Lean certificates.