Hi all,

I am not a math-comp user per se, as I mainly do proofs in HOL4, but I am currently trying to find out how different ITP systems have formalized pi, and proven properties of it.

I already found the definition and proofs for Pi from CCorn (https://github.com/coq-community/corn/blob/master/transc/Pi.v) but for math-comp I am struggling to search through the official documentation. Searching for pi in the definition index (https://math-comp.github.io/htmldoc_1_13_0/index_definition_P.html) I could not find any definition that looked like the mathematical constant pi.

Thanks in advance for any replies,

Heiko

have you seen this? http://www-sop.inria.fr/marelle/distant-decimals-pi/

references https://github.com/thery/Plouffe which builds with latest Coq

I did not run into this before. Thanks a lot for the pointer!

also, proof of transcendence for pi: https://arxiv.org/abs/1512.02791

I think the latest code for this is here: https://github.com/Sobernard/Lindemann

would be nice to get the Lindemann repo maintained and working with latest Coq/MathComp (cc: @Yves Bertot )

I think most of everyone is using the Pi definition from Stdlib as a spec: https://github.com/coq/coq/blob/master/theories/Reals/Rtrigo1.v#L227

There is also an interval enclosure computing function in CoqInterval https://gitlab.inria.fr/coqinterval/interval/-/blob/master/src/Interval/Float_full.v#L41

Last updated: Feb 27 2024 at 22:02 UTC