The last year has seen a shift in AI-assisted mathematics, with frontier language models producing proofs of and counterexamples to long-standing open conjectures. However, studying only the current set of major breakthroughs provides an incomplete picture of LLM capabilities and the computational resources needed to achieve reported results. To address this, we introduce a new dataset, OpenConjecture, which collects conjectures from mathematics papers published on the arXiv since February 2026. We use these conjectures as a source of open mathematical problems, and apply frontier GPT models to a random sample of 200 of these conjectures over three passes using a reproducible protocol without problem-specific mathematical guidance. Rather than attempt expert verification of these candidate solutions, we analyze the types of problems for which LLMs produce solutions and the characteristics of these solutions. The models we test produce candidate solutions for roughly 60% of the conjectures, with counterexamples about 1.3 times more common than proofs. We estimate solution novelty, assess how solutions cite and relate to existing literature, and analyze whether the proposed resolution relies on either an error in or underspecification of the conjecture. We find that models sometimes propose resolutions that are outside the authors' intent (e.g., proposing the trivial group as a counterexample) and that a number of proofs follow closely from existing results, but that some resolutions exhibit at least moderate novelty. Our findings underscore the need for evaluations that go beyond correctness to assess fidelity to the intended statement, attribution, and the nature of the mathematical contribution.
Figures & tables
Figure 1: All open conjectures with a math primary subject classification in the June 21st snapshot of OpenConjecture. Categories with a single conjecture are omitted.
Figure 2: Left: Final status of conjectures and the pass in which a resolution was proposed; hatching indicates the LLM verification outcome. Right: Final status by math subject classification, with verification status omitted. The seven single-conjecture categories are not shown (AT, CT, CV, HO, LO, OA, and SG, with outcomes: three counterexamples, two proofs, and two unresolved).
Figure 3: Left: LLM classification of object novelty for counterexamples that were ‘verified‘ by the review pass. Counterexamples are classified as ‘off-the-shelf’, ‘standard construction’, or ‘nontrivial modification’. Right: LLM responses to the question ‘is it plausible that the conjecture’s authors implicitly excluded this case’ (i.e., the conjecture is misstated rather than genuinely refuted)?
Figure 4: Left: Relation of proof responses to the existing literature. Right: GPT-5.4 scores of viability were weakly predictive of outcome.
Appendix figures & tables10 assets
Supplementary material from the paper’s appendix.
Appendix
Conjectures per paper
1
2
3
4
5
6
7
8
9
10
≥ 11
Paper count
1,049
353
130
66
30
12
9
5
6
6
9
Appendix
Table 1: Per-paper conjecture count distribution over 1,675 papers.
Figure 5: math.* category of papers from OpenConjecture June 21st snapshot.
Figure 6: Left: distribution of input tokens per solver pass. First pass (GPT-5.6 Sol): N=197 (3 of 200 CIDs had missing token data), second pass (GPT-5.6 Sol): N=118, third pass (GPT-6 Astra): N=92. Right: distribution of output tokens per solver pass.
Figure 7: Distribution of the number of web search calls per response in the first pass.
Figure 8: Left: Taxonomy of citations in first pass responses. Right: distribution of number of citations per response. Citations of the source paper are excluded.
Figure 9: Left: Taxonomy of citations in second pass responses. Right: distribution of number of citations per response. Citations of the source paper are excluded.
Figure 10: Left: Taxonomy of citations in thid pass responses. Right: distribution of number of citations per response. Citations of the source paper are excluded.
Figure 11: Response length as measured by the prose word count (left) and the total number of claims with proof (right).
Figure 12: Prose word count by math.* classification.
First pass
Second pass
Third pass
Total
# defns
Proof
CEX
Unres.
Proof
CEX
Unres.
Proof
CEX
Unres.
0
28
38
89
9
11
82
10
4
69
340
1
3
5
25
1
0
6
0
1
2
43
2
1
3
3
0
2
1
1
0
3
14
3
0
1
1
0
0
2
0
1
0
5
4
1
2
0
1
2
0
0
0
0
6
Appendix
Table 2: Distribution of explicit solver-introduced definitions by solver pass and response type: proof, counterexample (abbreviated CEX) or unresolved. Counts exclude definition items classified as from the source paper, external literature, or standard mathematical background.
We construct OEIS Open, a benchmark based on 492 open mathematical conjectures from the OEIS, formalized in Lean by Tsoukalas et al. Whereas these conjectures had previously been attempted only with a bespoke agent, our open-source evaluation code runs any generic language model (LM) against them, and is secure against LM cheating attempts. We find that LMs equipped with a minimal set of tools resolve 147 of these conjectures with a budget of $50 per attempt, scoring 30% on OEIS Open. OEIS Open Lite is a random subset of 100 conjectures for cheaper evaluation. When evaluated with a budget of $200 per attempt, the best current LM scores 44% on OEIS Open Lite. Giving LMs access to the mathematics literature via 476,000 papers from arXiv did not increase performance on OEIS Open Lite, and nor did using more sophisticated agent loops. The conjectures covered in this work are of uncertain mathematical significance, and most have likely received little previous attention. Nevertheless, our results show that LMs can resolve open research conjectures autonomously and at modest cost.
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.
Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck +4
ETH Zurich · Aarhus University · Independent Researcher +1