By Shalosh B. EKHAD, Mingjia YANG and Doron Zeilberger
First Written: July 15, 2017
Exclusively published in the Personal Journal of Shalosh B. Ekhad and Doron Zeilberger and arxiv.org .
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).
(most of the functions also work on current versions of Maple, but some of them may give error messages).
Doron Zeilberger's Home Page