Formalizing a Proof that e is Transcendental
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.
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2011-01-01
|
| Series: | Journal of Formalized Reasoning |
| Online Access: | http://jfr.cib.unibo.it/article/view/2269/1749 |