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. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments
In Exponential PSD rank of positively shifted matching matrices, 5 October 2026
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
There is a constant c>0 such that, for every fixed 0<\rho<1, there is n_0=n_0(\rho) for which
for every even n\ge n_0.
No Lean statement in the release is paired with this theorem.
In Exponential PSD rank of positively shifted matching matrices, 5 October 2026
Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.
There are constants c_0>0 and n_1 such that, for every even n\ge n_1, both A_n(0) and T_n(0) have real PSD rank at least 2^{c_0n}, and every exact semidefinite lift of P_n has size at least 2^{c_0n}.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.
Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
MatchingAffineLiftThe paper states
In Exponential PSD rank of positively shifted matching matrices, 5 October 2026
There are constants c_0>0 and n_1 such that, for every even n\ge n_1, both A_n(0) and T_n(0) have real PSD rank at least 2^{c_0n}, and every exact semidefinite lift of P_n has size at least 2^{c_0n}.
The words they share: even, exact, lift, lifts, rank, semidefinite, size.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
MatchingAffineLift.lean, the release lists it as a supporting statement.
theorem affine_lift_lower_bound : ∀ C : ℝ, 0 < C → ∃ n₀ : ℕ, 4 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n → Even n → ∀ r : ℕ, HasAffineLift n r → (n : ℝ) ^ C < (r : ℝ) := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
MatchingPSDThe paper states
In Exponential PSD rank of positively shifted matching matrices, 5 October 2026
For every fixed K>0, there are an integer d\ge1 and N_0 with the following property. Let N\ge N_0 be even, and let a,b,c be positive integers summing to N. For a uniform ordered partition into cells of these sizes, prescribe x,y,z edges between the first and second, first and third, and second and third cells, respectively. Assume that x,y,z are nonnegative integers and that
are nonnegative even integers. Let T_{x,y,z} average functions on perfect matchings subject to these counts, and let \Pi_d project onto the edge-product span of degree at most d, using uniform measures as above. Then
uniformly in all the sizes and admissible triples. For every fixed partition and matching function f, the values T_{x,y,z}\Pi_df are given by one polynomial of total degree at most d in (x,y,z) across all admissible triples.
The words they share: perfect, edge, ordered, uniformly, counts, matching, one, positive, integers, even.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
MatchingPSD.lean, the release lists it as a supporting statement.
def MainClaim : Prop := ∀ C : ℝ, 0 < C → ∃ n₀ : ℕ, 4 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n → Even n → (n : ℝ) ^ C < (psdRank n : ℝ)theorem main : MainClaim := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
IsPerfectMatching Model.lean, line 9Crosses Model.lean, line 19HasFactorization Model.lean, line 34MainClaim Model.lean, line 46Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express a weaker statement than the advertised result (their term: “weaker-statement”).
Their note: Superpolynomial (n^C for every C) lower bounds for exact affine SDP lifts and the unshifted PSD rank only; exponential size and the fixed-shift (0<rho<1) PSD-rank statements are not stated (superpolynomial still answers Rothvoss’ polynomial-size question).
Definitions the group asks readers to compare with the paper: psdRank n := sInf {r | 0 < r ∧ HasFactorization n r} over real PSD factors of the (unshifted) matching slack matrix with slack defined on edge and odd-cut rows (Crosses, crossingCount); IsPerfectMatching by exactly one incident edge per vertex
“weaker-statement”, in their words: The challenge statements do not imply the headline claim: they state a nontrivially weaker statement.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — DECLARED”).
The gap they name: Exponential (2^{Ω(n)}) lower bounds and the shifted matrices (0 < ρ < 1) are not stated; only superpolynomial bounds for the unshifted slack matrix and for affine lifts.
“NARROWER — DECLARED”, in their words: The challenge statements state less than the headline, and OpenAI’s Lean note says so.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
OpenAI’s own note on what its Lean covers
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.
Superpolynomial lower bound for affine semidefinite lifts MatchingAffineLift
Unreviewed AI draft: states a weaker form of a paper’s theorem. States that exact affine semidefinite lifts of the perfect-matching polytope need size above n^C for every C, a superpolynomial form of the paper’s exponential lift bound. The exponential bound for positively shifted matrices is not stated.
Superpolynomial PSD rank for the perfect-matching slack matrix MatchingPSD
Unreviewed AI draft: states a weaker form of a paper’s theorem. States that the PSD rank of the perfect-matching slack matrix eventually exceeds n^C for every C, a superpolynomial form of the paper’s exponential bounds. The exponential bound for positively shifted matrices is not stated.
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
MatchingAffineLiftTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
MatchingPSDThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 142 s; peak memory 6.4 GiB). | 11 October 2026 | Original report |
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
This family’s papers cite no paper elsewhere in the release.
No paper elsewhere in the release cites this family’s papers.
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Offer to write an explanationCompare one Lean statement with its paper: MatchingAffineLift, MatchingPSDSuggest a source attributionSuggest a change
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.
Author not stated. Source
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Theorem 1.1
In Exponential PSD rank of positively shifted matching matrices, 5 October 2026
Why this passage is shown
Corollary 1.2 (Unshifted rank and exact lifts)
In Exponential PSD rank of positively shifted matching matrices, 5 October 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, MatchingAffineLift
Proof-verification report
MathVet, MatchingAffineLift
Proof-verification report
cert-machine, MatchingPSD
Proof-verification report
MathVet, MatchingPSD
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, MatchingPSD
Lean statement
MatchingAffineLift
Lean statement
MatchingPSD