Zulip Chat Archive

Stream: triage

Topic: issue #2601: Linear programming


view this post on Zulip Random Issue Bot (Dec 04 2020 at 14:22):

Today I chose issue 2601 for discussion!

Linear programming
Created by @Johan Commelin (@jcommelin) on 2020-05-05
Labels: feature-request, please-adopt

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Frédéric Dupuis (Dec 04 2020 at 19:24):

I'm interested in this, and conic linear programming more generally, but I haven't started coding anything.

view this post on Zulip Reid Barton (Dec 04 2020 at 19:25):

This issue seems a bit vague; I assume it's supposed to be about the underlying theory, not implementing algorithms?

view this post on Zulip Mario Carneiro (Dec 04 2020 at 19:26):

This issue seems a bit vague

lol that looks like an understatement

view this post on Zulip Frédéric Dupuis (Dec 04 2020 at 19:43):

Well, it's a feature request, not really an "issue" per se.

view this post on Zulip Frédéric Dupuis (Dec 04 2020 at 19:45):

And yes, I meant that as proving theorems about linear programs, not about implementing LP algorithms in Lean.

view this post on Zulip Johan Commelin (Dec 05 2020 at 05:31):

:see_no_evil:

view this post on Zulip Random Issue Bot (Feb 13 2021 at 14:19):

Today I chose issue 2601 for discussion!

Linear programming
Created by @Johan Commelin (@jcommelin) on 2020-05-05
Labels: feature-request, please-adopt

Is this issue still relevant? Any recent updates? Anyone making progress?


Last updated: May 18 2021 at 23:14 UTC