Astra Solved Ten Math Problems for $2,000

On August 1, OpenAI published a 249-page manuscript and a GitHub repository holding ten formal proofs, every one machine-checked in the Lean 4 language down to its final inference step. The repository's "sorry" count, the placeholder Lean uses for a gap in an argument, sits at zero. According to the announcement, an internal version of Astra, OpenAI's next major model family, generated all ten results, and the total compute cost came to roughly $2,000 at the company's Sol token prices.

That combination of a stubborn problem set, a machine-verifiable answer, and a research budget smaller than a used car is new. Earlier AI math milestones were benchmark performances, systems scoring well on test suites that humans had already solved. This is a claim that an AI produced original mathematics that experts had not, across group theory, quantum complexity, high-dimensional geometry, and a half dozen other subfields. Noam Brown, a research scientist at OpenAI, posted on X: "An internal version of Astra, OpenAI's next major model family, solved 10 major open problems in mathematics, quantum complexity, and theoretical computer science. We believe it will be a major step for scientific reasoning."

The question now is how much of the claim survives contact with the mathematical community, and what the surviving parts reveal about the direction of research. The answers matter beyond the seminar room, because the same pipeline, a model that proposes and a machine that checks, is what will decide where AI can do original work and where it can't.

The Sofic Group That Took 27 Years

The headline result is the first explicit construction of a non-sofic group, a question open since Mikhail Gromov introduced the concept of soficity in 1999. Group theory is the study of symmetry, and a sofic group is one whose structure can be approximated by finite permutation groups with arbitrarily small error, a property that makes it tractable to computation. Mathematicians had long suspected that non-sofic groups exist, but nobody had built one, and the question had become a test case for whether the tools of the field were strong enough to settle its own conjectures. Sebastien Bubeck posted: "yes, nonsofic groups exist: this statement is one of many new beautiful results proved by Astra, our next major model."

The other results include a disproof of Connes's rigidity conjecture, a foundational claim about von Neumann algebras in operator algebra theory, a proof of Ehrhart's volume conjecture, new upper bounds for high-dimensional sphere packing, new circuit lower bounds for computing the permanent, and resolutions of three open problems from Paul Erdős. OpenAI says it chose problems where the main result had seen no progress for at least a decade, which makes the ten-for-ten scoreboard the most aggressive part of the announcement. Either the selection process was extremely good at picking tractable targets, or the model is doing something that resembles what mathematicians do when they choose where to dig.

Why Lean Proofs Change the Rules

The reason these results are being treated as mathematics rather than chatbot noise is the verification layer, and it's worth understanding from the ground up. Lean 4 is a programming language and proof assistant in which every theorem must be decomposed into steps small enough for a computer to check, and a single invalid inference halts the entire build. Submitting a proof to Lean is like handing blueprints to an inspector who tests every weld with a magnet and can't be persuaded to look away, no matter how prestigious the architect. Human peer review can be rushed, charmed, or simply exhausted; a compiler has none of those vulnerabilities.

This matters because the defining failure mode of large language models, confident hallucination, is exactly what formal verification catches. When Astra proposes a step that doesn't follow from the previous one, Lean rejects it and the model must revise. The proof files in the repository are therefore not assertions about what the model believes. They are artifacts that carry their own evidence. OpenAI released them under an Apache 2.0 license, and the "sorry" count of zero means every step in all ten proofs has been checked by software that can't be argued with.

What $2,000 Buys in Modern Research

The price tag deserves scrutiny of its own. OpenAI priced the runs at its Sol token rates, and depending on how you read the announcement, the $2,000 is either the total for all ten problems or the per-problem cost. Either way it's a rounding error next to what mathematics research usually costs. A single year of a graduate student's stipend covers it many times over, and these problems had absorbed decades of far more expensive human effort without yielding.

The previous week offered a useful contrast. Anthropic reported that Claude had discovered cryptographic weaknesses in a research setup that burned through $100,000 in tokens, according to coverage of the announcement. OpenAI is claiming results fifty times cheaper in a domain where correctness can be proven rather than suggested. Numbers like that change how research budgets get allocated, and they arrive as the cost of inference keeps falling on chips built for the workload. The pattern matches what NovaRift found when it followed AI's shift to the spreadsheet era: experimentation is giving way to accountable production.

But the economics cut both ways. The announcement doesn't say how many problems Astra attempted and failed, or how much compute was spent on dead ends before these ten succeeded. Publishing only the hits is survivorship bias, and it makes the true cost of autonomous discovery unknowable from outside the company. A model that solves ten problems out of ten attempted is one thing. A model that solves ten out of ten thousand is another, even if both produce the same press release.

The Missing Failure Log

That gap is the heart of the criticism the announcement attracted. Gary Marcus, the NYU professor emeritus who has spent years arguing that AI capabilities are routinely oversold, called the work amazing but vastly oversold in a widely read analysis, and pressed on exactly this point: OpenAI disclosed almost nothing about the model, its training, the number of failed attempts, or the human effort required to turn the output into publishable proofs. The company says Astra generated the arguments and that humans helped prepare them for publication, which is a reasonable division of labor, but it makes the "autonomous researcher" framing feel premature.

The transparency measures are real but partial. OpenAI released the Lean certificates, the 249-page paper, and a separate document in which the model reconstructs how each proof came together from its reasoning traces. It didn't release the prompts, the traces themselves, or the failure log. Simon Willison, who has tracked these model releases closely, noted that the prompts are the missing piece, since they would show how much human steering each result required.

The Verge's reporting described a mathematics community in a state of shock, with Fields Medalist Timothy Gowers responding positively while cautioning that the work is still being digested. There's also a question of what "ten advances" means as a category. Some of the results are complete resolutions, like the non-sofic group and the Connes disproof. Others are improvements to bounds, which is real progress but a different kind of claim. Grouping them under a single banner inflates the headline while the certificates themselves, to their credit, are precise about what each one establishes.

The Verifiability Constraint

Set the marketing aside, and the interesting question is what these ten certificates demonstrate about where AI research can operate. Mathematics is currently the only field where an AI can produce a result and have a computer certify it without a human expert in the loop, because formal verification exists and works. Biology, materials science, and economics have no equivalent of Lean. Their ground truth is messier, their checks are slower, and their mistakes hide longer.

The result says less about Astra's raw intelligence than about the domain it was aimed at. Mathematics is the one field where every claim can be mechanically adjudicated, and that property is what made the $2,000 price possible. The strategic lesson follows directly. The AI systems that do original research in the next few years won't be the ones with the most fluent prose. They'll be the ones paired with verification layers that make success and failure unambiguous.

The same pipeline is already being built for software verification, protocol design, and chip validation, where a confident mistake costs outages and recalls rather than a retracted paper. The compute economics accelerate the shift, because a failed attempt in a verifiable domain costs tokens and nothing else, a risk profile no human research program can match. The genuinely open problem is whether the reasoning process itself can be made legible. OpenAI published walkthroughs where Astra explains how it found its proofs, but those are reconstructions written after the fact, not the traces themselves.

Until the prompts, the attempt logs, and the failed runs are released, the community can't tell whether the model reasoned like a mathematician or searched an enormous space and got lucky. Building a verification layer for the process rather than just the output is the next hard problem, and the ten certificates in that repository, for all their rigor, don't contain the answer.