OpenAI's Astra: Ten Claimed Math Breakthroughs, One Unreleased Model

On August 1, OpenAI put a name to a week of rumors: Astra, “our next major model,” which the company says produced new results on ten long-open problems in mathematics and theoretical computer science. The manuscripts and Lean formalizations are public and extensive. The model is not public, and independent confirmation does not exist yet.

For a day, Astra was a name in other people’s reporting. On July 31, The Information wrote that OpenAI had been quietly previewing a model family tentatively called Astra to an audience in Washington, D.C. On August 1, OpenAI made the name official in an unusual way: not with a product launch, but with a mathematics paper drop.

The announcement, “Ten advances in mathematics and theoretical computer science,” makes four statements that carry the whole story:

• The results were produced by “an internal version of Astra.”
• Astra is OpenAI’s “next major model.”
• Humans prepared the generated arguments into manuscripts, assisted by the same model.
• The model then formalized each argument in Lean, the proof assistant that machine-checks every deductive step.

At a glance

• Astra is officially an OpenAI model name, confirmed August 1. Its final branding could still change.
• Astra is not released. No model card, no API, no access date, no parameter count, no architecture, no context length, no training-data disclosure, no benchmarks, no safety card.
• The mathematical artifacts are real and public: a 249-page manuscript collection, a 62-page set of discovery notes, and a GitHub repository of Lean formalizations.
• None of the ten claims has been independently confirmed yet. The release was hours old at this writing; the repository showed one publication commit and no external review history.
• The multi-agent architecture and the Washington previews are secondary reporting, not OpenAI technical disclosures.
• The “$2,000” figure is a token-price equivalent, not what the project cost.

The ten claims

“Advances” covers several different things here. Some of the ten resolve conjectures, some disprove them, some improve bounds that had not moved in decades. The list is not padding, though: several of these, if they hold, are results mathematicians would have celebrated from any human author.

1. Sphere packing

How densely can you pack identical balls in 100 or a million dimensions? Nobody knows, and the question matters beyond geometry because dense packings are essentially good error-correcting codes. Since 2003 the best general ceilings have come from one tool, the Cohn–Elkies linear-programming bound. The manuscript determines exactly how strong that tool can ever be, and extracts from it a better general density ceiling. By the paper’s own account, the first improvement of that exponent since 1978.

Even the best packings leave gaps. In high dimensions, nobody knows how small the gaps can be made.

2. Error-correcting codes

A code is a set of messages chosen so that any two differ in many positions; that spacing is what lets you correct transmission errors. The tradeoff question is how many messages you can fit at a given spacing. The ceiling in use since 1977, the MRRW bound, has resisted every attack. The manuscript constructs new certificates that push that ceiling strictly lower at every spacing, and does the same for codes on the surface of a sphere.

3. An explicit non-sofic group

A group is sofic if its multiplication can be approximated, piece by finite piece, by shuffling finite decks of cards. Every group anyone had ever exhibited was sofic, and several major theorems are known to hold for sofic groups automatically, so the question of whether every group is sofic sat open for decades. The manuscript names a concrete group, the unit group of a binary Leavitt algebra, and proves it is not sofic. If it holds, an entire assumption class in group theory loses its “maybe everything works this way” status.

4. A counterexample to Connes’s rigidity conjecture

Take a group and build from it a von Neumann algebra, an analytic object that acts like the group’s shadow. Connes conjectured in the 1980s that for the most rigid class of groups the shadow remembers everything: same algebra, same group. The manuscript constructs infinitely many genuinely different groups of exactly that rigid kind casting one identical shadow, which would end the conjecture, and a weaker fallback version of it too.

5. Lower bounds for the permanent

The permanent of a matrix looks almost like the determinant, but where the determinant is easy to compute, the permanent counts things like perfect matchings and is believed to be intractable. Believed, not proven: unconditional lower bounds are famously hard to get. The manuscript proves new ones, superquadratic for division-free arithmetic circuits and roughly quartic for formulas. Still far from the field’s holy grail, the VP-versus-VNP question, but floors in these models move rarely, and slowly.

6. Quantum parallel repetition

