Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Hermite–Lindemann–Weierstr...


view this post on Zulip 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: Sep 25 2021 at 09:17 UTC