OpenAI Said These Ten Math Breakthroughs Cost ,000. That Number Is Designed to Make You Stop Thinking.

OpenAI Said These Ten Math Breakthroughs Cost $2,000. That Number Is Designed to Make You Stop Thinking.

On August 1, 2026, OpenAI published a blog post announcing that its internal model — an unreleased system they are calling Astra Sol — had produced ten new results in combinatorics, graph theory, and theoretical computer science. The cost of generating the proofs, they said, was under $2,000 at Sol API prices. Hacker News pushed the story to 210 points in six hours. The comment thread immediately split into two factions: people who thought this was the most important scientific announcement in decades, and people who thought the $2,000 figure was marketing dressed up as a benchmark.

Both factions are arguing past the actual question. The $2,000 figure is technically true and epistemically useless at the same time. The math results are genuinely significant and also not what OpenAI’s blog post implies they are. I want to explain both of those claims precisely, because the engineering implications for people who build on top of these models are different from the narrative OpenAI is selling.

I have spent the last several years working on formal verification tooling and have watched AI-assisted theorem proving evolve from a research curiosity into something that occasionally surprises working mathematicians. My read of this announcement is that it is simultaneously a real scientific milestone and a carefully constructed piece of corporate communication, and that the gap between those two things tells you something important about where this technology actually is.

What the $2,000 Figure Actually Measures

The $2,000 is the token cost of the successful runs. It is not the cost of the experiment. This distinction is not subtle. It is the same methodological problem as reporting the cost of the lottery ticket that won, not the cost of all the tickets purchased before it.

To be precise about what I mean: if OpenAI ran 500 attempts against each of these ten problems, discarded the 499 that failed or produced incorrect proofs, and then published the one that succeeded at a token cost of $200 each, the reported figure would still be “under $2,000.” The actual experimental cost might be $1,000,000. The blog post does not disclose how many attempts were made, how many failed, what the failure modes were, or what the selection criterion was for choosing which attempts to present. There is no methodology section. There is a $2,000 figure and an implicit invitation to stop asking questions.

One commenter on the HN thread — a researcher posting as aabhay — articulated the problem precisely: his main gripe was the lack of transparency around the total experiment and construction. He doubted that OpenAI simply pointed their model at these ten specific problems alone and gave it one shot; therefore the $2,000 number could be completely misleading, similar to P-value hacking by not disclosing the total experimental setup. He wanted to know how many total problems were given to the model, what percent were left unsolved at what cost before giving up, how many attempts the model was given at each problem, and how expensive the harness was, including whether the model had access to a compute cluster for running intermediate calculations.

OpenAI has not answered these questions. They have pointed to the $2,000 figure and to the Lean formalization as if both of those things together constitute a complete accounting of what happened. One HN commenter pushed back on framing this as a cost comparison at all: even if the total cost was $1 million across the experimental runs, that might be ten to twenty math researchers for a year, and you would still get something those researchers could not necessarily deliver. That is a fair point. It does not change the fact that the $2,000 figure is presented in a way that implies something very different about reproducibility and cost than the actual experimental setup would warrant.

This matters for a specific and concrete engineering reason. If AI math reasoning is economically viable at $200 per solved open problem, it changes the cost structure of formal verification research in a way that should trigger immediate investment in automated theorem-search infrastructure. If the true cost is $200 per attempt with a 1-in-500 success rate, the economics are entirely different — you need independent evidence that a problem is approachable before it becomes worth spinning up the harness, and the selection of which problems to run on becomes the critical human bottleneck. These are not the same capability. One implies that AI can be pointed at any open problem and will reliably produce a proof. The other implies that AI can be pointed at problems that are, in retrospect, tractable for exhaustive search given the right constraint specification, and will sometimes find a proof.

The non-disclosure of attempt counts is not an oversight. OpenAI employs people who know how to write a methodology section. They chose not to include one. That choice is itself information about what the methodology section would have said.

What the Non-Sofic Group Result Actually Is

Of the ten results, the one that has attracted serious attention from working mathematicians is the claimed construction of a non-sofic group. I want to explain this result in some depth, because the blog post presents all ten advances as roughly equivalent in significance, which obscures the actual mathematical landscape considerably.

Sofic groups are a class of groups introduced by Mikhail Gromov in 1999 and named by Benjamin Weiss shortly after. A group is sofic if it can be approximated by finite symmetric groups in a precise technical sense. Informally, a group is sofic if its multiplication structure can be approximated arbitrarily well by finite permutation groups with a specific Hamming distance metric. The formal definition involves local convergence in the space of labeled Cayley graphs, but the intuition is that sofic groups are groups that behave, at finite scales, like groups that could be approximated by large finite permutation groups.

Since Gromov and Weiss formulated the definition, every group that researchers have been able to name has turned out to be sofic. Free groups are sofic. Amenable groups are sofic. Residually finite groups are sofic. Direct and inverse limits of sofic groups are sofic. Every group that arises naturally in the standard toolkit of topology, algebra, and geometry that researchers have examined has been sofic. But nobody could prove that all groups are sofic. The Sofic Group Problem — is every countable discrete group sofic? — has been one of the central open problems in geometric group theory for 27 years.

One commenter on the HN thread had a PhD advisor who reportedly spent 25 years on the non-sofic group problem and believed a solution would be Fields Medal-worthy. That assessment is not casual hyperbole. The Fields Medal is awarded for work that represents a major advance in mathematics, and a genuine construction of a non-sofic group would qualify. It would not just solve a named open problem. It would establish that the sofic boundary is a real and interesting mathematical phenomenon, open an entirely new research program of characterizing non-sofic groups, and require re-examination of a body of results in ergodic theory and topological dynamics that were developed under the working assumption that every group of interest is sofic.

If OpenAI’s claimed construction is correct, it is categorically different from the other nine results in the batch. It is a counterexample to what had functionally become a structural assumption in an entire subfield. It would change the shape of geometric group theory in a way that the other nine results — as valuable as some of them are — would not.

The Lean Formalization: What It Guarantees and What It Does Not

The proof has been formalized in Lean. Lean is a proof assistant that mechanically checks the logical validity of a proof given its stated premises and inference rules. A Lean-verified proof does not contain logical gaps — Lean does not accept them. When Lean says a proof is valid, it means that the argument from the stated premises to the conclusion is logically correct in a precise formal sense. This is a genuinely significant credibility marker for the nine results that are in areas with well-understood proof structures.

For the non-sofic group, the situation is more complicated in a way that the blog post does not fully acknowledge. The claim is that the model constructed an explicit group and proved it is not sofic. The proof of non-soficity requires defining soficity precisely in Lean — encoding what it means for a group to be sofic in the formal language — encoding the claimed group, and then proving that the group fails to satisfy the soficity criterion. Each of those three steps involves translation decisions made by a human. OpenAI explicitly acknowledges this responsibility: “We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness.” What this means in practice is that if there is an error in the final Lean-verified result, it will not be in the logical chain inside the Lean proof — that is mechanically guaranteed to be valid. The error, if any, would be in the translation from informal mathematical language to Lean’s formal language.

Translation errors in formal mathematics are common enough to be a recognized research problem. A theorem about connected graphs means something different depending on whether you define connectivity to allow self-loops, whether you require graphs to be finite, and whether you use the standard graph-theoretic definition or one of several alternatives. A Lean proof of a claim about connected graphs can be entirely valid while the informal English statement of the theorem is subtly different from what was actually proved. When the theorem in question is about a new mathematical object — a specific group constructed for the purpose of being non-sofic — the translation decisions become especially consequential, because there is no prior literature that constrains how the object should be formalized.

The verification burden for the non-sofic group result therefore falls on geometric group theorists who need to examine the Lean formalization of the soficity criterion and the group construction to determine whether OpenAI’s formalization captures the standard mathematical definition. This is not a simple check. It is substantive mathematical work that requires deep expertise in the area.

What “Solving Math Problems” Actually Means at This Stage

The sharpest framing of the real issue that appeared in the HN discussion came from a commenter named kcexn: did these problems seem like they had an intuitive answer and were feasible to prove before, just not high enough value targets for an expert to invest time into? Or were they fundamentally difficult prior to this point and it appears that AI has done something more than just throw the problem into a big solver?

This is the correct question, and my reading of the available evidence suggests the answer varies significantly across the ten results.

Several of the ten appear to be cases where the proof technique was known and the difficulty was finding an explicit construction or verifying a bound. Erdős-type problems in combinatorics and extremal graph theory often have this structure: the mathematical community has a clear sense of what a proof would look like, and the difficulty is finding the specific combinatorial object or the right numerical parameter that makes the argument go through. In these cases, the AI’s advantage is not mathematical insight in any conventional sense. It is the ability to systematically search a constrained space of constructions at a scale and speed that no human research team would fund, without the cognitive overhead of deciding which directions are promising. This is real and useful. It is also not what “AI solved a 30-year-old open problem” implies to a general audience.

The non-sofic group is structurally different from those results. If it is what it appears to be, it represents something closer to genuine mathematical discovery — a construction that the existing literature did not point toward, in a problem area where 27 years of expert effort had not produced a counterexample or a proof of universality. The exhaustive-search framing is harder to apply when there is no clear constrained space to search.

I want to be careful here, because I do not know the internal details of how the model was prompted or what the prompt structure looked like for the non-sofic group specifically. It is possible that a domain expert constructed an extremely precise constraint specification that substantially narrowed the search space. It is possible that the model found the construction through something that looks more like insight than exhaustive search. Without access to the prompts and methodology for this specific result, I cannot distinguish between those scenarios. This is another reason why the methodology omission matters.

What I am confident about is that these ten results are not ten instances of the same kind of achievement. Presenting them as a uniform batch obscures meaningful distinctions that affect how the mathematical community should receive them, how external researchers should allocate evaluation effort, and what engineers building on top of AI math reasoning should actually conclude about the technology’s current capabilities.

The Prompt Structure as Revealed by Published Examples

OpenAI published the prompts used for at least some of these problems. Looking at the prompt structure reveals something about the human-AI division of labor that the blog post presentation consistently downplays.

The prompts are not simple problem statements. They are detailed mathematical specifications that explicitly enumerate known partial approaches and rule them out, specify what constitutes an insufficient proof, describe the technical context in enough detail to rule out adjacent weaker results, and in some cases include explicit constraints on the form that a valid proof must take. One commenter reproduced a fragment of a prompt that contained language ruling out proofs for special graph classes, constructions of cycle covers with specific coverage patterns, bounded-length or prescribed-cycle variants, reductions to another unproved conjecture, computational verification through any fixed graph size, and candidate counterexamples without a complete nonexistence certificate.

Writing that constraint specification requires knowing that each of those approaches has been tried by the mathematical community and has failed to yield a complete proof. It requires understanding the proof-attempt history of the problem well enough to explicitly exclude approaches that look plausible but have documented dead ends. It requires knowing which weaker results already exist in the literature and therefore cannot be presented as solutions to the full problem.

The human who wrote that prompt did substantive mathematical work before the model ran. This is not incidental to the result. The constraint specification is doing real intellectual work by narrowing the search space the model explores to the regions where a valid proof is most likely to exist. Without the specification, the model would need to discover those constraints itself, which would require a qualitatively different kind of mathematical understanding.

From an engineering perspective, this suggests the following picture of what is actually happening: a domain expert provides problem selection, constraint specification, and output verification. The model provides exhaustive search within the specified constraints at a scale and speed that no human could match. Neither component alone produces the result. The $2,000 figure accounts for the model’s component and omits the human’s component entirely, not because the human’s contribution was small, but because human expert time is harder to quantify and less impressive-sounding in a headline.

