OpenAI Astra: 10 Math Results, $2,000 in Tokens, Lean 4 Certificates
Category: paper · AI reasoning / AI for Math Date: 2026-08-01, official OpenAI release Sources: OpenAI's official 249-page PDF (cdn.openai.com), the GitHub openai/ten-proofs repository (Lean 4 formalization), aiweekly.co, The Decoder
The Numbers
- 10 results spanning high-dimensional geometry, coding theory, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics.
- Total inference token cost, converted at Sol API pricing: roughly $2,000.
- Each result includes a Lean 4 formalization certificate (machine-checkable line by line).
- All arguments, Lean certificates, and reasoning-process notes are public on GitHub: https://github.com/openai/ten-proofs
- Before: 1 PhD student spending 5 years on 1 open problem.
- Now: 1 researcher + 1 model + 1 Lean verifier can run dozens of candidate problems in parallel over a few weeks.
- The math community has not had enough time to review all 10 results. Lean 4 certificates guarantee logical correctness, not that "the formalized proposition is the one mathematicians care about." A common concern: the formalization may have silently replaced the proposition with a weaker version.
- No public model weights, training data, or training costs for Astra. For peer review, mathematicians can only reverse-engineer "how the model produced output" from "what it produced" — an inherent information asymmetry.
- The word "solved" is contested. Refuting the Connes rigidity conjecture is a genuine counterexample; but asymptotic improvements like the sphere-packing and binary-code bounds are more often called "important progress" than "solving the problem."
- The 10 published problems were actively selected by OpenAI. Astra's failures were not disclosed.
- https://openai.com/index/ten-advances-in-mathematics/
- https://cdn.openai.com/pdf/ten-proofs-oai.pdf
- https://github.com/openai/ten-proofs
- https://aiweekly.co/alerts/openai-releases-ten-astra-math-proofs-with-lean-certificates
- https://the-decoder.com/2026/08/01/openai-ten-math-proofs
The List (10 Results)
1. High-dimensional sphere packing: pushed packing density exponents to the Cohn–Elkies threshold line — the first improvement since 1978. 2. Binary codes and spherical codes: improved upper bounds on maximum code size by an exponential factor for all parameters. 3. Non-sofic groups: explicit counterexample disproving that every countable group admits finite permutation approximation. 4. Connes rigidity conjecture: constructed infinitely many pairwise non-isomorphic groups sharing the same von Neumann algebra, refuting the conjecture. 5. Arithmetic circuit complexity: formula-size lower bound of n⁴/log n for the permanent. 6. Quantum parallel repetition: extended exponential parallel repetition theorems to arbitrary finite two-player entangled games. 7. Closest vector problem: a direct reduction from 3SAT yielding polynomial-factor inapproximability. 8. Ehrhart volume conjecture: proved tight upper bounds in every dimension for convex bodies whose centroid is the unique interior lattice point. 9. Multicolor Ramsey numbers: superexponential lower bounds resolving Erdős problem #183. 10. Extremal number conjecture: progress in extremal graph theory related to item 9.
Why This Matters More Than "AI Solved a Problem"
Over the past year, "AI cracks open math problem" headlines have appeared many times. Some were later found to have existed in prior literature, had gaps in the proofs, or were just AI restating known proofs.
OpenAI did two things right this time:
1. Formalization in Lean 4
Machine-checkable proof certificates mean correctness is no longer "correct because the authors say so." The Lean 4 community has already reviewed 80,000+ lines of formalized proofs, including Sphere Eversion, the liquid tensor experiment, and Busy Beaver bounds. Lean 4 cannot tell you the proof solves *the problem you care about*, but it can tell you whether every inference step is logically valid. This fundamentally eliminates the most common objection to AI-proved results: skipped intermediate steps.
2. Clarifying the role of human researchers
OpenAI is quite blunt: the arguments were generated by the model, and human researchers' contribution was "organizing the arguments into paper manuscripts." The Lean certificates were also converted by the model from its own arguments. Authorship and IP rules are based on this fact.
What the $2,000 Figure Means
Previous "AI solves unsolved math problem" cost framings were typically "millions of dollars of GPU time + a top-tier team."
Astra's total token cost for these 10 problems, at Sol API prices, is about $2,000. This is not a training cost — it's the inference-time token spend. Even adding researcher salaries and the engineering cost of Lean conversion, the marginal cost of a single-problem breakthrough has dropped from "PhD-thesis level" to "cloud-bill level."
The paradigm shift is visible in this number:
Astra is an internal OpenAI model. Researcher Sebastien Bubeck said on X: "this is illustrative, not everything Astra has done." In other words, this is only the portion OpenAI chose to publish.
Limitations
A Longer-Term Read
Tencent Hunyuan's Hyra (7-31) tackled a 50-year-old additive combinatorics conjecture via "AI search + human cap + Lean formalization"; Xiaohongshu's dots (7-23) hit IMO full marks reading LaTeX directly without Lean; OpenAI Astra this time follows "AI generates arguments + AI converts to Lean + humans organize papers."
The common thread: Lean formalization has shifted from a bonus to a default requirement. This is the most visible paradigm shift in the AI for Math line in 2026 H2 — "AI solved it" claims without a Lean certificate are now essentially disbelieved.
What to watch next: the math community's peer review of these 10 results, and whether Astra gets an external API.
Original links: