FrontierMath Erdős Benchmark

Sources#

• After Math
• Announcing FrontierMath Erdős
• FLT: Anthropic has beaten me to it
• FrontierMath Erdős
• Long-horizon autoformalization of a core theorem underlying MIP* = RE
• OEIS Open: How many conjectures can language models turn into theorems?
• On the Navier–Stokes Millennium Prize Problem
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Summary#

FrontierMath Erdős is Epoch AI's benchmark of 68 Erdős problems that were still open as of August 2026, formalized in Lean, which an AI system must prove or disprove within a fixed budget (Tom Adamczewski and Greg Burnham, announcement 2026-09-01, empirical). It is the corpus's first benchmark whose items have no known answer at all, and its first to make a dollar budget part of the score definition rather than a disclosure footnote.

The motivation is that Erdős problems had become "something of a central benchmark for tracking AI math capabilities, but this status is relatively informal" — used by DeepMind (9/353) and by OpenAI's unit-distance disproof with no shared item set, no shared budget and no shared verification standard. Epoch's contribution is three pieces of discipline on top of an existing practice: curation (which problems are hard and significant), verification (Lean, so a solve is machine-checked), and replicability (a published harness, a published item list, and a stated per-problem budget).

The three fixes, and what each one actually buys#

Curation: significance as a selection axis#

"Erdős problem" names anything Paul Erdős ever posed, and Erdős posed many hundreds. Thomas Bloom's erdosproblems.com catalogues 1,217 problems, of which 652 remain unsolved; Epoch asked Bloom to pick his favourites among the unsolved — those he believed both mathematically significant and difficult — and he selected 68, about 10% of the unsolved set, all open as of August 2026.

Epoch flags the obvious weakness itself: "This approach is highly subjective," and quotes Bloom's own standard from the sibling benchmark — "No doubt every mathematician will see some problems on this list and think 'why on earth did they include that?' — but as long as they also see others and think 'naturally that should be included, it's a deep and important problem', then I think we have done a good job." The calibration that makes the bar legible: Bloom roughly estimated that 3–5 Erdős problems of this calibre had been solved by AI in total as of August 2026. So the denominator is chosen to be near the edge of what has ever been done, not near the edge of what is currently measurable.

Verification: what "Lean-formalized" guarantees here, precisely#

A solve requires a Lean proof or disproof that passes verification, checked by Comparator, a proof checker built by the Lean FRO and "designed to be robust to a submission that actively tries to cheat." That is the strong half. The three qualifications are all stated by Epoch and all matter:

1. Soundness is conditional on Lean itself. The announcement's one footnote: the guarantee holds "so long as there aren't bugs in Lean itself — which there surely are. In practice, we expect false positives to be exceedingly rare, and not too laborious to recognize when they do occur." This is the standard caveat, stated rather than assumed.
2. Soundness is conditional on the statement being formalized correctly — the residual human job AI-Driven Formal Proof Search names. Epoch's formalizations are not uniformly sourced: 50 of the 68 were already formalized in Google's Formal Conjectures project; the remaining 18 were formalized by AI under Epoch's direction.
3. Those 18 have not been expert-reviewed. Epoch's own words: the 18 statements "are fairly simple, and the formalizations have so far passed our initial review. Still, we are not Lean experts, and so errors may exist. We are in the process of seeking additional expert review." So on 26% of the item set, the guarantee currently reduces to a non-expert reviewed an AI's formalization of an unsolved problem. The announcement does not say whether any of the solved problems came from that subset — which is what makes it a live question rather than a caveat.

Replicability: the $300 / 72-hour protocol#

The whole codebase is open-sourced with the harness and the 68 problems listed. The default protocol: one attempt per problem, $300 of inference budget and 72 hours of working time per attempt. Models run without internet access — they get an offline collection of mathematics papers plus tools such as a computer algebra system.

This is the part with the widest reach beyond mathematics. Epoch's stated target is the opacity of lab-internal results — "how many people have tried… which problems… with what scaffolds… how much inference compute" — and its answer is to make the budget a property of the score rather than a disclosure item. See Compute-Controlled Benchmarking for why that is the stronger move, and Expenditure Horizon for the other 2026 attempt to put capability on a dollar axis.

Results: 2 of 68, and what the other 3 cost#

Five models, one attempt each:

Model	Score
GPT-6 Astra (pre-release)	3%
GPT-5.6 Sol	0%
GPT-5.5	0%
Claude Fable 5.1	0%
Claude Fable 5	0%

