OpenAI Named Its Next Model Family and Published Ten Solved Problems. It Has Not Shipped Anything.

OpenAI spent Saturday doing something it rarely does: naming an unfinished model. A mathematics report and an accompanying post put the name Astra on the company's next major family, and attached to it a list of ten previously open problems that an internal version is said to have solved.

What was actually claimed

The ten results span high-dimensional geometry, coding theory, group theory, quantum complexity, lattice cryptography and extremal combinatorics. OpenAI's framing is that each had seen no progress for at least a decade. Each proof was formalised in Lean, the proof assistant, and the company puts the compute bill at roughly $2,000 at the current API rates for Sol. Thomas Bloom, who maintains the Erdős problems database, called the results big news — a comment from a working mathematician, not an independent audit.

What Lean does and does not certify

This is the distinction most of the coverage is dropping. A Lean-checked proof is valid: the steps follow. Lean says nothing about whether the statement was hard, whether it was genuinely open, or whether the result matters. Those are judgements the mathematical community makes over months, and none of it has been peer-reviewed. The results are self-reported.

Two events, not one

Aggregators have fused a private demonstration in Washington on Friday, reported by The Information, with Saturday's public mathematics report. They are separate. The Friday event was a closed briefing; Saturday was the artefact.

The name is not final either

OpenAI describes Astra as a tentative designation. The company has not said whether the family arrives as GPT-6, as GPT-5.7, or as a distinct tier sitting alongside the existing Sol, Terra and Luna line. Nothing is available to developers, there is no pricing, and there is no release date.

What Astra is reportedly for

The design goal attached to the family in earlier reporting is a model built to work on a single problem for hours or days, rather than answering in seconds. That is consistent with what a ten-problem mathematics run implies: long horizons, sustained search, and a bill measured in thousands of dollars per result rather than fractions of a cent per query. It also explains why the release is being teased through research output. A model whose selling point is spending a day on one question cannot be demonstrated in a chat window, and the only legible proof of it is a result somebody else could not get.