Announcing FrontierMath Erdős (Epoch AI, September 2026)

A benchmark announcement published September 12, 2026 by Tom Adamczewski and Greg Burnham of Epoch AI. It introduces FrontierMath Erdős, a set of 68 unsolved Erdős problems selected by the mathematician Thomas Bloom, formalized in Lean, and evaluated under a fixed protocol; and it reports initial results for five models. The stated purpose is to replace the informal use of Erdős problems as a capability signal with a protocol that fixes which problems are asked, what counts as a solution, and how much compute was spent.

What an Erdős problem is, and why the set needed curating

The phrase covers any problem posed by Paul Erdős (1913–1996), who posed many hundreds. Bloom began cataloguing them in 2023 at erdosproblems.com, which at the time of writing held 1,217 problems, of which 652 remain unsolved.

Epoch's first objection to the informal practice is that the label implies a uniformity it does not have. Some Erdős problems attracted little attention and proved easy; others became central to subfields. Epoch's response was to ask Bloom to select his favourites among the unsolved problems on grounds of mathematical significance and difficulty. He selected 68, all open as of August 2026 and about 10% of the unsolved set at that time.

Epoch states twice that this is subjective, and quotes Bloom's own disclaimer from an earlier collaboration: "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."

Bloom separately estimated that something like 3–5 Erdős problems of this calibre had been solved by AI as of August 2026, which Epoch offers as a measure of how high a bar the set sets.

Verification and replicability

Natural-language proofs are labour-intensive to verify, which is an obstacle to evaluating models at scale. FrontierMath Erdős therefore requires a Lean proof or disproof. Epoch describes its own contribution here as minor and built on two existing projects: 50 of the 68 problems were already formalized in Google's Formal Conjectures project, and Epoch "directed AI to formalize the remaining 18." Those 18 statements are described as fairly simple and as having passed Epoch's initial review, with the qualification stated in the text: "we are not Lean experts, and so errors may exist." Additional expert review was being sought at publication; Epoch's benchmark hub later stated that "Bloom reviewed each autoformalized statement to verify that it faithfully represents the original problem" (Source: epoch.ai). Checking uses Comparator, a proof checker built by the Lean FRO and designed to resist a submission that actively tries to cheat. A footnote qualifies the soundness claim further: it holds so long as Lean itself has no relevant bugs, which Epoch says it surely does, while expecting false positives to be rare and recognisable.

The replicability contribution is disclosure. Epoch's stated complaint is that the most impressive results to date have come from inside AI companies that disclose little about which problems were attempted, with which models, under which scaffolds, at what compute cost. The full harness is open-sourced at github.com/epoch-research/LeanOpenProblems, with the problem sets listed in the repository, and each system is run by default with an inference budget of $300 per problem.

Stated limitations

Epoch names three.

Formalization is a separate project bolted onto the mathematics. A system capable of a research breakthrough may not be able to formalize it, and the effort may be large regardless. Epoch's illustration is drawn from a different problem: when an OpenAI model produced a resolution of the Erdős unit-distance conjecture (problem 90 on Bloom's site), the natural-language proof ran to 18 pages while a subsequent Lean formalization ran to 1.2 million lines of code, largely because a deep result the paper could cite had not been formalized in Lean's standard library and had to be derived from first principles. Epoch treats this as a limitation of any Lean-based benchmark over open problems.

Contamination will arrive over time. Epoch treats the benchmark as a classical public benchmark with no strong contamination guards, noting that solutions will be published and discussed and will eventually enter training data. The models evaluated have no internet access and are instead given an offline collection of mathematics papers plus tools including a computer algebra system. Epoch argues contamination is not yet a concern, since no solution to any of the 68 was known as of August 2026, and that it can be corrected for later by filtering problems solved before a model's training cutoff. It adds that negative results stay informative: a later model failing a problem an earlier model solved is a data point about capability.

Erdős problems are not all of mathematics. Epoch expects progress here to correlate at least somewhat with general mathematical capability but states the inference "is not airtight."

