Distant decimals of $π$ - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Automated Reasoning Année : 2018

Distant decimals of $π$

Décimales distantes de $π$

Yves Bertot
Laurence Rideau
  • Fonction : Auteur
  • PersonId : 832430
Laurent Théry

Résumé

We describe how to compute very far decimals of $π$ and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment where 1 million decimals of $π$ and the billionth hexadecimal (without the preceding ones) have been computed in a formally verified way. Three methods have been studied, the first one relying on a spigot formula to obtain at a reasonable cost only one distant digit (more precisely a hexadecimal digit, because the numeration basis is 16) and the other two relying on arithmetic-geometric means. All proofs and computations can be made inside the Coq system. We detail the new formalized material that was necessary for this achievement and the techniques employed to guarantee the accuracy of the computed digits, in spite of the necessity to work with fixed precision numerical computation.
Fichier principal
Vignette du fichier
main.pdf (351.14 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01582524 , version 1 (06-09-2017)
hal-01582524 , version 2 (11-12-2017)

Licence

Paternité - Pas de modifications

Identifiants

Citer

Yves Bertot, Laurence Rideau, Laurent Théry. Distant decimals of $π$: Formal proofs of some algorithms computing them and guarantees of exact computation. Journal of Automated Reasoning, 2018, 61, pp.33-71. ⟨10.1007/s10817-017-9444-2⟩. ⟨hal-01582524v2⟩
461 Consultations
226 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More