Automatic Derivation of the irrationality of e

摘要

As part of a project on automatic generation of proofs involving both logic and com- putation, we have automatically generated a proof of the irrationality of e. The proof involves inequalities, bounds on infinite series, type distinctions (between real numbers and natural numbers), a subproof by mathematical induction, and significant math- ematical steps, including correct simplification of expressions involving factorials and summing an infinite geometrical series.