FrontierMath Erdős

Epoch AI launched FrontierMath Erdős, a benchmark of 68 unsolved problems selected by mathematician Thomas Bloom from his erdosproblems.com catalog, to rigorously track AI math capabilities. The benchmark addresses curation, verification, and replicability, with Bloom estimating that only 3–5 such problems had been solved by AI as of August 2026.

If you’ve followed AI math capabilities at all this year, you’ve likely heard of Erdős problems. Some of the first https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/ open math problems to be solved by AI were Erdős problems. The first unequivocal “wow” moment https://openai.com/index/model-disproves-discrete-geometry-conjecture/ for AI in math came on an Erdős problem. Erdős problems have become something of a central benchmark for tracking AI math capabilities, but this status is relatively informal. With our new math benchmark, FrontierMath Erdős /benchmarks/frontiermath-erdos , we aim to add some rigor when it comes to using Erdős problems to measure AI math capabilities. What is an Erdős problem? The phrase has come to mean any problem posed by the prolific mathematician Paul Erdős 1913-1996 . Most math problems closely associated with a specific mathematician are referred to as “a problem posed by so-and-so”, but Erdős was unusual for posing many hundreds of problems. In 2023, the mathematician Thomas Bloom began an effort to catalog all problems Erdős had ever posed, creating the website erdosproblems.com https://www.erdosproblems.com/ to do so. Bloom’s site currently contains 1217 problems, of which 652 remain unsolved. These problems were recognized as a possible proving ground for AI systems as early as early 2025 https://x.com/dsavitt/status/1895501573255823658 and by the end of 2025 https://www.erdosproblems.com/forum/thread/blog:1 :~:text=500%20registered%20users.-,The%20arrival%20of%20AI,-Soon%20after%20the such efforts had grown dramatically. Addressing curation, verification, and replicability This benchmark addresses three main issues. Curation: Erdős problems vary widely in mathematical significance and difficulty The name “Erdős problem” suggests uniformity — like “Millennium Prize Problem” — but this is not so. Many Erdős problems never attracted much attention from mathematicians and eventually proved easy to solve with a modest effort whether from humans or AI . Others have been studied extensively, becoming central to entire subfields of math. Tracking AI capabilities requires knowing the difference. Our contribution is simple: we asked Bloom to select his favorite unsolved Erdős problems, those which he believed to be both mathematically significant and difficult. He selected 68, all open as of August 2026 and about 10% of the unsolved problems at that time. This approach is highly subjective, even though Bloom is a well-regarded mathematician and highly familiar with the Erdős problems. When helping us curate our other benchmark of unsolved math problems, Bloom said, 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 same is surely true of these 68 Erdős problems, but we believe that even a coarse categorization is a marked improvement over the prior state of affairs. Bloom roughly estimated that something like 3–5 Erdős problems of this caliber had been solved by AI as of August 2026, so this sets a fairly high bar for AI solutions. Verification: solutions to Erdős problems are hard to verify In research math, humans present solutions as natural-language proofs. Verifying such natural language proofs is extremely labor intensive, which poses a challenge for evaluating AI systems at scale. One salient approach is to use Lean https://en.wikipedia.org/wiki/Lean %28proof assistant%29 , a specialized programming language for expressing mathematical proofs. Any proof written in Lean can be checked for correctness programmatically. So long as the problem statement is formalized correctly, we can be confident in the soundness of any AI solution which passes Lean’s checks. 1 user-content-fn-1 Our contribution here is minor, largely building on two existing projects. The first is Google’s Formal Conjectures https://github.com/google-deepmind/formal-conjectures/tree/main project, a collection of mathematical conjectures formalized in Lean. Of the 68 problems we include, 50 are already formalized as part of that project. We directed AI to formalize the remaining 18. These 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. The second is Comparator https://github.com/leanprover/comparator , a proof checker built by the Lean FRO, the organization that develops Lean, which is designed to be robust to a submission that actively tries to cheat. Replicability: the methods used to get AI to solve Erdős problems have been opaque How many people have tried to get AI to solve Erdős problems? Which problems did they try? Which AI models did they use? With what scaffolds? How much inference compute did they spend? We can’t expect comprehensive answers since anyone — hobbyist or mathematician alike — can take a crack at the problems. But, to date, the most impressive results have come from within AI companies, and these companies have not disclosed much about the experiments by which their results were obtained. Our contribution is one of transparency: we give a clear answer to these questions. The entire codebase for running the benchmark is open-sourced here https://github.com/epoch-research/LeanOpenProblems , with the main harness here https://github.com/epoch-research/LeanOpenProblems/blob/main/apn/solver.py and the 68 problems listed here https://github.com/epoch-research/LeanOpenProblems/blob/bloom-verdicts/apn/data/erdos/subsets/bloom selection.json and here https://github.com/epoch-research/LeanOpenProblems/blob/bloom-verdicts/apn/data/erdos autoformalized/subsets/bloom selection.json . By default we run each AI system with an inference budget of $300 per problem. We report on the specific models we have run to-date below. Caveats We highlight three limitations of FrontierMath Erdős. Formalization adds an additional burden for AI systems Making a breakthrough on an important math research problem is a tall enough order. Formalizing such a result is essentially an entirely separate project, bolted on. We may hope that an AI system capable of making a major math breakthrough can also formalize it, though this is certainly not guaranteed. But even if so, the effort to formalize it may be enormous. For instance, when an OpenAI model generated a resolution of the Erdős unit distance conjecture problem 90 https://www.erdosproblems.com/90 on Bloom’s website , the natural language proof was 18 pages long whereas a subsequent effort https://github.com/plby/Erdos90 that formalized the result in Lean consisted of 1.2 million lines of code. This was 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. This is a limitation of any Lean-based benchmark that asks AI systems to solve open problems. Data contamination will become an issue over time We will initially treat this benchmark as a “classical” public benchmark, where we run models as they are released and have no strong guards against data contamination. Solutions to any problem will likely be published and discussed, in some cases widely. The models we evaluate have no internet access — instead, they get an offline collection of mathematics papers, plus tools like a computer algebra system — but solutions will eventually make their way into training data. We plan to monitor to what degree this becomes a problem. For now, this is not a concern: 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. For future models, we can correct for contamination after the fact. Problems solved before a model’s training cutoff can be filtered out, and all models compared on the remaining problems. At very least, negative results should still be 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. Erdős problems aren’t all of mathematics As wide as Erdős’s interests were, math is much wider. This benchmark should not be taken as a sample from all fields of math. We expect progress on it to be at least somewhat correlated with general math capabilities progress, but this inference is not airtight. Initial Results We have so far run five models: a pre-release version of GPT-6 Astra, GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, and Claude Fable 5. Each model got one attempt at each problem, with a budget of $300 and 72 hours of working time per attempt. A problem counts as solved when the model produces a Lean proof, or disproof, that passes verification. | Model | Score | |---|---| | GPT-6 Astra | 3% | | GPT-5.6 Sol | 0% | | GPT-5.5 | 0% | | Claude Fable 5.1 | 0% | | Claude Fable 5 | 0% | Only GPT-6 Astra solved anything: 2 of the 68 problems. It disproved problem 74 https://www.erdosproblems.com/74 by finding a counterexample, at a cost of $218 and 15 hours of working time, and it proved problem 126 https://www.erdosproblems.com/126 , at a cost of $247 and 16 hours. All of its other attempts, and every attempt by the other four models, ran out of budget without a verified proof. Additional attempts Separately from the benchmark run, we made a number of further, less systematic attempts on the same problems with the same pre-release version of GPT-6 Astra, with larger budgets per attempt and with variations in the agent setup. These attempts are not a FrontierMath Erdős score. They do not follow the benchmark’s fixed protocol: budgets were larger, the agent setup varied, and problems were attempted different numbers of times. GPT-6 Astra’s FrontierMath Erdős score remains the 3% from the benchmark run above. We report the additional attempts anyway because any solution to one of these problems is of mathematical interest however it was obtained, and because repeated attempts give some sense of how much the outcome varies from one attempt to the next. 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. Across all attempts, GPT-6 Astra solved 5 of the 68 problems at least once: the two above, plus problem 1 https://www.erdosproblems.com/1 , which it disproved, and problem 548 https://www.erdosproblems.com/548 and problem 571 https://www.erdosproblems.com/571 , which it proved. Most of the remaining problems were attempted between two and five times in total 172 attempts , and none was solved. Reaching these five solutions took over $220,000 of compute across all attempts, compared with roughly $20,000 for the benchmark run itself. | Problem | Result | Solved in | Cost of each solution | |---|---|---|---| | 74 https://www.erdosproblems.com/74 126 https://www.erdosproblems.com/126 548 https://www.erdosproblems.com/548 571 https://www.erdosproblems.com/571 To repeat: the table above is not a benchmark result. The FrontierMath Erdős scores are the ones in the first table. Full details, including brief summaries of the five solutions, are in the paper /files/frontiermath-erdos.pdf . We will keep evaluating new models as they are released, and the latest results are on the FrontierMath Erdős benchmark page /benchmarks/frontiermath-erdos . Conclusion The most impressive AI math results have come from efforts internal to AI companies, but with fairly little transparency into how these results were obtained. We hope FrontierMath Erdős helps to clarify the situation. From its initial runs, we believe it is serving this purpose: in this scaffold, at this budget, Astra solved about 3% of problems from this list of significant open math problems. This provides a useful data point on the prevalence of AI-driven math breakthroughs: real but still fairly uncommon. While it is remarkable that any problem of this caliber can be solved by AI at all, 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. The nature of the AI solutions to these five problems will also be informative. For that, we’ll have to wait for mathematicians to digest and comment on the results. About the authors Tom AdamczewskiTom Adamczewski started Epoch AI's benchmark engineering team. He now works on developing new evals to measure economically important AI capabilities. Before Epoch AI, he created a Monte Carlo simulation application and worked on payments technology. /about/team/tom-adamczewski Greg BurnhamGreg Burnham is the head of benchmarks at Epoch AI. Prior to this, he worked at Elemental Cognition and Bridgewater Associates. He has a BA in mathematics from Princeton University. /about/team/greg-burnham