From: Lawrence Paulson <firstname.lastname@example.org>
I’m happy to announce yet another substantial contribution by the prolific Manuel Eberl:
The Hermite–Lindemann–Weierstraß Transcendence Theorem
This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory. … This has a number of direct corollaries, e.g. e, pi and numerous expressions involving transcendental functions are transcendental.
Manuel remarks that this theorem is “#56 on Freek Wiedijk's list. That puts us on par with HOL Light.”
You’ll find it online at https://www.isa-afp.org/entries/Hermite_Lindemann.html
Manuel, many thanks!
Last updated: Sep 25 2021 at 09:17 UTC