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

TL;DR - OEIS Open benchmarks language models on 492 open mathematical conjectures formalized in Lean. Generic LMs autonomously proved up to 30% of the full benchmark, suggesting they can resolve some neglected conjectures at modest cost.

• Minimal-tool LMs solved 147 of 492 conjectures with a $50 budget per attempt.
• The best model solved 44% of the 100-problem OEIS Open Lite subset at $200 per attempt.
• Access to 476,000 arXiv papers did not improve Lite performance.
• More sophisticated agent loops also provided no improvement.