Zulip Chat Archive

Stream: maths

Topic: transcendence of $$e$$


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

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

Johan Commelin (Jul 09 2020 at 04:41):

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!

Heather Macbeth (Jul 09 2020 at 05:55):

(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: Dec 20 2023 at 11:08 UTC