OEIS Open: How many conjectures can language models turn into theorems?

OEIS Open: How many conjectures can language models turn into theorems?

Tom Adamczewski, Epoch AI

arXiv:2608.11941v1 [cs.AI] 12 Aug 2026

Abstract

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.

1. Introduction

The paper notes that recent examples of AI systems solving open problems in mathematics are impressive but fall short of a systematic study of AI capabilities for several reasons: they do not disclose the universe of problems attempted, the extent of human guidance is unclear, and different AI models are not systematically compared on the same problems.

Existing benchmarks of open problems include HorizonMath [101 problems] and FrontierMath: Open Problems [FM:OP, 50 problems]. Both make unsolved problems verifiable by restricting attention to problems with a generator–verifier gap. These strategies face challenges:

1. They cannot be used to test most of research mathematics (most open problems have no generator–verifier gap).

2. Passing the check is evidence rather than proof.

3. Soundness rests on hand-crafted verification code and filters.

4. Computational checking is one-sided (if no object exists, the task is unsolvable).

The authors 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. This addresses the first challenge: eligibility requires only that a conjecture’s statement be formalizable. The other challenges are avoided outright: an accepted proof is definitive, soundness rests on the Lean kernel, and false conjectures remain solvable tasks because the model may prove the negation.

Using formal proofs has downsides:

1. Not all research mathematics can be covered (must be stateable with Mathlib definitions).

2. Results reflect formalization ability as well as mathematical ability.

There is a risk of misformalization, but the authors use conjectures about integer sequences to reduce this risk.

2. Methods

2.1 Conjectures

The conjectures were collected and formalized by Tsoukalas et al. They began with a corpus of 2649 open conjectures drawn from the OEIS, prompted Gemini to select 500 problems that are non-trivial, mathematically interesting, not famous open problems, and good candidates for automated theorem-proving, and used a Gemini-based agent to formalize them in Lean. Eight of the 500 were excluded for technical reasons, leaving 492.

Conjectures about integer sequences have relatively low misformalization risk because they generally involve only integers and elementary operations.

2.2 Conjecture metadata

The authors collected metadata on each conjecture: provenance (who proposed it, and when) and attention its sequence has received. The 492 conjectures concern 444 distinct OEIS sequences. They used GPT-5.5 to match each Lean conjecture to the OEIS text and identify proposer and date. This yielded a proposer for 488 and a date for 489 of the 492 conjectures.

Literature attention was measured via citations on the OEIS entry and works in OpenAlex whose full text references the sequence. Both measures exclude references to Tsoukalas et al.'s own results.

2.3 Proof verification

Following Tsoukalas et al., the authors accept a submission only if it passes SafeVerify, an open-source checker that checks the proof against the theorem specification and guards against environment exploits (e.g., axiom injection). SafeVerify is adapted from lean4checker. Each target declaration must be present with the same name, kind, and kernel type, and may use no axioms beyond the standard three (propext, Quot.sound, Classical.choice).

The evaluation splits every attempt across three Docker containers, none with network access:

1. Agent container (model works on proof)

2. Compile container (clean Lean toolchain, proof compiled to olean)

3. Scorer container (runs SafeVerify on the submission)

This design defeats many attack classes: tampering with agent environment, malicious compile-time code, proving a different statement, redefining definitions, smuggling in extra axioms, and bypassing the kernel.

2.4 AI agent

The base agent is a ReAct-style tool loop built on the Inspect library, with three tools: bash, a text editor, and a resources tool. The agent container provides Lean 4 with Mathlib, SageMath, Python with sympy, mpmath, numpy, and pantograph.

The agent can either prove or disprove the conjecture. The agent iterates until it resolves the conjecture or hits a limit (typically 50 per conjecture on the full set, 200 on LITE; agents also cannot use more than 72 hours).

Notably, all agents are considerably simpler than the full-featured agent used by Tsoukalas et al., which runs an AlphaEvolve-style evolutionary search with prover subagents (Gemini 3.1 Pro), AlphaProof, and rater subagents (Gemini 3.0 Flash).

