repr of reals

Stream: Is there code for X?

[Mario Carneiro]

e was the first irrational in mathlib but I think it didn't get a computable definition. It could be made computable with some work

[Alex J. Best]

Wait did we really have $e$ before $\sqrt 2$?

[Damiano Testa]

Possibly "irrational" should be replaced by "transcendental"?

[Anne Baanen]

Violeta Hernández said:

Does it work for irrationals too? Surely there's some irrational in mathlib with a computable Cauchy sequence...

Square roots are not computable at the moment (because sqrt x is defined as nnreal.sqrt (max 0 x) with the default noncomputable value of max).

[Anne Baanen]

And nnreal.sqrt is also noncomputably defined as an arbitrary (hence unique) inverse of the surjective function λ x, x * x.

[Mario Carneiro]

Yes, I'm fairly sure that we got exp before sqrt

[Alex J. Best]

Ah I see what you mean, we had the number but not the proof of irrationality?!

[Mario Carneiro]

when I say e was the first irrational, I mean it is the first number to be defined that turns out to be irrational

[Kevin Buzzard]

I guess one could always look these things up, but my memory was that I wrote a preliminary real.sqrt in summer 2017 because I needed it for my teaching, and you (Mario) laughed at it and removed the hx : 0 < x hypothesis after pointing out that it was never used. I'm not sure we even had infinite sums back then.

[Kyle Miller]

Here's the commit where Mario added real.sqrt in Jan 2018.