Category: paper · AI reasoning / AI for Math Date: 2026-08-01, official OpenAI release Sources: OpenAI official 249-page PDF (cdn.openai.com), GitHub openai/ten-proofs repo (Lean 4 formalizations), aiweekly.co, Decoder
Key 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, is roughly $2000.
- Each result comes with a Lean 4 formalization certificate (machine-checkable line by line).
- All arguments, Lean certificates, and reasoning traces are public on GitHub: https://github.com/openai/ten-proofs
- Before: 1 PhD student, 5 years, 1 open problem.
- Now: 1 researcher + 1 model + 1 Lean verifier, spreading dozens of candidate problems over a few weeks.
- The mathematical 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 objection: when translating a proposition into a formal statement, you may already have replaced it with a weaker version.
- Astra's weights, training data, and training cost are not public. Mathematicians doing peer review can only infer "how the model produced output" from "what it output" — an inherent information asymmetry.
- The literal meaning of "cracked" is contested. Refuting Connes rigidity is a genuine counterexample; but asymptotic improvements like the sphere packing and binary code bounds are more often called "important progress" rather than "solving the problem."
- The 10 released problems were curated by OpenAI. Which problems Astra failed on was 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 10 results
1. High-dimensional sphere packing: pushed the packing density exponent to the Cohn–Elkies threshold line — the first improvement since 1978. 2. Binary codes and spherical codes: improved the upper bound on maximum code size by an exponential factor for all parameters. 3. Non-sofic groups: constructed an explicit counterexample, disproving that "every countable group admits finite permutation approximations." 4. Connes rigidity conjecture: constructed infinitely many pairwise non-isomorphic groups sharing the same von Neumann algebra — the conjecture is refuted. 5. Arithmetic circuit complexity: an n⁴/log n lower bound on formula size for the permanent. 6. Quantum parallel repetition: extended the exponential parallel repetition theorem to arbitrary finite two-player entangled games. 7. Closest vector problem: a direct reduction from 3SAT yields polynomial-factor inapproximability. 8. Ehrhart volume conjecture: proved exact upper bounds in every dimension for convex bodies whose barycenter is the unique interior lattice point. 9. Multicolor Ramsey numbers: a super-exponential lower bound 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 another hard problem"
Over the past year, "AI cracks open math problem" headlines have appeared repeatedly. Some turned out to be problems already in the literature, proofs with gaps, or AI merely "reciting" known proofs.
OpenAI got two things right this time:
1. Formalization into Lean 4
Machine-checkable proof certificates mean correctness is no longer "true because the author says 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 cared about," but it can verify whether every inference step is logically valid. This fundamentally eliminates the most common objection to AI problem-solving — skipped steps in the middle of an argument.
2. Being explicit about the human researchers' role
OpenAI was quite direct: the arguments were generated by the model; human researchers "organized 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 $2000 figure means
Previously, "AI solves unsolved math problem" cost statements were usually "millions of dollars of GPU time + a top-tier team."
Astra ran these 10 problems at roughly $2000 total in tokens, priced at Sol API rates. That is not training cost — it is the token cost of inference. Even adding researcher salaries and Lean-conversion engineering, the marginal cost of a single-point breakthrough dropped from "PhD-thesis scale" to "cloud-bill scale."
The paradigm shift shows up in that number:
Astra is an internal OpenAI model. Researcher Sebastien Bubeck said on X that "this is illustrative, not everything Astra can do." In other words, this is only the small portion OpenAI chose to make public.
Limitations
A longer-term view
Tencent Hunyuan Hyra (7-31) solved a 50-year-old additive combinatorics conjecture via the three-stage "AI search + human capping + Lean formalization" pipeline; Xiaohongshu dots (7-23) hit a perfect IMO score reading LaTeX directly without Lean; OpenAI Astra now does "AI writes the argument + AI converts to Lean + humans organize the paper."
The common thread: Lean formalization has gone from a bonus to a default requirement. This is the most visible paradigm shift in AI for Math in 2026 H2 — "AI-solved" 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 will ever get a public API.
Original links: