linear programming

Stream: general

[Chris Hughes]

I did some linear programming last summer. I wouldn't describe it as a small project. If this should be in mathlib, in what form should it be. The version I did was actually somewhat efficiently computable. There are some lemmas that can be proven from the termination of the simplex algorithm, such as the duality theorem, but I guess the goal wouldn't be to have a computer program.

[Johan Commelin]

Sorry, the original title of the thread was only about Lagrange interpolation...
I've modified the title

[Johan Commelin]

I also didn't label the linear programming issue with 'easy' :wink:

[Johan Commelin]

Maybe the goal is also to have a computer program?

[Johan Commelin]

Or maybe we want two versions?

[Johan Commelin]

One meta, and one for proving?

[Chris Hughes]

Just because it's executable doesn't make it meta..

[David Wärn]

Wouldn't a fast, untrusted implementation be more useful than a slow, trusted one though? You can easily verify the solution to any given linear program

[Johan Commelin]

But we also want one for proving stuff, right?

[David Wärn]

I think we want some way to prove strong duality for linear programming over an ordered field

[Apurva Nakade]

Is anyone working on this?

I recently started learning LP and the book I'm currently following has a purely geometry proof of the duality theorems that do not use the halting of the simplex algorithm. Something to do with Farkas' lemma and complementary slackness, still don't understand these fully...

[Alexander Bentkamp]

Yes, I am working on a related project. @Jeremy Avigad and I are developing a library to solve convex optimization problems. That subsumes LP problems. The plan is to let external solvers do the hard work and verify the results using duality. We are still at the beginning of the project, but I have a proof of weak duality of cone programming (also subsumes LP). It's not up to date with the current mathlib, but I could make it mathlib-ready if you are interested.

[Alexander Bentkamp]

And @Ramon Fernandez Mir is working on integrating SOS programming solvers into Lean. This could probably extended to work for LPs as well.

[Apurva Nakade]

Oh, wow. Even if you could just add the definitions to mathlib that'd be great. Then I can have some standardized framework to experiment with.

[Alexander Bentkamp]

Maybe it's actually the definitions that are not up to date :D

[Alexander Bentkamp]

I did this before matrices and inner products were as advanced as they are now in mathlib.

[Alexander Bentkamp]

Here you can have a look: https://github.com/skbaek/cvx/blob/master/src/cone_program.lean

[Alexander Bentkamp]

Don't try to load it up in Lean, though. It's all a bit broken now :D

[Apurva Nakade]

Awesome, thanks! I'll play around with the code and see if I can update the definitions.

[Alexander Bentkamp]

@Apurva Nakade I should warn you though: @Seul Baek already experimented with verifying the results of an LP solver here: https://github.com/skbaek/cvx/blob/master/src/LP.lean. Unfortunately, verifying the results of the external solver in Lean3 is extremely slow. We are planning to move on to Lean4 as soon as possible to achieve faster verification.

[Apurva Nakade]

I see, thanks! This much metaprogramming is beyond my understanding anyways :P
I'm kinda just interested in the "linear algebra" aspects of LP. I'll play around with the code and see what can be done purely theoretically.