View source for Exponential semidefinite complexity of perfect matching

'''Exponential semidefinite complexity of perfect matching''' concerns the size of semidefinite lifts of the perfect matching polytope of the complete graph ''K''<sub>''n''</sub>, that is, representations of the polytope as an affine image of an affine section of a cone of positive semidefinite matrices. Rothvoss proved that every linear extended formulation of the polytope has exponential size and asked whether a polynomial-size semidefinite lift exists. A manuscript dated 5 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims an exponential lower bound for exact semidefinite lifts, through an exponential lower bound for the positive semidefinite rank of a shifted odd-cut matrix. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; this page does not certify them.

== Background ==
* As recounted in the introduction of the manuscript:
** Edmonds described the perfect matching polytope by nonnegativity, degree equations and odd-cut inequalities. Yannakakis developed the nonnegative-factorization framework and proved an exponential lower bound for symmetric linear formulations, and Rothvoss proved the unrestricted exponential lower bound for linear extended formulations. The cone-factorization theorem of Gouveia, Parrilo and Thomas identifies the minimum size of a semidefinite lift with the positive semidefinite rank of a slack matrix.
** For the shifted matrix with entries |''M'' ∩ δ(''U'')| − 1 + ρ, indexed by odd vertex sets ''U'' and perfect matchings ''M'', Braun and Pokutta proved exponential nonnegative rank for each fixed 0 < ρ < 1. Braun and collaborators proved exponential lower bounds for coordinate-symmetric semidefinite formulations of matching. Lee, Raghavendra and Steurer developed a general approach to unrestricted semidefinite lower bounds through sums of squares, and Kaniewski, Lee and de Wolf showed that matrices of subexponential positive semidefinite rank approximate the unshifted slack matrix with exponentially small entrywise error, so exactness matters.

== The original result ==
* '''Claim.''' Theorem ''thm:main'' of ''Exponential PSD rank of positively shifted matching matrices'' states that there is a constant ''c'' &gt; 0 such that for every fixed 0 &lt; ρ &lt; 1 the shifted matrix has real positive semidefinite rank at least 2<sup>''cn''</sup> for all sufficiently large even ''n'', where the threshold may depend on ρ. Corollary 1.2 concludes that the unshifted slack matrix has exponential positive semidefinite rank and that every exact semidefinite lift of the perfect matching polytope has size 2<sup>Ω(''n'')</sup>, answering the polynomial-size question negatively. At ρ = 1 the matrix has a factorization of size ''n''(''n'' − 1)/2, so the endpoint is excluded.
* ''Method, as described:'' the proof follows the sums-of-squares approach of Lee, Raghavendra and Steurer, with a transfer argument tailored to matching: local averaging over vertex blocks, an orthogonal splitting lemma, a Fourier smoothing theorem, and an expander graph with a parity functional. The manuscript states no explicit value of ''c''.
* '''Sources.''' At commit <code>1581d4c</code>: [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Exponential-PSD-rank-of-positively-shifted-matching-matrices-October-5-2026 Exponential PSD rank of positively shifted matching matrices].
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/126.md scope note] states that the Lean formalization records superpolynomial lower bounds: for every fixed ''C'' &gt; 0, the positive semidefinite rank of the selected perfect-matching slack matrix exceeds ''n''<sup>''C''</sup> for all sufficiently large even ''n'', and every exact affine semidefinite lift requires matrix size greater than ''n''<sup>''C''</sup>. It states that these statements do not include the exponential bound for every fixed positive shift. The Comparator statements are <code>MatchingAffineLift</code> and <code>MatchingPSD</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 24 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "weaker statement": the Lean statements give superpolynomial lower bounds for exact affine semidefinite lifts and for the unshifted positive semidefinite rank, which still answer the polynomial-size question, while the exponential and fixed-shift statements are not formalized. It records sandboxed Comparator passes for both challenges. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/MatchingPSD.json cert-machine], openai/math lane K, run 38019899278 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>MatchingPSD</code> solution (402 s) and the <code>MatchingAffineLift</code> solution (395 s). || Repository.
|-
| 2026-10-10 || GitHub account acprk, [https://github.com/acprk/psd-rank-matching-explicit-constant acprk/psd-rank-matching-explicit-constant], note ''An explicit constant for the exponential PSD rank of perfect matching'' with a certificate, at commit [https://github.com/acprk/psd-rank-matching-explicit-constant/tree/5ff8844426b38648e65c2f06bf174c3aae460cfa 5ff8844] || Extends (explicit constant) || States that the manuscript's route, made explicit, gives log<sub>2</sub>(1/''c'') = 2<sup>101</sup> + 3.2·10<sup>6</sup> up to lower-order terms, and that four local modifications of the same proof, including Ramanujan bipartite multigraphs of degree four in place of random expanders and the exact spectrum of the local averaging operator, give log<sub>2</sub>(1/''c''′) = 259.094… with an explicit 76-digit cell size. || Unrefereed note, not formalized; it states that it is conditional on the manuscript and introduces no new mechanism, and that it was written by AI agents under the direction of the repository owner, whose name the note leaves as a placeholder.
|-
| 2026-10-16 || J. Jardine, Lattice24, referee review [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_464.json rank_464] of the manuscript in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] || Review (AI-assisted audit) || Reports no gap, with one minor note: the reduction from the positive semidefinite rank of the slack matrix to the size of an exact semidefinite lift is only sketched and relies on the hypotheses of Gouveia, Parrilo and Thomas without checking them, although the review finds the standard argument correct. It reads the main proof path in full and checks the local averaging operator, the orthogonal splitting lemma, the expander constants and the tail arithmetic by hand and by computation. || Part of an audit of the collection's manuscripts that the audit describes as complete.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]