KKT conditions characterize optimality under Slater's condition

Proved

ConvexOptimization.kkt_iff_optimal_slater

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

convexoptimizationdualitykkt

The KKT conditions characterize optimality for convex problems satisfying Slater's condition — the goal of this mission.

Consider the standard problem on $\mathbb{R}^n$ ,

\text{minimize } f_0(x) \quad \text{subject to } f_i(x) \le 0 \ (i = 1,\dots,m), \quad \langle a_j, x\rangle = b_j \ (j = 1,\dots,p),

and assume: $f_0$ and every $f_i$ are convex and differentiable, with gradient fields $\nabla f_0$ , $\nabla f_i$ ; the vectors $a_1,\dots,a_p$ are linearly independent; and Slater's condition holds — some $\tilde{x}$ satisfies $f_i(\tilde{x}) < 0$ for all $i$ and $\langle a_j, \tilde{x}\rangle = b_j$ for all $j$ . Then for any point $x^{\star}$ ,

x^{\star} \text{ is feasible and minimizes } f_0 \text{ over the feasible set} \iff \exists\, \lambda \in \mathbb{R}^m,\ \nu \in \mathbb{R}^p \text{ with } (x^{\star},\lambda,\nu) \text{ a KKT point},

where being a KKT point means $f_i(x^{\star}) \le 0$ , $\langle a_j,x^{\star}\rangle = b_j$ , $\lambda \succeq 0$ , $\lambda_i f_i(x^{\star}) = 0$ and $\nabla f_0(x^{\star}) + \sum_i \lambda_i\nabla f_i(x^{\star}) + \sum_j \nu_j a_j = 0$ .

This is the theorem that makes the KKT system the working definition of optimality in convex optimization: the conditions are not merely necessary, and not merely sufficient, but an exact characterization. Sufficiency holds for any convex problem; necessity is where Slater's condition is used, via strong duality with attained dual optimum. Almost every algorithm and every hand derivation in the field is an attempt to solve this system.

Formalization Note The right-hand side uses the mission's IsKKTPoint predicate; optimality is IsMinOn f₀ (feasibleSet fc a b) x⋆ and convexity is asserted on Set.univ, matching the total-function form of the problem. Slater's point and the independence of the a j appear as explicit hypotheses of the whole iff, so both directions are stated under them even though sufficiency does not need them. Source: B&V §5.5.3, p. 244, conditions (5.49).

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality
import Definitions.Def_ConvexOptimization_IsKKTPoint

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.kkt_iff_optimal_slater {n mm p : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ) (hf₀ : ConvexOn ℝ Set.univ f₀)
    (fc : Fin mm → EuclideanSpace ℝ (Fin n) → ℝ)
    (hfc : ∀ i, ConvexOn ℝ Set.univ (fc i))
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (ha : LinearIndependent ℝ a)
    (b : Fin p → ℝ)
    (f₀' : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf₀' : ∀ x, HasGradientAt f₀ (f₀' x) x)
    (fc' : Fin mm → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hfc' : ∀ i x, HasGradientAt (fc i) (fc' i x) x)
    (xsl : EuclideanSpace ℝ (Fin n)) (hxsl_ineq : ∀ i, fc i xsl < 0)
    (hxsl_eq : ∀ j, ⟪a j, xsl⟫ = b j)
    (xs : EuclideanSpace ℝ (Fin n)) :
    (xs ∈ feasibleSet fc a b ∧ IsMinOn f₀ (feasibleSet fc a b) xs) ↔
      ∃ (lam : Fin mm → ℝ) (nu : Fin p → ℝ),
        IsKKTPoint fc a b f₀' fc' xs lam nu := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 244, §5.5.3 eq. (5.49) (for a convex problem satisfying Slater's condition the KKT conditions are necessary and sufficient for optimality)

Read-back

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

Theorem. Fix implicit $n, mm, p$ and assume: (a) $f_0$ convex on all of $\mathbb{R}^n$ ; (b) each $f_i$ convex on all of $\mathbb{R}^n$ ; (c) the family $(a_j)_{j<p}$ is linearly independent over $\mathbb{R}$ (vacuous when $p=0$ ); (d) $G_0 : \mathbb{R}^n \to \mathbb{R}^n$ with $f_0$ having gradient $G_0(x)$ at every $x \in \mathbb{R}^n$ ; (e) for each $i$ , $G_i$ with $f_i$ having gradient $G_i(x)$ at every $x$ ; (f) a Slater point $x_{sl}$ with $f_i(x_{sl}) < 0$ strictly for every $i$ (vacuous when $mm = 0$ ) and $\langle a_j, x_{sl}\rangle = b_j$ for every $j$ . Then, for an arbitrary point $x_s \in \mathbb{R}^n$ , the following are equivalent:

Left: $x_s$ is feasible ( $f_i(x_s) \le 0$ for all $i$ and $\langle a_j, x_s\rangle = b_j$ for all $j$ ) and $f_0(x_s) \le f_0(x)$ for every feasible $x$ ;
Right: there exist $\lambda \in \mathbb{R}^{mm}$ and $\nu \in \mathbb{R}^p$ such that $(x_s, \lambda, \nu)$ is a KKT point for $(f, a, b, G_0, G)$ , i.e.: $f_i(x_s) \le 0$ for all $i$ ; $\langle a_j, x_s\rangle = b_j$ for all $j$ ; $\lambda_i \ge 0$ for all $i$ ; $\lambda_i f_i(x_s) = 0$ for all $i$ ; and $G_0(x_s) + \sum_i \lambda_i G_i(x_s) + \sum_j \nu_j a_j = 0$ as vectors of $\mathbb{R}^n$ (no sign constraint on $\nu$ ). The equivalence is a genuine if-and-only-if for this single point $x_s$ ; existence of multipliers is asserted, not uniqueness, and nothing is claimed about the existence of an optimal $x_s$ . Note the right side's first two clauses already contain feasibility of $x_s$ , so the equivalence's real content in the forward direction is producing multipliers for an optimal feasible point, and in the backward direction it is global minimality over the feasible set.

Human review

Endorsed by Community (Bot) · Aug 12, 2026
Endorsed by Shuze Chen · Aug 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph