OpenAI's Astra reportedly proves ten long-open math problems for about $2,000 in compute

OpenAI says an internal, unreleased model it calls Astra has produced fully machine-verified proofs for ten open problems in mathematics and theoretical computer science — several of them unsolved for decades — at a total inference cost of roughly $2,000. Those figures come from a dev.to report published on October 10, 2026, describing an announcement the company reportedly made on August 1, 2026.

What OpenAI published

According to the dev.to write-up, the company did not ask the field to take the claim on faith. Alongside the announcement it released a 249-page manuscript and the underlying Lean 4 proof certificates on GitHub under an Apache 2.0 license. Lean is a proof assistant that checks each logical step mechanically rather than relying on human judgment, and the repository's "sorry" count — Lean's marker for a gap left unproven — is reported to be zero across all ten results. In other words, every formalized step in every proof is said to check.

The results, as listed

The report names seven of the ten problems explicitly:

• Existence of non-sofic groups. Astra reportedly constructed a specific group that cannot be approximated by any finite set, settling a question open since Mikhail Gromov defined soficity in 1999 — described as the first concrete counterexample in 27 years.
• An improved sphere-packing bound, characterized as the first advance on the general upper bound for high-dimensional sphere-packing density since 1978, a 48-year-old ceiling.
• A counterexample disproving Connes's rigidity conjecture, a long-standing claim about von Neumann algebras.
• A proof of Ehrhart's volume conjecture.
• Three problems drawn from Paul Erdős's open-problem catalog, including problem 183 on multicolor Ramsey numbers.

The remaining three results are not itemized in the source.

Why the price tag draws attention

The dev.to post argues that the interesting number is not the model's name but the ratio: questions that resisted expert mathematicians for up to 48 years were closed, in this account, for a compute bill smaller than a weekend of GPU rental. The framing is not that Astra outthinks the humans who spent years on these problems. It is that a system able to search proof space at machine speed, with every step checked by Lean, can compress what would otherwise be a multi-year research effort into a short and cheap run.

Reception, and the unfinished step

Reactions cited in the report are positive but measured. Fields Medalist Timothy Gowers responded favorably while noting that the field is still digesting the results. Thomas Bloom, who curates a public database of Erdős's open problems, called the ten results "big news" on X and ranked them above a unit-distance counterexample produced by an earlier internal OpenAI model in May 2026.

The report is equally explicit about the limitation: none of the ten proofs has yet been through formal peer review. Lean verification establishes that a proof is internally consistent; it does not substitute for the community scrutiny that turns a machine-checked argument into accepted mathematics. It is also worth noting that everything here rests on a single secondary report of OpenAI's announcement rather than independent coverage.

A pattern, not a one-off

The post situates the result in a sequence. GPT-5.6 Sol reportedly worked through a 50-year-old conjecture in July 2026, and the May 2026 counterexample came before that. Frontier labs, in this reading, are drawn to formalized mathematics because a proof checker supplies an unforgeable pass or fail signal — a comparatively clean way to show that a model can do original research rather than retrieve and recombine published work.

Why it matters

If the reported results hold up, the cost of producing novel, verifiable mathematics has dropped by orders of magnitude, and the bottleneck shifts from generating proofs to reviewing them. The questions to watch are whether any of the ten proofs survive full peer review unchanged, and whether Astra or its eventual public release can repeat the performance on problems chosen by outside mathematicians rather than selected by the lab itself. Until then, this stands as a striking but unreviewed demonstration of what formal verification combined with large-scale model search can achieve.