Abstract
An elementary proof is formalised: that exp r is irrational for
every nonzero rational number r. The mathematical development comes
from the well-known volume Proofs from THE BOOK,
by Aigner and Ziegler, who credit the idea to Hermite. The development
illustrates a number of basic Isabelle techniques: the manipulation of
summations, the calculation of quite complicated derivatives and the
estimation of integrals. We also see how to import another AFP entry (Stirling's formula).
As for the theorem itself, note that a much stronger and more general
result (the Hermite--Lindemann--Weierstraß transcendence theorem) is
already available in the AFP.