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

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/