FrontierMath Erdős

# FrontierMath Erdős
Source: [https://arxiv.org/html/2609.25050](https://arxiv.org/html/2609.25050)
###### Abstract

We introduce FrontierMath Erdős \(FME\), a benchmark of 68 Erdős problems that are open as of August 2026\. To solve a task in FME, AI systems must resolve \(prove or disprove\) one of the 68 conjectures in the proof assistant Lean\. Our 68 problems were selected by the second author among 652 open problems onerdosproblems\.comfor their mathematical interest and difficulty\. AIs have recently resolved several open problems in mathematics, but these demonstrations fall short of a systematic study of AI capabilities\. FME evaluates every AI model on the same fixed problems, autonomously and under the same budget\. We evaluated five AIs with a budget of $300 per problem\. One \(GPT\-6 Astra\) scored 3%, and all others scored 0%\.

## 1Introduction

There have been several recent examples of AI systems solving open problems in mathematics\.111On 20 May 2026, OpenAI announced an AI had disproved the unit distance conjecture\[[1](https://arxiv.org/html/2609.25050#bib.bib1)\]; on July 19, Levent Alpöge presented an explicit counterexample to the Jacobian conjecture in three\-dimensional space, stating that it was discovered using Claude Fable 5\[[2](https://arxiv.org/html/2609.25050#bib.bib2)\]; on 1 August OpenAI provided new results achieved by AI for ten problems in mathematics and theoretical computer science\[[3](https://arxiv.org/html/2609.25050#bib.bib3)\]\(including several problems of Erdős\)\.These are impressive demonstrations of AI’s ability to contribute to research mathematics\. However, in his 2026 ICM lecture,[Tao \[4\]](https://arxiv.org/html/2609.25050#bib.bib4)observes that evidence of this kind has mostly “not been gathered under controlled scientific conditions” and falls short of a systematic study of AI capabilities\. He identifies four shortcomings, to which we add a fifth:

1. 1\.*Reporting bias\.*“Successes are announced and failures are not\.” The universe of problems attempted by AI is not disclosed, so we do not know the success rate: announced solutions are a numerator without a denominator\.
2. 2\.*Costs\.*The number of attempts and the compute expended are frequently left undisclosed, so we do not know the cost at which these results were obtained\.
3. 3\.*Human scaffolding\.*The extent of guidance by human mathematicians is unclear\. These projects are likely to involve mathematically sophisticated users, and the prompts and interactions behind the results have not been published, so human insight may have steered the search to an unknown degree\.
4. 4\.*Contamination\.*It is often unclear how much of an announced solution already existed in the literature, and hence in the model’s training data\.222[Tao \[4\]](https://arxiv.org/html/2609.25050#bib.bib4), discussing the available evidence on whether AI tools can “accomplish some research\-level mathematical tasks”, speaks of “the degree of contamination of the problem with prior literature”\. At one end of the spectrum, the solution is already in the literature and hence in the model’s training data, so that the model reproduces it rather than deriving it; this is what contamination usually means in AI evaluation\. Towards the other end, the solution applies or recombines known results and techniques in ways that can amount to legitimate research\-level mathematics\. Where a given solution lies on this spectrum can be hard to judge \(see below\)\.
5. 5\.*Comparison across models\.*Different AI models are not systematically compared on the same problems, so we do not know when AI models first became capable of proving these results, nor whether some current models perform better than others\.

Benchmark evaluation under controlled conditions addresses every shortcoming except the fourth\. The universe of problems is fixed in advance and results are reported for all of them\. Every attempt runs under a fixed, disclosed budget\. Models work autonomously inside a fixed, published harness, and no human guidance is involved\. All models attempt the same problems under the same conditions, so we learn which models perform best and can track trends in AI capabilities over time\.

The remaining shortcoming, contamination, is addressed by the choice of problems rather than by the evaluation protocol: we benchmark on problems that are open\. An open problem has no complete solution in the literature for a model to reproduce\. Open problems also have a more fundamental advantage: success on them directly measures what we ultimately want to know, namely whether AI can push forward the frontier of a research field, not merely whether it can solve difficult problems with known answers\.

Benchmarking on open problems raises an obvious difficulty, however: a solution cannot be graded against a known answer\. The two existing benchmarks of open problems,*HorizonMath*\[[5](https://arxiv.org/html/2609.25050#bib.bib5)\]and*FrontierMath: Open Problems*\[[6](https://arxiv.org/html/2609.25050#bib.bib6), FM:OP;\], make unsolved problems verifiable by restricting attention to problems with a generator–verifier gap\. In such problems the solution is a concrete object, for example a graph, a polynomial, or an algorithm, that is hard to find but cheap to check computationally\. This approach comes at a steep price\. Most open problems ask for a proof of a general statement, not a checkable object, and cannot be posed in this format at all\. And even for problems that fit the format, verification is far from reliable, with both false positives and false negatives; Section[2](https://arxiv.org/html/2609.25050#S2)details these challenges\.

We instead require solutions to be formal proofs\. Each conjecture is stated in the Lean proof assistant, and a model must prove either the conjecture or its negation\.333One caveat: a conjecture, whether true or false, could in principle be independent of Lean’s axiomatic foundation, in which case neither it nor its negation is provable and the task is unsolvable\.This format reaches much further into research mathematics \(a problem is eligible whenever its statement is formalizable\) and makes verification definitive \(an accepted proof is a proof\)\.

Choosing open problems prevents models from succeeding by memorizing an exact result from training data\. Furthermore, we attempted to select problems whose resolution would be of mathematical interest \(section[3\.1](https://arxiv.org/html/2609.25050#S3.SS1)\)\. However, this does not guarantee that the results contain significant new ideas\. In particular, solutions to open problems often use a synthesis of existing ideas and techniques, even if the final arrangement of these ideas is new\. This makes it difficult to quantify the novelty present in any solution to an open problem; even famously difficult open problems may fall to a small tweak of existing methods that was previously missed\. It can take time and attention by human experts to identify what is a significant new idea and what is a repackaging of existing work\.

The questions chosen for this benchmark were asked by Paul Erdős, one of the most prolific and influential mathematicians of all time, and one of the leading figures in number theory and combinatorics for most of the 20th century\. Erdős was famous in particular for posing a large number of questions, of varying levels of difficulty, many of which have been very influential\. The websiteerdosproblems\.com\(run by the second author\) collects many of these problems, and has already received a lot of attention from AI solvers\. More details on the selection of problems are given in Section[3\.1](https://arxiv.org/html/2609.25050#S3.SS1)\.

## 2Related work

As described above, HorizonMath\[[5](https://arxiv.org/html/2609.25050#bib.bib5), 101 problems;\]and FM:OP\[[6](https://arxiv.org/html/2609.25050#bib.bib6), 50 problems;\]rely on problems with a generator–verifier gap\. HorizonMath draws on problems from three classes: conjectured closed forms, optimization problems, and constructions of objects not known to exist\. FM:OP sources problems from working mathematicians, with a bespoke verifier program written for each\. These strategies face considerable challenges:

1. 1\.They cannot be used to test most of research mathematics\. The vast majority of open problems have no generator–verifier gap: they call for a proof of a general statement rather than the exhibition of a checkable object, and so cannot be expressed in this format at all\.
2. 2\.Passing the check is evidence rather than proof\. HorizonMath describes accepted closed forms as “best regarded as conjectures until proven” and FM:OP explicitly allows verifiers that provide “strong numerical evidence” short of full proof\.
3. 3\.Soundness rests on hand\-crafted verification code and filters\. - •For example, HorizonMath accepts a conjectured closed form if it matches a high\-precision numerical reference value\. HorizonMath therefore uses an LLM judge to reject hard\-coded constants and operations like numerical root\-finding\. - •FM:OP’s bespoke verifiers are labor\-intensive to formulate and implement\. They are also error\-prone: in July 2026, two problems were removed because their verifiers “would not detect correct solutions with high enough fidelity”\.
4. 4\.Computational checking is one\-sided\. A verifier can confirm that an exhibited object works, but if no such object exists, the benchmark task is unsolvable\. Both benchmarks knowingly include problems that may have no solution of the required form\. FM:OP estimates that 10–40% of its problems are unsolvable\.

FME’s formal\-proof format addresses the first challenge: eligibility requires only that a conjecture’s statement be formalizable, not that its solutions be computationally checkable objects\. The other challenges are avoided outright: an accepted proof is definitive rather than evidence, soundness rests on the Lean kernel rather than per\-problem verification code, and false conjectures remain solvable tasks because the model may prove the negation\. Nevertheless, using formal proofs still has some downsides:

1. 1\.Not all research mathematics can be covered: it must be possible to state conjectures with the definitions available in Mathlib \(or short auxiliary definitions\)\.
2. 2\.Results reflect formalization ability as well as mathematical ability, since a model may find a correct argument yet fail to formalize it\. Often the obstacle lies not in the argument itself but in its prerequisites: the argument may rely on standard results from the literature that are missing from Mathlib, so the model would have to recreate them in Lean\.

[Tsoukalas et al\. \[7\]](https://arxiv.org/html/2609.25050#bib.bib7)ran a formal proof\-search agent over all 353 Erdős\-problem statements then formalized in the open\-source Formal Conjectures repository\[[8](https://arxiv.org/html/2609.25050#bib.bib8)\], resolving nine\. The attempted set was determined by what the community had formalized rather than selected for mathematical interest, and its statements include multi\-part subdivisions of problems as well as variants of varying strength drawn from the commentary accompanying each problem\.444The nine resolved statements span seven problems, four of which were unambiguously resolved: \#152, \#846, \#125, and \#26 \(the latter by disproving a weaker variant posed by Tenenbaum — a stronger result\)\. \#741 is also now marked solved onerdosproblems\.com, though “density” in its part \(i\) required interpretation: the agent disproved the exact\-density reading and proved the upper\-density reading, while the lower\-density reading remains open\. \#12 was settled in two of its three parts, and for \#138 only a variant, itself posed by Erdős, was resolved; these two problems remain open\.FME’s problems were instead curated for mathematical interest and difficulty \(Section[3\.1](https://arxiv.org/html/2609.25050#S3.SS1)\)\.

OEIS Open\[[9](https://arxiv.org/html/2609.25050#bib.bib9)\]follows a similar methodology, benchmarking language models on formally verified resolutions of open conjectures; its 492 conjectures, autoformalized from the On\-Line Encyclopedia of Integer Sequences by[Tsoukalas et al\. \[7\]](https://arxiv.org/html/2609.25050#bib.bib7), are of uncertain mathematical significance\. The Lean FRO maintains LeanEval\[[10](https://arxiv.org/html/2609.25050#bib.bib10)\], a benchmark and public leaderboard of Lean formalization and software\-verification tasks that also includes some open problems; as in FME, a problem counts as solved exactly when Comparator \(Section[3\.3](https://arxiv.org/html/2609.25050#S3.SS3)\) accepts the submission\.

The First Proof project\[[11](https://arxiv.org/html/2609.25050#bib.bib11),[12](https://arxiv.org/html/2609.25050#bib.bib12)\]responds to the same concerns that motivate FME, with different design choices\. Its problems arose in the contributors’ own research and were already solved by them, with short proofs that had never been published or posted online\. This guarantees that every problem is solvable and of known difficulty\. However, these problems are limited in number and may not be sufficiently challenging for current AI systems\. In the second round, the organizers ran four AI systems themselves, and 7 of the 10 problems received at least one passing grade\. Solutions are natural\-language proofs and grading is entirely manual: a pool of thirty expert referees reviewed the 39 submissions in a double\-blind, journal\-style process, with two or three referees per submission\. Referees weighed more than correctness, also assessing novelty, exposition, and the accuracy of citations, and could rate a flawed proof as requiring minor or major revisions rather than rejecting it\. This accommodates problems that resist formalization and yields more nuanced verdicts than a binary check, but the judgments are subjective, and the considerable grading effort must be repeated for every new system\.

## 3Methods

### 3\.1Problem selection

The problems were selected by the second author from among the open \(at the time of selection\) problems on the websiteerdosproblems\.com, which he curates\. The full list is given in Appendix[A](https://arxiv.org/html/2609.25050#A1)\. 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\.

This is, of course, a very personal and subjective judgement\. No doubt every mathematician interested in Erdős problems would produce a different version of such a list, although hopefully all would find many of their favourites among those chosen\.

In the past, this author has criticised using the problems listed onerdosproblems\.comas a meaningful benchmark for AI progress; in part this is because the problems vary hugely in difficulty, importance, and the amount of effort previously invested in finding a solution\. Many of the Erdős problems solved by AI were obscure, forgotten by human mathematicians until the website popularised them, and had solutions that were straightforward modifications of well\-known techniques\.

This is not the case with all of the problems solved by AI – most notably the solutions to problems \#90 \(the unit distance conjecture\), \#146, and \#183\. In these cases the problems were famous problems in their field, and all been the subject of numerous papers and partial results\. As such their solution by AI represents a watershed moment in the ability of AI to conduct meaningful mathematical research\.

This collection is an attempt to identify, in advance, the most interesting open problems, whose solutions may have a similar impact\. Most of these problems have also received a great deal of attention from mathematicians in the past few decades\. As such, any solution from an AI would be of interest to those in the relevant areas – and, with high probability, would contain important new ideas, rather than just involve a slight modification of existing techniques\. \(Although, as noted earlier, this is not a certainty; some of these problems may yet have surprisingly simple solutions\.\)

There was no particular target number of problems in mind when making this selection, nor was any upper bound on the \(perceived\) difficulty used as a criterion\. Erdős often offered prizes for his problems, with the amount offered a reflection of his own view of the importance and/or difficulty of the problem\. As such this list includes many problems with large prize values, although it also includes many with no prize attached at all, and omits some open problems with large prizes\.

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\.555The exception is the collection of three conjectures representing the Hadwiger–Nelson problem \(Section[3\.2](https://arxiv.org/html/2609.25050#S3.SS2)\), which are mutually exclusive by construction: proving any one of the three would immediately disprove the other two, although disproving one would leave the other two open\.The discovery of such an implication between two problems on this list would, in itself, be an interesting result\.

There is, of course, a heavy bias towards topics that not only were favourites of Erdős, but also of the second author\. For example, 7 of the problems are concerned with Sidon sets\. As such they are not completely independent – it may be that a single new insight into the nature of Sidon sets would be sufficient to answer all 7 of these problems, although this would be surprising, to say the least\.

Where a problem was not well\-posed, but contained several candidate questions \(for example \#138, \#208, or \#812\), a single question was chosen that was deemed to best capture the ‘spirit’ of the problem \(usually, but not always, being the hardest of the possible questions\)\.

For a proper history of each problem, including where it was discussed by Erdős and the history of progress towards it, we refer to the problem entries onerdosproblems\.com\. Several of the problems \(for example \#172, \#431, \#500, \#508, \#952, and \#970\) are not originally due to Erdős himself, but we follow the philosophy of the website in including problems of others that Erdős liked and popularised\.

### 3\.2Lean statements

Each conjecture in FME is a statement in Lean 4, using its mathematical library Mathlib\. The statements of 50 of the 68 conjectures \(covering 48 problems\) are taken from Formal Conjectures\[[13](https://arxiv.org/html/2609.25050#bib.bib13)\], an open\-source library of formalized open problems maintained by Google DeepMind, whose contributors had already formalized these Erdős problems\. Where Formal Conjectures offers several statements for a problem \(a default statement plus variants, or a subdivision into parts\), the second author selected the statement that best represents the problem\. The Hadwiger–Nelson problem \([\#508](https://www.erdosproblems.com/508)\) is a special case\. Its Formal Conjectures statement asks for the value of the chromatic number of the plane, which does not fit the prove\-or\-disprove format\. We therefore replace it with three conjectures, one for each candidate value; the answer666If an unambiguous answer exists; it is also possible that the answer is independent of the axioms of ZFC\.is known to be 5, 6, or 7\.

The remaining 17 problems had no statement in Formal Conjectures\. We formalized these ourselves using an autoformalization pipeline, yielding the remaining 18 conjectures \(the two parts of[\#713](https://www.erdosproblems.com/713)are formalized separately\)\. The second author reviewed each autoformalized statement to verify that it faithfully represents the original problem\.

### 3\.3Proof verification

We accept a submission only if it passes Comparator \([github\.com/leanprover/comparator](https://github.com/leanprover/comparator)\), a proof checker maintained by the Lean FRO, the organization that develops Lean\. Comparator is designed to be robust to a submitter that actively tries to cheat\. 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\. This design defeats many classes of attacks:

1. 1\.*Tampering with the agent environment\.*An agent could modify its own copy of Mathlib, the Lean toolchain, or the statement file\. This is powerless because only the submission’s Lean source ever leaves the agent container\.
2. 2\.*Malicious compile\-time code\.*Lean elaboration can execute arbitrary code \(e\.g\. a compile\-time\#eval\), which could otherwise tamper with the verdict\. Comparator compiles the submission inside an operating\-system sandbox \(Linux’s Landlock\) with tightly restricted write access, and the verdict is computed outside the sandbox\.
3. 3\.*Proving a different statement\.*A submission could prove a theorem that merely resembles the conjecture\. Comparator requires the submitted theorem’s statement to be identical to our trusted copy\.
4. 4\.*Redefining a dependency of the statement\.*A submission could redefine a definition the conjecture depends on, so that it becomes trivially true\. Comparator requires every declaration the statement depends on to be identical to the trusted version\.
5. 5\.*Assuming the result\.*A declared axiom, or asorryplaceholder \(which introduces the axiomsorryAx\), fails the axiom check: we permit no axioms beyond Lean’s standard three \(propext,Quot\.sound,Classical\.choice\)\.
6. 6\.*Bypassing the kernel\.*A submission can evade kernel checking at compile time: the optiondebug\.skipKernelTCdisables it outright, metaprogramming can insert declarations into the environment without it, and a buggy tactic can emit an ill\-typed proof term\. Comparator defeats this class of attacks by replaying the entire submission through the Lean kernel from scratch, trusting nothing from the agent’s own compilation\. Anative\_decideproof instead shifts trust from the kernel to the Lean compiler, and is known to be subvertible via@\[implemented\_by\]\. However,native\_decideintroduces the axiomLean\.ofReduceBool, which fails the axiom check\.

What remains trusted is the Lean kernel, Comparator itself, and its sandbox\.

### 3\.4AI agent

Our agent is built ondeepagentfrom the Inspect evaluation framework\[[14](https://arxiv.org/html/2609.25050#bib.bib14)\]\. The model is givenbash, a text editor, and a tool reporting its remaining time and token budgets;deepagentadds delegation to subagents, persistent memory, and a todo\-list tool\. The agent container \(Section[3\.3](https://arxiv.org/html/2609.25050#S3.SS3)\) provides a Lean 4 toolchain with Mathlib, the SageMath computer algebra system, and Python withsympy,mpmath,numpy, andpantograph\. Because the container has no network access, we provide an offline snapshot of the mathematics literature: theLaTeXsource trees of 476,000 pure\-mathematics arXiv papers dated up to 2022\.777The corpus is the arXiv subset of proof\-pile\[[15](https://arxiv.org/html/2609.25050#bib.bib15)\]: papers in arXiv’s mathematics archive \(themathcategories\), as of proof\-pile’s compilation in 2022\.

Both affordances \(thedeepagentand the literature snapshot\) were evaluated as agent variants in OEIS Open\[[9](https://arxiv.org/html/2609.25050#bib.bib9)\], and neither made a difference to accuracy on those conjectures relative to a basic ReAct agent with minimal tools\. We include these affordances anyway in our default configuration, as future models may be able to make better use of them\.

In our default configuration, 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\.

### 3\.5Limitations

#### Formalization cost may understate mathematical ability\.

As noted in Section[2](https://arxiv.org/html/2609.25050#S2), a model may find a correct argument yet fail to formalize it\. The argument itself may be laborious to formalize\. Or it may rely on standard results from the literature that are missing from Mathlib, which the model must then recreate in Lean at a cost that may exceed that of the argument itself\. FME scores may therefore substantially underestimate mathematical ability\.

#### No credit for reductions to famous open problems\.

Our setup accepts only a proof of the conjecture or of its negation, but mathematicians also value results that relate a conjecture to a famous open problem\. Proving that the conjecture implies a famous open problem, such as the Collatz conjecture, would often be considered the definitive word on it\.

#### Resolved conjectures may leak into training data\.

Once a conjecture in FME 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, the issue can be mitigated after the fact: conjectures resolved before a model’s training cutoff can be filtered out, and all models compared on the remaining smaller set\.

## 4Results

### 4\.1Benchmark results

We evaluated five models on all 68 conjectures in our default configuration \(Section[3\.4](https://arxiv.org/html/2609.25050#S3.SS4)\): one attempt per conjecture, with a budget of $300 and 72 hours of working time\. The models were a pre\-release version of GPT\-6 Astra, GPT\-5\.6 Sol, GPT\-5\.5, Claude Fable 5\.1, and Claude Fable 5\. Table[1](https://arxiv.org/html/2609.25050#S4.T1)gives the results\. Only GPT\-6 Astra resolved any of the conjectures: it resolved 2 of the 68, and the other four models resolved none\.

Table 1:Benchmark scores in the default configuration: one attempt per conjecture, $300 and 72 hours of working time per attempt\. The score is the percentage of the 68 conjectures resolved\.The two conjectures resolved by GPT\-6 Astra were[\#74](https://www.erdosproblems.com/74), disproved by counterexample, and[\#126](https://www.erdosproblems.com/126), proved\.888GPT\-6 Astra was a pre\-release model whose prices OpenAI had not published at the time of our evaluation, so our harness metered its spend at the per\-token prices of GPT\-5\.6 Sol as a stand\-in\. GPT\-6 Astra’s actual prices are about twice as high, so every attempt ran with a larger budget than intended: the attempts that hit the metered $300 limit had in fact spent $545–572\. We correct for this after the fact by recomputing the cost of every attempt from its token counts at the actual prices \(1\.8–2\.0 times the metered cost, depending on the mix of tokens\) and counting a conjecture as resolved only if its resolution cost at most $300 at the actual prices\. Attempts that failed with the larger budget would also have failed with $300, so the correction affects only[\#1](https://www.erdosproblems.com/1), which GPT\-6 Astra disproved in this run at a cost of $405: we do not count that resolution here, and report it with the additional attempts in Section[4\.2](https://arxiv.org/html/2609.25050#S4.SS2)\. The correction is imperfect in one regard\. The agent’s budget tool reported spend in metered dollars, so when the model had spent $300 at actual prices, the tool showed a spend of only about $160 and $140 still available\. The model paced its work accordingly, and a model told its true remaining budget might have behaved differently\. We judged this acceptable, the alternative being to discard the run\. All costs we report for GPT\-6 Astra are at its actual prices\.Table[2](https://arxiv.org/html/2609.25050#S4.T2)reports the cost and working time of each\. The remaining 66 attempts by GPT\-6 Astra ran to the $300 limit without a verified submission\.

Table 2:Cost and working time of the two resolutions in the default configuration\.
### 4\.2Additional non\-systematic attempts

The scores in Table[1](https://arxiv.org/html/2609.25050#S4.T1)are the results we consider comparable across models: one attempt per conjecture under a fixed budget\. Separately from them, and less systematically, we also made a number of further 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 configuration\. These attempts do not follow the protocol of Section[3\.4](https://arxiv.org/html/2609.25050#S3.SS4)and should not be read as a benchmark score\. We report them because any resolution of these problems is of mathematical interest regardless of how it was obtained, and because repeated attempts give some indication of the variance in outcomes\. Across all of them, GPT\-6 Astra resolved 5 of the 68 conjectures in at least one attempt: the two above, and additionally[\#1](https://www.erdosproblems.com/1), which was disproved, and[\#548](https://www.erdosproblems.com/548)and[\#571](https://www.erdosproblems.com/571), which were proved\. Table[3](https://arxiv.org/html/2609.25050#S4.T3)summarizes every resolution, together with how often each conjecture was resolved when attempted more than once\. Of the remaining 63 conjectures, 56 were attempted to completion between two and five times, 172 attempts in total, and none were resolved\.999Not every conjecture was attempted the same number of times, owing to the ad\-hoc nature of these additional experiments and to infrastructure failures that terminated some attempts before a verdict; such failed attempts are not counted here\.Reaching these 5 resolutions took over $220,000 of compute across all attempts, compared to roughly $20,000 for the benchmark run itself\. Brief summaries of the five solutions are given in Appendix[B](https://arxiv.org/html/2609.25050#A2)\.

Where a conjecture was resolved more than once, it is natural to ask whether the repeated resolutions were different arguments or re\-derivations of the same one\. The extent to which different proofs are genuinely distinct, or essentially the same, is a subtle and subjective matter, and will take time to form a proper opinion on\. After an initial superficial examination, we believe the two disproofs of[\#1](https://www.erdosproblems.com/1)to be essentially the same; the six disproofs of[\#74](https://www.erdosproblems.com/74)to consist of three distinct arguments; and the four proofs of[\#126](https://www.erdosproblems.com/126)to consist of three distinct arguments\.

Table 3:All resolutions by GPT\-6 Astra across every attempt, including the non\-systematic additional attempts described in the text\. Unlike Table[2](https://arxiv.org/html/2609.25050#S4.T2), this is not a benchmark result: attempts differ in budget and agent configuration, and conjectures were attempted different numbers of times\. “Resolved in” counts attempts that had reached a verdict by the time of writing\.

## 5Discussion and conclusion

We have conducted a systematic evaluation of AI systems on 68 open Erdős problems, selected in advance for their mathematical interest and difficulty, under a fixed and disclosed budget of $300 per problem, with every solution formally verified\. A pre\-release version of GPT\-6 Astra resolved 2 of the 68 conjectures and the four other models resolved none\. These results establish, under controlled conditions, that a current AI system can autonomously resolve open problems of genuine mathematical interest\. Each problem was selected on the criterion that its resolution by a human would merit a paper in a high\-level journal\. The capability is also both new and limited: only the newest model we evaluated displayed it, and 63 of the 68 conjectures remain open\. At $300 per attempt and a 3% success rate, the expected cost of a resolution is roughly $10,000, which may be considered modest for the resolution of an important open problem\. The additional attempts of Section[4\.2](https://arxiv.org/html/2609.25050#S4.SS2)indicate that spending more finds more: two conjectures were resolved in only one of three attempts, and four of the resolutions cost more than $300\. We would be excited for future work to investigate inference scaling on these problems systematically, measuring how the number of resolutions grows with the budget per attempt and with the number of attempts\.

Finally, FME measures the ability to solve problems, not to find them\. Erdős himself was celebrated as much for the questions he asked as for the theorems he proved\. In much of research mathematics, finding the right question is the harder part:[Litt \[16\]](https://arxiv.org/html/2609.25050#bib.bib16)writes that in his own work “discovering the statements of crucial lemmas is often much more difficult than proving them”, and describes his research as “trying to identify the most basic situation in which our understanding fails”, with problem\-solving secondary\[[17](https://arxiv.org/html/2609.25050#bib.bib17)\]\. A system that resolved every conjecture in FME would be an extraordinarily useful tool, but the impact of these results on mathematics will depend on human experts understanding the solutions and the ideas they contain; that work has only begun\.

## Appendix

## Appendix AList of benchmark problems

Table[4](https://arxiv.org/html/2609.25050#A1.T4)gives an informal one\-line description of each of the 68 conjectures, identified by its ID in the benchmark\.101010IDs are shortened for display by eliding the redundant problem number:Erdos208\.parts\.istands for the IDErdos208\.erdos\_208\.parts\.i, andErdos508\.eq5forErdos508\.HadwigerNelsonProblem\.eq5\.Each ID links to the corresponding entry onerdosproblems\.com\. The authoritative form of each conjecture is its Lean statement, which is what a model must prove or disprove; the Lean statements are available at[github\.com/epoch\-research/LeanOpenProblems](https://github.com/epoch-research/LeanOpenProblems)\. The 68 conjectures cover 65 distinct problems as numbered onerdosproblems\.com: the Hadwiger–Nelson problem \([\#508](https://www.erdosproblems.com/508)\) is represented by three conjectures, one for each candidate value of the chromatic number of the plane, and the two parts of[\#713](https://www.erdosproblems.com/713)are separate conjectures\. For the other multi\-part problems \([\#208](https://www.erdosproblems.com/208),[\#812](https://www.erdosproblems.com/812),[\#1206](https://www.erdosproblems.com/1206)\), only the part named in the ID is included\.

Table 4:The 68 conjectures of FrontierMath Erdős\.IDConjecture[Erdos1](https://www.erdosproblems.com/1)If every subset ofA⊆\{1,…,N\}A\\subseteq\\\{1,\\ldots,N\\\}has a distinct sum, thenN≫2\|A\|N\\gg 2^\{\|A\|\}\.[Erdos3](https://www.erdosproblems.com/3)IfA⊆ℕA\\subseteq\\mathbb\{N\}has∑n∈A1/n=∞\\sum\_\{n\\in A\}1/n=\\infty, thenAAcontains arbitrarily long arithmetic progressions\.[Erdos5](https://www.erdosproblems.com/5)EveryC≥0C\\geq 0is a limit point of the normalised prime gaps\(pn\+1−pn\)/log⁡n\(p\_\{n\+1\}\-p\_\{n\}\)/\\log n\.[Erdos7](https://www.erdosproblems.com/7)There is a covering system of the integers all of whose moduli are odd and greater than11\.[Erdos20](https://www.erdosproblems.com/20)Sunflower conjecture: the minimalf⁡\(n,k\)f\(n,k\)such that every family off⁡\(n,k\)f\(n,k\)manynn\-element sets contains akk\-sunflower satisfiesf⁡\(n,k\)<cknf\(n,k\)<c\_\{k\}^\{n\}\.[Erdos23](https://www.erdosproblems.com/23)Every triangle\-free graph on5​n5nvertices can be made bipartite by deleting at mostn2n^\{2\}edges\.[Erdos28](https://www.erdosproblems.com/28)IfA⊆ℕA\\subseteq\\mathbb\{N\}andA\+AA\+Acontains all sufficiently large integers, then the number of representations ofnnasa\+ba\+bwitha,b∈Aa,b\\in Ais unbounded\.[Erdos30](https://www.erdosproblems.com/30)The maximum size of a Sidon set in\{1,…,N\}\\\{1,\\ldots,N\\\}isN\+Oε​\(Nε\)\\sqrt\{N\}\+O\_\{\\varepsilon\}\(N^\{\\varepsilon\}\)for everyε\>0\\varepsilon\>0\.[Erdos39](https://www.erdosproblems.com/39)There is an infinite Sidon setAAwith\|A∩\{1,…,N\}\|≫εN1/2−ε\|A\\cap\\\{1,\\ldots,N\\\}\|\\gg\_\{\\varepsilon\}N^\{1/2\-\\varepsilon\}for everyε\>0\\varepsilon\>0\.[Erdos41](https://www.erdosproblems.com/41)IfA⊆ℕA\\subseteq\\mathbb\{N\}is infinite and all triple sumsa\+b\+ca\+b\+cfromAAare distinct, thenlim infN\|A∩\{1,…,N\}\|/N1/3=0\\liminf\_\{N\}\|A\\cap\\\{1,\\ldots,N\\\}\|/N^\{1/3\}=0\.[Erdos52](https://www.erdosproblems.com/52)Sum–product conjecture:max\(\|A\+A\|,\|A⋅A\|\)≫ε\|A\|2−ε\\max\(\|A\+A\|,\|A\\cdot A\|\)\\gg\_\{\\varepsilon\}\|A\|^\{2\-\\varepsilon\}for finiteA⊆ℤA\\subseteq\\mathbb\{Z\}\.[Erdos61](https://www.erdosproblems.com/61)Erdős–Hajnal conjecture: for every graphHHthere isc\>0c\>0such that everyHH\-free graph onnnvertices contains a clique or independent set of size at leastncn^\{c\}\.[Erdos66](https://www.erdosproblems.com/66)There is a setA⊆ℕA\\subseteq\\mathbb\{N\}such that the number of representations ofnnasa\+ba\+bwitha,b∈Aa,b\\in A, divided bylog⁡n\\log n, tends to a nonzero limit\.[Erdos68](https://www.erdosproblems.com/68)The sum∑n≥21/\(n\!−1\)\\sum\_\{n\\geq 2\}1/\(n\!\-1\)is irrational\.[Erdos74](https://www.erdosproblems.com/74)For everyf⁡\(n\)→∞f\(n\)\\to\\inftythere is a graph of infinite chromatic number in which everynn\-vertex subgraph can be made bipartite by deleting at mostf⁡\(n\)f\(n\)edges\.[Erdos86](https://www.erdosproblems.com/86)Every subgraph of the hypercubeQnQ\_\{n\}with at least\(12\+o⁡\(1\)\)​n​2n−1\(\\tfrac\{1\}\{2\}\+o\(1\)\)n2^\{n\-1\}edges contains a44\-cycle\.[Erdos89](https://www.erdosproblems.com/89)Every set ofnnpoints inℝ2\\mathbb\{R\}^\{2\}determines≫n/log⁡n\\gg n/\\sqrt\{\\log n\}distinct distances\.[Erdos97](https://www.erdosproblems.com/97)Every convex polygon has a vertex with no four other vertices equidistant from it\.[Erdos101](https://www.erdosproblems.com/101)Amongnnpoints inℝ2\\mathbb\{R\}^\{2\}with no five on a line, the number of lines containing exactly four points iso⁡\(n2\)o\(n^\{2\}\)\.[Erdos104](https://www.erdosproblems.com/104)Amongnnpoints inℝ2\\mathbb\{R\}^\{2\}, the number of unit circles containing at least three of the points iso⁡\(n2\)o\(n^\{2\}\)\.[Erdos107](https://www.erdosproblems.com/107)Happy ending problem: the minimalNNsuch that anyNNpoints inℝ2\\mathbb\{R\}^\{2\}, no three on a line, contain the vertices of a convexnn\-gon is2n−2\+12^\{n\-2\}\+1\.[Erdos120](https://www.erdosproblems.com/120)Erdős similarity problem: for every infiniteA⊆ℝA\\subseteq\\mathbb\{R\}there is a set of positive measure containing no affine copya⋅A\+ba\\cdot A\+b\(witha≠0a\\neq 0\) ofAA\.[Erdos126](https://www.erdosproblems.com/126)Letf⁡\(n\)f\(n\)be the largestmmsuch that∏a≠b∈A\(a\+b\)\\prod\_\{a\\neq b\\in A\}\(a\+b\)has at leastmmdistinct prime factors whenever\|A\|=n\|A\|=n; thenf⁡\(n\)/log⁡n→∞f\(n\)/\\log n\\to\\infty\.[Erdos128](https://www.erdosproblems.com/128)If every induced subgraph on at leastn/2n/2of thennvertices ofGGhas more thann2/50n^\{2\}/50edges, thenGGcontains a triangle\.[Erdos138](https://www.erdosproblems.com/138)The van der Waerden numbers satisfyW​\(k\)1/k→∞W\(k\)^\{1/k\}\\to\\infty\.[Erdos172](https://www.erdosproblems.com/172)In any finite colouring ofℕ\\mathbb\{N\}there are arbitrarily large finite setsAAsuch that all sums and products of distinct elements ofAAreceive the same colour\.[Erdos181](https://www.erdosproblems.com/181)The Ramsey number of the hypercube satisfiesR⁡\(Qn\)≪2nR\(Q\_\{n\}\)\\ll 2^\{n\}\.[Erdos184](https://www.erdosproblems.com/184)Erdős–Gallai conjecture: every graph onnnvertices can be decomposed intoO⁡\(n\)O\(n\)edge\-disjoint cycles and edges\.[Erdos208\.parts\.i](https://www.erdosproblems.com/208)The gaps between consecutive squarefree numberssns\_\{n\}satisfysn\+1−sn≪εsnεs\_\{n\+1\}\-s\_\{n\}\\ll\_\{\\varepsilon\}s\_\{n\}^\{\\varepsilon\}for everyε\>0\\varepsilon\>0\.[Erdos213](https://www.erdosproblems.com/213)For everyn≥4n\\geq 4there arennpoints inℝ2\\mathbb\{R\}^\{2\}, no three on a line and no four on a circle, with all pairwise distances integers\.[Erdos241](https://www.erdosproblems.com/241)Bose–Chowla conjecture: the maximum size ofA⊆\{1,…,N\}A\\subseteq\\\{1,\\ldots,N\\\}with all triple sums distinct is∼N1/3\\sim N^\{1/3\}\.[Erdos242](https://www.erdosproblems.com/242)Erdős–Straus conjecture: for everyn\>2n\>2there are integers1≤x<y<z1\\leq x<y<zwith4/n=1/x\+1/y\+1/z4/n=1/x\+1/y\+1/z\.[Erdos322](https://www.erdosproblems.com/322)For everyk≥3k\\geq 3there isc\>0c\>0such that infinitely manynnhave more thanncn^\{c\}representations as a sum ofkkmanykkth powers\.[Erdos324](https://www.erdosproblems.com/324)There is a polynomialf∈ℤ⁡\[x\]f\\in\\mathbb\{Z\}\[x\]such that the sumsf⁡\(a\)\+f⁡\(b\)f\(a\)\+f\(b\)witha<ba<bnonnegative integers are all distinct\.[Erdos364](https://www.erdosproblems.com/364)There are no three consecutive powerful numbers\.[Erdos371](https://www.erdosproblems.com/371)The set ofnnwithP⁡\(n\+1\)\>P⁡\(n\)P\(n\+1\)\>P\(n\), whereP⁡\(n\)P\(n\)is the largest prime factor ofnn, has density1/21/2\.[Erdos376](https://www.erdosproblems.com/376)There are infinitely manynnsuch that\(2​nn\)\\binom\{2n\}\{n\}is coprime to105105\.[Erdos406](https://www.erdosproblems.com/406)Only finitely many powers of22have only the digits00and11when written in base33\.[Erdos431](https://www.erdosproblems.com/431)There are infinite setsA,B⊆ℕA,B\\subseteq\\mathbb\{N\}such thatA\+BA\+Bagrees with the set of primes up to finitely many exceptions\.[Erdos478](https://www.erdosproblems.com/478)The number of distinct residuesk\!modpk\!\\bmod pfor1≤k<p1\\leq k<pis∼\(1−1/e\)​p\\sim\(1\-1/e\)pas the primep→∞p\\to\\infty\.[Erdos508\.eq5](https://www.erdosproblems.com/508)Hadwiger–Nelson problem: the chromatic number of the unit\-distance graph onℝ2\\mathbb\{R\}^\{2\}is exactly55\.[Erdos508\.eq6](https://www.erdosproblems.com/508)Hadwiger–Nelson problem: the chromatic number of the unit\-distance graph onℝ2\\mathbb\{R\}^\{2\}is exactly66\.[Erdos508\.eq7](https://www.erdosproblems.com/508)Hadwiger–Nelson problem: the chromatic number of the unit\-distance graph onℝ2\\mathbb\{R\}^\{2\}is exactly77\.[Erdos548](https://www.erdosproblems.com/548)Erdős–Sós conjecture: every graph onn≥k\+1n\\geq k\+1vertices with at leastk−12​n\+1\\frac\{k\-1\}\{2\}n\+1edges contains every tree onk\+1k\+1vertices\.[Erdos564](https://www.erdosproblems.com/564)There isc\>0c\>0such thatR3​\(n\)≥22c​nR\_\{3\}\(n\)\\geq 2^\{2^\{cn\}\}, whereR3​\(n\)R\_\{3\}\(n\)is the22\-colour Ramsey number of the complete33\-uniform hypergraph onnnvertices\.[Erdos571](https://www.erdosproblems.com/571)For every rationalα∈\[1,2\)\\alpha\\in\[1,2\)there is a bipartite graphGGwith extremal numberex⁡\(n,G\)≍nα\\mathrm\{ex\}\(n;G\)\\asymp n^\{\\alpha\}\.[Erdos583](https://www.erdosproblems.com/583)Every connected graph onnnvertices can be partitioned into at most⌈n/2⌉\\lceil n/2\\rceiledge\-disjoint paths\.[Erdos595](https://www.erdosproblems.com/595)There is an infinite graph containing noK4K\_\{4\}which is not the union of countably many triangle\-free graphs\.[Erdos647](https://www.erdosproblems.com/647)There is somen\>24n\>24such thatm\+τ⁡\(m\)≤n\+2m\+\\tau\(m\)\\leq n\+2for allm<nm<n, whereτ⁡\(m\)\\tau\(m\)counts the divisors ofmm\.[Erdos672](https://www.erdosproblems.com/672)The product of an arithmetic progressionn,n\+d,…,n\+\(k−1\)​dn,n\+d,\\ldots,n\+\(k\-1\)dof positive integers withk≥4k\\geq 4andgcd⁡\(n,d\)=1\\gcd\(n,d\)=1is never a perfect power\.[Erdos713\.parts\.i](https://www.erdosproblems.com/713)For every bipartite graphGGwith at least two edges there areα∈\[1,2\)\\alpha\\in\[1,2\)andc\>0c\>0such thatex⁡\(n,G\)∼c​nα\\mathrm\{ex\}\(n;G\)\\sim cn^\{\\alpha\}\.[Erdos713\.parts\.ii](https://www.erdosproblems.com/713)Any exponentα\\alphaarising as in part \(i\) is rational\.[Erdos714](https://www.erdosproblems.com/714)ex⁡\(n,Kr,r\)≫n2−1/r\\mathrm\{ex\}\(n;K\_\{r,r\}\)\\gg n^\{2\-1/r\}for everyr≥2r\\geq 2\.[Erdos723](https://www.erdosproblems.com/723)Every finite projective plane has prime\-power order\.[Erdos773](https://www.erdosproblems.com/773)The largest Sidon subset of the squares\{1,4,…,N2\}\\\{1,4,\\ldots,N^\{2\}\\\}has sizeN1−o⁡\(1\)N^\{1\-o\(1\)\}\.[Erdos812\.parts\.i](https://www.erdosproblems.com/812)There isc\>0c\>0such that the diagonal Ramsey numbers satisfyR⁡\(n\+1\)/R⁡\(n\)≥1\+cR\(n\+1\)/R\(n\)\\geq 1\+cfor all largenn\.[Erdos821](https://www.erdosproblems.com/821)For everyε\>0\\varepsilon\>0there are infinitely manynnsuch thatϕ⁡\(m\)=n\\phi\(m\)=nhas more thann1−εn^\{1\-\\varepsilon\}solutionsmm\.[Erdos829](https://www.erdosproblems.com/829)The number of representations ofnnas a sum of two cubes is at most\(log⁡n\)O⁡\(1\)\(\\log n\)^\{O\(1\)\}\.[Erdos952](https://www.erdosproblems.com/952)There is an infinite sequence of distinct Gaussian primes with uniformly bounded gaps between consecutive terms\.[Erdos970](https://www.erdosproblems.com/970)Jacobsthal’s function satisfiesh⁡\(k\)≪k2h\(k\)\\ll k^\{2\}\.[Erdos972](https://www.erdosproblems.com/972)For every irrationalα\>1\\alpha\>1there are infinitely many primesppsuch that⌊α​p⌋\\lfloor\\alpha p\\rflooris also prime\.[Erdos975](https://www.erdosproblems.com/975)For every irreduciblef∈ℤ⁡\[x\]f\\in\\mathbb\{Z\}\[x\]which is eventually positive,∑n≤xτ⁡\(f⁡\(n\)\)∼c​x​log⁡x\\sum\_\{n\\leq x\}\\tau\(f\(n\)\)\\sim c\\,x\\log xfor some constantc\>0c\>0\.[Erdos1003](https://www.erdosproblems.com/1003)There are infinitely manynnwithϕ⁡\(n\)=ϕ⁡\(n\+1\)\\phi\(n\)=\\phi\(n\+1\)\.[Erdos1020](https://www.erdosproblems.com/1020)Erdős matching conjecture: forr≥3r\\geq 3andn≥r​k−1n\\geq rk\-1, the maximum number of edges in anrr\-uniform hypergraph onnnvertices with nokkpairwise disjoint edges ismax⁡\(\(r​k−1r\),\(nr\)−\(n−k\+1r\)\)\\max\\bigl\(\\binom\{rk\-1\}\{r\},\\binom\{n\}\{r\}\-\\binom\{n\-k\+1\}\{r\}\\bigr\)\.[Erdos1057](https://www.erdosproblems.com/1057)The number of Carmichael numbers up toxxisx1−o⁡\(1\)x^\{1\-o\(1\)\}\.[Erdos1083](https://www.erdosproblems.com/1083)For everyd≥3d\\geq 3, the minimum number of distinct distances determined bynnpoints inℝd\\mathbb\{R\}^\{d\}isn2/d−o⁡\(1\)n^\{2/d\-o\(1\)\}\.[Erdos1159](https://www.erdosproblems.com/1159)There isC\>1C\>1such that every finite projective plane has a set of points meeting every line in at least11and at mostCCpoints\.[Erdos1206\.parts\.i](https://www.erdosproblems.com/1206)The cubes\{1,8,…,N3\}\\\{1,8,\\ldots,N^\{3\}\\\}contain a Sidon set of size≫N\\gg N\.
## Appendix BSummary of AI solutions

We present brief discussions of the five problems solved by GPT\-6 Astra, as discussed in Section[4](https://arxiv.org/html/2609.25050#S4)\. More in\-depth, but still informal, expositions written by the second author can be found on the relevant problem pages onerdosproblems\.com\. While the formalisation process ensures we can be confident that the proofs are correct, they have not yet been properly ‘digested’\. These informal expositions should be viewed as placeholders, to highlight the ideas involved, until a more traditional paper, with full details and context, is prepared by human experts\.

### B\.1Disproof of[\#1](https://www.erdosproblems.com/1)

A finite set of natural numbersAAis dissociated if the map which takesS⊆AS\\subseteq Ato∑n∈Sn\\sum\_\{n\\in S\}nis injective\. Erdős problem[\#1](https://www.erdosproblems.com/1)concerns how dense a dissociated set can be found in an interval: more precisely, ifA⊆\{1,…,N\}A\\subseteq\\\{1,\\ldots,N\\\}is a dissociated set of sizenn, then is it true that111111Here we use the Vinogradov notationf≫gf\\gg gto mean there exists an absolute constantc\>0c\>0such thatf≥c​gf\\geq cg\.N≫2nN\\gg 2^\{n\}? Erdős called this ‘perhaps my first serious problem’, and it dates back to 1931 \(when Erdős was 18\), as reported in\[[18](https://arxiv.org/html/2609.25050#bib.bib18)\]\. As such it is probably the longest\-standing open Erdős problem, and has a special historic significance\.

TakingA=\{1,2,4,…,2n−1\}A=\\\{1,2,4,\\ldots,2^\{n\-1\}\\\}shows thatN≤2n−1N\\leq 2^\{n\-1\}is possible\. The best upper bound previously available wasN≤0\.22002⋅2nN\\leq 0\.22002\\cdot 2^\{n\}by Bohman\[[19](https://arxiv.org/html/2609.25050#bib.bib19)\]\. The best lower bound known so far isN≫2n/nN\\gg 2^\{n\}/\\sqrt\{n\}, first proved by Erdős and Moser\[[20](https://arxiv.org/html/2609.25050#bib.bib20)\]\. The solution provided by GPT\-6 Astra is a counterexample to Erdős’ conjecture\.

###### Theorem 1

For anyϵ\>0\\epsilon\>0there exist arbitrarily largenn, with associated dissociated setsA⊆\{1,…,N\}A\\subseteq\\\{1,\\ldots,N\\\}of sizenn, such that

N≤ϵ​2n\.N\\leq\\epsilon 2^\{n\}\.

The AI proof is, in its current form, ineffective, in that it gives no information how largennmust be in terms ofϵ\\epsilon; this ineffectivity is not intrinsic to the method, and could likely be removed with a little more work\. The argument uses linear algebra to construct a sequence ofn×nn\\times nrational matrices, withn→∞n\\to\\inftyand determinant→0\\to 0, with specific properties that allow one to construct from this matrix large dissociated sets\. While attempting to understand this proof the second author reinterpreted it in terms of lattices, which he found to be a more natural perspective; a detailed sketch is available aterdosproblems\.com\.

### B\.2Disproof of[\#74](https://www.erdosproblems.com/74)

LetGGbe an infinite graph which is close to being bipartite, in the sense that every finite subgraph onnnvertices can be made bipartite by deleting at mostf⁡\(n\)f\(n\)edges, wheref⁡\(n\)f\(n\)tends to infinity very slowly\. Erdős, Hajnal, and Szemerédi\[[21](https://arxiv.org/html/2609.25050#bib.bib21)\]asked whether this must force the chromatic number ofGGto be small, or whether it can be infinite? They suspected that an example existed with infinite chromatic number, however slowlyf⁡\(n\)f\(n\)diverged\. The solution provided by GPT\-6 Astra shows that, on the contrary, no such graph can exist iff⁡\(n\)f\(n\)diverges slowly enough\.

###### Theorem 2

There exists a functionf⁡\(n\)f\(n\)such thatf⁡\(n\)→∞f\(n\)\\to\\inftyasn→∞n\\to\\inftywith the following property\.

IfGGis a \(finite or infinite\) graph in which every finite subgraph onnnvertices can be made bipartite by deleting at mostf⁡\(n\)f\(n\)edges thenGGhas chromatic number≤3\\leq 3\.

The formalisation just proves the existence statement above, but it appears the argument given proves this forf⁡\(n\)≍log⁡nlog⁡log⁡nf\(n\)\\asymp\\frac\{\\log n\}\{\\log\\log n\}\. The argument is elementary and proceeds inductively\. Roughly speaking, the idea is to consider a sequence

G=G0⊇G1⊇⋯G=G\_\{0\}\\supseteq G\_\{1\}\\supseteq\\cdotswhereGkG\_\{k\}has no odd cycles of lengthO⁡\(k\)O\(k\)and is obtained fromGk−1G\_\{k\-1\}by deleting few edges\. Eventually \(ifGGis finite, which can be assumed by compactness\) such aGkG\_\{k\}is bipartite, so has a22\-colouring\. A gluing argument, using thatGkG\_\{k\}andGk−1G\_\{k\-1\}differ in only a small number of edges, then shows how a33\-colouring ofGkG\_\{k\}\(where the location of the third colour is carefully controlled\) yields a33\-colouring ofGk−1G\_\{k\-1\}with similar control, and eventually constructs a33\-colouring ofG0G\_\{0\}\.

### B\.3Proof of[\#126](https://www.erdosproblems.com/126)

IfAAis a finite set of natural numbers then letS⁡\(A\)S\(A\)be the set of primes that divide integers of the shapea\+ba\+bwitha≠b∈Aa\\neq b\\in A\. In their first joint paper Erdős and Turán\[[22](https://arxiv.org/html/2609.25050#bib.bib22)\]investigated how smallS⁡\(A\)S\(A\)can be as a function ofn=\|A\|n=\\lvert A\\rvert\. They proved that\|S⁡\(A\)\|≫log⁡n\\lvert S\(A\)\\rvert\\gg\\log n\. Much later Erdős asked, on several occasions, for an improvement of this bound such as\|S⁡\(A\)\|/log⁡n→∞\\lvert S\(A\)\\rvert/\\log n\\to\\infty\. This was proved in a strong form by GPT\-6 Astra\.

###### Theorem 3

IfA⊂ℕA\\subset\\mathbb\{N\}is a finite set of sizennthen

\|S⁡\(A\)\|≫n1/2\.\\lvert S\(A\)\\rvert\\gg n^\{1/2\}\.

TakingA=\{1,…,n\}A=\\\{1,\\ldots,n\\\}shows that\|S⁡\(A\)\|≪n/log⁡n\\lvert S\(A\)\\rvert\\ll n/\\log nis possible\. GPT\-6 Astra provided three distinct proofs of\|S⁡\(A\)\|≫nc\\lvert S\(A\)\\rvert\\gg n^\{c\}with different values ofcc\(1/81/8,1/31/3, and1/21/2\)\. All three proofs use elementary methods, and are reasonably short, but appear to be distinct\.

### B\.4Proof of[\#548](https://www.erdosproblems.com/548)

The Erdős\-Sós conjecture, proposed by Erdős and Sós in 1962, states that, ifn≥kn\\geq k, every graph onnnvertices with\>k−22​n\>\\frac\{k\-2\}\{2\}nedges contains every tree onkkvertices\. The weaker result that\>\(k−2\)​n\>\(k\-2\)nedges suffice is easy to prove by induction, but the Erdős\-Sós conjecture itself remained open, despite being proved in many special cases\. Chung’s collection of Erdős problems on graphs described it as ‘one of the most tantalizing problems in extremal graph theory’\. The solution provided by GPT\-6 Astra gives a proof of the full conjecture\.

###### Theorem 4

Letn≥kn\\geq k\. IfGGis a graph onnnvertices with\>k−22​n\>\\frac\{k\-2\}\{2\}nedges thenGGcontains a copy of every tree onkkvertices\.

The proof is surprisingly short and elegant\. It considers the number of pairs\(π,j\)\(\\pi,j\)whereπ=\(v1⋯vn\)\\pi=\(v\_\{1\}\\cdots v\_\{n\}\)is an ordering of the vertices ofGGand2≤j≤n2\\leq j\\leq nis a label such thatv1​vjv\_\{1\}v\_\{j\}is an edge inGG\. The number of such pairs is easily calculated as2​m​\(n−1\)\!2m\(n\-1\)\!, wheremmis the number of edges ofGG\. On the other hand, for any fixed treeTTonkkvertices, an inductive argument shows this number to be at mostC⁡\(T\)\+\(k−2\)​n\!C\(T\)\+\(k\-2\)n\!, whereC⁡\(T\)C\(T\)counts the number of\(π,j\)\(\\pi,j\)in which\(v1⋯vj\)\(v\_\{1\}\\cdots v\_\{j\}\)contains a copy ofTTrooted atv1v\_\{1\}\. IfGGdoes not contain any copy ofTTthenC⁡\(T\)=0C\(T\)=0, and rearranging yields the result\.

### B\.5Proof of[\#571](https://www.erdosproblems.com/571)

The Turán numberex⁡\(n,G\)\\mathrm\{ex\}\(n;G\)is the maximum number of edges that a graph onnnvertices can have before it must contain a copy ofGGas a subgraph\. The study of such numbers is a cornerstone of extremal graph theory; whenGGhas chromatic number≥3\\geq 3these are well\-understood, but their behaviour for bipartiteGGis much more mysterious\.

Erdős asked a number of questions concerning this quantity \(in this benchmark collection there are two further problems associated with[\#713](https://www.erdosproblems.com/713), still open\)\.[\#571](https://www.erdosproblems.com/571), a problem of Erdős and Simonovits, asks about the possible orders of growth of this function – in particular, is it true that, for any rationalα∈\[1,2\)\\alpha\\in\[1,2\), there must exist a bipartite graphGGsuch that121212We writef≍gf\\asymp gto meanf≪g≪ff\\ll g\\ll f\.

ex⁡\(n,G\)≍nα​?\\mathrm\{ex\}\(n;G\)\\asymp n^\{\\alpha\}?Many special cases of this conjecture, for various families of rationalα\\alpha, have been proved\. The solution provided by GPT\-6 Astra gives a proof of the full conjecture\.

###### Theorem 5

For any rationalα∈\[1,2\)\\alpha\\in\[1,2\)there exists a bipartite graphGGsuch that

ex⁡\(n,G\)≍nα\.\\mathrm\{ex\}\(n;G\)\\asymp n^\{\\alpha\}\.

The AI proof of this is, in the opinion of the second author, the most difficult of the five solutions given\. A proper human understanding of this proof, including crucial information such as the relation between the AI proof and the substantial existing work on this problem, will take some time\.

## References

- \[1\]OpenAI\.An OpenAI model has disproved a central conjecture in discrete geometry\.[https://openai\.com/index/model\-disproves\-discrete\-geometry\-conjecture/](https://openai.com/index/model-disproves-discrete-geometry-conjecture/), 2026a\.Published 20 May 2026\.
- \[2\]Melissa Lee\.‘hello there the jacobian conjecture is false thanx’: why a tiny social media post has mathematicians rethinking AI\.The Conversation,[https://theconversation\.com/hello\-there\-the\-jacobian\-conjecture\-is\-false\-thanx\-why\-a\-tiny\-social\-media\-post\-has\-mathematicians\-rethinking\-ai\-283883](https://theconversation.com/hello-there-the-jacobian-conjecture-is-false-thanx-why-a-tiny-social-media-post-has-mathematicians-rethinking-ai-283883), 2026\.Published 22 July 2026\.
- \[3\]OpenAI\.Ten advances in mathematics and theoretical computer science\.[https://openai\.com/index/ten\-advances\-in\-mathematics/](https://openai.com/index/ten-advances-in-mathematics/), 2026b\.Published 1 August 2026\.
- \[4\]Terence Tao\.Mathematics in the age of AI, 2026\.Based on a public lecture delivered at the 2026 International Congress of Mathematicians; arXiv:2608\.16753\.
- \[5\]Erik Y\. Wang, Sumeet Motwani, James V\. Roggeveen, Eliot Hodges, Dulhan Jayalath, Charles London, Kalyan Ramakrishnan, Flaviu Cipcigan, Philip Torr, and Alessandro Abate\.HorizonMath: Measuring AI progress toward mathematical discovery with automatic verification, 2026\.arXiv:2603\.15617\.
- \[6\]Epoch AI\.FrontierMath: Open problems\.[https://epoch\.ai/frontiermath/open\-problems](https://epoch.ai/frontiermath/open-problems), 2026\.Accessed 11 August 2026\.
- \[7\]George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, et al\.Advancing mathematics research with AI\-driven formal proof search, 2026\.arXiv:2605\.22763\.
- \[8\]Google DeepMind\.Formal conjectures\.[https://github\.com/google\-deepmind/formal\-conjectures](https://github.com/google-deepmind/formal-conjectures), 2026\.Accessed 31 August 2026\.
- \[9\]Tom Adamczewski\.OEIS Open: How many conjectures can language models turn into theorems?, 2026\.arXiv:2608\.11941\.
- \[10\]Lean FRO\.LeanEval\.[https://lean\-lang\.org/eval/](https://lean-lang.org/eval/), 2026\.Accessed 31 August 2026\.
- \[11\]Mohammed Abouzaid, Andrew J\. Blumberg, Martin Hairer, Joe Kileel, Tamara G\. Kolda, Paul D\. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, and Lauren Williams\.First proof, 2026a\.arXiv:2602\.05192\.
- \[12\]Mohammed Abouzaid, Nikhil Srivastava, Rachel Ward, and Lauren Williams\.First proof second batch, 2026b\.arXiv:2606\.18119\.
- \[13\]Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z\. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, and Pushmeet Kohli\.Formal conjectures: An open and evolving benchmark for verified discovery in mathematics, 2026\.arXiv:2605\.13171\.
- \[14\]UK AI Security Institute\.Inspect AI: Framework for large language model evaluations\.[https://github\.com/UKGovernmentBEIS/inspect\_ai](https://github.com/UKGovernmentBEIS/inspect_ai), 2024\.
- \[15\]Zhangir Azerbayev, Edward Ayers, and Bartosz Piotrowski\.proof\-pile\.Hugging Face dataset,[https://huggingface\.co/datasets/hoskinson\-center/proof\-pile](https://huggingface.co/datasets/hoskinson-center/proof-pile), 2022\.
- \[16\]Daniel Litt\.Mathematics in the Library of Babel\.Blog post,[https://www\.daniellitt\.com/blog/2026/2/20/mathematics\-in\-the\-library\-of\-babel/](https://www.daniellitt.com/blog/2026/2/20/mathematics-in-the-library-of-babel/), 2026a\.Published 21 February 2026\.
- \[17\]Daniel Litt\.Reply to a post by Jacob Tsimerman on problem\-solving in mathematics\.Post on X,[https://x\.com/littmath/status/2051298982287012297](https://x.com/littmath/status/2051298982287012297), 2026b\.Published 4 May 2026\.
- \[18\]Paul Erdős\.Some of my new and almost new problems and results in combinatorial number theory\.*Number theory \(Eger, 1996\)*, pages 169–180, 1998\.
- \[19\]Tom Bohman\.A construction for sets of integers with distinct subset sums\.*Electron\. J\. Combin\.*, 5:Research Paper 3, 14, 1998\.ISSN 1077\-8926\.doi:10\.37236/1341\.URL[https://doi\-org\.manchester\.idm\.oclc\.org/10\.37236/1341](https://doi-org.manchester.idm.oclc.org/10.37236/1341)\.
- \[20\]P\. Erdős\.Problems and results in additive number theory\.*Colloque sur la Théorie des Nombres, Bruxelles, 1955*, pages 127–137, 1956\.
- \[21\]P\. Erdős, A\. Hajnal, and E\. Szemerédi\.On almost bipartite large chromatic graphs\.*Theory and practice of combinatorics*, 60:117–123, 1982\.
- \[22\]Paul Erdős and Paul Turan\.On a problem in the elementary theory of numbers\.*Amer\. Math\. Monthly*, 41\(10\):608–611, 1934\.ISSN 0002\-9890\.doi:10\.2307/2301909\.URL[https://doi\.org/10\.2307/2301909](https://doi.org/10.2307/2301909)\.