2.4.1 Literature

This variant gives agents access to an offline snapshot of the mathematics literature: the LATEX source trees of 476,000 pure-mathematics arXiv papers dated up to 2022.

2.4.2 DeepAgent

The DeepAgent variant replaces the ReAct loop with Inspect's deepagent, which adds delegation to subagents, persistent memory, a todo-list tool, and a longer system prompt.

3. Results

3.1 AI performance

A model resolves a conjecture when it submits a proof of the conjecture or of its negation that passes verification. On the full OEIS OPEN set, each model ran once with a 50 spending cap per conjecture.

Language models can resolve many open OEIS conjectures, and outperform AlphaProof Nexus:

• Claude Opus 4.8 resolved 30% of the 492 conjectures (147)

• GPT-5.5 resolved 26%

• Gemini 3.5 Flash resolved 22%

• AlphaProof Nexus resolved 44 of the same 492 conjectures (9%)

On OEIS OPEN LITE, with the cap raised to 200 per conjecture:

• Gemini 3.5 Flash: 29%

• Claude Fable 5: 44%

• GPT-5.6 Sol: 43% (evaluated only on LITE)

Agent variants had no effect. Neither giving models access to the mathematics literature, nor using the more complex DeepAgent affected accuracy on LITE.

Solve rates appear to rise log-linearly with spend, on the order of ten percentage points per tenfold increase.

4. Discussion

Formalized open conjectures are reusable infrastructure. A simple harness performed well: the base agent resolved more than three times as many conjectures as AlphaProof Nexus's elaborate evolutionary search. This fits the bitter lesson: rather than prescribing how the model should work through problem-specific structure, it may be better to give a model simple tools and let it choose how to use them.

On this benchmark, Claude Fable 5 and GPT-5.6 Sol do not represent a qualitative jump in autonomous AI proving. The two newest-generation models scored highest on OEIS OPEN LITE (43–44%), but their lead over the previous generation is only a few percentage points.

Further scaling inference would resolve more conjectures. At 200 per conjecture, the best current models would resolve about 216 of the 492 conjectures, up from 147 at 50. Solve rates rose roughly log-linearly in spend without a clear plateau, so larger budgets would likely push past 44% (at exponential cost).

4.1 Limitations

• Though open, most conjectures have likely received little attention. The prolific conjecturer Zhi-Wei Sun proposed 37% of OEIS OPEN and 36% of OEIS OPEN LITE. For 47% of the conjectures, the underlying sequence's OEIS entry lists no links or references.

• Misformalization risk: Tsoukalas et al. explained that all 44 conjectures resolved by their system were reviewed by a human and no misformalizations were found. The authors took the dataset as-is without further validation. Misformalizations are likely to be easier to resolve than correctly formalized conjectures.

• No credit for reductions to famous open problems: the setup accepts only a proof of the conjecture or its negation, not results relating a conjecture to a famous open problem.

• Resolved conjectures may leak into training data: models evaluated have training cutoffs that predate the publication of Tsoukalas et al., so they cannot have learned the proofs released with that paper. For future models, the issue can be mitigated by filtering out conjectures resolved before a model's training cutoff.

Appendix A.1

The appendix includes Table 1 showing the 100 costliest of the 153 conjectures resolved by either Claude Fable 5 on OEIS OPEN LITE or Claude Opus 4.8 on the full set. The table includes sequence numbers, conjecture statements, proof summaries (written by GPT-5.6 Sol agents), and costs. Examples include:

• A364173: Proved at cost 130. The proof applies Legendre's Gamma duplication formula, factors out powers of p, and uses reciprocal-sum cancellations and a Morley-type parity identity.

• A333096: Proved at cost 119. The proof rewrites the sequence using a Cartier fixed-point identity and Legendre–Kummer/Stirling-number valuation bounds.

• A232616: Disproved at cost 56. The counterexample is n = 550172, showing a(550172) ≥ 17135927 while 2(p550172 − 1) ≤ 17135926.

