Topic: transcendence of $$e$$
Jujian Zhang (Jul 09 2020 at 04:40):
Hi, everyone. I proved and transcendence of .
Here is the repo.
Johan Commelin (Jul 09 2020 at 04:41):
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!
Heather Macbeth (Jul 09 2020 at 05:55):
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