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.
@article{arxiv.2304.02986,
title = {A Mathematical Benchmark for Inductive Theorem Provers},
author = {Thibault Gauthier and Chad E. Brown and Mikolas Janota and Josef Urban},
journal= {arXiv preprint arXiv:2304.02986},
year = {2023}
}