Email Gateway (Mar 12 2021 at 14:38): Email Gateway (Mar 12 2021 at 14:38):From: Lawrence Paulson <lp15@cam.ac.uk>
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!
Larry Paulson
Last updated: Jul 15 2022 at 23:21 UTC