FrontierMath Erd\H{o}s

• Earlier demonstrations leave success rates, costs, human guidance, contamination, and systematic comparisons across models unclear.The paper identifies these as shortcomings of the available evidence on AI mathematics.Source: §1 · p. 1
• FME evaluates the same open problems autonomously under a fixed, published harness and shared conditions, addressing controlled comparison and reporting concerns.The paper says this makes it possible to compare models and track capability trends over time.Source: §1 · pp. 1–2
• Existing open-problem benchmarks focus on concrete objects that are hard to find but cheap to check, excluding most problems asking for general proofs.Their computational verification can also produce false positives and false negatives.Source: §1 · p. 2
• Each FME conjecture is stated in Lean, where a model must prove it or its negation; accepted proofs provide definitive verification.Eligibility requires a formalizable statement rather than a computationally checkable solution object.Source: §1 · p. 2
• Open problems prevent reproducing an exact known result, but their solutions may still repackage existing ideas, making novelty difficult to assess.The paper notes that expert attention may be needed to distinguish significant new ideas from repackaging.Source: §1 · p. 2

• Generator–verifier benchmarks cannot cover most general proof problems, and their checks provide evidence rather than proof while relying on hand-crafted code and filters.Some tasks may also be unsolvable when no object of the required form exists.Source: §2 · pp. 2–3
• FME accepts formal proofs of conjectures or their negations, broadening eligibility beyond checkable objects and avoiding per-problem verification code.Accepted proofs are definitive, and false conjectures remain solvable through proofs of their negations.Source: §2 · p. 3
• FME covers only statements expressible with Mathlib definitions, and scores reflect formalization ability as well as mathematical ability.A model may need to recreate standard results missing from Mathlib before formalizing an argument.Source: §2 · pp. 2–3
• Other formal benchmarks include statements of uncertain mathematical significance or sets determined by prior formalization rather than curation for mathematical interest.The paper contrasts these choices with FME’s curated problem selection.Source: §2 · p. 3
• First Proof uses already-solved research problems and manual expert review, accommodating problems that resist formalization but requiring subjective, repeated grading.Its referees assess more than correctness, including novelty, exposition, and citation accuracy.Source: §2 · p. 3

3.1 Problem selection

• 3.1 Problem selection: Problems were chosen for apparent difficulty and interest, with human solutions expected to merit high-level journal papers, though selection is subjective.The collection aims to identify in advance problems whose solutions may have substantial impact.Source: §3.1 · pp. 3–4
• 3.1 Problem selection: Selection had no target count or difficulty ceiling; problems were intended to be independent, despite topic bias and possible links among Sidon-set questions.The collection includes problems both with and without Erdős prizes, and omits some with large prizes.Source: §3.1 · p. 4

3.2 Lean statements

• 3.2 Lean statements: Fifty conjecture statements came from Formal Conjectures, while the remaining 18 were formalized by the authors; Hadwiger–Nelson is represented by three mutually exclusive conjectures.The author reviewed the newly formalized statements, and the Hadwiger–Nelson answer is known to be among 5, 6, or 7 if unambiguous.Source: §3.2 · p. 4

3.3 Proof verification

• 3.3 Proof verification: Comparator accepts only an identical theorem statement that replays through the Lean kernel using permitted axioms, with sandboxing and checks against tampering.The trusted components are the Lean kernel, Comparator, and its sandbox.Source: §3.3 · p. 5

3.4 AI agent

• 3.4 AI agent: The agent has Lean, Mathlib, computational tools, and an offline mathematics-literature snapshot, and each default attempt stops at $300 or 72 hours.Deepagent and the literature snapshot did not improve accuracy in OEIS Open relative to a basic ReAct agent, but remain in the default configuration.Source: §3.4 · p. 5

3.5 Limitations

• 3.5 Limitations: Formalization costs may understate mathematical ability; reductions to famous open problems receive no credit, and resolved conjectures may later leak into training data.The paper suggests filtering problems resolved before future models’ training cutoffs, leaving a smaller comparison set.Source: §3.5 · p. 6

4.1 Benchmark results

• GPT-6 Astra resolved 2 of 68 conjectures; the other four models resolved none.Table 1 reports scores for one attempt per conjecture under the default configuration.Source: Table 1 · p. 6, §4.1 · p. 6
• The cost correction excluded GPT-6 Astra’s disproof of #1, which cost $405 at actual prices, from the benchmark score.The harness initially metered spend at GPT-5.6 Sol prices; the authors recomputed costs using Astra’s actual prices.Source: §4.1 · p. 6

4.2 Additional non-systematic attempts

• Across the additional attempts, GPT-6 Astra resolved five conjectures; none of 172 completed attempts on 56 other conjectures resolved one.These attempts used larger budgets and varied agent configurations, and reaching the five resolutions took over $220,000 of compute.Source: §4.2 · p. 7, Table 3 · p. 7
• The additional-attempt resolutions included repeated results that the authors initially judged to contain distinct arguments: three for #74 and three for #126.They judged the two disproofs of #1 to be essentially the same; the assessment was preliminary and subjective.Source: §4.2 · p. 7
• The additional attempts are not comparable benchmark scores because budgets, agent configurations, and numbers of attempts varied.Table 3 summarizes resolutions across these non-systematic attempts, unlike the fixed-protocol results in Table 2.Source: Table 3 · p. 7, §4.2 · p. 7

5 Discussion and conclusion

