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

Maple packages

• SCHUTZENBERGER.txt, an expanded version of an older package that includes automatic discovery and proofs of recurrences satisfied by coefficients of algebraic equations given in terms of radicals.

• The following does a better job, but works better in Maple 12: SCHUTZENBERGER12.txt   .

  (most of the functions also work on current versions of Maple, but some of them may give error messages).

Sample Input and Output for SCHUTZENBERGER12.txt

• If you want to see an automatically generated article proving 33 of Mathar's conjecture

  the input file generates the output file.

Doron Zeilberger's Home Page