• A381358: Proved at cost 46. The proof uses stable prefix/suffix patterns and a positive left-eigenvector functional to show the limit is approximately 1.5550575766.

• A263001: Disproved at cost 41. A certified computation shows a(51156) = 1 with unique pair (k, m) = (16, 1119), contradicting the claimed uniqueness classification.

• A309391: Disproved at cost 27. Let p = 16843, a Wolstenholme prime; n = p2 = 283686649 is composite but A309391(n) = n.

• A355898: Disproved at cost 13. Assuming the first identity, fast doubling modulo p = 195318521017 shows p would divide both a249580077006 and a249580077007, contradicting the defining recurrence at n = 249580077008.

• A194806: Proved at cost 7. The proof uses a covering set consisting of [1, K] together with primes at most n, showing a(n) ≤ 5π(n).

• A248802: Proved at cost 3. Modular-order reduction and a periodicity lemma show 67 always divides the relevant number and no smaller prime does.

Appendix A.2

Figure 3 shows accuracy on OEIS OPEN LITE by model and agent variant (base, DeepAgent, literature), with no significant differences between variants.

Appendix A.3

Solve rates are broken down by conjecture metadata:

• Figure 4: Solve rate binned by citation metadata (OEIS page citations and OpenAlex works). No clear pattern of higher solve rates for more-cited sequences.

• Figure 5: Conjectures by proposer, with solve outcomes. Zhi-Wei Sun proposed the largest share.

• Figure 6: Solve rate by year proposed. No strong trend across years.

Based on this paper, I can make the following specific improvements to AI systems:

1. Implement a minimal-tool ReAct agent loop as the default proving architecture

• Replace complex multi-agent evolutionary search systems with a simple bash + text editor + resource tool loop. This improves solve rates by 3x over elaborate agent designs (30% vs 9%).

• The improved system can autonomously explore Lean proofs, run computations, and iterate without prescriptive problem-specific scaffolding.

2. Add a formal-proof verification layer with container isolation

• Integrate SafeVerify-style checking across three isolated Docker containers (agent, compile, scorer) to prevent environment exploits, axiom injection, and statement tampering.

• The improved system can securely verify proofs against kernel-level checks, making it safe to deploy on untrusted mathematical conjectures.

3. Enable disproving capability alongside proving

• Allow the system to prove either the conjecture or its negation. This doubles the solution space and handles false conjectures (e.g., A232616, A263001, A309391 were all disproved).

• The improved system can resolve open problems even when the original statement is incorrect, producing counterexamples with certified computations.

4. Integrate a spend-scaling scheduler

• Since solve rates rise log-linearly with budget (10 percentage points per 10x spend), implement dynamic budget allocation that increases per-conjecture spend until a plateau is detected.

• The improved system can automatically decide when to escalate from 50 to 200+ per problem, potentially resolving 216/492 conjectures at 200 vs 147 at 50.

5. Add literature access as an optional, non-blocking tool

• The paper shows literature access (476k arXiv papers) did not improve performance, so make it available but not mandatory. This avoids wasted computation while retaining potential benefits for future harder problems.

• The improved system can query relevant papers only when the agent explicitly requests them, without degrading baseline performance.

6. Implement a training-data leakage filter

• For future model versions, filter out conjectures resolved before the model's training cutoff to prevent memorization artifacts.

• The improved system can maintain a dynamic benchmark subset that ensures fair evaluation across model generations.

7. Add a formalization-quality validator

• Use the paper's metadata (proposer, date, citation counts) to flag low-attention conjectures that may have misformalizations. Prioritize solving high-attention, well-formalized problems first.

• The improved system can triage conjectures by estimated correctness, focusing compute on problems with lower misformalization risk.

8. Enable proof summarization and knowledge distillation

• Use the system's successful proofs (e.g., Legendre duplication, Cartier fixed-point identities, modular-order reductions) to generate human-readable proof summaries.

• The improved system can automatically produce reusable lemmas and proof patterns that accelerate future solving on similar number-theoretic problems.

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.