Decidable algorithms on real numbers

Stream: new members

[Rekkyn]

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]

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]

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

[Eric Wieser]

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

[Rekkyn]

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]

Is Float close enough for you?

[Kyle Miller]

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]

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]

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]

Michael Wahlberg 말함:

You wanna collaborate?

sure!