Résumé : We report on the formal verification of an irrationality proof of the evaluation at 3 of the Riemann zeta function. This verification uses
the Coq proof assistant in conjunction with algorithmic calculations in Maple. This irrationality result was first proved by Apéry in
1978, and our formalization follows the proof path of his original presentation. The crux of it is to establish that some sequences
satisfy a common recurrence. We formally prove this by an a posteriori verification of calculations performed by a Maple
session. This bases on computer-algebra algorithms implementing Zeilberger's approach of creative telescoping. This experience
illustrates the limits of the belief that creative telescoping can discover recurrences for holonomic sequences that are easily checked a
posteriori. We discuss this observation and describe the protocol we devised in order to produce complete formal proofs of the recurrences.
Beside establishing the recurrences, our proof combines the formalization of arithmetical ingredients and of some asymptotic analysis.
Joint work with Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi.
Dernière modification : vendredi 13 novembre 2015 | Contact : Cyril.Banderier at lipn.univ-paris13.fr |