Distant Decimals of PI

This page contains links to the Coq sources for experiments we made to compute decimals of π. An article has been published on the subject, the preprint is available here.

Computing hexa-decimals using the Bailey-Borwein-Plouffe formula

Sources of the coq code can be gathered from the following git repository

Computing millions of decimals using arithmetic geometric means

Sources of the coq code can be gathered from the following git repository

Opam packages

Opam packages are also available for both developments, under the names coq-plouffe and coq-pi-agm. Both packages are part of the coq-released opam repository.

Synchronised version with submitted articles

article "distant decimals of π"

We submitted a paper "distant decimals of π" for a special issue of the Journal of Automated Reasoning. The versions of the sources at the time of submission are here:

Minor improvements were later proposed, mostly to obtain versions that are compatible with more recent version of coq and Coquelicot (both archives made on April 6, 2017).

These developments are compatible with coq-8.6, Coquelicot 2.1.2 and mathcomp-ssreflect 1.6.1.

Another version is proposed for the Bailey-Borwein-Plouffe formula, which is compatible with Coquelicot version 3.0.0.

Instruction on how to install these developments

Once the packages are installed, to load these developments in your version of Coq and display the statements of the main theorems, you should run the following commands.

Require Import Plouffe.CPlouffe Plouffe.Million agm.rounding_correct agm.alg2.
Import rounding_big Reals.
(* correctness statement for the 1000000 hexa-decimal. The computation
   has already been performed at installation time. *)
About piDigit_1000000.

(* correctness statement for arbitrary digit rank. *)

About piDigit_correct.

(* Correctness statement to compute one million digits.
   This does not launch the computation. *)
About big_pi_osix.

(* correctness statement for arbitrary sizes. *)
About big_compute_eq.

(* running computations. This is is less than a second. *)
Eval native_compute in thousand_digit_pi.

(* The next one is about 3 minutes. *)
Eval native_compute in hundred_thousand_digit_pi.

If you want to run the computation for one million digit, you can replace hundred_thousand with million in the last command above, this computation will take around two hours.

Instructions on how to run these proofs step-by-step

If you want to run these proofs step-by-step, you need to re-compile them. For this follow the instructions from the previous section on installing, and then download the archives for plouffe and for the arithmetic-geometric mean extract them, and re-compile them.

(cd Plouffe-Submitted_article_version_nob; ./configure.sh; make)
(cd pi-agm-submitted-article-version-8.6; coq_makefile -f _CoqProject -o Makefile; make)

You should now be able to one of the interactive editing tool, either coqide, or Emacs with Proof general (follow this link for instructions on how to install these programs).

Edited on April 6, 2017