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

Tom Adamczewski

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 a…