The PSD cone is self-dual

Proved

ConvexOptimization.psd_cone_self_dual

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

convexanalysisconvexoptimizationlog-concavity

The positive semidefinite cone is self-dual.

Equip the space of symmetric real $n \times n$ matrices with the trace inner product $\langle A, B\rangle = \operatorname{tr}(AB)$ . Let $A$ be symmetric. Then

\bigl(\operatorname{tr}(AB) \ge 0 \ \text{ for every } B \succeq 0\bigr) \qquad\Longleftrightarrow\qquad A \succeq 0 .

In the language of dual cones, $\mathbb{S}^n_{+}{}^{*} = \mathbb{S}^n_{+}$ : the cone of positive semidefinite matrices coincides with its own dual.

Self-duality is why semidefinite programming is dual to semidefinite programming, with the same cone appearing on both sides — the same phenomenon that makes linear programming dual to linear programming through self-duality of the nonnegative orthant. The forward direction is also the standard route to certifying $A \succeq 0$ by testing against rank-one matrices $B = vv^{T}$ , for which $\operatorname{tr}(AB) = v^{T}Av$ .

Formalization Note Matrices are Matrix (Fin n) (Fin n) ℝ, symmetry is A.IsSymm, and the trace pairing is written (A * B).trace; the statement is an iff, so both the duality inclusion and its converse are asserted. Source: B&V §2.6.1, example 2.24, p. 52.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.psd_cone_self_dual {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsSymm) :
    (∀ B : Matrix (Fin n) (Fin n) ℝ, B.PosSemidef → 0 ≤ (A * B).trace) ↔
      A.PosSemidef := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 52, §2.6.1 example 2.24 (the positive semidefinite cone is self-dual)

Read-back

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

Theorem statement. For every $n$ and every real $n \times n$ matrix $A$ that is symmetric ( $A^{\mathsf T} = A$ , this is a hypothesis), the following equivalence holds: $\big(\forall B \in \mathbb{R}^{n\times n},\ B \text{ positive semidefinite} \Rightarrow 0 \le \operatorname{tr}(AB)\big) \iff A \text{ positive semidefinite}$ . Here "positive semidefinite" is Mathlib's notion for real matrices: the matrix is symmetric and $x^{\mathsf T} M x \ge 0$ for every vector $x \in \mathbb{R}^n$ (so the quantifier over $B$ on the left ranges only over symmetric PSD matrices — the semidefiniteness bundles symmetry). $\operatorname{tr}(AB)$ is the trace of the matrix product $AB$ , i.e. $\sum_{i,j} A_{ij}B_{ji}$ . Both inequalities are non-strict. The forward direction of the iff uses the trace condition against all PSD $B$ ; the backward direction asserts the trace nonnegativity from PSD-ness of $A$ . Degenerate case $n = 0$ : the unique empty matrix is PSD and all traces are $0$ , so both sides are trivially true.

Human review

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

View graph