Coq and Maple scripts for the formal proof of Apéry's theorem

(June 2014)

The following files will help the readers of our paper understand our formalization work. We provide:

• our Coq formalization sources,
• for readers who have access to Maple, the Maple scripts that generated the generated part in our Coq scripts: a pretty-printer of Maple expressions to Coq syntax, d-finite algorithmic cascade in Maple. (Put both in a new directory, run Maple on the second.)