The proof of the formula Plouffe.html, Plouffe.v

The proof of the program CPlouffe.html CPlouffe.v

It requires ssreflect and coquelicot to compile. We can have a tar file or an opam package.

Require Import CPlouffe. Compute digit 1000000. = "2"%string : string

or the one billionth decimal :

Compute digit 1000000000. = "F"%string : stringThe computation is performed in fixed size (the default is 40 bits). If it is not enough the program returns ? as a digit. Increasing the size will solve the problem.

Laurence Rideau & Laurent Théry