Initial results

Five models were run, each with one attempt per problem at a budget of $300 and 72 hours of working time. A problem counts as solved when the model produces a Lean proof or disproof that passes verification.

Only Astra solved anything: 2 of 68. It disproved problem 74 by counterexample at a cost of $222 and 10 hours, and proved problem 126 at $172 and 10 hours. Every other attempt by every model exhausted its budget without a verified proof. The claim is scoped to these five models; Bloom's own 3–5 estimate indicates AI solutions to comparable problems predate the benchmark.

Both the benchmark run and the additional attempts below used a pre-release version of GPT-6 Astra supplied by the developer, the same arrangement under which Epoch's other Astra figures were produced.

The additional attempts, which are not a score

Separately from the benchmark, Epoch made further and less systematic attempts on the same problems with the same pre-release Astra, using larger budgets and varying agent setups. It states three times — in the text, in bold, and in an italicised repetition under the results table — that these are not a FrontierMath Erdős score, because the protocol differs: budgets were larger, the setup varied, and problems were attempted different numbers of times. Astra's score remains 3%.

Epoch reports them anyway on two grounds: a solution to such a problem is of mathematical interest however obtained, and repeated attempts give some sense of run-to-run variance.

Across all attempts Astra solved 5 of the 68 at least once — the two above, plus problem 1 disproved and problems 548 and 571 proved.

The denominator is published alongside the numerator. Most of the remaining 63 problems were attempted between two and six times — 269 attempts in total — and none was solved. Reaching the five solutions took over $220,000 of compute across all attempts, against roughly $20,000 for the benchmark run that produced two of them. Per-solution cost varies by more than an order of magnitude, and so does reliability: problem 74 was solved on 7 of 7 attempts, problem 548 on 1 of 4.

That pairing of cost and denominator answers directly the objection Ernie Davis raised against OpenAI's announcement of ten mathematical advances — that a count of successes without the number of attempts, and a cost figure covering successes only, cannot support an inference about capability (OpenAI's amazing — but vastly oversold — new model Astra (Marcus, August 2026)). Epoch publishes attempts, failures, per-solution cost, and total cost including failures.

Brief summaries of the five solutions are in a companion paper (Source: epoch.ai), which is not held here.

Epoch's own reading

The concluding assessment is deliberately bounded: "in this scaffold, at this budget, Astra solved about 3% of problems from this list of significant open math problems." Epoch reads that as a data point on the prevalence of AI-driven mathematical breakthroughs — "real but still fairly uncommon" — and writes that while it is notable that any problem of this calibre can be solved by AI, "it is not yet the case that AI has a particularly high chance of solving an arbitrary such problem — at least not if it has to formalize the result within a budget of $300 per problem." It defers judgement on the nature of the five solutions to mathematicians who have yet to read them.

Provenance

Published at epoch.ai on September 12, 2026; captured complete September 14, 2026. The publisher's page metadata carries September 1, 2026, while the Epoch Brief that carried the announcement and the digest that named it both place it on September 12; the later date is used. Adamczewski founded Epoch's benchmark engineering team; Burnham is its head of benchmarks. The benchmark page is at epoch.ai/benchmarks/frontiermath-erdos and the harness at github.com/epoch-research/LeanOpenProblems.

Relationships

• supports: AI Benchmarks and Evaluation — a worked case of replacing a saturated benchmark with harder items and publishing the evaluation protocol
• supports: Machine-produced mathematics: claims, verification and credit — supplies the attempt counts and costs that the company-internal results omit
• related: Astra — the only model to score above zero
• related: Epoch AI — publisher
• related: AI for Science
• related: Ten Advances in Mathematics and Theoretical Computer Science — the company-internal result whose disclosure practice this benchmark is a response to
• related: OpenAI's amazing — but vastly oversold — new model Astra (Marcus, August 2026) — the denominator and cost objections this benchmark's reporting answers