• Only GPT-6 Astra showed the ability to resolve conjectures in the benchmark, and 63 of the 68 conjectures remain open.The authors characterize this capability as both new and limited.Source: §5 · p. 7
• The authors call for systematic study of how resolutions grow with the budget per attempt and the number of attempts.They note that additional attempts found more resolutions, but were not systematic.Source: §5 · p. 7
• FME evaluates solving selected problems, not finding them, and the impact of its results depends on human experts understanding the solutions and ideas.The authors say this work has only begun.Source: §5 · p. 7
• Some additional attempts were not counted because ad-hoc experiments and infrastructure failures prevented every conjecture from being attempted equally often.The note specifies that failed attempts terminated before a verdict are not counted.Source: §5 · p. 7

A List of benchmark problems

• The 68 conjectures represent 65 distinct problems, with three conjectures for Hadwiger–Nelson and separate entries for the two parts of #713.For problems #208, #812, and #1206, the list includes only the part named in the ID.Source: A List of benchmark problems · p. 8
• The list pairs benchmark IDs with informal conjecture descriptions; each ID links to its erdosproblems.com entry, while the Lean statement is authoritative.The Lean statements are available in the benchmark repository.Source: A List of benchmark problems · p. 8, Table 4 · p. 8
• Examples include geometric conjectures about integer distances and convex polygons, and number-theoretic conjectures about Carmichael numbers and prime factors.The list also includes conjectures on graph properties, Ramsey numbers, and additive sets.Source: A List of benchmark problems · pp. 8–9

B Summary of AI solutions

• The appendix briefly discusses the five problems GPT-6 Astra solved.More in-depth, informal expositions by the second author are available on the corresponding problem pages.Source: B Summary of AI solutions · p. 9
• Formalization supports confidence that the proofs are correct, but the solutions have not yet been properly digested.The authors call the informal expositions placeholders until human experts prepare a traditional paper with full details and context.Source: B Summary of AI solutions · p. 10

B.1 Disproof of #1

• A set is dissociated when its subset-sum map is injective, and the conjecture asked whether size-n sets in {1, . . . , N} require N ≫ 2^n.Erdős posed the problem in 1931; the paper describes it as probably the longest-standing open Erdős problem.Source: §B.1 · p. 10
• GPT-6 Astra’s counterexample disproves the conjecture; the previous best bounds were N ≤ 0.22002 · 2^n and N ≫ 2^n/√n.The upper bound was due to Bohman, and the lower bound was first proved by Erdős and Moser.Source: §B.1 · p. 10
• The proof uses linear algebra to construct rational matrices with determinants tending to zero, then uses their properties to build large dissociated sets.The AI proof is currently ineffective: it gives no bound on how large n must be for a given ϵ.Source: §B.1 · p. 10

B.2 Disproof of #74

• This result answers the question of whether slow growth in the edge-deletion bound can coexist with infinite chromatic number: sufficiently slow divergence rules that out.Erdős, Hajnal, and Szemerédi had suspected that such an infinite-chromatic example existed.Source: §B.2 · p. 10
• If every finite subgraph on n vertices can be made bipartite by deleting at most f(n) edges for some f(n) → ∞, then the graph has chromatic number at most 3.The theorem applies to finite and infinite graphs.Source: §B.2 · p. 10
• The proof inductively removes edges to form graphs without short odd cycles, then transfers a carefully controlled 3-coloring back through the sequence.Compactness lets the argument assume the graph is finite; the terminal graph is bipartite and hence 2-colorable.Source: §B.2 · p. 10

B.3 Proof of #126

• For a finite set A, S(A) is the set of primes dividing sums a + b for distinct a,b in A.Erdős and Turán proved |S(A)| ≫ log n; Erdős later sought an improvement such as |S(A)|/log n → ∞.Source: §B.3 · p. 10
• GPT-6 Astra gave three distinct proofs that |S(A)| ≫ n^c, with c equal to 1/8, 1/3, and 1/2.The proofs use elementary methods, are reasonably short, and appear distinct.Source: §B.3 · p. 11
• The bound |S(A)| ≪ n/log n is attainable, as shown by taking A = {1, . . . , n}.This supplies an upper comparison for the lower bounds proved by Astra.Source: §B.3 · p. 11

B.4 Proof of #548

• The conjecture states that the same edge threshold forces every tree on k vertices, whereas the weaker threshold (k−2)n was easy to prove by induction.Erdős and Sós proposed the conjecture in 1962.Source: §B.4 · p. 11
• For n ≥ k, every graph on n vertices with more than (k−2)n/2 edges contains every tree on k vertices.This is the full Erdős–Sós conjecture, which had remained open despite proofs of many special cases.Source: §B.4 · p. 11
• The proof counts vertex orderings and labels where the first vertex is adjacent to the labeled vertex, then bounds that count inductively for a fixed tree.If the graph contains no copy of that tree, the tree-rooted count is zero, yielding the edge threshold.Source: §B.4 · p. 11

B.5 Proof of #571

• The problem asks which orders of growth are possible for ex(n; G), the maximum edge count before an n-vertex graph must contain G as a subgraph.The passage describes bipartite graphs as a less-understood case than graphs with chromatic number at least 3.Source: §B.5 · p. 11
• The proof establishes the full conjecture: for every rational α in [1, 2), some bipartite graph has extremal number ex(n; G) ≍ n^α.The paper identifies this as the solution to Erdős and Simonovits’s problem #571.Source: §B.5 · p. 11
• The second author considers this the most difficult of the five solutions and says understanding its relation to substantial existing work will take time.The author says proper human understanding of the AI proof will take some time.Source: §B.5 · p. 11