# Zulip Chat Archive

## Stream: general

### Topic: sqrt

#### Reid Barton (Aug 01 2018 at 20:29):

Curiosity provoked by Kevin's comment elsewhere: Could sqrt be computable?

Obviously there is some potential problem near 0, but my feeling is that it could be worked out, but I'm not 100% sure.

#### Patrick Massot (Aug 01 2018 at 20:29):

I think classical reals are noncomputable from start to end

#### Patrick Massot (Aug 01 2018 at 20:30):

The equality `(sqrt x)^2 = x`

would be non decidable

#### Reid Barton (Aug 01 2018 at 20:34):

I think you can at least add Cauchy sequences constructively, but I guess there's no real point because there is no information you can get out of an element of ℝ

#### Mario Carneiro (Aug 01 2018 at 20:36):

Pretty much every continuous function is computably definable

#### Mario Carneiro (Aug 01 2018 at 20:36):

but it's more work

#### Mario Carneiro (Aug 01 2018 at 20:36):

A real number is data, you can compute with it if you want

#### Reid Barton (Aug 01 2018 at 20:37):

But I have to compute a function which is constant on the equivalence class, right? what could I compute?

#### Reid Barton (Aug 01 2018 at 20:37):

besides other real numbers

#### Mario Carneiro (Aug 01 2018 at 20:37):

any constant expression, like pi

#### Kevin Buzzard (Aug 01 2018 at 20:40):

We have a team working hard on constructing pi :-)

The main problem at the minute is that nobody can be bothered to type in the proof that a power series is continuous within its radius of convergence :-/

#### Mario Carneiro (Aug 01 2018 at 20:42):

meh, I went for a low tech proof of continuity of exp in metamath

#### Mario Carneiro (Aug 01 2018 at 20:42):

it's easy to bound `x+1 < e^x < 1/(1-x)`

and use the squeeze lemma

#### Mario Carneiro (Aug 01 2018 at 20:43):

(wait, that's differentiability. Continuity is probably even easier)

#### Reid Barton (Aug 01 2018 at 20:45):

Oh yes, at one point I wanted continuity of the sum of a Cauchy sequence of bounded continuous functions also. I was kind of hoping Johannes would make it magically appear.

Last updated: May 15 2021 at 23:13 UTC