2023/04/06 by Thibault Gauthier, Gauthier, Thibault, Chad E. Brown +5
Computer Science · Mathematics · #Algebra over a field #Algorithm #Benchmark (surveying) #Calculus (dental) #Computability, Logic, AI Algorithms #Computer science #Discrete mathematics #Encyclopedia #Equivalence (formal languages) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Mathematical induction #Mathematical proof #Mathematics #Pure mathematics #Recursion (computer science) #Sequence (biology) #Theoretical computer science #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2304.02986
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2023/04/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.