Formal proofs of hypergeometric sums
Dedicated to the memory of Andrzej
Journal of Automated Reasoning, vol. 55, pp. 223-243 (2015).
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.
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"}