$ cat wiki/models/astra.md
Astra
OpenAI's next major model, named publicly for the first time on 2026-08-01 in a post attributing ten solved open problems in mathematics and theoretical computer science to an internal version of it (source).
Spec
| Attribute | Value |
|---|---|
| Developer | OpenAI |
| Released | not yet |
| Announced | 2026-08-01 (named, no launch) |
| Context window | unknown |
| Pricing | unknown |
| License | unknown |
| Availability | unknown — no API identifier, no availability date stated in any source read |
Every unknown above is genuinely unstated: the 2026-08-01 post is a results | |
| announcement, not a product announcement, and no source read here gives a shipping | |
| date, a price, or an endpoint | |
| (source). |
Release Date
Not released. OpenAI describes the model used as an internal version of Astra, and Sébastien Bubeck (OpenAI) calls it "our next major model" (@SebastienBubeck).
The cost figure is quoted at Sol API prices rather than at Astra's own — roughly $2,000 in tokens for all ten results — which is consistent with Astra having no published price of its own (source).
Benchmarks
No standard benchmark scores have been published for Astra. What exists instead is a set of ten claimed research results, each shipped with a Lean 4 certificate and a chain-of-thought walkthrough, alongside a 249-page manuscript (source):
| Result | Field |
|---|---|
| First explicit non-sofic group | Group theory |
| Connes' Rigidity Conjecture disproved | Operator algebras / von Neumann algebras |
| Quantum parallel repetition for general two-player entangled games | Quantum complexity |
| Ehrhart's volume conjecture proved | Discrete geometry |
| First improvement to the general high-dimensional sphere-packing upper bound since 1978 | High-dimensional geometry |
| New circuit complexity lower bounds | Arithmetic circuit complexity |
| Monochromatic triangles in multicoloured graphs | Extremal combinatorics |
| Three Erdős problems | Combinatorics |
| The problems are stated to have been open at least ten years, and in several cases | |
| much longer. Remaining results fall in coding theory and lattice cryptography | |
| (source). |
Per Eval Harness Configuration, these are not comparable to benchmark scores and are not recorded as such: there is no shared harness, no baseline, and no other model has been run on the same ten problems.
Use Cases
Only one use is demonstrated: autonomous production of novel mathematical arguments, with human editors organising the output into papers and a separate formalization step producing the Lean certificates (source). See AI for Mathematics for what that division of labour does and does not establish.
Compared To
- GPT-5.6 Sol (and Terra, Luna) — the currently shipping OpenAI frontier tier, and the price basis the $2,000 figure is quoted in. Sol had already been credited by OpenAI with rewriting its own serving kernels (2026-07-30); Astra is the same programme pointed at research output rather than infrastructure
- AlphaEvolve — Google DeepMind's search-based system for mathematical and algorithmic discovery. Different mechanism (evolutionary search over programs against an evaluator) for an overlapping goal
- Leanstral 1.5 — Mistral AI's open-weight Lean 4 theorem prover. Occupies the verification half of the pipeline Astra's results depend on, as an open-weight artefact rather than a closed internal one
- Gemini 3.1 Deep Think — the other frontier line whose public case has leaned on competition-level mathematics
- Claude Science, Co-Scientist (Google DeepMind) — the same "model as research instrument" framing in the natural sciences
Conflicting Reports
Release status. OpenAI's own framing is an internal version of an unreleased model. Several aggregators instead describe Astra as having been "launched" or "released" — for example KuCoin's flash ("OpenAI has launched a new model, Astra"). No source read here supplies an availability date, price or API identifier, so the page follows OpenAI's framing per the source-priority rule and records the discrepancy rather than resolving it.
Relationship to the GPT line. Some coverage glosses Astra as "GPT-6" (@kimmonismus, which writes "Astra model (GPT6?)" with the question mark). Nothing from OpenAI read here states that Astra is or is not a GPT-line successor.
Sources
- OpenAI — Ten advances in mathematics and theoretical computer science (2026-08-01) → snapshot
- @SebastienBubeck — OpenAI, naming the model and the result set
- the-decoder — coverage, and the Leiden declaration context
- Techmeme — the internal-version framing and the cost figure