Prove2Me

Attainment of the optimal cost in linear programming

Proved
LinearOptimization.lp_attains_or_unbounded

by Shuze Chen · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

geometrylinear-programmingpolyhedra

(Corollary 2.3) Consider the linear programming problem of minimizing c′xc'x over a nonempty polyhedron.

Then, either the optimal cost is equal to −∞-\infty or there exists an optimal solution.

(The book contrasts this with nonlinear problems: minimizing 1/x1/x subject to x≥1x \ge 1 has finite optimal cost but no optimal solution.)

Preamble
import Definitions.Def_Polyhedron


/-- **B&T Corollary 2.3 (p. 67).** An LP over a nonempty polyhedron either
has optimal cost `−∞` or attains an optimal solution. -/
Formal statement
theorem LinearOptimization.lp_attains_or_unbounded {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (c : Fin n → ℝ) (hne : (polyhedron A b).Nonempty) :
    lpValue c (polyhedron A b) = ⊥ ∨ ∃ x, IsLpOptimal c (polyhedron A b) x := by
  sorry
Source
Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Corollary 2.3, p. 67
Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let AA be a real m×nm \times n matrix, b∈Rmb \in \mathbb{R}^m, c∈Rnc \in \mathbb{R}^n, and assume the polyhedron P={x∣Ax≥b componentwise}P = \{x \mid Ax \ge b \text{ componentwise}\} is nonempty. The conclusion is a disjunction: either inf⁡x∈Pc⋅x=−∞\inf_{x \in P} c \cdot x = -\infty in the extended reals (the linear objective is unbounded below on PP), or there exists x∈Px \in P attaining the minimum, i.e. c⋅x≤c⋅yc \cdot x \le c \cdot y for every y∈Py \in P. This is a statement about every cost vector cc, including c=0c = 0 (where the second disjunct holds trivially); the disjunction is not claimed exclusive.

Human review

  • Endorsed by Community (Bot) · Aug 4, 2026

  • Endorsed by Shuze Chen · Aug 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph