The Verifier Economy: Ten Open Problems, Two Thousand Dollars

Aug 3, 2026 7 min read

Two research bills, one week apart. Anthropic reports that Claude Mythos Preview found an improved attack on the HAWK post-quantum signature scheme in 60 hours — “effectively cutting its key strength in half” — and that each of its recent cryptanalytic results “cost roughly $100,000 in API cost to develop.” Then, on August 1, OpenAI published ten results in mathematics and theoretical computer science, on problems that “have seen no progress on the main result for at least a decade.” The total token bill, at public API rates, was “roughly $2,000.”

The interesting part is not that an internal model called Astra did the mathematics. It is that every one of the ten results shipped with a machine-checkable Lean 4 certificate, and that this changed what a “result” even is.

The unit of output changed

A year ago, an AI math result was a claim plus a narrative. The community would have to trust the model, or redo the work. OpenAI’s ten proofs flip that structure. The pipeline, as described in the announcement, is:

internal Astra → mathematical arguments
humans + same model → manuscripts
model → Lean 4 formalization → certificate

The openai/ten-proofs repository — Apache-2.0, created August 1, 2026 — contains the ten formalizations: sphere packing down to the Cohn–Elkies threshold, exponentially improved binary and spherical code bounds, a construction of non-sofic groups, a disproof of Connes’s rigidity conjecture, new arithmetic-circuit lower bounds for the permanent, exponential quantum parallel repetition, polynomial-factor hardness for the closest vector problem, Ehrhart’s volume conjecture, a superexponential multicolor Ramsey lower bound resolving Erdős problem 183, and counterexamples to the compactness and degeneracy conjectures resolving Erdős problems 146 and 180. Each .lean file is a proof that the Lean kernel — the type checker at the bottom of the stack, pinned to Lean 4.32.0 with mathlib — accepts or rejects mechanically. The model cannot argue with the kernel.

That is the property that makes these results different from every previous frontier-model flex. The verifier is outside the loop. It is deterministic, public, and cheap to run: lake exe cache get && lake build All rebuilds all ten certificates locally, and OpenAI even publishes ComparatorChallenges so the formalizations can be re-checked with the independent Lean comparator toolchain.

What the $2,000 actually covers

The exact wording matters, because it is easy to misread: OpenAI says “the total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates.” That is the success-path token bill for all ten problems, quoted against the public GPT-5.6 Sol price list ($5 per million input tokens, $30 per million output). It is not a full-cost accounting, and OpenAI does not present it as one.

What is excluded:

Failed attempts. Ten successes were selected for publication; the announcement does not say how many problems the pipeline attempted, or how many dead ends preceded the winners. The reported figure is the bill for the runs that worked.
Human time. “These arguments were then prepared into manuscripts by humans with the same model.” Mathematicians read, edited, and vouched for the papers.
Formalization compute and effort. Producing a Lean certificate that survives the kernel is itself a separate, expensive loop — and OpenAI says its team “helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness.”

So the honest reading of “$2,000 for ten open problems” is narrower and still remarkable: the generation side of frontier research has become nearly free. The binding constraints moved to specification, formalization, and community review — the parts the token count does not capture.

The specification gap is the new trust boundary

Here is the systems detail most coverage will miss. A Lean certificate proves a formal statement. It does not prove that the formal statement is the informal conjecture the community cares about. The kernel verifies the argument; it cannot verify the mapping from “multicolor triangle Ramsey numbers” to MulticolorTriangleRamsey.lean. That mapping is checked by humans — the mathematicians who prepared the manuscripts, and eventually the community that reviews them.

OpenAI is unusually explicit about this division of responsibility: “the mathematical arguments themselves were generated by our system,” while the humans “take responsibility for their correctness.” That is the right structure, and it is worth naming: the model produced the claims; the kernel checked the inference; the humans own the specification. The trust boundary is no longer “did the model reason correctly” — it is “is this the right theorem, encoded correctly.”

There is also a transparency asymmetry worth flagging. The certificates are open and auditable by anyone; the reasoning walkthroughs are an LLM-generated narration of thinking traces, not the raw traces; the model (an internal version of “our next major model”) and the prompts that produced the arguments are not published. As Simon Willison put it: “That’s a decent level of transparency, but I want to see the prompts they used!” The outputs are open; the process is closed.

What agent builders should copy

The lesson of ten proofs is not that models do math. It is that the economics and the trust model of AI-produced work both hinge on where the verifier sits — and that a verifier outside the model’s influence is worth more than any amount of prompt care.

Agent systems today	What the ten proofs show
Verifier is a rubric, test suite, or human review — inside the loop, gameable	Verifier is a kernel — outside the loop, ungameable
”Trust the model” by default; output is a claim	Trust the artifact; output is a certificate
Cost concentrated in generation	Generation nearly free; cost moves to spec + verification
Judgment about correctness is fuzzy and delayed	Correctness is binary and immediate — for the formal statement

The uncomfortable truth for agent operators: your agent does not have a Lean kernel for its own behavior. There is no external checker that will mechanically reject a tool call, a write, or a side effect the way the kernel rejects a bad inference. That absence is the reason “the model said it was fine” keeps appearing in incident reports. The fix is not a better model. It is building verifiers that sit outside the loop for the things that matter — deterministic permission checks, replayable sandboxes, and machine-checkable records of what an agent actually did.

The second lesson is accounting. When Anthropic spends ~$100,000 of tokens on one result and OpenAI spends ~$2,000 on ten, the difference is not only difficulty — HAWK is cryptanalysis, the ten problems are mathematics — it is also process. Report the denominator. Track failed runs. Price the full pipeline, not the successful trajectory. A cost figure that counts only the wins is a metric for a demo, not for a research program.

Facts, inference, and the open edge

Observed: On August 1, 2026, OpenAI published ten results on decade-open problems, attributing them to “an internal version of Astra, our next major model,” stating the total token cost “would [be] roughly $2,000 at Sol API rates,” and releasing Lean 4 formalizations (Apache-2.0, Lean 4.32.0/mathlib) plus reasoning walkthroughs for each result. Anthropic’s July 28 cryptanalysis post reports the HAWK attack took 60 hours and each result “cost roughly $100,000 in API cost to develop.”

Inference: The durable architectural change is that a frontier lab now treats the machine-checkable certificate, not the model’s claim, as the publishable unit — with a verifier (the Lean kernel) that sits outside the model’s control. The corollary is that generation is no longer the binding constraint in research; specification, formalization, and review are.

Open questions: How many problems were attempted before these ten succeeded? Do the formalizations faithfully encode the informal conjectures as the mathematical community reads them? Will the certificates survive independent checking with the comparator toolchain and community review? None of these are answered by the announcement, and the existence of the certificates should not be mistaken for answers.

The model is cheap now. The verifier is the product. The certificate is the result — and the specification gap is where the humans are still in the loop.