English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

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 ofmathematics that are often considered separately: calculus (real and elementarycomplex analysis) and algebra. For the work on calculus, we rely on theCoquelicot library and for the work on algebra, we rely on the MathematicalComponents library. Moreover, some of the elements of our formalized prooforiginate in the more ancient library for real numbers included in the Coqdistribution. The case of $\pi$ relies extensively on properties ofmultivariate polynomials and this experiment was also an occasion to put totest a newly developed library for these multivariate polynomials.

Formal Proofs of Transcendence for e and $\pi$ as an Application of Multivariate and Symmetric Polynomials