Formal Proofs of Transcendence for e and $\pi$ 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 $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are often conside…