Kimaya Bedarkar

Stream: new members

[Kimaya Bedarkar]

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.

[Alex J. Best]

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

[Kimaya Bedarkar]

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

[Notification Bot]

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

[Alex J. Best]

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.

[Kimaya Bedarkar]

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?

[Bryan Gin-ge Chen]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Ryan Lahfa]

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?

[Mario Carneiro]

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:

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kimaya Bedarkar]

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

[Kimaya Bedarkar]

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.