## Stream: maths

### Topic: transcendence of $e$

#### Jujian Zhang (Jul 09 2020 at 04:40):

Hi, everyone. I proved $\sum_{i=0}^\infty\frac{1}{10^{i!}}$ and transcendence of $e$.
Here is the repo.
https://github.com/jjaassoonn/transcendental

Fantastic!

#### Kenny Lau (Jul 09 2020 at 04:46):

Everything not PR'ed into mathlib is lost. -- Ancient Chinese Proverb

#### Scott Morrison (Jul 09 2020 at 05:33):

Let us know if you want advice about how to carve it up into mathlib-ready chunk!

(wrong thread)

#### Kevin Buzzard (Jul 09 2020 at 09:47):

The proof relies on the fundamental theorem of calculus, a version of which is assumed as an axiom.

#### Johan Commelin (Jul 11 2020 at 07:08):

It would be really cool if we could formalise Tent–Ziegler, Computable functions of reals.

#### Aaron Anderson (Jul 12 2020 at 00:17):

I didn't know there was another Tent-Ziegler project, I only knew their model theory book...

Last updated: May 11 2021 at 16:22 UTC