Formal proofs of hypergeometric sums

Dedicated to the memory of Andrzej Trybulec.

Journal of Automated Reasoning, vol. 55, pp. 223-243 (2015).

Abstract:

Algorithmic methods can successfully automate the proof, and even the discovery, of a large class of identities involving sums of hypergeometric terms. In particular, the Wilf-Zeilberger (WZ) algorithm is a uniform framework for a substantial class of hypergeometric summation problems. This algorithm can produce a rational function certificate that can, on the face of it, be used to verify the result by routine algebraic manipulations, independently of the working of the algorithm that discovered it. It is therefore very natural to consider using this certificate to produce, by automated means, a rigorous deductive proof in an interactive theorem prover. However, naive presentations of the WZ method tend to gloss over trivial-looking but rather knotty questions about zero denominators, which makes their rigorous formalization tricky and their ultimate logical justification somewhat obscure. We describe how we have handled these difficulties to produce rigorous WZ proofs inside the HOL Light theorem prover.

PDF

Bibtex entry:

@ARTICLE{harrison-wz,
        author          = "John Harrison",
        title           = "Formal proofs of hypergeometric sums
                           (Dedicated to the memory of Andrzej Trybulec)",
        journal         = "Journal of Automated Reasoning",
        year            = 2015,
        volume          = 55,
        pages           = "223--243"}