(The two Anthropic entries are Fable 5 and its point release.) Only the pre-release GPT-6 Astra solved anything: 2 of 68. It disproved problem 74 by finding a counterexample at $222 and 10 hours (superseded 2026-09-29 by FrontierMath Erdős: $218 and 15 hours), and proved problem 126 at $172 and 10 hours (superseded: $247 and 16 hours). The paper recomputes every Astra cost at its actual token prices (see "What the methods paper adds" below), which is the likely source of the drift; the announcement's original figures were printed without saying which price basis they used. Every other attempt by every model "ran out of budget without a verified proof."

The headline is two events, and that is worth stating plainly. 2/68 against 0/68 on the same 68 items is a difference of two successes; taken as a two-by-two it gives a two-sided Fisher exact p ≈ 0.50. The ranking of Astra over the other four therefore rests on a difference the protocol cannot resolve at n = 68 with one attempt each — the off-protocol repetitions below are what make Astra's capability credible, and no other model was run off-protocol at all. Epoch does not make this point; it is what the numbers support.

The cost ladder: $300 → >$220,000#

Separately from the benchmark, Epoch ran less systematic attempts on the same problems with the same pre-release Astra, at larger budgets, with varied agent setups and varied attempt counts. Epoch labels these emphatically: "These attempts are not a FrontierMath Erdős score." Astra's score remains 3%.

Across all attempts Astra solved 5 of the 68 at least once — the two above plus problem 1 (disproof), 548 (proof) and 571 (proof):

Problem	Result	Solved in	Cost of each solution
1	disproof	2 of 5 2 of 4 attempts	$405 (27 h) and $1,384 (84 h)
74	disproof	7 of 7 6 of 6 attempts	$47 (5 h) to $271 (19 h)
126	proof	5 of 5 4 of 4 attempts	$154 (8 h) to $249 (17 h)
548	proof	1 of 4 1 of 3 attempts	$363 (20 h)
571	proof	1 of 4 1 of 3 attempts	$617 (41 h)

The remaining problems were attempted two to six times each — 269 attempts (superseded 2026-09-29 by FrontierMath Erdős: 56 of the 63 were attempted to completion two to five times, 172 attempts in total; the other seven are not counted, and infrastructure failures that ended attempts before a verdict are excluded) — and none was solved. The table above carries the paper's counts, which exclude verdict-less attempts. Total spend to reach the five: over $220,000, against roughly $20,000 for the benchmark run itself (68 × ~$294, i.e. nearly every scored attempt burned its full $300).

Three readings the announcement leaves on the table:

