FrontierMath Erdős
Tom Adamczewski, Thomas F. Bloom
cs.CL · cs.AI
Quick verdict
Benchmark of 68 Lean-formalized open Erdős problems across five AIs; verification is rigorous but the 3%-vs-0% gap rests on one attempt per task — low power.
Summary
The paper introduces FrontierMath Erdős (FME), a benchmark of 68 conjectures — covering 65 Erdős problems, all open as of August 2026 — stated in Lean 4, where a task counts as solved only if the AI formally proves the conjecture or its negation. Problems were selected by the second author from 652 open problems on erdosproblems.com for interest and difficulty; 50 statements come from the Formal Conjectures repository and 18 were autoformalized in-house. Verification uses Comparator, a Lean-FRO checker that replays submissions through the kernel in an isolated container and rejects unpermitted axioms or statement tampering. Five models ran autonomously in a fixed harness (no network, offline arXiv corpus, 72 hours, $300 per attempt). Only a pre-release GPT-6 Astra solved anything, resolving 2 of 68 (3%): #74 by disproof and #126 by proof; the other four models (GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, Claude Fable 5) scored 0%. Non-systematic extra attempts raised GPT-6 Astra's tally to 5 of 68 for over $220,000 of total compute. Main limitations: one attempt per problem gives no variance estimates; a metering error meant the flagship model's budget tool displayed roughly half its true spend, weakening budget comparability; scores conflate formalization skill with mathematical ability; and single-curator problem selection is admittedly subjective.
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 2
● low 2
5 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- Requiring kernel-verified Lean proofs of open conjectures, graded by Comparator in an isolated sandbox, makes open-problem benchmarking definitive and cheat-resistant where generator-verifier benchmarks (HorizonMath, FM:OP) offer only evidence.
- Under one autonomous attempt per problem with a $300 and 72-hour budget, only pre-release GPT-6 Astra resolved any of the 68 conjectures (2 of 68, 3%); GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, and Claude Fable 5 each scored 0%.
- Across all additional attempts, GPT-6 Astra resolved 5 of 68 conjectures — including disproving #1, posed in 1931 — for over $220,000 of total compute versus roughly $20,000 for the benchmark run.
- These results establish under controlled conditions that a current AI system can autonomously resolve open problems whose human solutions would merit a paper in a high-level journal, while 63 of 68 remain open.
Strengths
Directly operationalizes Tao's five methodological criticisms
Section 1 fixes the problem universe in advance, reports all outcomes, discloses budgets, removes human scaffolding, and runs all models on identical problems — exactly the controlled conditions the 2026 ICM lecture argued were missing from ad-hoc announcements.
Verification is tamper-resistant and definitive
Section 3.3 enumerates six attack classes (environment tampering, compile-time code, statement substitution, dependency redefinition, sorryAx abuse, kernel bypass via debug.skipKernelTC or @[implemented_by]) and shows how Comparator's Landlock-sandboxed kernel replay defeats each; grading reduces to the Lean kernel, not per-problem verifier code.
Unusual transparency about its own flaws
Variance evidence from repeated attempts
Public, inspectable artifacts
Weaknesses
No statistical power behind the headline comparison
Budget integrity compromised for the flagship model
Single-curator selection with acknowledged bias
Scores conflate formalization with mathematics
Cost comparability is asymmetric
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
FrontierMath Erdős (FME) is a benchmark of 68 Lean-formalized conjectures covering 65 Erdős problems open as of August 2026, selected by the second author from 652 open problems on erdosproblems.com. The central claim is methodological: benchmarking open problems with formal-proof grading addresses five documented shortcomings of ad-hoc 'AI solves open problem' announcements — reporting bias, undisclosed costs, human scaffolding, cross-model incomparability (Section 1, citing Tao's 2026 ICM lecture), and contamination. Verification is definitive because an accepted proof replays through the Lean kernel (Section 3.3). Empirical claims: under one autonomous attempt per problem ($300, 72 hours), only pre-release GPT-6 Astra resolved anything — 2/68 (3%), problems #74 and #126 — while GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, and Claude Fable 5 scored 0% (Table 1). Non-systematic extra attempts raised GPT-6 Astra to 5/68 for over $220,000 of total compute (Table 3), versus roughly $20,000 for the benchmark run itself.
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is FrontierMath Erdős and how does it differ from the original FrontierMath?
FrontierMath Erdős (FME) is a benchmark of 68 open Erdős mathematics conjectures stated in the Lean proof assistant. Unlike the original FrontierMath, whose problems have known answers checked by programs, FME uses problems that are genuinely unsolved as of August 2026: an AI must produce a formal Lean proof of the conjecture or its negation, verified by the Lean kernel through the Comparator checker rather than a hand-written verifier.
Which AI models solved problems in the benchmark, and what were the scores?
In the controlled run ($300 and 72 hours per problem, one attempt each), only a pre-release version of GPT-6 Astra solved anything: 2 of 68 conjectures (3%) — problem #74, disproved by counterexample, and #126, proved. GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, and Claude Fable 5 each scored 0%. In additional, less systematic attempts with larger budgets, GPT-6 Astra solved 5 of the 68 in total, including disproving Erdős problem #1, which dates to 1931.
Can the AI solutions to open problems actually be trusted?
Yes in the narrow sense of formal correctness: every submission must replay through the Lean kernel inside an isolated sandbox via Comparator, which permits no axioms beyond Lean's standard three, rejects 'sorry' placeholders, and requires the proven statement and all its dependencies to match the trusted versions bit-for-bit. Whether the proofs contain genuinely new mathematical ideas is a separate human question the authors say is not yet settled.
How much did the evaluation cost?
The systematic benchmark run (68 problems x 5 models, up to $300 each) cost roughly $20,000. The additional non-systematic attempts with GPT-6 Astra consumed over $220,000 of compute in total; individual successful resolutions ranged from $47 (problem #74, cheapest of six) to $1,384 (one disproof of #1).
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- PDF extraction linearizes mathematical notation (superscripts and subscripts flattened, e.g. the Table 4 conjecture statements like N ≫ 2|A| for N ≫ 2^|A|); this affects display of informal statements but not the review's substance, and the full text including Appendices A-B and all references appears complete.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.