Computing thousands or millions of digits of PI with arithmetic-geometric means This is a proof of correctness for an algorithm to compute PI to high precision using an algorithm based on arithmetic-geometric means. A first file contains the calculus-based proofs for an abstract view of the algorithm, where all numbers are real numbers. A second file describes how to approximate all computations using large integers. The whole development can be used to produce mathematically proved and formally verified approximations of PI.

opam install coq-pi-agm.1.0.0

- homepage
- http://www-sop.inria.fr/members/Yves.Bertot/
- license
- CeCILL-B
- bugs tracker
- yves.bertot@inria.fr
- dependencies
- coq (>= 8.4pl4 & < 8.5~) & coq-ssreflect = 1.5.0 & coq-coquelicot = 2.0.1
- source
- http://www.inria.fr/sophia/members/Yves.Bertot/proofs/pi_agm_1_0_0.tar.gz
- package
- https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-pi-agm/coq-pi-agm.1.0.0