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序列，并由一个带有循环操作符的学习指导综合系统猜测。这些运算符实现了对自然数的递归，因此许多证明都需要对自然数进行归纳。基准数据集中包含了来自广泛数学领域的各种难度的问题。我们认为这些特征将使其成为衡量这个领域中的归纳定理证明进展的有效评判标准。