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.

 [Slides.pdf]

Dernière modification : Monday 27 May 2024

Contact pour cette page : Cyril.Banderier at lipn.univ-paris13.fr