The Verification Problem at Scale

There is a structural consequence of AI-generated proofs that the current discussion is not adequately addressing. The peer review bottleneck has shifted location, not been eliminated.

Before AI math provers, the bottleneck was proof production. Human mathematicians spent careers working on open problems, and the limiting factor was the finite supply of people who understood a problem domain deeply enough to make progress. This created a natural rate limit on mathematical results — there are only so many researchers alive who work in geometric group theory, and they can only produce so many proofs per year.

After AI math provers, the bottleneck becomes proof verification. OpenAI published ten results in a single blog post. The mathematical community now needs researchers who understand geometric group theory, Ramsey theory, extremal combinatorics, formal verification in Lean, and the specific proof-attempt history of each problem to evaluate these results. That verification work requires exactly the same domain expertise as the original proof work would have required. The humans needed to check AI-generated mathematics are the same humans who would have been working on these problems by conventional means.

The Lean formalization helps with one well-defined part of this. It guarantees that given the theorem statement and the mathematical axioms encoded in Lean’s type theory, the logical chain from premises to conclusion is valid. It does not guarantee that the theorem statement captures what the mathematical community cares about. It does not guarantee that the model avoided proving a vacuously true special case. It does not help with the community-level work of connecting the result to surrounding literature, identifying follow-on questions, understanding what the proof technique implies for adjacent problems, or extending the result to more general settings.

The interpretive work — understanding why the proof works and what it means — is where most of the value of mathematical research actually lives. A proof is not just a certificate of truth. It is an explanation. The mathematical tradition values proofs as objects that carry insight from the proved theorem back to the surrounding mathematical landscape. An AI-generated proof that nobody understands in that sense is, in the mathematical tradition, an incomplete contribution even if it is logically valid.

I will make a specific falsifiable prediction here: within 18 months, we will see an AI-generated proof that is Lean-verified, publicly claimed as a breakthrough, and later found to be either vacuously true or to prove a weaker statement than claimed, due to a formalization error in the theorem statement. This is not a criticism of the current results specifically. It is a prediction about what happens when proof generation scales faster than verification capacity, in a system where the Lean formalization provides a false sense of complete validation.

The Model Nobody Outside OpenAI Can Use

Astra Sol, the model that produced these results, is not publicly available. This is presented as an operational detail in the blog post, but it is the central fact that determines how much independent verification is actually possible.

When a human mathematician publishes a proof, other mathematicians can read it, check it, understand it, and attempt to generalize or extend the technique. The proof is fully transparent. When an AI model produces a proof that is then formalized in Lean, the Lean proof is transparent but the process that generated it is not. Other researchers cannot examine what intermediate reasoning steps the model used, whether the model arrived at the construction through something resembling mathematical insight or through a process of exhaustive enumeration, or whether the approach would generalize to adjacent problems. The model is a black box whose outputs happen to be checkable by Lean.

For results that are primarily existence proofs — show that an object with certain properties exists — this matters less. The object either has the properties or it does not, and Lean can verify that. For results whose value lies partly in the proof technique — where mathematicians want to understand not just that something is true but how to see why it is true — the inaccessibility of the model is a significant limitation on the scientific value of the result.

The non-sofic group falls into this second category. Geometric group theorists who have spent decades thinking about soficity will want to understand what property of the constructed group makes it non-sofic, whether the construction technique illuminates why soficity has been so hard to break, and whether the same ideas apply to related problems in the field. None of that interpretive work is possible from the Lean proof alone, and none of it is accessible without the model’s internal processing.

This creates an unusual epistemic situation: a potentially major mathematical result that has been verified to be logically valid but cannot be fully understood because the process that generated it is proprietary to a single company.

What Actually Changes If the Result Is Confirmed