Two players who share quantum entanglement face a referee’s test they can pass, say, 90 percent of the time. If the referee runs many independent rounds at once, does their chance of passing every round collapse exponentially? Intuitively obvious, notoriously hard to prove: entangled strategies can correlate rounds in strange ways. The classical version of this took years of work in the 1990s. The manuscript claims the general entangled version, open since then.

7. Hardness of the Closest Vector Problem

A lattice is an infinite regular grid of points in high-dimensional space; the Closest Vector Problem asks for the grid point nearest to an arbitrary target. Much of post-quantum cryptography is built on the assumption that this is hard. The manuscript proves that even approximating the answer within a small polynomial factor is NP-hard, under a deterministic reduction. To be clear about a headline that invites misreading: this is evidence that lattice problems are hard, not a technique for solving them. It does not weaken post-quantum cryptography. If anything, it shores up the foundations.

The Closest Vector Problem: given a point off the grid, find the nearest grid point. Post-quantum cryptography bets that this is hard in high dimensions.

8. Ehrhart’s volume conjecture

Draw a convex shape whose center of mass sits on a grid point, and arrange it so that point is the only grid point inside. How big can the shape be? Ehrhart conjectured the exact ceiling in 1964, and a particular simplex shows the ceiling is reachable. The manuscript proves the ceiling holds in every dimension. What it leaves open, and says so, is whether that simplex is the only shape that reaches it.

A convex shape whose center of mass, in teal, is the only grid point inside it. Ehrhart’s 1964 conjecture caps how big it can be.

9. Multicolor triangle Ramsey numbers

Color every edge of a network on N points with one of k colors. Ramsey theory says that once N is large enough, some triangle must come out entirely one color; the question is how fast that threshold grows with k. This is Erdős problem 183, and the specific mystery was whether the threshold’s k-th root stays bounded. The manuscript’s new lower bound, combined with the classical upper bound, settles the growth at k raised to a power on the order of k itself, so the k-th root grows without bound. The manuscript credits an existing combinatorial construction as its engine; the claimed novelty is the application, not the gadget.

Six points, every pair connected. Color the connections and, once the network is large enough, a single-color triangle becomes unavoidable.

10. Two extremal graph theory counterexamples

Extremal graph theory asks how many edges a network can have before some forbidden pattern becomes unavoidable. The manuscript answers two more Erdős catalogue problems with counterexamples: a finite family of patterns that is jointly far harder to avoid than any single member of it, something forbidden-pattern arithmetic was not expected to allow, and a sparse pattern (2-degenerate, meaning it can be peeled apart two connections at a time) that requires polynomially more edges to force than the natural conjecture predicted.

Ten fields, ten literatures, ten referee pools. The breadth is the most impressive thing about the release, and it is also the verification problem: no individual on Earth is qualified to check all of this.

What the Lean checkmark means

The formal artifacts deserve to be taken seriously. The repository pins its entire toolchain to Lean and Mathlib 4.32.0, declares an axiom budget limited to the three standard ones every classical Lean development uses, and ships a per-chapter checking harness. This is not formalization theater. It is set up the way you would set it up if you wanted strangers to be able to check you.

But a green checkmark from Lean means something narrower than “the famous problem is solved.” The kernel certifies that a formal theorem follows from its encoded assumptions. It cannot certify that the encoding is the historical conjecture, with no quantifier quietly weakened and no assumption quietly added. And OpenAI’s own metadata labels the formalizations “agent-reviewed”: reviewed by a model, not yet by independent people.

The pipeline so far: generated argument, human-prepared manuscript, machine-checked formalization. The dashed circle is independent human review. It has not happened yet.

Four checks remain open to anyone:

1. Build it. Compile the repository cleanly from a fresh checkout.
2. Audit the axioms. Scan every theorem for hidden assumptions or trust-boundary tricks.
3. Check statement fidelity. Line up the historical conjecture, the manuscript theorem and the exact Lean declaration, side by side, for each result.
4. Search the literature. Confirm each result is genuinely new rather than a rediscovery.

None of that had happened publicly as of this writing. That is not a strike against work that was hours old. It is simply the difference between published and confirmed.

