## Stream: new members

### Topic: Decidable algorithms on real numbers

#### Rekkyn (Jul 17 2023 at 14:45):

I was a bit surprised to learn that equalities and inequalities on real numbers are undecidable, but it makes sense that infinite strings of digits cannot be compared. However does this mean that any algorithm that operates on real numbers in this way is undecidable? If so, how would an algorithm that claims to work on real numbers (for example linear programming) be implemented in Lean?

#### Michael Wahlberg (Jul 17 2023 at 14:52):

So, you can actually look into the Tarski–Seidenberg theorem , whose converse gives us decidability on real-closed fields. So, all equalities and inequalities on algebraic integers is decidable

#### Rekkyn (Jul 17 2023 at 15:09):

That's interesting, thanks! Is there an implementation of decidable equality of algebraic integers in Lean?

#### Eric Wieser (Jul 17 2023 at 15:31):

We haveAlgebraicClosure Int (docs#AlgebraicClosure), but I suspect it's useless for computation

#### Rekkyn (Jul 17 2023 at 16:09):

Is there an idiomatic way of writing algorithms on "real" numbers (or some other type that is close enough) in Lean or has that not come up much yet?

#### Martin Dvořák (Jul 17 2023 at 16:28):

Is Float close enough for you?

#### Kyle Miller (Jul 17 2023 at 16:31):

You can't prove anything about Lean's Float, so probably not. (Also floats are a very very small portion of the computable reals, and they don't even form a field.)

#### Jihoon Hyun (Jul 18 2023 at 02:55):

I'm interested in this topic, and would like to join the implementation if there are enough resources. However I think there should be a concrete definition of semi/computability of functions. So this can be implemented after algorithms are formally defined.
My question here is: Is there a progress on formal definition of algorithms? I know there is a thread talking about it, but didn't join the talk.

#### Michael Wahlberg (Jul 18 2023 at 03:13):

Jihoon Hyun said:

I'm interested in this topic, and would like to join the implementation if there are enough resources. However I think there should be a concrete definition of semi/computability of functions. So this can be implemented after algorithms are formally defined.
My question here is: Is there a progress on formal definition of algorithms? I know there is a thread talking about it, but didn't join the talk.

You wanna collaborate?

#### Jihoon Hyun (Jul 18 2023 at 03:17):

Michael Wahlberg 말함:

You wanna collaborate?

sure!

Last updated: Dec 20 2023 at 11:08 UTC