Automated Proofs of Many Conjectured Recurrences in the OEIS made by R.J. Mathar

TL;DR

This paper presents an automated method and implementation for proving many conjectured linear recurrences in the OEIS, transforming conjectures into rigorously proven theorems, and proposes a new category for such conjectures.

Contribution

The paper introduces an algorithm and Maple package to automatically prove OEIS conjectures about linear recurrences, and suggests a new category of 'provable conjecture' for the database.

Findings

Successfully proved many OEIS conjectures using the algorithm.

Implemented the proof process in a Maple package.

Proposed a new category 'provable conjecture' for the OEIS.

Abstract

The On-Line Encyclopedia Of Integer Sequences , that wonderful resource that most combinatorialists, and many other mathematicians and scientists, use at least once a day, is a treasure trove of mathematical information, and, one of its charms is that it contains many intriguing conjectures. But one should be on one's guard, because some of the conjectures are either already theorems, or can be routinely proved. In this case study we demonstrate, and actually fully implement (in an accompanying Maple package), how to turn many conjectures made in the OEIS by R.J. Mathar, regarding linear recurrences satisfies by a certain class of sequences, into fully rigorously-proved theorems, but we argue, that one should not emulate us, and while it is nice to have one example, of an algorithm to actually construct proofs (that are known to exist by a priori theoretical reasons), life is too short to do it in all cases, and hence we propose a new category for the OEIS, that of "provable conjecture", as opposed to "proved conjecture" (alias theorem).