Formalizing a Proof that e is Transcendental
Journal of Formalized Reasoning, Volume 4 (2011), / Harvested from Journal of Formalized Reasoning

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.

Published online : 2011-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/2269
@article{2269,
title = {Formalizing a Proof that e is Transcendental},
journal = {Journal of Formalized Reasoning},
volume = {4},
year = {2011},
doi = {10.6092/issn.1972-5787/2269},
language = {EN},
url = {http://dml.mathdoc.fr/item/2269}
}

Bingham, Jesse. Formalizing a Proof that e is Transcendental. Journal of Formalized Reasoning, Volume 4 (2011) . doi : 10.6092/issn.1972-5787/2269. http://gdmltest.u-ga.fr/item/2269/