Search papers, labs, and topics across Lattice.
This paper introduces OEIS Open, a benchmark that evaluates language models (LMs) on 492 open mathematical conjectures formalized in Lean. The study reveals that LMs can autonomously resolve 147 conjectures with a budget of $50 per attempt, achieving a score of 30% on the benchmark, while a more extensive evaluation on a subset of 100 conjectures shows a maximum score of 44% with a $200 budget. Notably, providing access to a vast mathematics literature did not enhance performance, indicating that LMs can tackle these conjectures effectively without extensive prior knowledge.
Language models can autonomously resolve open mathematical conjectures at a surprisingly low cost, achieving notable success without relying on extensive prior literature.
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.
