Formalizing a Proof that e is Transcendental

Jesse Bingham


We describe a HOL Light formalization of Hermite's proof that the base of the natural logarithm e is transcendental.
This is the first time a proof of this fact has been formalized in a theorem prover.

Full Text:

PDF (English)

DOI: 10.6092/issn.1972-5787/2269

Copyright (c) 2011 Jesse Bingham

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.