The missing denominator

The sharpest limitation of the release is not mathematical. OpenAI published a highlight reel without the game footage. The company says the selected problems had gone at least a decade without progress. It does not say:

• how many problems Astra attempted, or how the ten were selected;
• how many candidate proofs were generated and discarded;
• what prompts, tools and retrieval access were used during discovery;
• how much human steering happened before a successful argument emerged;
• what was done to rule out contamination from work the model may have seen.

Ten successes without a denominator cannot be converted into a success rate, and a curated portfolio cannot be compared to a benchmark score, however tempting the headline math.

Even the release’s most quotable number is narrower than it sounds. OpenAI says the tokens “needed to find solutions” would cost roughly $2,000 at the API rates of Sol, the top tier of its current flagship GPT-5.6. That is a retail-price conversion of a token count, not a spend report. Training and researcher time sit outside it by definition, since neither is billed in tokens. Whether the count includes the failed attempts along the way, or the later Lean formalization, depends on how you read “needed to find solutions”, and OpenAI does not say. As a statement about marginal inference cost it is interesting. It is not “$2,000 worth of math.”

The 62-page discovery notes carry a similar asterisk: the document itself says they were reconstructed afterward, by a model reading the original chains of thought alongside the finished papers. A retrospective narration, useful for the ideas. Not a lab notebook.

A track record that cuts both ways

• For (May 2026): an internal OpenAI model disproved Erdős’s 80-year-old unit-distance conjecture, and that result went through the wringer Astra’s haven’t yet. Gowers, Alon, Bloom and Tsimerman engaged publicly; follow-on work built on the construction.
• Against (late 2025): claims that GPT-5 had “solved” ten Erdős problems collapsed under scrutiny. Several turned out to be literature retrieval, and the claims were publicly walked back.
• Against (February 2026): in OpenAI’s “First Proof” exercise, the company initially favored a submission it later concluded was incorrect, and acknowledged the evaluation involved retries and human selection.

None of that discredits the Astra manuscripts, which are far better documented than either earlier episode. The earlier episodes are the reason the documentation exists. OpenAI says it takes responsibility for the correctness of the results. Responsibility is not the same thing as review.

What would settle it

For the mathematics: independent clean builds of the Lean repository, with the axiom and statement-fidelity audits done in public; field specialists reading each chapter the way referees do; novelty searches against the unpublished as well as the published record; and, ideally, OpenAI disclosing the denominators. Failed proofs are data. A company that wants credit for a research system should show its error bars.

For the model: the mundane indicators. A model card, a system card, an API identifier with pricing and context specs, safety evaluations, benchmarks anyone can rerun. None exists today. Until then, the accurate description is the one OpenAI’s own wording supports: an unreleased internal system, reportedly previewed to policymakers, credited with a remarkable stack of mathematics the community has not yet had time to check.

If most of the ten claims survive expert review, and the depth of the released artifacts suggests OpenAI expects them to, August 1, 2026 will mark the point where AI-generated mathematics stopped being an anecdote and became a portfolio. If the checks turn up the kind of statement-weakening or prior art that sank earlier claims, the release becomes a case study in why formally verified and true as advertised are different claims. Either way, the verification is now the story. We will report on it as it lands.

---

Sourcing: OpenAI’s August 1, 2026 announcement “Ten advances in mathematics and theoretical computer science”, its 249-page manuscript collection, the “How the Ideas Came Together” discovery notes, and the openai/ten-proofs Lean repository; The Information’s July 31 report on the Astra preview in Washington; OfficeChai’s coverage of the announcement; and, for the earlier episodes, OpenAI’s First Proof publications, contemporaneous reporting by Ars Technica and TechCrunch on the May 2026 unit-distance result, and public commentary by the mathematicians named. This article reflects the state of the evidence on August 1, 2026, the day of the release: the absence of independent confirmation at publication time is an early-release condition, not a verdict. Claim-level details, including the $2,000 token-price framing, the “agent-reviewed” formalization status and the reconstructed nature of the discovery notes, follow OpenAI’s own published wording.