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

arXiv: https://arxiv.org/abs/2608.11941 · HTML: https://mlsanity.com/paper/2608.11941/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 13 references that are in the map.
- First posted on arXiv 12 Aug 2026.

## Builds on (most cited first, 3 of 3)

- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verification](https://mlsanity.com/paper/2603.15617/) (2026)

## Built on by (most cited first, 2 of 2)

- [FrontierMath ErdHos](https://mlsanity.com/paper/2609.25050/) (2026)
- [LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models](https://mlsanity.com/paper/2609.32264/) (2026)

## Abstract (arXiv)

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.