A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)

Abstract : This paper describes the formal verification of an irrationality proof of ζ(3), the evaluation of the Riemann zeta function, using the Coq proof assistant. This result was first proved by Apéry in 1978, and the proof we have formalized follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and some asymptotic analysis that we conduct by extending the Mathematical Components libraries. The formalization of this proof is complete up to a weak corollary of the Prime Number Theorem.
Type de document :
Communication dans un congrès
ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-00984057
Contributeur : Assia Mahboubi <>
Soumis le : dimanche 27 avril 2014 - 11:01:22
Dernière modification le : jeudi 9 février 2017 - 15:49:37
Document(s) archivé(s) le : dimanche 27 juillet 2014 - 10:36:15

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00984057, version 1

Collections

Citation

Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria. 2014. <hal-00984057>

Partager

Métriques

Consultations de
la notice

604

Téléchargements du document

402