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

By Shalosh B. EKHAD and Mingjia YANG

.pdf   .ps   .tex

First Written: July 15, 2017

Exclusively published in the Personal Journal of Shalosh B. Ekhad and Doron Zeilberger and .

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).

Maple packages

Sample Input and Output for SCHUTZENBERGER12.txt

Personal Journal of Shalosh B. Ekhad and Doron Zeilberger

Doron Zeilberger's Home Page