Zulip Chat Archive

Stream: new members

Topic: Kimaya Bedarkar


view this post on Zulip Kimaya Bedarkar (Feb 04 2021 at 09:46):

Hello!
This is my first time posting here. Please forgive me if I am making some mistakes.
I am an undergrad studying math and cs at BITS Pilani University in India. I recently got into the field of interactive theorem provers and used coq for a while before switching to Lean.
I am interested in understanding how real numbers are defined in Lean. Could someone please direct me to some resources about this topic.

view this post on Zulip Alex J. Best (Feb 04 2021 at 09:47):

Hi @Kimaya Bedarkar sure, first you should probably post in the new members stream instead. This stream is for an old conference only.

view this post on Zulip Kimaya Bedarkar (Feb 04 2021 at 09:49):

Oh!
I am sorry!
Can this message be moved there

view this post on Zulip Notification Bot (Feb 04 2021 at 09:49):

This topic was moved here from #Lean for the curious mathematician 2020 > (no topic) by Rob Lewis

view this post on Zulip Alex J. Best (Feb 04 2021 at 09:54):

The reals in lean are defined via Cauchy sequences of rationals, you can see the doc at docs#real there isn't a huge amount of description there, but from there you can see the main results click to view the source of each definition. Check out https://leanprover-community.github.io/mathlib_docs/data/real/cau_seq.html also. If you just want to get a feel for proving things about the reals in lean maybe look at the tutorial project (second on https://leanprover-community.github.io/learn.html) as this has some exercises doing this.

view this post on Zulip Kimaya Bedarkar (Feb 04 2021 at 09:56):

I am actually interested in exploring an alternative definition of reals which can help in formalising computational geometry proofs
Has any work previously been done in finding some alternative definition of reals which might be computationally better?

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2021 at 14:28):

Not in Lean yet, as far as I know. We do have an open issue about adding some definition of computable reals to mathlib, but I don't believe anyone has worked on it: #1038.

view this post on Zulip Mario Carneiro (Feb 04 2021 at 18:40):

I think this depends on what you mean by "computationally better". I think that most things that would fit the definition of "computable reals" would actually not be computationally better than what we already have. What you really need is something like interval arithmetic and/or (possibly arbitrary-precision) floating point arithmetic if you want to actually compute with real numbers at a reasonable speed

view this post on Zulip Mario Carneiro (Feb 04 2021 at 18:41):

Note that we are already doing some nontrivial real computations, e.g. to calculate e and pi to 10 decimals, and the fact that real numbers are defined in a "noncomputable" way doesn't matter at all

view this post on Zulip Ryan Lahfa (Feb 04 2021 at 18:43):

Mario Carneiro said:

Note that we are already doing some nontrivial real computations, e.g. to calculate e and pi to 10 decimals, and the fact that real numbers are defined in a "noncomputable" way doesn't matter at all

Is there some source to read about the computation of those constants with such precision?

view this post on Zulip Mario Carneiro (Feb 04 2021 at 18:50):

Not really, but I have a whole philosophy about how to do verified numerical computations that I will tell anyone who seems to be interested :wink:

view this post on Zulip Mario Carneiro (Feb 04 2021 at 18:51):

The short version is: it's not actually computing on real, it's doing computations on rational numbers reduced to questions about nat that can be decided by norm_num

view this post on Zulip Mario Carneiro (Feb 04 2021 at 18:54):

The high precision estimates of e are done in src#real.exp_one_near_10, although the actual proof depends on src#real.exp_1_approx_succ_eq and the few theorems in the section on src#real.exp_near

view this post on Zulip Kimaya Bedarkar (Feb 05 2021 at 07:41):

Bryan Gin-ge Chen said:

Not in Lean yet, as far as I know. We do have an open issue about adding some definition of computable reals to mathlib, but I don't believe anyone has worked on it: #1038.

Thanks for this. I checked it out and it was quite helpful

view this post on Zulip Kimaya Bedarkar (Feb 05 2021 at 07:42):

Mario Carneiro said:

I think this depends on what you mean by "computationally better". I think that most things that would fit the definition of "computable reals" would actually not be computationally better than what we already have. What you really need is something like interval arithmetic and/or (possibly arbitrary-precision) floating point arithmetic if you want to actually compute with real numbers at a reasonable speed

Thank you. I will try to think about this.


Last updated: May 11 2021 at 22:14 UTC