Journal of Formalized Reasoning (Jan 2011)
Formalizing a Proof that e is Transcendental
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.