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: Sep 25 2021 at 09:17 UTC