Off-the-shelf language models can autonomously prove many formalized OEIS conjectures: Claude Opus 4.8 solved 30% of 492 problems at $50 a try, while the best models solved 44% of a 100-problem subset with $200 budgets—access to large math corpora or more elaborate agent loops provided no clear benefit.

Main Finding

Language models, equipped with a minimal toolset and run in a secure formal-verification harness, can autonomously convert a substantial fraction of open OEIS conjectures into machine-checked theorems. On a 492-conjecture Lean benchmark (OEIS OPEN) LMs resolved 147 conjectures (30%) using a $50-per-conjecture budget; on a 100-conjecture subset (OEIS OPEN LITE) the best model reached 44% with $200-per-conjecture. More complex agents or giving models access to a 476k-paper arXiv math corpus did not improve results. Solve rates increase roughly log-linearly with per-instance spend.

Key Points

• Benchmark: OEIS OPEN — 492 open conjectures from the OEIS, formalized in Lean (derived from Tsoukalas et al.).
• Top result (OEIS OPEN, $50/case): Claude Opus 4.8 resolved 30% (147/492). Other models: GPT-5.5 (26%), Gemini 3.5 Flash (22%).
• OEIS OPEN LITE (100 cases, $200/case): best models ≈ 43–44% (Claude Fable 5, GPT-5.6 Sol).
• Baseline comparison: AlphaProof Nexus (more elaborate search) previously resolved ~9% on the same 492 problems; the simple ReAct-style agent here substantially outperformed it.
• Agent simplicity: a minimal ReAct loop with three tools (bash, text editor, budget/resource reporter) plus a Lean toolchain, SageMath, and Python libraries sufficed; richer agents (DeepAgent) did not improve accuracy.
• Adding literature (476k arXiv math papers, up to 2022) did not improve solve rates.
• Cost efficiency: average cost per resolved conjecture in runs was low (roughly $6–$10 depending on model); solve rate scales roughly linearly with log(spend) — ~10 percentage points gained per tenfold spend increase.
• Security/verifiability: submissions accepted only if SafeVerify (kernel-level replay/check) in an isolated container accepts them; compilation and verification split across isolated containers to prevent cheating.
• Limitations noted by authors: uncertainty about the mathematical significance of these conjectures, risk of misformalization, potential for solved proofs to leak into future training data (changing difficulty), and lack of credit for reductions to known hard problems.

Data & Methods

• Problem source and formalization
  • Starting pool: 2,649 OEIS open conjectures; Gemini selected 500 candidates and Tsoukalas et al. formalized them in Lean; final set analyzed here is 492 conjectures.
  • Conjectures mostly concern integer sequences—chosen to reduce misformalization risk.
• Metadata
  • For each conjecture the authors extracted proposer, proposal date, and measures of literature attention (OEIS entry links/references and OpenAlex full-text matches). GPT-5.5 was used to match Lean statements to OEIS text.
  • Observed concentration: a small number of prolific proposers (e.g., Zhi-Wei Sun contributed ~37%).
• Verification pipeline
  • Proofs must be submitted as Lean source and pass SafeVerify (adapted from lean4checker). SafeVerify replays declarations through a fresh kernel and enforces a three-axiom whitelist; it rejects axioms or environment tampering.
  • Three-container sandbox: agent container (no network), compile container (clean toolchain produces olean), and scorer container (runs SafeVerify against trusted statement olean). This isolates and mitigates many attack vectors.
• Agent design and tools
  • Base agent: ReAct-style loop (Inspect library) with tools: bash, text editor, resource reporter. Provided runtime: Lean 4 + Mathlib, SageMath, Python (sympy, mpmath, numpy, pantograph).
  • Variants: (1) Literature-enabled agent (offline LaTeX of 476k arXiv math papers), (2) DeepAgent (adds subagents, persistent memory, todo list, more opinionated prompt).
  • Agents allowed to either prove or disprove a conjecture. Per-conjecture caps: $50 for full set runs; $200 for LITE; 72-hour runtime cap.
• Models evaluated (examples)
  • Claude Opus 4.8, GPT-5.5, Gemini 3.5 Flash, Claude Fable 5, GPT-5.6 Sol (some models evaluated only on LITE).
• Outcome measurement
  • A conjecture is counted resolved when a submitted proof/disproof passes SafeVerify. Cross-checks with another verifier (Comparator) changed a few verdicts but not high-level conclusions.

Implications for AI Economics

• Low marginal cost to produce formal results (per-proof)
  • Measured average cost per resolved conjecture was on the order of single-digit U.S. dollars ($6–$10) under the reported budgets. If broadly representative, automated formal proving could be a highly cost-effective way to produce verifiable mathematical results, implying high short-term returns to deploying inference compute for discovery tasks with formal verification.
• Diminishing but steady returns to inference spending
  • Solve rates rise roughly linearly with log(spend), so improving total solved share requires exponential increases in per-instance spend for linear absolute gains. This shapes cost-benefit tradeoffs: modest budgets yield many low-hanging results; moving to majority-solve rates becomes increasingly expensive.
• Development vs. deployment investment tradeoff
  • A very simple agent plus off-the-shelf LMs outperformed a bespoke, compute-heavy evolutionary system. For commercial or academic services, this suggests higher ROI from investing in model access and simple tooling rather than complex bespoke search infrastructure—lower engineering costs to reach strong performance.
• Data-acquisition value may be task-dependent
  • Adding a large offline literature corpus (476k arXiv math papers) did not help on these OEIS conjectures. For product decisions, the marginal value of collecting/curating large specialized corpora can be small for some automated discovery tasks—implying careful prior analysis before investing heavily in data procurement for similar tasks.
• Market and incentive effects
  • If automated systems can cheaply produce formal proofs for many open (though not necessarily high-impact) conjectures, markets may emerge for automated theorem-proving-as-a-service, formalization pipelines, and verification tooling. However, the economic value of solved problems depends on their external scientific importance, which here is unclear for many OEIS conjectures.
• Externalities and measurement challenges
  • Resolved conjectures entering training data create positive feedback (easier solves later) and complicate benchmarking and competition among providers (models may reproduce seen proofs). This poses an economic externality: early solvers create assets that advantage later models unless benchmarks and evaluations proactively filter solved items.
• Risk, reliability, and downstream cost
  • Misformalization risk and differences between formalization effort and mathematical significance introduce potential reputational and verification costs. Buyers of automated-proving services or funders should budget for human audit, curation, and validation when high-stakes or high-value results are sought.
• Policy and public-good considerations
  • The benchmark and verification infrastructure are reusable public goods. Public investment or open releases can have high social value by enabling independent evaluation, reproducibility, and competition—lowering barriers to entry for small actors in automated research services.

Overall, the paper shows that accessible LM + tooling setups can produce many machine-checked theorems at modest monetary cost, but economic value per theorem depends on problem importance, and scaling to higher coverage requires substantially more spend.