%0 Journal Article
%T Formalizing a Proof that e is Transcendental
%A Jesse Bingham
%J Journal of Formalized Reasoning
%D 2011
%I University of Bologna
%X 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.
%U http://jfr.cib.unibo.it/article/view/2269/1749