Zulip Chat Archive

Stream: maths

Topic: linear programming


Arthur Paulino (Dec 26 2021 at 12:51):

Do we have formalized content on linear programming? I'm searching through mathlib docs but I can't find it

Martin Dvořák (Dec 26 2021 at 12:54):

No.

Yaël Dillies (Dec 26 2021 at 13:38):

analysis.convex. contains all the convexity stuff, but there isn't much more than that, no.

Apurva Nakade (Jun 13 2022 at 02:50):

Hello, is there anyone working on linear programming? My summer break has just started and I'm looking for a short project to do. I'm thinking of adding 1) hyperplane separation, 2) Farkas' lemma, 3) Weak duality, 4) Strong duality (both dualities only for linear programs only).

Yaël Dillies (Jun 13 2022 at 08:20):

Isn't hyperplane separation docs#geometric_hahn_banach_closed_compact?

Yaël Dillies (Jun 13 2022 at 08:40):

I also have Stone's separation in #14677, but that's probably not what you want.

Apurva Nakade (Jun 13 2022 at 14:34):

Yaël Dillies said:

Isn't hyperplane separation docs#geometric_hahn_banach_closed_compact?

Yes, thanks! :)

Alexander Bentkamp (Jun 28 2022 at 10:20):

@Apurva Nakade I have some old code here formalizing the duality theorem for cone programs (https://github.com/abentkamp/duality, see cone_duality in src/cone_program.lean). Maybe you are better off starting from scratch though because the code is very old and goes beyond linear programming.

Apurva Nakade (Jun 28 2022 at 15:46):

Thank you, this is very helpful! It helps me see that conic programming is the easiest to code. I suspect that most of the auxiliary files you have are already in mathlib. I'll try to see adapt cone_program.lean to the current mathlib.


Last updated: Dec 20 2023 at 11:08 UTC