The downstream implications for ergodic theory and topological dynamics would be real and non-trivial. A significant body of results in both fields was developed under the assumption that soficity was essentially universal — that any group arising naturally in practice would be sofic, so soficity assumptions were functionally assumptions about all groups. Those results would need to be re-examined to determine whether the soficity hypothesis was doing real work or whether the results extend to the non-sofic case with appropriate modifications. This kind of ripple effect through connected fields is exactly what major results in pure mathematics produce.

The Correct Frame for Engineers Building on AI Math Reasoning

Here is the direct version of what I actually believe, stripped of the hedging: OpenAI has probably produced several genuine mathematical results, and at least one of them — the non-sofic group — may be one of the more significant results in geometric group theory in the last two decades. The results are real enough that domain experts are being asked to review preprints, which is the correct response to a potentially major mathematical claim.

At the same time, the presentation of these results is optimized for maximum coverage impact rather than for enabling evaluation. The $2,000 figure is misleading without attempt-count data. The batch-announcement format obscures the heterogeneity of the results. The use of a non-public model means no external researcher can reproduce the experiment. The absence of a methodology section is a deliberate choice that benefits OpenAI’s narrative at the cost of scientific transparency.

For engineers and builders deciding what this means for their work: the capability being demonstrated is not “AI can solve any open math problem for $200.” The capability is “AI, guided by a domain expert who can write precise constraint specifications, can exhaustively search constrained proof spaces and sometimes find results that domain experts working conventionally could not find.” That is a genuinely powerful capability. It is also more limited and more human-dependent than the headline implies, and the human component — the domain expert who writes the constraint specification — is not being scaled or made more accessible by anything in this announcement.

The bottleneck in AI-assisted mathematics right now is not model capability. It is the supply of people who can write the mathematical constraint specifications that tell the model where to look. That supply is small, concentrated in academic institutions with long time-to-expertise, and requires the same deep mathematical knowledge that AI is supposedly making obsolete. This is the structural tension that the $2,000 figure is designed to obscure.

Predictions

The non-sofic group result will receive independent evaluation by geometric group theorists over the next several months. I assign roughly 65% probability that it survives review and enters the mathematical canon as a genuine result, 30% probability that reviewers find a formalization error in the theorem statement that substantially changes what was proved, and 5% probability of something more fundamental going wrong with the result.

The 65% figure is higher than my baseline for an AI-generated mathematical claim of this magnitude because of two factors. First, OpenAI apparently showed the preprint to at least one domain expert before publishing, based on HN comments from people with apparent direct knowledge. Second, the Lean formalization makes certain classes of errors impossible, narrowing the remaining risk to formalization translation errors, which are harder to introduce accidentally when the mathematical community knows what it is looking for.

Within 18 months, we will see an AI-generated Lean-verified proof claimed as a breakthrough that is later found to prove a weaker statement than claimed, due to a formalization translation error. This will produce a brief crisis of confidence in AI math provers that will then be resolved by the mathematical community developing better conventions for what counts as adequate validation of an AI-generated result.

Within 24 months, we will see multiple labs — DeepSeek, Google DeepMind, and at least one academic group — publish competing AI-assisted math results with more methodology detail than OpenAI provided here. Competitive pressure will eventually force some degree of methodological standards onto AI math announcements, including disclosure of attempt statistics and harness documentation. This is what happened in AI benchmarking when competition revealed that cherry-picked evaluation conditions were producing misleading capability claims.

The $2,000 figure will be cited in board presentations and investor decks for the next three years. It will be cited by people who did not read the blog post carefully and do not know that the methodology was omitted. The number will become a fact that propagates through organizations without context, which is exactly what a $2,000 figure without a denominator is designed to do.

The mathematics may be real. The accounting is incomplete. Knowing the difference between those two things is the minimum necessary for thinking clearly about where AI actually is in formal reasoning — and where the humans who spend decades understanding these problems still matter more than the headline is designed to suggest.