• The marginal cost of a solve rises by two and a half orders of magnitude inside one model. The protocol's two solves cost $222 and $172 $218 and $247 (paper). The three extra ones cost ~$200,000 of additional spend between them — about $67,000 per marginal problem — because the money goes mostly into the fruitless attempts (269 per the announcement, 172 per the paper) that solved nothing.
• Both axes bind, and they are not the same axis. All three off-protocol solves cost more than the $300 cap ($363, $405/$1,384, $617), and all three came from low per-attempt success rates (2/5, 1/4, 1/4 2/4, 1/3, 1/3 on the paper's counts). The two the benchmark found are the two that are both cheap and reliable (74: 7/7 6/6; 126: 5/5 4/4). So the fixed protocol is not simply a budget filter — it selects for problems that are reliably solvable at a single draw, and the per-problem success rate is bimodal.
• Repetition is the cheaper knob than budget, up to a point. 74 solved at $47 on some attempts and $271 on others: a 5.8× per-solve cost spread on the same problem and model, which is the variance a one-attempt protocol converts into a binary.

Epoch names the missing experiment itself: "Future work could test this inference scaling more systematically, measuring how the number of solutions grows with the budget per attempt and with the number of attempts."

The formalization tax, quantified#

Epoch's first caveat is the one with the largest consequence for AI-Driven Formal Proof Search: "Formalizing such a result is essentially an entirely separate project, bolted on." Its example is the corpus's sharpest number on the subject, and it is the same result this wiki already tracks under a different description — Erdős problem 90 is the unit distance conjecture that OpenAI's model disproved (see Latent Capability Overhang):

the natural-language proof was 18 pages; a subsequent effort that formalized the result in Lean consisted of 1.2 million lines of code — "primarily due to the need to invoke a 'deep' result that had not yet been formalized in the Lean standard library. The 18-page paper could simply refer to this result, whereas the Lean formalization needed to derive it from first principles."

That is roughly 67,000 lines of Lean per page of prose, and the stated cause is mathlib coverage, not proof difficulty — the same vocabulary bottleneck AI-Driven Formal Proof Search records from AutoGraphForge, here priced on a result that was actually formalized rather than anticipated. Note what it is not: the 1.2M lines were a separate human-led effort (github.com/plby/Erdos90), not the model's output, so this measures the tax, not an AI's ability to pay it. Epoch states the generalization: "This is a limitation of any Lean-based benchmark that asks AI systems to solve open problems" — which is, read the other way, the strongest argument in the corpus for the unformalized branch.

And a vendor claimed to pay it in 17 hours, one week later. [[navier-stokes-ai-claim|OpenAI's Navier–Stokes announcement]] (On the Navier–Stokes Millennium Prize Problem, 2026-09-08, vendor-claim) states that "Lean formalization and verification took an additional 17 hours via GPT‑6 Astra" — i.e. that the model scored 2/68 on this page's protocol formalized a Millennium-Prize blow-up proof in under a day. Held against the paragraph above, one of three things is true: the tax is enormously variable across results, an AI can now pay a tax that took a human-led effort 1.2 million lines, or the two artifacts are not the same kind of object (a full derivation versus a skeleton, a different statement, or a differently-bounded notion of "verification"). The announcement contains nothing that distinguishes them — no line count, no statement, no axiom discipline, no library version, and the repository it links is not in this corpus. Recorded here because this page owns the only measured number on the subject, and because a vendor-claim of a 1000×-cheaper tax is exactly the kind of claim the measured number exists to discipline.

A second, blunter consequence for this page's headline. The only non-zero score here belongs to a pre-release GPT‑6 Astra. The same announcement says the Navier–Stokes result came from "an internal model that is significantly more capable than GPT‑6 Astra," trained from August 28 — a week before this benchmark published. So the model this page measures was, on the vendor's own account, already superseded internally when its 2/68 was announced, and the benchmark's 3% is a statement about the most capable model available to an external evaluator, not about the frontier. That does not weaken the protocol, which is the page's contribution; it bounds what the number means, and it is the extracted-and-withheld gap appearing inside a scored benchmark for the first time.

The Mathlib-gap cost this section prices has a measured counterpart in ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization (empirical): to formalize stochastic-optimization convergence proofs its agents build a 109,634-line domain library, and removing that library on four tasks left human ratings unchanged (mean 6.8) while raising tokens 7.7% to 154% (Many-Agent Proof Harnesses). Reuse cheapens the rebuild; on those tasks it did not change what was reached.

The objection to scoring this at all (2026-09-12)#

Three days after the Navier–Stokes announcement, De Toffoli and Duede (After Math, practitioner-opinion) published the argument that a benchmark like this one measures the wrong thing, and it is worth recording on the page it aims at:

"If mathematical success comes to be identified too closely with the production of certified answers, mathematics risks adapting itself to precisely those features that are easiest to benchmark and automate away."

Their case is that a certified answer is not yet a solution — a solution additionally requires an intelligible argument that lets the result enter mathematics as practiced (see Logical vs Intelligible Proof) — and that mathematics has aims beyond problem-solving at all: theory-building, training, community, cumulative knowledge, aesthetic value. They report that the concern is institutional as well as philosophical: a declaration at mathandai.org, initially signed by 25 Fields Medallists, warns of a "severe misalignment" between AI companies' goals and the mathematical community's.

How much of this actually lands here. The Goodhart risk is real and unmeasured; it is also aimed at the discipline's norms rather than at the protocol, and this page's own contribution — a fixed budget, a curated denominator, a kernel's verdict — is a better instrument for exactly what it claims to measure than anything else in the corpus. Two things blunt the objection specifically against this benchmark: Epoch's problems were curated for significance by a human expert against a background estimate that only 3–5 problems of that calibre had ever been solved by AI, which is the opposite of selecting for what is easy to score; and a 2/68 is a statement about difficulty, not a claim that solving the other 66 would constitute solving mathematics. What survives is a caution about reading: a rising number on this page measures certified answers on curated open problems and nothing about whether mathematicians can use them. It is an argument, from authors with no measurement and no stake, and it should be weighed below everything else on this page on any question of fact.

Contamination by construction, with a stated expiry#

Epoch will run this as a "classical" public benchmark — models evaluated as released, no strong guards — and its argument for why that is currently safe is unusual and worth generalizing: no solution to any of the 68 problems was known as of August 2026, so a model whose training data ends before then cannot have learned one. This is contamination immunity from the item set's own unsolvedness rather than from a holdout, a hash or a sandbox (Benchmark Contamination and Decontamination).

The expiry is built in and acknowledged: solutions will be published and discussed, and will reach training data. Two stated mitigations, of unequal strength:

• Post-hoc filtering — "problems solved before a model's training cutoff can be filtered out, and all models compared on the remaining problems." This works, and it shrinks the denominator every time the benchmark succeeds.
• Negative results remain informative — "if a later model fails to solve a problem that an earlier model solved, that is presumably a data point suggesting that the later model's math capabilities are weaker." Weaker than it sounds at these numbers: with two solves in the scored run, the informative negative is one or two events.

The third caveat is scope, briefly: "Erdős problems aren't all of mathematics." Epoch expects progress here to be "at least somewhat correlated" with general math capability and says the inference "is not airtight."

What the methods paper adds (2026-09-29)#

Adamczewski and Bloom (FrontierMath Erdős, arXiv 2609.25050, 2026-09-06, 12 pp, empirical; Bloom is the curator, so the item selection is described by the person who made it) is the companion paper the announcement pointed at. It does not change the headline (Astra 3%, four models 0%); it supplies the protocol, the provenance and a re-costing.

The re-costing is the main correction. Astra was pre-release with unpublished prices, so the harness metered it at GPT-5.6 Sol's per-token prices as a stand-in. Its real prices are about twice as high (1.8-2.0x depending on token mix): attempts that hit the metered $300 cap had actually spent $545-572. The authors recompute every attempt from token counts and count a solve only if it cost at most $300 at actual prices. One effect: problem 1 was disproved inside the scored run at $405, and is therefore excluded from the score (it appears only among the additional attempts) — so the fixed-budget correction, not the model, is what holds the score at 2/68 rather than 3/68. One admitted flaw: the agent's budget tool showed metered dollars, so at a true $300 it displayed ~$160 spent and $140 remaining, and the model paced itself against a budget looser than the real one. The authors judged that preferable to discarding the run. An unreconciled figure: the paper still says the benchmark run cost "roughly $20,000", which matches 68 x $300 nominal, whereas 66 failed attempts at $545-572 would be ~$36-38k of real Astra spend by this page's arithmetic; treat $20,000 as the nominal budget, not the actual spend.

Expected cost per resolution, as the authors put it: ~$10,000 ($300 per attempt at a 3% rate), which they call "modest for the resolution of an important open problem." Read against the ladder above, that is the cost under the protocol; the marginal cost of the three extra solves stays ~$67,000 each.

Item-set provenance, per problem. The 68 conjectures cover 65 distinct problems: Hadwiger-Nelson (#508) is three conjectures (chromatic number of the plane is exactly 5, 6 or 7 — Formal Conjectures' "what is the value" statement does not fit prove-or-disprove), and #713's two parts are separate. The three HN conjectures are mutually exclusive by construction (proving one disproves the other two; disproving one settles nothing else), so the set is not fully independent: one such result resolves the other two as a by-product. Other multi-part problems (#208, #812, #1206) contribute only the named part; where a problem was ill-posed (#138, #208, #812) Bloom picked the single question best capturing its "spirit", usually the hardest. 50 of 68 conjectures (48 problems) come from Formal Conjectures; 17 problems had no statement there and were autoformalized (18 conjectures), and Bloom reviewed each autoformalized statement for fidelity. That refines the announcement's "not Lean experts" caveat: the review was by the problem's curator and a mathematician, not by a Lean expert, and the paper does not say which of the five solved problems fell in the autoformalized subset. Also disclosed: 7 problems concern Sidon sets (Bloom's own favourite topic), so a single Sidon insight could in principle answer all seven; several problems (#172, #431, #500, #508, #952, #970) are not originally Erdős's; selection criterion was "worthy of a paper in a high-level journal" if solved by a human, with no target count and no difficulty ceiling. Bloom notes he has previously criticised erdosproblems.com as a benchmark because difficulty varies hugely and many AI-solved problems were obscure; his exceptions are #90 (unit distance), #146 and #183, famous problems with long partial-result histories.

Comparator, as used. Every attempt is split across two Docker containers, neither with network access: an agent container (full shell) and a comparator container with a pristine Lean toolchain. Only the submission's Lean source leaves the agent container. Comparator compiles the submission in a Landlock OS sandbox with the verdict computed outside it, and accepts only if the theorem statement and every declaration the statement depends on are identical to the trusted copy, only the three standard axioms appear (sorry fails via sorryAx; native_decide fails via Lean.ofReduceBool), and the whole submission replays through the kernel from scratch (defeating debug.skipKernelTC, metaprogramming that inserts declarations, and buggy tactics emitting ill-typed terms). What stays trusted: the Lean kernel, Comparator and its sandbox. Six attack classes are enumerated; see Kernel-Level Proof Auditing for how this sits against SafeVerify and #print axioms.

The agent. Inspect's deepagent (bash, text editor, a time/token budget tool, plus subagent delegation, persistent memory and a todo list); a Lean 4 + Mathlib toolchain with SageMath and Python (sympy, mpmath, numpy, pantograph); an offline snapshot of 476,000 pure-mathematics arXiv papers to 2022 (the arXiv subset of proof-pile). Limits: $300 and 72 hours. Both the deepagent and the literature snapshot made no difference to accuracy on OEIS Open Benchmark versus a minimal ReAct agent; they are kept here "as future models may be able to make better use of them."

Additional limitations stated. FME scores may "substantially underestimate" mathematical ability (formalization cost, missing Mathlib prerequisites); no credit for showing a conjecture implies a famous open problem such as Collatz; a conjecture could be independent of the axioms (task unsolvable); and resolved conjectures will leak into training data, with the no-proof-as-of-August-2026 immunity as the stated basis.

The five solutions, in brief (Appendix B; the paper warns they are not yet "digested" by human experts and the informal write-ups on erdosproblems.com are placeholders):

• #1 (dissociated sets, dating to 1931): disproof of N >> 2^n; for any epsilon there are arbitrarily large n with a dissociated set in {1..N}, N <= epsilon * 2^n. Ineffective (no bound on n in terms of epsilon), by linear algebra on rational n x n matrices with determinant -> 0; Bloom re-derived it in terms of lattices. Prior best: 0.22002 * 2^n (Bohman). The two disproofs are judged essentially the same.
• #74: there is f(n) -> infinity such that any graph whose n-vertex subgraphs are bipartite after deleting at most f(n) edges has chromatic number at most 3; elementary, inductive, seems to work for f(n) ~ log n / log log n (the Lean statement is only existence). Six disproofs, three distinct arguments.
• #126: |S(A)| >> n^(1/2), far stronger than the asked-for |S(A)|/log n -> infinity; three distinct elementary proofs with exponents 1/8, 1/3 and 1/2 out of four.
• #548 (Erdos-Sos tree conjecture, 1962): a full proof, "surprisingly short and elegant", by double counting orderings of the vertices.
• #571: every rational alpha in [1,2) is an extremal-number exponent for some bipartite graph; in Bloom's opinion the hardest of the five, and its relation to the substantial existing literature is unassessed.

The paper also rules against an easy reading of "solved": the AI proofs are machine-verified but unread, and "the impact of these results on mathematics will depend on human experts understanding the solutions."

Related-work corrections to this page's other comparisons. DeepMind's 9 resolved statements (of 353 formalized Erdős statements) span seven problems, four unambiguously resolved (#152, #846, #125, #26); #741 is marked solved on erdosproblems.com but only under an interpretation of "density"; #12 was settled in two of three parts and #138 only via a variant, and both remain open. So "9/353" counts statements including variants and sub-parts, not 9 problems. The paper also places the benchmark against HorizonMath (101 problems), FM:OP (50 problems, 10-40% estimated unsolvable, two removed in July 2026 for verifier fidelity), OEIS Open, LeanEval (the Lean FRO's leaderboard, also scored by Comparator) and First Proof (natural-language proofs by 30 referees; in round two 7 of 10 problems got at least one passing grade across four AI systems), with the objection set already recorded on OEIS Open Benchmark.

Reconciling with DeepMind's 9/353#

The wiki already carries an Erdős solve count — 9 of 353 attempted from the Formal Conjectures repo, by AlphaProof Nexus at "a few hundred dollars" per problem. That number is not superseded: it is a different item set, a different protocol and a different question, and both remain live.

	DeepMind (2026-05)	FrontierMath Erdős (2026-09)
Item set	353 attempted from Formal Conjectures, unfiltered for significance	68 hand-picked by Bloom as significant and difficult
Rate	9/353 = 2.5%	2/68 = 2.9%
Budget	"a few hundred dollars" per problem, excluding the cost of finding tractable problems across all 353	$300 and 72 hours, one attempt, every problem attempted
Verifier	SafeVerify (compiles, no sorryAx)	Comparator (Lean FRO, cheat-resistant)
Reporting	a list of what was solved	a score with a denominator

The rates look alike and are not. Two things pull in opposite directions. Epoch's denominator is deliberately harder — Bloom's significance filter, against a set Epoch describes as containing many problems that "never attracted much attention… and eventually proved easy to solve with a modest effort." But Epoch's protocol is also stricter in the direction that matters for cost: DeepMind's per-problem figure excludes the search cost of finding which problems were tractable at all, and that is exactly the cost a fixed one-attempt-on-every-item protocol forces you to pay — visible here as the ~$20,000 total for 68 problems yielding two solves. The right summary is that the two numbers agree on magnitude (low single-digit percent) while measuring different mixtures of problem difficulty and search cost, and that FrontierMath Erdős is the first of the two whose number can be compared against a later model's without re-deriving what was attempted.

The same evaluator's other number: 30% on 492 open conjectures (OEIS Open, 2026-08)#

Six weeks before this announcement, its own first author published OEIS OPEN (OEIS Open: How many conjectures can language models turn into theorems?, arXiv 2608.11941, 2026-08-12, empirical): 492 open OEIS conjectures formalized in Lean, $50 per conjecture, every item attempted by every model — Claude Opus 4.8 resolves 147 of 492, 30%. Ten times this page's rate at a sixth of the budget, from the same organization, the same author, and the same prove-or-disprove-under-a-kernel standard.

The two do not conflict; read together they isolate the curation axis. Everything else is held roughly constant — Lean formalization, prove-or-disprove, a fixed dollar cap in the score's definition, an open harness, 2026 frontier models. What differs is how the items were chosen:

	FrontierMath Erdős	OEIS Open
Items	68, hand-picked by Bloom as significant and difficult	492, from a Gemini prompt for problems "non-trivial, mathematically interesting, not famous open problems"
Budget	$300 / 72h, one attempt	$50 / 72h, one attempt ($200 on the 100-item LITE subset)
Best score	2/68 = 3% (pre-release GPT-6 Astra)	147/492 = 30% (Claude Opus 4.8)
Checker	Comparator	SafeVerify, cross-checked by Comparator (→ 144/492)
Attention on items	Erdős problems, catalogued and studied	47% of entries list no references; 451/492 sequences have zero OpenAlex citing works

So "how many open problems can AI resolve" has no answer without naming the selection procedure, and the gap between the two procedures is an order of magnitude in solve rate at a sixth of the spend. This is the strongest argument in the corpus for this page's curation step — and equally the strongest warning that a headline percentage on open problems means nothing until someone states who chose the problems and against what bar. It also reframes the Fisher-exact caveat above: the 2-vs-0 difference this page cannot resolve is not a measurement failure but a consequence of running a hard denominator, and Epoch's own easy denominator shows what the same instrument looks like when the items move.

Three transfers between the two. OEIS Open partially discharges this page's budget-scaling open question — its spend curve rises roughly log-linearly at about ten percentage points per tenfold increase with no plateau at $200 — but at a 30% base rate, so it says little about the 3% regime. It supplies the cost-ladder contrast directly: $6–$10 average per resolved conjecture with a $47 maximum, against this page's $172–$1,384 per solve and ~$67,000 marginal. And it sharpens the misformalization concern rather than easing it: this page's residual is 18 of 68 AI-formalized statements reviewed only by non-experts; OEIS Open's is all 492, autoformalized by a Gemini agent and taken as-is with no further validation, defended only on the relative ground that misformalizations probably do not favour one model over another.

What "formalization ability" hides on the other side: statement fidelity (2026-09-29)#

This page's cost accounting is about proofs that fail to compile. SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization (empirical) measures the opposite error on generated statements: the best agent compiles 61.8% of 178 hard Lean problems but only 11.2% are aligned with the intended theorem, so a compiled formalization of an informal problem is not evidence the intended statement was proved. It bears here indirectly. The 68 statements are given (50 from Formal Conjectures, 18 AI-produced and not yet expert-reviewed, the subject of the first open question below), so this failure concerns the formalization step behind the benchmark, not the agents' proofs; the method (forward and backward implication checks against shadow theorems) is what a review of those 18 would use. Detail on Kernel-Level Proof Auditing.

Connections#

• Kernel-Level Proof Auditing — why the Comparator row in the table above is not a formality: the weaker check it replaces (compile, then grep the source for sorry) admits sorryAx-dependent proofs at a measured 31–44% rate for one released prover on PutnamBench

• Logical vs Intelligible Proof — the argument that a scored count of certified answers measures the wrong property, and the "easiest to benchmark and automate away" warning aimed at denominators like this one. It also names what this page's Erdős-90 datum actually is: one result existing as two artifacts, 18 pages and 1.2 million lines, of which only one is readable

• AI-Driven Formal Proof Search — the paradigm this benchmark scores, and the page whose 9/353 this reconciles with rather than replaces; the formalization-tax datum (18 pages → 1.2M lines of Lean, cause stated as mathlib coverage) is that page's vocabulary bottleneck priced on a completed formalization

• AlphaProof Nexus — the system behind the 9/353, and the protocol contrast: per-problem cost excluding the search for tractable problems, versus a fixed budget spent on every item

• Compute-Controlled Benchmarking — the clearest instance in the corpus of that page's prescription taken to its conclusion: the budget is not disclosed alongside the score, it is the score's definition, and off-protocol runs at larger budgets are published and explicitly refused the label

• Expenditure Horizon — the other 2026 dollar-denominated capability measure, and the opposite corner of the same design space: METR needs smooth returns and a human-returns curve, which open Erdős problems cannot supply, so this benchmark reports a solve count at a fixed budget plus a per-solve cost distribution where METR reports a crossing point

• Benchmark Contamination and Decontamination — a third form of prevention-by-construction: items with no answer anywhere to leak, immune until they are solved, with post-hoc denominator filtering as the stated succession plan

• Latent Capability Overhang — the measured version of that page's thesis inside one model: 2/68 at $300 per attempt, 5/68 at unbounded budget and repeated attempts, for over $220,000; and the page's worked example gets a number, since the unit-distance conjecture is Erdős problem 90

• The Navier–Stokes AI Claim — the same month's undisciplined counterpart: no denominator, no budget cap, no published verification standard, a model the vendor says is a generation past the one scored here, and a claimed 17-hour Lean formalization against this page's measured 1.2-million-line one

• Many-Agent Proof Harnesses — the branch that declines to formalize, and whose best argument is this page's first caveat: formalization is "an entirely separate project, bolted on," priced at 1.2 million lines for an 18-page proof

• Large-Scale Test-Time Compute — the cost ladder read as an inference-scaling curve on open research problems, and the one Epoch says nobody has measured systematically yet

• OEIS Open Benchmark — the same author's other 2026 open-problem benchmark and this page's calibration partner: 492 OEIS conjectures selected to exclude famous problems, $50 each, 147/492 = 30% against this page's 2/68 = 3%. Also the checker datum this page's Comparator choice now has: re-running SafeVerify-accepted submissions through Comparator moves a score by three conjectures in both directions

• Epoch AI — the benchmark's author

• Lean — the formalization target; Comparator is the cheat-resistant checker layered on it

• Statement Drift — where this page's 18 autoformalized statements and Bloom's fidelity review sit: Comparator guarantees the proof matches the trusted copy, and only the curator's read guarantees the copy is the Erdős problem

Open Questions#

• Do the 18 AI-produced formalizations survive expert review — and are any of the five solved problems among them? Epoch states the 18 passed only its own initial review by self-described non-Lean-experts, with expert review "in process," and never says which subset the solves came from. A misformalization inside the solved set would turn a headline into an artifact; one outside it would leave the score intact and the denominator soft. Extended 2026-09-29 by FLT: Anthropic has beaten me to it (case-study): a contrasting case where the statement was expert-read: Buzzard states he checked that the FLT statement matches the theorem, and that this is the one part the machine cannot check. Says nothing about Epoch's 18. Extended 2026-09-29 by Long-horizon autoformalization of a core theorem underlying MIP* = RE (case-study): the second contrasting case, and the first where expert review changed the formal statement: a coauthor of the source paper audited the top-level theorem and gap resolutions, and 25 gap notes led to corrections of two errors in the published statement and three in the error budget (final bound preserved). It also shows why unreviewed AI formalizations are risky: agents produced tautological aliases and conclusion-inlined hypotheses that compiled. Still nothing on Epoch's 18. Partially answered 2026-09-29 by FrontierMath Erdős (empirical): the statements were not left unreviewed — Bloom reviewed each of the 18 autoformalized conjectures (17 problems) for fidelity to the original problem — but he is the curator, not a Lean-formalization auditor, and the paper does not say whether any of the five solved problems is among the 18. Two questions remain: an independent Lean-expert review, and the provenance of the five solves.

• How does the solve count actually grow with budget per attempt and with number of attempts? Epoch names this as future work and its own off-protocol data is the uncontrolled version: 5 solved, 269 172 fruitless attempts (paper's recount), >$220,000 against ~$20,000. The falsifiable form: run the same model on the same 68 at $300 / $1,000 / $3,000 with k attempts each and check whether coverage climbs log-linearly, as it does on closed benchmarks with a verifier, or hits a ceiling set by which problems are reachable at all. Partially answered 2026-09-23 by OEIS Open: How many conjectures can language models turn into theorems?, on a different item set. OEIS Open runs exactly this measurement — solve rate against per-sample spend at the moment of solve, across eight runs, two budget caps and five models — and finds it roughly linear in log-spend at about ten percentage points per tenfold increase, with no visible plateau at the $200 cap; within one model, Claude Opus 4.8 goes 30% at $50 to 39% at $200, and Epoch projects ~216 of 492 at $200 against 147 measured at $50. So on some open-problem set the curve is log-linear rather than ceilinged, which is the first evidence either way. Three reasons it stays open here: the base rate is 30% rather than 3%, so the slope is measured entirely in a regime this benchmark never reaches; the spend axis is reconstructed from when a solve happened inside a capped run rather than from independent runs at different caps, and the paper flags the bias itself (agents are told their budget, which may change their behaviour); and the number-of-attempts axis is untouched — OEIS Open is one run per model per configuration, so the k-attempts half of this question has still never been run.

• Does the post-hoc contamination correction keep scores comparable, or does the usable denominator shrink faster than capability grows? Epoch's plan is to filter problems solved before a model's cutoff and compare on the remainder. Trigger event: the first model run against this set after solutions to some of the 68 have been published.

• Do the five AI proofs survive human digestion, and are #1 and #571 genuinely new? The paper says the proofs are kernel-verified but "not yet digested", and that the relation of the #571 proof to existing work "will take some time". Falsifiable by the human write-up the authors promise, or by a literature match. Trigger: the first refereed exposition of any of the five.

Sources#

• On the Navier–Stokes Millennium Prize Problem — OpenAI (no byline), openai.com, 2026-09-08 with a 2026-09-10 update, ~1,900 words, vendor-claim. Cited here for exactly two claims, both quoted from prose: the 17-hour Lean formalization "via GPT‑6 Astra", and the internal model being "significantly more capable than GPT‑6 Astra" as of a training start of 2026-08-28. Neither is checkable — the linked proof PDF and Lean repository were not fetched, the model is unreleased, and the result is disputed. Used to bound this page's numbers, never to adjust them. Full treatment on The Navier–Stokes AI Claim
• Announcing FrontierMath Erdős — Tom Adamczewski and Greg Burnham (Epoch AI), "Announcing FrontierMath Erdős", epoch.ai, 2026-09-01, ~2,250 words, empirical. A web article, not PDF-derived: its two tables are transcribed from real HTML tables and both are quoted in full above. What the tier rests on and where it is thin. The measurement is real and the harness and item list are open-sourced, but three things bound it: the headline model is a pre-release GPT-6 Astra, so the number nobody outside Epoch can reproduce is the only non-zero one, and the pre-release access implies a lab relationship the announcement does not describe; the companion paper (epoch.ai/files/frontiermath-erdos.pdf), which carries the per-solution summaries and the full method, is not in this corpus — everything here comes from the announcement; and the scored run is one attempt per problem, so 2/68 versus 0/68 is two events (Fisher exact p ≈ 0.50 two-sided), a statistical caveat the announcement does not make. Epoch is an independent evaluator rather than a model vendor, and it disciplines itself in the direction that costs it a headline — the >$220,000 off-protocol run that reaches 5/68 is published and explicitly refused the label of a score, which is the opposite of benchmark-maxxing. Erdős problem numbers (1, 74, 90, 126, 548, 571) are Bloom's erdosproblems.com numbering
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), "OEIS Open: How many conjectures can language models turn into theorems?", arXiv 2608.11941, 2026-08-12, 27pp, empirical. Same first author as this page's primary source and six weeks earlier. Cited here for the 492-conjecture denominator and its selection prompt, the $50/$200 caps, the 147/492 and 144/492 scores, the per-solve cost range, the log-linear spend curve, and the item-attention metadata. PDF-derived; every number above is from prose or a figure image, and its single table is reconciled against pdftotext -layout but cited nowhere. Full treatment on OEIS Open Benchmark
• After Math — De Toffoli & Duede, "After Math", guest post on Terence Tao's blog, 2026-09-12, ~2,000 words, practitioner-opinion. Cited here for the benchmarkability warning, the answer/solution distinction and the mathandai.org declaration (25 Fields Medallists, "severe misalignment"). The post never mentions FrontierMath, Epoch AI or this benchmark — it is aimed at OpenAI's announcement and at disciplinary norms generally; the application here is this wiki's. No measurement of any kind; the declaration itself was not fetched. Full treatment on Logical vs Intelligible Proof
• FLT: Anthropic has beaten me to it — Buzzard, 2026-09-04, case-study. Cited only for the statement-review contrast in the open question.
• Long-horizon autoformalization of a core theorem underlying MIP* = RE — Lu, Deng, Zhu & Ji, arXiv 2609.19814 v2, 2026-09-17, case-study. Cited only in the expert-review open question, for the audited-statement contrast. Full note in wiki/sources.md.
• FrontierMath Erdős — Tom Adamczewski (Epoch AI) and Thomas F. Bloom (University of Manchester), "FrontierMath Erdős", arXiv 2609.25050, 2026-09-06, 12 pp, empirical (tier kept). PDF-derived; every number above is from prose, captions or Table 1-3 read against the prose (Table 3 row #126 holds four per-attempt costs in one cell, a real list and a false-positive collapse warning, confirmed against the prose's "four proofs of #126"). Table 4 (the 68 one-line statements) is cited nowhere row-by-row. Bloom is co-author, curator and reviewer of the autoformalized statements, so selection and statement review are not independent of the benchmark's authors; the announcement's figures for the same runs differ and are superseded above. Full compile note in wiki/sources.md.
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization — Han et al., arXiv 2608.29270, 2026-08-29, empirical. Cited here for one paragraph: 61.8% compile against 11.2% semantic alignment for generated Lean statements, and the forward/backward shadow-check method as the available review for the 18 AI-produced formalizations. Full treatment on Kernel-Level Proof Auditing.
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — Wang, Li & Yuan, arXiv 2609.34960, 2026-09-28, empirical. Cited for the library-removal paragraph only.