Zulip Chat Archive

Stream: general

Topic: linear programming


Chris Hughes (May 05 2020 at 06:25):

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 (May 05 2020 at 06:47):

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

Johan Commelin (May 05 2020 at 06:47):

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

Johan Commelin (May 05 2020 at 06:48):

Maybe the goal is also to have a computer program?

Johan Commelin (May 05 2020 at 06:48):

Or maybe we want two versions?

Johan Commelin (May 05 2020 at 06:49):

One meta, and one for proving?

Chris Hughes (May 05 2020 at 07:13):

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

David Wärn (May 05 2020 at 08:33):

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 (May 05 2020 at 08:53):

But we also want one for proving stuff, right?

David Wärn (May 05 2020 at 09:04):

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

Apurva Nakade (Jun 14 2021 at 14:00):

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 (Jun 14 2021 at 14:39):

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 (Jun 14 2021 at 14:56):

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 (Jun 14 2021 at 15:04):

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 (Jun 14 2021 at 15:04):

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

Alexander Bentkamp (Jun 14 2021 at 15:05):

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

Alexander Bentkamp (Jun 14 2021 at 15:06):

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

Alexander Bentkamp (Jun 14 2021 at 15:06):

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

Apurva Nakade (Jun 14 2021 at 15:09):

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

Alexander Bentkamp (Jun 14 2021 at 15:58):

@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 (Jun 14 2021 at 16:10):

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.


Last updated: Dec 20 2023 at 11:08 UTC