2 papers
cs.LO2017
Distant decimals of
Yves Bertot, Laurence Rideau, Laurent Théry
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…
cs.LO2015
Formal Proofs of Transcendence for e and as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau +1
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 conside…