Formalizing a Proof that e is Transcendental

Jesse Bingham

doi:10.6092/issn.1972-5787/2269

Formalizing a Proof that e is Transcendental

Authors

Jesse Bingham Intel corporation

DOI:

https://doi.org/10.6092/issn.1972-5787/2269

Abstract

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.

Downloads

Published

2011-12-14

How to Cite

Bingham, J. (2011). Formalizing a Proof that e is Transcendental. Journal of Formalized Reasoning, 4(1), 71–84. https://doi.org/10.6092/issn.1972-5787/2269