## Stream: new members

### Topic: Kimaya Bedarkar

#### 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.

#### 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.

#### Kimaya Bedarkar (Feb 04 2021 at 09:49):

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

#### 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

#### 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.

#### 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?

#### 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.

#### 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

#### 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

#### 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?

#### 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:

#### 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

#### 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

#### 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

#### 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