OpenAI Just Priced Mathematical Discovery at $200 a Problem

OpenAI introduced its next model family on Saturday without a keynote, a demo, or even a product. Instead it dropped a 249-page manuscript claiming that an internal version of Astra had produced new results on ten open problems in mathematics and theoretical computer science — every one of them unsolved for at least a decade — plus machine-checkable proof certificates for all ten. Buried in the release is the number that matters more than any theorem: finding the solutions took roughly $2,000 worth of tokens, billed at the API rates of GPT-5.6 Sol, the model OpenAI currently sells.

That works out to about $200 per decade-old open problem. The results are probably real. The price is real too, but it's doing a lot of rhetorical work — and unpacking it tells you more about where this is going than the theorems do.

The receipts, this time

OpenAI has been here before, badly. In October 2025, VP Kevin Weil claimed GPT-5 had "solved" ten open Erdős problems; it had actually surfaced existing papers, Thomas Bloom of erdosproblems.com called it "a dramatic misrepresentation," and the post was deleted. The echo of that number — ten, again — can't be accidental. The difference is what shipped alongside the claim this time.

Every result is formalized in Lean 4 and published on GitHub under Apache 2.0, with zero sorry placeholders. You don't have to trust OpenAI, a peer reviewer, or anyone's vibes: clone the repo, build it against mathlib, and the kernel returns a binary verdict. Bloom, burned once, called these results "big news."

The haul is not benchmark trivia. The headline is the first explicit construction of a non-sofic group, a question open since Gromov introduced soficity in 1999. There's a disproof of Connes's 1980 rigidity conjecture, via infinitely many non-isomorphic property (T) groups sharing one von Neumann algebra. Also: Ehrhart's volume conjecture, an exponential parallel repetition theorem for two-player quantum games, new hardness-of-approximation results for the closest vector problem, circuit lower bounds for the permanent, improved sphere-packing and coding bounds, and three problems off the Erdős list, including a superexponential lower bound for multicolor Ramsey numbers.

Two caveats keep this short of a coronation. Lean verifies that the proof proves the stated theorem; whether the formal statement faithfully captures the informal open problem, and whether the techniques are actually new, is human work that hasn't happened yet. None of the ten has been peer reviewed, and Henry Yuen — who has worked on quantum parallel repetition — reacted with a mix of awe and "I don't understand it yet." The certificates settle correctness. They don't settle meaning.

What $2,000 actually buys

The figure is the marginal token cost of the winning runs, priced at a released model's list rates. It excludes everything that made those runs possible: the failed attempts — OpenAI's Noam Brown admitted "we did try other major problems without success" — the human curation of which problems to aim at, the formalization pipeline, and the training of an unreleased frontier model. Quoting $2,000 for this is like quoting the fuel cost of a Formula 1 lap.

But dismissing it misses the direction of travel. In December 2024, o3's high-compute runs on ARC-AGI cost thousands of dollars per puzzle — per colored-grid pattern-matching task. Twenty months later, the same order of compute spend averages out to $200 per decade-open research problem, formalized proof included. Against the fully loaded cost of a postdoc-year, a "point the model at the entire open-problems list and see what falls" strategy is now a rounding error. When marginal cost collapses that far, the bottleneck shifts to exactly the two things the $2,000 doesn't price: choosing targets and verifying output.

Half of it fell to a model you can already rent

The most deflationary detail didn't come from OpenAI. Within about a day of the problem list going public, Harvard's Levent Alpoge — who in July used Anthropic's Claude Fable to disprove the Jacobian conjecture — reported reproducing five of the ten results with Fable, a shipped, rentable model, using a generic prompt and no internet access.

Sit with that. Half of a "decade-plus open" problem set was within reach of a model that's been generally available for weeks. Nobody had gotten these results before because nobody had pointed a frontier model at these specific problems with a serious verification loop — not because the capability didn't exist. That's a capability overhang hiding in plain sight, and it cuts both ways for OpenAI: Astra's long-horizon, multi-agent architecture is presumably what carried the other five, but the moat is thinner than the announcement's framing suggests. Given DeepMind's trajectory — AlphaProof's IMO silver in 2024, gold in 2025, AlphaEvolve grinding out bound improvements — expect a response measured in weeks.

The playbook is portable, and that's the developer story

Strip the math away and the architecture is: a generator proposing candidate solutions, a mechanical verifier issuing cheap binary verdicts, and enough budget to iterate thousands of times. Lean is mathematics' compiler. If your domain has anything resembling one — a type checker, property-based tests, a fuzzer, a model checker, TLA+ specs — the same loop runs today on models you can already call.

The practical shift is where engineering effort goes. Prompt cleverness matters less than harness quality: how much of your correctness criteria you can make machine-checkable determines how much of this capability you can actually harvest. A team that encodes its invariants as executable specs can burn $2,000 in tokens the way Astra did — wastefully, in parallel, discarding almost everything — and keep only what passes the kernel. A team whose definition of "correct" lives in a senior engineer's head cannot. That's the real dividing line this episode exposes: verifiable work is about to get absurdly cheap, and work that requires human judgment to evaluate inherits none of the speedup.

Real shift, wrong headline

This isn't "AI is now a great mathematician." Astra failed on other major problems, needed humans to pick its targets, and its proofs await expert digestion — Daniel Litt, who once bet $100k against AI producing top-journal number theory by 2030, conceded the trend, while others pushed back on the "most important day in mathematics" hyperbole. Both reactions fit the evidence.

The demonstrated fact is narrower and, for working developers, more consequential: in any domain with a mechanical verifier, decade-hard problems now fall for cloud-bill money, and at least two vendors' models can do it. The theorems made the headlines. The invoice is the announcement.