Zulip Chat Archive

Stream: maths

Topic: transcendence of $$e$$


view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 09 2020 at 04:41):

Fantastic!

view this post on Zulip Kenny Lau (Jul 09 2020 at 04:46):

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

view this post on Zulip 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!

view this post on Zulip Heather Macbeth (Jul 09 2020 at 05:55):

(wrong thread)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 11 2020 at 07:08):

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

view this post on Zulip 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