FrontierMath Erdős consists of 68 problems posed or studied by mathematician Paul Erdős. Problems are formulated in Lean and AI must write complete Lean proofs or disproofs. These problems are sourced from ErdősProblems.com. Thomas Bloom, the mathematician who maintains that website, helped us curate a set of 68 problems which he finds to be especially interesting and difficult. All of these problems were open as of August 2026, when we first formulated the benchmark. Bloom estimates that only 3–5 Erdős problems of this caliber had been previously solved by AI.

For more details, see the paper or the open-source repository, which contains the Lean statement of each conjecture and the evaluation scaffold.

The full methodology is described in the paper. In brief:

Problem selection. The problems were selected by Thomas Bloom from among the problems on erdosproblems.com, which he curates, that were open as of August 2026. They were selected to represent the most apparently difficult and interesting Erdős problems that remained open. A necessary condition was that the solution (positive or negative) to any of these problems would be, if produced by a human, worthy of a paper in a high-level journal, and be of interest to many people in the relevant field. The problems were selected to be independent, in the sense that solving any one of the problems (either positively or negatively) should not immediately yield another of the problems.

Lean statements. Each conjecture is a statement in Lean 4, using its mathematical library Mathlib. The benchmark’s 68 conjectures cover 65 distinct problems as numbered on erdosproblems.com: the Hadwiger–Nelson problem (#508) is represented by three conjectures, one for each candidate value of the chromatic number of the plane, and the two parts of #713 are separate conjectures. The statements of 50 of the 68 conjectures (covering 48 problems) are taken from Formal Conjectures, an open-source library of formalized open problems maintained by Google DeepMind. The remaining 17 problems had no statement in Formal Conjectures. We formalized these ourselves using an autoformalization pipeline, and Bloom reviewed each autoformalized statement to verify that it faithfully represents the original problem.

Proof verification. A model resolves a conjecture when it submits a proof of the conjecture or of its negation that passes verification. We accept a submission only if it passes Comparator, a proof checker maintained by the Lean FRO, the organization that develops Lean. Given our trusted Lean statement of the conjecture and the untrusted submission, Comparator compiles each in an isolated sandbox and accepts only if the submission proves the identical statement, using only permitted axioms, with a proof that replays through the Lean kernel. Every attempt is split across two Docker containers, neither of which has network access: an agent container, where the model works on its proof and has full shell access, and a comparator container, holding a pristine Lean toolchain, where Comparator checks the submission. What remains trusted is the Lean kernel, Comparator itself, and its sandbox.

AI agent. Our agent is built on deepagent from the Inspect evaluation framework. The model is given bash, a text editor, and a tool reporting its remaining time and token budgets; deepagent adds delegation to subagents, persistent memory, and a todo-list tool. The agent container provides a Lean 4 toolchain with Mathlib, the SageMath computer algebra system, and Python with sympy, mpmath, numpy, and pantograph. Because the container has no network access, we provide an offline snapshot of the mathematics literature: the LaTeX source trees of 476,000 pure-mathematics arXiv papers dated up to 2022.

Each problem is attempted once by the agent. During an attempt, the agent iterates until it either resolves the conjecture, or hits one of two limits: $300 of spend and 72 hours of working time. Accuracy is the fraction of the 68 conjectures resolved; error bars are ±1 standard error. Spend is metered at each model’s standard API prices. Where a model’s prices were not published at the time of evaluation, we recompute the cost of every attempt at the actual prices after the fact, and count a conjecture as resolved within the budget only if its resolution cost at most $300 at those prices (see the paper for details).

Data contamination. Once a conjecture is resolved, whether by an AI system or by a human mathematician, its proof may enter the pretraining data of future models. No proof of any of the 68 conjectures was known as of August 2026, so a model whose training cutoff predates that date cannot have learned one. For future models, conjectures resolved before a model’s training cutoff can be filtered out, and all models compared on the remaining smaller set.