Showing 1–2 of 2 results for author: Rideau, L

Distant decimals of $π$

Authors: Yves Bertot, Laurence Rideau, Laurent Théry

Abstract: 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… ▽ More 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. △ Less

Submitted 11 December, 2017; v1 submitted 6 September, 2017; originally announced September 2017.

Comments: Journal of Automated Reasoning, Springer Verlag, A Para{î}tre

Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials

Authors: Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub

Abstract: We describe the formalisation in Coq of a proof that the numbers e and $π$ are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreov… ▽ More We describe the formalisation in Coq of a proof that the numbers e and $π$ are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of $π$ relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials. △ Less

Submitted 9 December, 2015; originally announced December 2015.

Comments: in Jeremy Avigad and Adam Chlipala. Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. ACM Press, pp.12, 2016