∑math20

Theoretical computer science · Result 126

Exponential semidefinite complexity of perfect matching

1 paperLean

Proves that every exact semidefinite lift of the perfect matching polytope has exponential size, answering Rothvoss's polynomial-size lift question negatively. The bound holds even for the positive semidefinite rank of its odd-cut slack matrix after any fixed shift \(0\lt \rho\lt 1\), allowing arbitrary real positive semidefinite factors.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Exponential PSD rank of positively shifted matching matrices

Exponential PSD rank of positively shifted matching matrices

OpenAI · October 5, 2026

For every fixed \(0\lt \rho\lt 1\), the matrix indexed by odd vertex sets U and perfect matchings M of Kn, with entries \(|M\cap\delta(U)|-1+\rho\), has real positive semidefinite rank \(2^{\Omega(n)}\) as even n tends to infinity. Here \(\delta(U)\) is the edge cut of U. Consequently, every exact semidefinite lift of the perfect matching polytope has exponential size.

Read PDF Download Source

Cite
@misc{OAI:Exponential-PSD-rank-of-positively-shifted-matching-matrices-October-5-2026,
  author = {{OpenAI}},
  title = {{Exponential PSD rank of positively shifted matching matrices}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Exponential-PSD-rank-of-positively-shifted-matching-matrices-October-5-2026/shifted-matching-psd.pdf}{OAI:Exponential-PSD-rank-of-positively-shifted-matching-matrices-October-5-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The paper proves exponential PSD-rank lower bounds for positively shifted matching matrices. The linked formalization records the related superpolynomial lower bounds: for every fixed \(C>0\), the PSD rank of the selected perfect-matching slack matrix exceeds \(n^C\) for all sufficiently large even \(n\). Every exact affine semidefinite lift of the perfect-matching polytope likewise requires matrix size greater than \(n^C\).

These selected statements give superpolynomial growth. They do not state the paper's exponential bound for every fixed positive shift.

Comparator links

ResultComparator statement
Superpolynomial lower bound for affine semidefinite liftsMatchingAffineLift.lean
Superpolynomial PSD rank for the perfect-matching slack matrixMatchingPSD.lean

Scope note on GitHub →