J. Bingham, “Formalizing a Proof that e is Transcendental”, JFR, vol. 4, no. 1, pp. 71–84, Jan. 2011.