Distant decimals of $π$

• Published in 2017
• Added on 2023-08-14

We describe how to compute very far decimals of \(\pi\) 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 \(\pi\) 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.

Links

• http://arxiv.org/abs/1709.01743v2
• http://arxiv.org/pdf/1709.01743v2

Other information

BibTeX entry

@article{DistantdecimalsofPi,
	key = {DistantdecimalsofPi},
	type = {article},
	title = {Distant decimals of {\$}π{\$}},
	author = {Yves Bertot and Laurence Rideau and Laurent Th{\'{e}}ry},
	abstract = {We describe how to compute very far decimals of \(\pi\) 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 \(\pi\) 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.},
	comment = {},
	date_added = {2023-08-14},
	date_published = {2017-12-07},
	urls = {http://arxiv.org/abs/1709.01743v2,http://arxiv.org/pdf/1709.01743v2},
	collections = {basically-computer-science,fun-maths-facts},
	url = {http://arxiv.org/abs/1709.01743v2 http://arxiv.org/pdf/1709.01743v2},
	year = 2017,
	urldate = {2023-08-14},
	archivePrefix = {arXiv},
	eprint = {1709.01743},
	primaryClass = {cs.LO}
}