OpenAI's Astra solved 10 open problems for $2,000: the lesson is the verifier
Summary. On 1 August 2026 OpenAI published ten results in mathematics and theoretical computer science, all produced by an internal version of Astra, its next major model. Every one of the ten problems had seen no progress on the main result for at least a decade. The tokens needed to find all ten solutions would cost roughly $2,000 at Sol API rates. The part worth copying is not the model: it is that the model then formalised each argument as a Lean 4 certificate and OpenAI released the lot in a public repository under Apache 2.0, built against Lean 4.32.0 and mathlib. Anyone with a laptop can run lake build All and get an independent yes or no.
That last property is what turns an impressive claim into a usable one. It is also the property almost no production AI agent has.
What OpenAI actually published
OpenAI's 1 August 2026 publication lists ten results across high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. Among them: new upper bounds on sphere-packing density down to the Cohn-Elkies threshold, a construction establishing the existence of non-sofic groups, a disproof of Connes's rigidity conjecture, an arithmetic-formula lower bound of order n^4/log n for computing the permanent, and a superexponential lower bound for multicolor triangle Ramsey numbers that resolves Erdos problem 183. Two more results resolve Erdos problems 146 and 180.
The workflow OpenAI describes is three steps, and the ordering matters. The model generated the arguments. Humans then prepared those arguments into manuscripts, working with the same model. Only afterwards did the model formalise each argument into a Lean certificate. OpenAI states plainly that it helped prepare the manuscripts and formalise the proofs and takes responsibility for their correctness, while the mathematical arguments themselves were generated by the system.
Thomas Bloom, a University of Manchester mathematician who runs erdosproblems.com, gave the reaction that matters most, as reported by The Decoder on 1 August 2026: "Maybe not bigger than a proof of unit distance would have been, but in terms of constructions, this is big." Bloom also rejected the framing that AI is replacing mathematicians, on the grounds that the system draws on more than a century of mathematical theory, was built by mathematicians, and was trained on everything mathematicians have written.
OpenAI researcher Noam Brown supplied the counterweight in the same reporting: "Sadly, no Millennium Prize Problems (yet)." He added that the team did not spend a lot of compute on each problem and that test-time compute could be pushed much further.
The number that gets misread
$2,000 is the headline figure and it is the one most likely to be quoted out of context in a board meeting. Read it precisely: OpenAI says the total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates. That is the cost of the successful token path, priced at public rates, for an internal model that is not generally available. It is not the cost of the research programme. Noam Brown's remark about failed attempts on other major problems is the tell: the denominator is missing.
The same arithmetic error is everywhere in enterprise AI budgeting. A team benchmarks a task, sees the winning run cost eleven cents, and forecasts against eleven cents. The real unit cost includes the runs that produced nothing, the human time spent deciding which output to keep, and the eventual re-run when the model changes. We wrote about the general version of this problem in our AI cost attribution playbook; Astra is the most vivid example yet.
| What the figure covers | What it does not cover |
|---|---|
| Tokens on the successful solution paths for all ten problems | Tokens spent on problems the model failed to crack |
| Public Sol API list rates | Any training or research cost for an unreleased model |
| Generation of the mathematical arguments | Human time preparing the manuscripts |
| The model's own Lean formalisation pass | Review time by the mathematical community |
| One model family, one attempt window | Re-runs after a model version change |
Why the Lean certificate is the actual story
Strip out the mathematics and the structure is a pattern any engineering team can recognise. A generator produced a candidate answer whose correctness a human could not cheaply confirm. A second, mechanical step converted that answer into an artifact whose correctness a machine can confirm, in bounded time, without trusting the generator.
The openai/ten-proofs repository carries one Lean file per result, from SpherePacking.lean through CompactnessAndDegeneracy.lean, under an Apache 2.0 licence. The project builds against Lean 4.32.0 with mathlib and Lake:
lake exe cache get
lake build All
Two commands, and the proof checker either accepts every formalisation or it does not. The repository also ships a ComparatorChallenges directory with instructions for checking the formalisations using Comparator, a separate checker. That detail is the one to steal. The claim is not "trust OpenAI's checker"; it is "here is the artifact, bring your own checker."
This is why formalisation changes the epistemics and a benchmark score does not. A benchmark tells you a model scored 87% on a held-out set someone else built. A Lean certificate tells you this specific output is correct, and you can confirm it yourself in the time it takes to compile.
The generate-then-check pattern in ordinary software
Very little production code has a Lean-grade verifier available. That is fine. The useful question is not "can I formally verify this" but "what is the cheapest mechanical check that would catch the failure I actually fear."
| Agent output | Mechanical check available today | What it catches | What it misses |
|---|---|---|---|
| Generated application code | Compiler plus a strict type checker, then the existing test suite | Type errors, broken call sites, regressions the suite already covers | Logic that is wrong but well-typed and untested |
| A database migration | Apply to a restored snapshot, diff the schema, run the query plan check | Destructive changes, missing indexes, plan regressions | Semantic data loss that the schema permits |
| Infrastructure change | Terraform plan plus policy-as-code rules evaluated on the plan | Public buckets, missing encryption, disallowed regions | Cost and blast-radius judgement calls |
| A refactor with no behaviour change | Property-based tests and differential testing old against new | Behavioural divergence on generated inputs | Divergence outside the generator's input space |
| An extracted fact or summary | Span-level citation check against the source document | Fabricated figures with no supporting span | A correctly cited but misleading emphasis |
| A support or sales reply | Deterministic policy assertions on the output text | Prohibited claims, missing disclosures, wrong pricing | Tone and appropriateness |
The pattern is the same in every row. Do not ask the model to be right. Make the output cheap to check, run the check every time, and let the check decide whether the output ships. Where no mechanical check exists, that step needs a human in the loop, and the honest response is to say so rather than to raise the temperature on the eval suite.
Our own view, from putting agents into client delivery pipelines: the teams that get value out of agentic AI are the ones that spent the first sprint building the verifier, not the prompt. A weak generator behind a strong checker converges. A strong generator behind no checker produces confident output nobody can sign off, and the review cost eats the saving. That is the whole economics of it.
A decision rule for where agents are safe
Score a candidate workflow on three axes before automating it.
Checkability. Is there a mechanical check that would fail on the errors you actually fear, and does it run in seconds rather than hours? If the only check is a human reading the output, the agent has moved work, not removed it.
Blast radius. If a wrong output slips past the check, what breaks and how long does the rollback take? A generated migration on a production database and a generated draft in a review queue are not the same risk even if the model is identical.
Reversibility. Can the action be undone by the same automation that took it? Anything that sends an email, moves money, or publishes to a customer surface belongs behind a confirmation step regardless of how good the eval numbers look.
High checkability plus small blast radius plus reversibility is where agents earn their keep today, and that combination describes a lot of engineering work: code generation behind a compiler and a test suite, infrastructure changes behind a plan and policy gate, data transformations behind schema and row-count assertions. The failure mode we see most often is teams starting at the opposite corner, automating the judgement-heavy work with the largest blast radius because it looks the most valuable. The measurement discipline for the rest of it is covered in our note on silent failures in agent evals, and the adversarial side in prompt injection guardrails. Both sit under our enterprise AI agents in production guide.
What Astra is, and what it is not yet
Astra is a model family, not a shipped product. Reporting by The Information, relayed by The Decoder, describes Astra as a new model class alongside OpenAI's existing Sol, Terra and Luna families, designed to coordinate multiple agents on problems for hours or days. Whether it ships as GPT-6 or as a variant inside the GPT-5 line has not been decided, and there is no release date. The models are expected to be the first submitted under the planned United States federal review framework that would require government sign-off before public release.
So nothing here is procurable. The results were produced by an internal version, at rates quoted against a different model's public pricing. Any 2026 plan that assumes access to this capability is planning on a press release.
There is a critical reading worth holding alongside the enthusiasm. Gary Marcus published a response titled "OpenAI's amazing, but vastly oversold, new model Astra", and the general shape of that objection, that a curated set of ten successes says little about the base rate across attempts, is the same denominator problem as the $2,000 figure. Both things can be true: the constructions are a real advance, and the sample is selected.
The wider context is that mathematicians are not uniformly comfortable. OpenAI's own publication points to the Leiden declaration on AI and mathematics as the reference for how credit should be assigned, and states that claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work. That is an unusually clean attribution stance, and it only works because the Lean certificates make the division of labour auditable.
India-specific considerations
For Indian engineering teams the practical takeaway is procurement-shaped rather than research-shaped. Formal methods talent is scarce everywhere, and Lean specifically is a research skill, not a hiring pool. The realistic move is not to formalise anything: it is to raise the mechanical-check coverage on the workflows you already automate, using tools your team already runs, and to buy verification capacity rather than model capacity where the two compete for budget.
For teams handling personal data, the checkability question has a compliance edge. Under the Digital Personal Data Protection Act 2023, a data fiduciary has to be able to show what happened to personal data, and an agentic pipeline whose outputs cannot be independently checked is difficult to evidence. Log the check result, not just the model output. A stored pass or fail from a deterministic verifier is auditable in a way that a model's self-assessment is not.
FAQ
What did OpenAI announce on 1 August 2026?
OpenAI published ten results in mathematics and theoretical computer science produced by an internal version of Astra, its next major model. Each problem had seen no progress on the main result for at least a decade. The model formalised every argument as a Lean certificate, released publicly under an Apache 2.0 licence.
Did Astra really solve ten problems for $2,000?
OpenAI states the tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates. That covers successful solution paths priced at public rates. It excludes failed attempts on other problems, human manuscript preparation and any cost of the unreleased model itself.
What is a Lean certificate and why does it matter?
Lean is a proof assistant. A Lean certificate is a formalisation of an argument that a proof checker accepts or rejects mechanically. It matters because correctness stops depending on trusting the generator: the repository builds against Lean 4.32.0 with mathlib, and anyone can run the check themselves.
Can I use Astra in production today?
No. Astra is a model family in testing, described as sitting alongside OpenAI's Sol, Terra and Luna families. Whether it ships as GPT-6 or a GPT-5 variant has not been decided and no release date exists. It is also expected to be the first model submitted for United States federal review before release.
How does this apply to software that has no formal proof?
Use the cheapest mechanical check that catches the failure you fear: a compiler and type checker for generated code, a plan plus policy-as-code for infrastructure, schema and row-count assertions for data work, span-level citation checks for extracted facts. The principle transfers even when full verification does not.
Where are AI agents safe to deploy right now?
Where the output is cheaply checkable by machine, the blast radius of a missed error is small, and the action is reversible by the same automation. Code behind a compiler and test suite qualifies. Sending money, emailing customers or publishing externally does not, regardless of eval scores.
Do mathematicians accept these results?
Reaction is mixed and the review is ongoing. Thomas Bloom of the University of Manchester called the constructions big news while rejecting the claim that AI replaces mathematicians. Gary Marcus published a piece arguing the release is vastly oversold. OpenAI itself cites the Leiden declaration on attribution.
What should we change in our pipeline this quarter?
Pick one automated workflow and add a deterministic check that runs on every output and can block it. Store the check result alongside the output. Under the Digital Personal Data Protection Act 2023 that stored pass or fail is far easier to evidence than a model's own confidence score.
How eCorpIT can help
eCorpIT builds and runs agentic pipelines for engineering and operations teams, and we start with the verifier rather than the prompt: the deterministic check that decides whether a generated output ships, and the audit trail that records the decision. We are a Gurugram-based organisation founded in 2021, CMMI Level 5, MSME certified and ISO 27001:2022 certified, with senior-led teams across AI engineering, cloud and platform work, and we design agent pipelines aligned with DPDP Act 2023 requirements. If you have an agent in production whose outputs nobody can independently check, talk to our team about what the check should be.
References
- OpenAI, "Ten advances in mathematics and theoretical computer science", 1 August 2026
- openai/ten-proofs, Lean 4 certificates repository
- OpenAI, "Ten advances" paper (PDF)
- OpenAI, reasoning walkthroughs (PDF)
- The Decoder, "OpenAI announces its next major model Astra by dropping ten previously unsolved math solutions", 1 August 2026
- openai/ten-proofs, SpherePacking.lean
- Leiden declaration on AI and mathematics
- Gary Marcus, "OpenAI's amazing, but vastly oversold, new model Astra"
- OpenAI, "A model disproves a discrete geometry conjecture", May 2026
- OpenAI, ChatGPT for Academic Researchers
- elan, the Lean toolchain manager
Last updated: 3 August 2026.
Top comments (0)