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.

翻译：我们提出一个由在线整数序列百科全书（OEIS）衍生的包含29687个问题的基准。每个问题表达了两个语法不同但生成相同OEIS序列的程序之间的等价性。这些程序由使用带循环算子语言的学习引导合成系统推测得出。这些算子实现了递归，因此许多证明需要对自然数进行归纳。该基准包含来自广泛数学领域、难度各异的问题。我们相信，这些特性将使其在未来数年成为衡量该领域归纳定理证明器进展的有效判据。