# A Mathematical Benchmark for Inductive Theorem Provers

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Apr 2023.

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

- [Learning Conjecturing from Scratch](https://mlsanity.com/paper/2503.01389/) (2025)
- [Artifical intelligence and inherent mathematical difficulty](https://mlsanity.com/paper/2408.03345/) (2024)

## Abstract (arXiv)

We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come.