Approximation and quadratic strong-operator paving

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves that every self-adjoint element of a complex von Neumann algebra admits strong-operator paving relative to any maximal abelian subalgebra with \(O(\varepsilon^{-2})\) blocks. The norm bound holds after compression by a projection arbitrarily close to the identity in the strong topology, resolving the Popa–Vaes quadratic paving conjecture.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1

In Approximation Paving over Arbitrary Maximal Abelian Subalgebras, 25 September 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 universal constant C_{\mathrm{ap}}>0 such that for every 0<\varepsilon<1 there is an integer R(\varepsilon)\leq C_{\mathrm{ap}}\varepsilon^{-6} with the following property. Let M\subseteq\mathcal B(H) be a complex von Neumann algebra, let A\subseteq M be a MASA, and let x=x^*\in M. For every finite F\subset H and every \delta>0, there exist y=y^*\in M, a partition \mathcal P=(p_i)_{i=1}^{R(\varepsilon)} of the unit in A, and a=a^*\in A, such that

\norm{y}\leq3\norm{x},\qquad \norm{(y-x)\xi}<\delta\quad(\xi\in F),

and

\norm{a}\leq\norm{y},\qquad \norm{C_{\mathcal P}(y)-a}\leq\varepsilon\norm{y}.

Zero projections may be included in the partition.

Corollary 1.2

In Approximation Paving over Arbitrary Maximal Abelian Subalgebras, 25 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

Suppose that a MASA A\subseteq M is the range of a normal conditional expectation. For each 0<\varepsilon<1 there is an integer R_s(\varepsilon), independent of the inclusion, such that for every x=x^*\in M and every strong-operator neighborhood \mathcal V of zero, there exist an R_s(\varepsilon)-partition \mathcal P in A, an a=a^*\in A with \norm{a}\leq\norm{x}, and a projection q\in M with \one-q\in\mathcal V, satisfying

\norm{q(C_{\mathcal P}(x)-a)q}\leq\varepsilon\norm{x}.

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.

Three more possible matches

Corollary 1.2 (Quadratic norm paving in Ocneanu ultrapowers) in Quadratic Strong-Operator Paving over Arbitrary Maximal Abelian Subalgebras, 25 September 2026.
Theorem 1.1 in Quadratic Strong-Operator Paving over Arbitrary Maximal Abelian Subalgebras, 25 September 2026.
Corollary 1.3 (Quadratic approximation paving for expected MASAs) in Approximation Paving over Arbitrary Maximal Abelian Subalgebras, 25 September 2026.

Reported proof verification: The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations: Two current papers, each readable here as a page beside its PDF.

Papers

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.

Approximation Paving over Arbitrary Maximal Abelian Subalgebras

25 September 2026, current edition.

Read it here PDF

We prove the approximation-paving conjecture of Popa and Vaes for every maximal abelian subalgebra of a complex von Neumann algebra. For each \(0\lt \varepsilon\lt 1\), every self-adjoint operator is a strong limit of self-adjoint operators of norm at most three times its norm, each admitting a norm paving with error at most ε times the approximant’s own norm. The number of projections is at most \(C\varepsilon^{-6}\) for a universal constant C. No separability or conditional-expectation hypothesis is required.

Quadratic Strong-Operator Paving over Arbitrary Maximal Abelian Subalgebras

25 September 2026, current edition.

Read it here PDF

We prove the quadratic strong-operator paving conjecture of Popa and Vaes. For every \(0\lt \varepsilon \lt 1\), every self-adjoint element of a von Neumann algebra admits strong-operator paving over each maximal abelian subalgebra with at most \(5\times10^8\varepsilon ^{-2}\) projections. The bound is uniform over representations and requires no separability or conditional-expectation assumption.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

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.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

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

Explain a result, compare statements or propose a correction

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 explanation Suggest a source attribution Suggest a change

What people have said

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 “Solid publication, could lead to tenure”. The page says that nothing on it is verified.
Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

Family 300 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

Family 300 The release has no Lean statement for this family. Open the form