Patrick Johnstone (mathematical optimizer)

Stream: new members

[Patrick Johnstone]

Greetings! I am brand new to Lean, I just completed the natural number game, great fun. I am totally on-board with this general project though, I think it's great.

I am a researcher in the general field of mathematical optimization. I prove theorems about algorithms like gradient descent. As far as I know, almost no one in the math programming community is using Lean. Am I wrong? Does anyone know of formalizations of, for example, the proof that gradient descent converges to a minimizer of a smooth convex function? Or that the convergence rate is 1/k...

I feel this is completely open territory... The proofs in math optimization are very algebra heavy and ripe for automation. Yet I don't see anyone doing it. Perhaps there are reasons. Perhaps no one could be bothered yet. Or there were no tools like Lean...

Anyway, if anyone knows of work in Lean related to proving convergence properties of optimization algorithms like gradient descent, Newton's method etc. let me know.

Thanks,

[Kevin Buzzard]

To put your "as far as I know" into some kind of context, almost no-one in any mathematical community is using any theorem prover at all.

[Kevin Buzzard]

One thing I discovered very early on is that you can just do stuff which is regarded as totally basic in your field, but do it in a theorem prover, and then get a publication :D (because nobody did anything like it before)

[Yaël Dillies]

Hey! Yury G. Kudryashov, Frédéric Dupuis, Oliver Nash, Yakov Pechersky and myself (at least! hope I didn't forget anyone) are working on and around convex analysis. I don't know about convex optimization specifically.

[Johan Commelin]

@Patrick Johnstone There is https://github.com/dselsam/certigrad by @Daniel Selsam .

[Johan Commelin]

There is a youtube talk about this as well, by Daniel

[Patrick Johnstone]

Thank you! This is definitely along the lines of what I'm interested in. Although I don't think they proved convergence of the optimization algorithm, but they do prove the method produces the right stochastic gradients, which is neat.

[Patrick Johnstone]

That's good to know. Would these be publications in journals related to formal verification? Or in the field of the work itself. Because I don't know how optimization people would react to theorem provers, they might not be welcoming.

[Kevin Buzzard]

Right, journals related to formal verification (if you are pushing these systems to do things they've never done before)

[Patrick Massot]

Journals and conference proceedings (which is a standard venue for publication in computer science).

[Jeremy Avigad]

@Alexander Bentkamp and I have begun to explore another way of using proof assistants to solve optimization problems: http://www.andrew.cmu.edu/user/avigad/Papers/verified_optimization_wip_paper.pdf. We argue that applied mathematics is a natural market for formal methods. They allow you to specify complex models more precisely and use symbolic and numeric software more rigorously.

[Patrick Johnstone]

Jeremy Avigad said:

Alexander Bentkamp and I have begun to explore another way of using proof assistants to solve optimization problems: http://www.andrew.cmu.edu/user/avigad/Papers/verified_optimization_wip_paper.pdf. We argue that applied mathematics is a natural market for formal methods. They allow you to specify complex models more precisely and use symbolic and numeric software more rigorously.

Great, thanks. Do you have a github for this project yet?

My interest is more in convergence proofs for optimization algorithms - since that's what my research focuses on. But it's definitely related to what you are working on.

[Patrick Johnstone]

Yaël Dillies said:

Hey! Yury G. Kudryashov, Frédéric Dupuis, Oliver Nash, Yakov Pechersky and myself (at least! hope I didn't forget anyone) are working on and around convex analysis. I don't know about convex optimization specifically.

Great, I don't think you can do much convex optimization without at least some basic convex analysis.

[Scott Morrison]

I think it's a great time for this sort of stuff to be formalised. When we transition to Lean 4 ("soon"), it will be possible to write algorithms that run fast, and prove theorems about them, in the same language.

(That said, algorithms that involve manipulating real numbers are hard to formalise naively, because floats are horrible.)

[Patrick Johnstone]

Scott Morrison said:

I think it's a great time for this sort of stuff to be formalised. When we transition to Lean 4 ("soon"), it will be possible to write algorithms that run fast, and prove theorems about them, in the same language.

(That said, algorithms that involve manipulating real numbers are hard to formalise naively, because floats are horrible.)

I hadn't thought about the floating point issue before. In optimization we simply prove theorems about infinite precision algorithms. Normally not a care in the world goes into the fact that we actually implement them with floats.

When you say floats are horrible, has anyone tried to formalize floats in lean? Like have a float datatype and prove stuff about them?

[Scott Morrison]

mathlib is fine for proving theorems about infinite precision algorithms --- of course they can't be run, so my point about Lean4 being fast is irrelevant.

I'm not an expert on the float datatype. My understanding is that there are astonishingly few true theorems about it. :-)

[Mario Carneiro]

There is docs#data.fp.basic

[Mario Carneiro]

which hasn't been touched in years

[Mario Carneiro]

there are even a few low hanging fruits in that file requiring a proof (they were postponed because the proofs weren't the focus); all the meta defs are only meta because they use undefined instead of sorry

[Kevin Buzzard]

So basically we can prove that your algorithms work in theory, but not in practice :-)

[Patrick Johnstone]

I don't think the finite precision issue is a deal-breaker. I had a look today and there are a few optimization papers on the effects of finite precision, but mostly this is not studied. Probably there is just a lot of accumulated wisdom and empirical experience that round off errors tend to be benign for optimization algorithms, so it's not attractive to study theoretically.

[Joseph Myers]

And when you do have true theorems about floats, there's still lots of room for bugs to creep in in the gap between what the true theorems actually say and what you need for the real algorithm implementation in some programming language.

There are lots of new floating-point functions in the next (2023) version of the C standard, many of which I've been implementing for glibc. For some of those functions, it's convenient to use a standard floating-point technique (round-to-odd), the correctness of which is the subject of a true theorem (formalized in Coq some years ago). Despite the functions being simple and the implementation technique being formally verified, I've found quite a few bugs in the implementations that come in some way from that gap between the theorem and the implementation (sometimes in parts of the gap that might be a lot harder to formalize than floating point itself) - including bugs that survived in some functions for a few years between when I originally implemented them and when I recently discovered them accidentally while implementing more such functions.

[Patrick Johnstone]

Hi all,
I have been tinkering with Lean in my spare time for the last few months.

I wanted to clarify some things I've gathered in my reading: if I define a function from \R\to\R, Lean cannot #eval it, correct?

Like, even for "computable" functions like f(x)=2*x or f(x)=x+5 or f(x)=sin(x). These are "computable" according to certain definitions of Turing machines over the reals. I understand that a real number has potentially infinitely many digits, so computable here means informally "can compute an arbitrary number of digits".

So if I write
#eval (λ x:ℝ,x) 14

then I am doomed to get gibberish.

And further, there is no way to "force" lean to just use floating point representations? I see that there is a native.float type, so one could potentially just define a flag and switch everything over to native.float if one wants to do any computation...

I assume the certigrad code has a way around this, because they prove stuff about their code assuming infinite precision reals but then allow computation using an external linear algebra package. I had a brief look through the code but couldn't fully understand it. I think they somehow defines their own "real numbers" and lists a bunch of axioms it must satisfy.

Thanks for your help in advance...

[Johan Commelin]

Yup, currently in Lean 3 you can not compute with ℝ directly. If you want to compute, you need to use tactics that do the computation for you.

[Anne Baanen]

In fact, you can do a bit of computations with reals if you're lucky and the functions happen to be computable according to Lean, but mathlib has not been designed to keep computable real functions computable.

[Anne Baanen]

The gibberish that you're getting is because docs#real is defined as some quotient of cauchy sequences, so you're seeing the λ term defining the sequence

[Anne Baanen]

You can define a custom docs#has_repr instance to convert it to a readable string:

import data.real.basic

instance : has_repr ℝ :=
{ repr := λ x, x.cauchy.lift (λ (xs : cau_seq ℚ abs), repr (xs.1 100))
  sorry /- this is actually not true (since `0.9999...` and `1.000...` should have the same `repr` but don't if we don't round the value above -/ }

#eval (1 + 1 : ℝ) -- 2

[Kevin Buzzard]

Just don't try #eval (1/2 + 1/2 : ℝ) .

Think about it in general: in Lean we defined pi to be twice the smallest positive real root of the cosine function. Then pi is an uncomputable but well-defined real number (we proved cos(0)=1, cos(2)<0 and that cos was continuous). What can #eval do with this? We proved a lot of theorems about pi such as sin(n*pi)=0 etc but it was quite a long time before we proved pi>3; this was not necessary for any trig computations. We did happen to know that cos(1)>0 and that cos was decreasing on [0,2] so it wasn't too hard to deduce from this that $2<\pi<4$ but that was all we had for quite some time (even though we had a bunch of theorems about trig functions and pi)

[Patrick Johnstone]

Is Lean 4 different?

[Kevin Buzzard]

Not in this regard!

[Kevin Buzzard]

Real numbers are not floats. You have to think about them in a totally different way. They are the uncountable type which mathematicians use. Mathematicians can prove theorems about real numbers without ever having some kind of algorithm which can be used to write down an expression which attempts to represent, or approximate, the real number. I'm assuming you're expecting an answer in base 10. But this is a purely human construct. Real numbers are abstract objects in Lean. Floats are totally different. There are only finitely many and they do not satisfy the axioms of e.g. an abelian group; they are a highly imperfect representation of the reals. Mathematicians do not need that representation to prove theorems about or involving real numbers.

[Arthur Paulino]

A (maybe simpler) example are the natural numbers, which usually have an inductive definition in formal systems (being zero or the successor of a natural number). This definition is sufficient to prove results about natural numbers, but it's not the best representation for actually performing operations on the natural numbers.

For the later purpose, a low level byte array would be more suitable for the CPU. Hence the difference between, say, UInt32 and Nat in Lean 4. And again, a mathematical limitation that's similar to the one that Kevin pointed out arises. UInt32 can't represent infinite numbers and may overflow. You can think of Float and UInt32 as computational tricks for mimicking mathematical objects like the real and natural numbers respectively.

[Patrick Johnstone]

Thanks. Makes sense. So I suppose there is little support for "floating point extraction"? I.e: define an algorithm/function in Lean for the Reals, prove stuff about it, then extract a floating point approximation in another language or in Lean itself.

[Kevin Buzzard]

There's nothing like that in Lean 3 or 4 but I'm sure other people would be interested. For computational real numbers I should think you'd be much better off with Coq right now.

[Arthur Paulino]

On that direction, Lean 4 supports accessing low level (C) implementations via FFI. For example:

@[extern "c_sqrt_sqrt"] def sqrtSqrt (x : Float) : Float :=
  Float.sqrt (Float.sqrt x)

You would be able to reason and prove results about sqrtSqrt in Lean, but executing sqrtSqrt would trigger a computation on a function called c_sqrt_sqrt that you would need to provide C code for (and call it that way). The responsibility for the consistency of the result, however, would be totally on the author of the C implementation.

[Arthur Paulino]

Then if you wanted to write functions on ℝ^n → Float, you would need to unwrap (the term adopted by the FFI is actually "unbox") the real number representation in C, extract a double from it, perform the computations and return the result

[Tomas Skrivan]

Patrick Johnstone said:

Thanks. Makes sense. So I suppose there is little support for "floating point extraction"? I.e: define an algorithm/function in Lean for the Reals, prove stuff about it, then extract a floating point approximation in another language or in Lean itself.

What I'm currently doing is to define reals as def Real := Float and just postulate that Real form a field. This way you keep the computability(executing with floats) and still be able to do proofs about Real.

Doing this can maybe(I do not know) introduce inconsistency i.e. ability to prove False. However, I was unable to do so as everything about Float is hidden behind constant.

[Henrik Böving]

I'd guess that rounding and loss of significance/cancellation make this approach inconsistent somehow

[Tomas Skrivan]

But are you actually able to prove False? I don't think so. Of course, the program might not be doing what you have proven it is supposed to be doing because of the rounding errors.

[Tomas Skrivan]

You are proving only computations on some hypothetical machine capable of computing with reals. If you can prove, in addition, that your program is a continuous function, then you have a proof that the program is doing the correct thing in the limit of infinite precision.

[Henrik Böving]

I would guess that due to cancellation one might be able to proof that two things that are not actually equally are equal due to the field axioms? But I'm unsure whether the framework around floats allows for that.

[Tomas Skrivan]

Can you prove that 1.0 + 0.1 = 1.1? I do not know how.

What about this:

def x : Float := 1.0000000000000000000000
def y : Float := 0.00000000000000000000001

example : (x + y) - x = 0.0 := sorry   -- If you can prove this then using `Real := Float` is bad
example : (x + y) - x = y   := sorry   -- You can prove this using `Real := Float`

[Henrik Böving]

Yeah that's exactly what I don't know either :/

[Damiano Testa]

What about trying to prove that y^2=0? Is that any easier?

[Tomas Skrivan]

Damiano Testa said:

What about trying to prove that y^2=0? Is that any easier?

I do not think so, exponentiation on floats is defined as: (in Lean 4, probably similarly in Lean 3 too)

@[extern "pow"] constant Float.pow : Float → Float → Float

i.e. with constant so you are not able to prove anything about it. You just know some kind of function like that exists.

[Arthur Paulino]

I suspect that operations involving floats are ultimately hidden behind the FFI. It's not like you can get to the bottom of things in terms of Lean declarations

[Tomas Skrivan]

Yes exactly, so the interesting question is: If you postulate that Float form a field, can you prove False?

[Arthur Paulino]

I don't think so. The problem is that you wouldn't account for floating point errors, which would most certainly break your consistency in practice

[Tomas Skrivan]

If you can't, then I would argue that postulating Float as a field(maybe additionally Archimedean property and completenes to really get reals) is a viable option how to approach computations with reals.

To actually prove that your program is doing what you have proven in the limit of infinite precision. You would have to, for example, show that your program is continuous. Even better, if you prove your program to be Lipshitz, then you can have some meaningful bound on the error.

[Arthur Paulino]

Not a serious trouble if you're satisfied with C's double precision

[Arthur Paulino]

Yeah, the approach I see as most complete is offering some guarantee of error boundary

[Arthur Paulino]

So you'd formally account for imprecisions

[Arthur Paulino]

But not having this guarantee wouldn't stop me from using your package if needed :D

[Henrik Böving]

I would assume you cannot prove everything about reals just because you postulate that Float is a field and treating it like reals though right?

[Henrik Böving]

So the interesting question to me would be, what additional things would you need to actually treat Float like a real.

[Tomas Skrivan]

Henrik Böving said:

I would assume you cannot prove everything about reals just because you postulate that Float is a field and treating it like reals though right?

Well you need these axioms, i.e. field + total order + compatibility of order and arithmetic + completeness.

[Marc Huisinga]

Floats satisfy very few of these axioms though, or am I misunderstanding this conversation?

[Tomas Skrivan]

This requires one additional data: sup of a bounded sets. Everything else should be in Prop.

[Henrik Böving]

Marc Huisinga said:

Floats satisfy very few of these axioms though, or am I misunderstanding this conversation?

Floats don't even qualify as a field if you view at the actual values they produce, however (at least in Lean 4) float operations are (this is an hypothesis of us) exposed in a way that doesn't allow you to actually reason about them to the point where you could show that the assumption that float is a field is inconsistent. This would in theory allow value extraction from computation on reals by just treating Float like reals.

[Tomas Skrivan]

Marc Huisinga said:

Floats satisfy very few of these axioms though, or am I misunderstanding this conversation?

Yes they don't, but the question is: can you prove False if you postulate these axioms about floats? If not, you can treat Float as reals and keep your programs runnable.

[Henrik Böving]

So basically instead of the current mathlib approach to reals we would have a typeclass Real that is a combination of these 4 structures and then just instance : Real Float := sorry(well not exactly sorry, we would have to put the operations there and sorry the laws out), which should allow real functions to just be used with float input right?

[Kevin Buzzard]

Addition on float is provably not associative so if you assume it is then surely you can prove false

[Henrik Böving]

We are aware of that, but the way that it is exposed in Lean 4 is as a constant so you cannot actually prove anything about addition on floats.

[Tomas Skrivan]

Henrik Böving said:

So basically instead of the current mathlib approach to reals we would have a typeclass Real that is a combination of these 4 structures and then just instance : Real Float := sorry(well not exactly sorry, we would have to put the operations there and sorry the laws out), which should allow real functions to just be used with float input right?

Hmm, in my current code I just do def Real := Float and then provide instance : Add Real := Float.add etc. and postulate instance : Field Real := { ... := sorry }(I make sure that I sorry only Prop)

[Kevin Buzzard]

Are you saying you can't prove e.g. 0 ≠ 1 in float?

[Tomas Skrivan]

Kevin Buzzard said:

Are you saying you can't prove e.g. 0 ≠ 1 in float?

At least, I do not know how.

[Henrik Böving]

That I don't know, but I'm saying you cannot prove: 1 + 0 = 1 or 1 * 1 = 1 in float due to the way the API is built.

[Alex J. Best]

It seems a lot easier to me to just make your algorithms polymorphic on the underlying type, assuming HasAdd HasMul etc on that type, show that they are correct for a mathematical definition of the reals, and then run them for Float? Am I missing something?

[Kevin Buzzard]

Does float not have decidable equality?

[Henrik Böving]

Lean 4 says it doesn't, I'd have to check for lean 3

[Arthur Paulino]

I just tried example : (0.0 : Float) ≠ (1.0 : Float) := by simp [OfScientific.ofScientific, Float.ofBinaryScientific] in Lean 4 and it broke my server :upside_down:

[Marc Huisinga]

Kevin Buzzard said:

Addition on float is provably not associative so if you assume it is then surely you can prove false

The thing is that all Float operations in Lean 4 are constants, so you know nothing about them except that the type is inhabited. You can use them to evaluate stuff, but for the purpose of proof, they're just as good as arbitrary types. So postulating that they have certain structure should be fine (as long as what you postulated isn't inconsistent itself).
That said, I'm not sure if this approach is super practical. My intuition is that things with floats can go wrong badly, even if your proof over reals says that things are fine.
If I wanted to build a model of floats that's practical for proofs, I'd probably go for something like http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf, and not try to model them as bit vectors.

[Henrik Böving]

Alex J. Best said:

It seems a lot easier to me to just make your algorithms polymorphic on the underlying type, assuming HasAdd HasMul etc on that type, show that they are correct for a mathematical definition of the reals, and then run them for Float? Am I missing something?

Yes but what if I wanted to e.g. reason about the derivative of my function? Surely one would want to use the mathlib tools that are available for this right? But this is not possible with these type class constraints. If we instead made Real itself a typeclass and provide an instance for Float where the axioms are sorried out (which is hopefully valid, we don't know this for sure) and mathlib would switch to this approach on reals one should be able to reason about the derivative of a function of the form: (R : Type) [Real R] : R -> R using mathlib tools AND compute it using floats.

[Reid Barton]

Alex J. Best said:

It seems a lot easier to me to just make your algorithms polymorphic on the underlying type, assuming HasAdd HasMul etc on that type, show that they are correct for a mathematical definition of the reals, and then run them for Float? Am I missing something?

If you really want to run the algorithm, you might not trust the specializer enough or you might want to do things that don't generalize (e.g. using unboxed arrays of Float).

[Alex J. Best]

Henrik Böving said:

Lean 4 says it doesn't, I'd have to check for lean 3

In lean 4 there is floatDecLe for decidable le though, so you could give a decidable equality check assuming the le relation was irreflexive

[Marc Huisinga]

Arthur Paulino said:

I just tried example : (0.0 : Float) ≠ (1.0 : Float) := by simp [OfScientific.ofScientific, Float.ofBinaryScientific] in Lean 4 and it broke my server :upside_down:

I don't know why it broke the server, but ofScientific and the like also use constants, such as scaleB. The same should be true for equality; see this (the type used for Floats, here Unit, is hidden behind a constant), so I think you can do nothing with Float equality at the proof level either.

[Tomas Skrivan]

Marc Huisinga said:

Kevin Buzzard said:

Addition on float is provably not associative so if you assume it is then surely you can prove false

The thing is that all Float operations in Lean 4 are constants, so you know nothing about them except that the type is inhabited. You can use them to evaluate stuff, but for the purpose of proof, they're just as good as arbitrary types. So postulating that they have certain structure should be fine (as long as what you postulated isn't inconsistent itself).
That said, I'm not sure if this approach is super practical. My intuition is that things with floats can go wrong badly, even if your proof over reals says that things are fine.
If I wanted to build a model of floats that's practical for proofs, I'd probably go for something like http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf, and not try to model them as bit vectors.

Let me be a bit adversarial here :) All these approaches(those I have seen) to model errors of floating point arithmetic in my opinion/for what I want to do are really unsatisfactory. They usually deal with simple arithmetic expression involving handful of variables. I want do to numerical linear algebra and have some proper bounds on the error.

I want to see some framework that can give me some proper bounds on floating point arithmetic in Conjugate Gradient(CG) method or GMRES. (I took a full semester course on studying floating point errors in Conjugate Gradient method. It was super tough and we didn't even dare to analyze GMRES)

Until someone provides me such a framework, I will just not bother proving anything about floating point arithmetic and just follow best practices to hopefully dodge any/most problems with it.

[Alex J. Best]

Reid Barton said:

Alex J. Best said:

It seems a lot easier to me to just make your algorithms polymorphic on the underlying type, assuming HasAdd HasMul etc on that type, show that they are correct for a mathematical definition of the reals, and then run them for Float? Am I missing something?

If you really want to run the algorithm, you might not trust the specializer enough or you might want to do things that don't generalize (e.g. using unboxed arrays of Float).

What does trusting the specializer mean in this context?
The second reason definitely makes sense though, but I would in that situation definitely trust a proof that an implementation with unboxed array of floats agrees with a reference implementation that is correct for reals.

[Reid Barton]

Trust in the sense that it will deliver good performance, of course correctness is not in question.
The generic implementation (look up the add method in the class dictionary and call it via a function pointer, while passing boxed Floats) might be ~1000 times as expensive as the specialized/inlined implementation (a single instruction).

[Alex J. Best]

Henrik Böving said:

Alex J. Best said:

It seems a lot easier to me to just make your algorithms polymorphic on the underlying type, assuming HasAdd HasMul etc on that type, show that they are correct for a mathematical definition of the reals, and then run them for Float? Am I missing something?

Yes but what if I wanted to e.g. reason about the derivative of my function? Surely one would want to use the mathlib tools that are available for this right? But this is not possible with these type class constraints. If we instead made Real itself a typeclass and provide an instance for Float where the axioms are sorried out (which is hopefully valid, we don't know this for sure) and mathlib would switch to this approach on reals one should be able to reason about the derivative of a function of the form: (R : Type) [Real R] : R -> R using mathlib tools AND compute it using floats.

I certainly agree that having a typeclass that is equivalent to real is a good thing (I even wrote one for lean 3), I just don't still understand why Float needs to have an instance Real Float to do what you are saying, looking at the definition of has_deriv_at in lean 3 docs#has_deriv_at the type of the function f is f : 𝕜 → F, so if you define polymorphic functions def f {T :Type} [Add T] [Mul T] .. which only use the data fields of the Real typeclass you can reason about their derivatives over fields satisfying the axioms, but still evaluate them on floats.

[Tomas Skrivan]

Alex J. Best said:

I certainly agree that having a typeclass that is equivalent to real is a good thing (I even wrote one for lean 3), I just don't still understand why Float needs to have an instance Real Float to do what you are saying, looking at the definition of has_deriv_at in lean 3 docs#has_deriv_at the type of the function f is f : 𝕜 → F, so if you define polymorphic functions def f {T :Type} [Add T] [Mul T] .. which only use the data fields of the Real typeclass you can reason about their derivatives over fields satisfying the axioms, but still evaluate them on floats.

I do not have a solid reason for it, but I would certainly get tired of typing [Add T] [Mul T] [Sub T] [Neg T] [Inv T] [HPow T Nat T] ..., of course I can define class RealData (T : Type) extends Add T, Mul T .... Still I would get tired of writing foo {X} [RealData X] (x : X) instead of foo (x : Real)

I'm playing around with differentiable programming and some of my function definitions look like this:

def foo (f : (ℝ ⟿ ℝ)) (t : ℝ) : (ℝ ⟿ ℝ) := ...

where (ℝ ⟿ ℝ) is a set of all smooth function from reals to reals. Of course, I could have definition like def foo (f : (X -> X)) (t : X) : (X -> X) and then provide a theorem that if f : X -> X is smooth then foo f t is smooth. Again, this is too much additional typing that I do not want to do, plus it is making things look more complicated then they truly are.

[Henrik Böving]

You could have a variable {ℝ: Type} [RealData ℝ] at the top of your file / section....or agree on some default representation of reals that is actually exported as Real.

[Tomas Skrivan]

But you can't have (ℝ ⟿ ℝ) because that requires notion of differentiability that you can't define if you only have RealData.

[Kevin Buzzard]

You certainly can't define differentiability on float though ;-)

[Tomas Skrivan]

Kevin Buzzard said:

You certainly can't define differentiability on float though ;-)

:grinning: That is the whole point of the discussion. With the definition of Float as it is in Lean 4 you can hopefully postulate all axioms of real numbers without getting into inconsistency and thus you can define differentiability on Float.

[Kevin Buzzard]

And what would it say?

[Ruben Van de Velde]

What would be the point, though? Aren't you just proving things about \R at that point, rather than about floats?

[Tomas Skrivan]

The usual stuff, definition through a limit. Probably using somewhere non-computable function sup defined on bounded sets that would just be postulated to exist. Float would effectively turn into reals for any sake formal reasoning.
The way I see it now:

1. Float is type representing floating point numbers, it is defined though constants therefore you can't do any form of reasoning. Like proving 1.0 + 0.1 = 1.1 but you can do computations #eval (1.1 : Float) + (0.1 : Float)
2. real in mathlib is completely non-computational(not 100% sure about this). You can't do #eval (1 : real) + (0.1 : real) but can prove 1.0 + 0.1 = 1.1 in real

Why not to merge these two types together? Define def Real := Float and postulate axioms of real numbers on Real. Now you can prove stuff about Real and do computations with #eval. What you prove will not 100% correspond to what you compute with #eval but I still find it useful.

[Kevin Buzzard]

The reason not to merge the types together is presumably because, as you've just shown, they're completely different objects :-) Attempting to identify them is probably dangerous in terms of consistency?

[Tomas Skrivan]

I feel like we are arguing in a circle :) sure I'm worried about consistency too. If you can prove False from assuming axioms of reals on Float then I will agree it is a bad idea. However, many people want extract runable code by replacing reals with floats. This can be easily done by merging these two types together as I propose.

[Kevin Buzzard]

Can you make a MWE of what you propose?

[Kevin Buzzard]

And perhaps put it in another thread? We're talking about Lean 4, right? How about you start in the lean 4 stream with a mwe of what you propose to do and then perhaps other people can have some fun trying to prove false from it. This conversation has drifted and the current thread/stream are no longer appropriate.

[Tomas Skrivan]

Kevin Buzzard said:

Can you make a MWE of what you propose?

Here it is and in a new thread as you suggested.

[Patrick Johnstone]

Alex J. Best said:

It seems a lot easier to me to just make your algorithms polymorphic on the underlying type, assuming HasAdd HasMul etc on that type, show that they are correct for a mathematical definition of the reals, and then run them for Float? Am I missing something?

I really like this idea. Here is my beginner attempt at making gradient descent polymorphic

def gd_poly (α : Type)
            (hsub : has_sub α)
            (hmul : has_mul α)
            (η : α) (x0 : α) (gradf : α → α): (ℕ → α)
| 0      := x0
| (n+1)  := gd_poly(n) - η*gradf(gd_poly(n))

[Patrick Johnstone]

Then

#check gd_poly ℝ real.has_sub real.has_mul (0.1 : ℝ) (2 : ℝ) (λ x:ℝ,x) 10

and

#eval gd_poly native.float native.float.has_sub native.float.has_mul (0.1 : native.float) (2 : native.float) (λ x:native.float,x) 10

seem to work, although verbose.

[Henrik Böving]

You can omit the type class instances (has_sub and has_mul) by passing them in [] instead of () which will let the type class system figure them out for you.ALso since the arguments already contain the type α you can make it implicit by putting in in {} instead of () which will let lean figure the type argument out based on the arguments, that way it should become a lot less verbose already @Patrick Johnstone

[Patrick Johnstone]

Henrik Böving said:

You can omit the type class instances (has_sub and has_mul) by passing them in [] instead of () which will let the type class system figure them out for you.ALso since the arguments already contain the type α you can make it implicit by putting in in {} instead of () which will let lean figure the type argument out based on the arguments, that way it should become a lot less verbose already Patrick Johnstone

Much better, see below, thanks.

def gd_poly {α : Type}
            [has_sub α]
            [has_mul α]
            (η : α) (x0 : α) (gradf : α → α): (ℕ → α)
| 0      := x0
| (n+1)  := gd_poly(n) - η*gradf(gd_poly(n))

#eval gd_poly (0.1 : native.float) 2 (λ x,x) 15
#check gd_poly (0.1 : ℝ) 2 (λ x,x) 10

[Fadil Ahmed]

I am newbie to lean and i just set it up in vs code, but when i open it it says 'waiting for lean server to start'. Could anyone among you please tell what the problem is and how to solve it

[Kevin Buzzard]

Can you please ask this question in a new thread? This is about something else. My guess is that you've not used VS Code's "open folder" functionality to open a lean project. You can't just open a random lean file and expect it to work.