In plain words: A test set of 492 open conjectures from the integer-sequences encyclopedia, written in a proof-checking language, lets any language model try to prove them with tools, blocking cheating. Models proved 30% of them cheaply, showing they can settle real open problems on their own.
Abstract · OEIS Open: How many conjectures can language models turn into theorems?
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.
Tom Adamczewski
arXiv:2608.11941 · cs.AI · submitted Aug 12, 2026 · updated Aug 13, 2026
abstract · pdf · html · 26 pages, 6 figures. Code: https://github.com/epoch-research/LeanOpenProblems, results: https://github.com/epoch-research/LeanOpenProblems-results