Duality theory in linear optimization and its extensions -- formally verified
Not on the map. Why?
Abstract (arXiv)
Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). First posted on arXiv 12 Sep 2024.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2026: 1.
1 paper.