The Popa–Vaes paving conjecture

The Popa–Vaes paving conjecture asks whether the paving property behind the Kadison–Singer problem, proved by Marcus, Spielman and Srivastava for the diagonal matrices, extends in weakened forms to every maximal abelian subalgebra of a von Neumann algebra. Two manuscripts in OpenAI's public mathematics collection, both dated 25 September 2026, claim strong-operator paving over every such subalgebra with a number of blocks of the optimal quadratic order, and approximation paving over every such subalgebra. The collection has no Lean formalization of these results.

Background

As recounted in the manuscripts' introductions:
- Kadison–Singer and paving. Kadison and Singer posed the pure-state extension problem for the atomic diagonal subalgebra of the bounded operators on ℓ². Anderson formulated its paving counterpart, and Marcus, Spielman and Srivastava resolved it with mixed characteristic polynomials. Ravichandran and Srivastava later obtained asymptotically optimal multipaving bounds from mixed determinantal polynomials.
- General maximal abelian subalgebras. For a maximal abelian subalgebra A of a von Neumann algebra M, norm paving of every operator is too restrictive: by a theorem of Popa and Vaes, for separable predual it holds exactly when M is of type I and A is the range of a normal conditional expectation. Popa and Vaes introduced strong-operator paving, which estimates the pinched operator after compression by a projection close to the identity in the strong operator topology, and approximation paving, which paves a nearby operator. They conjectured that every maximal abelian subalgebra has both properties, and conjectured a quadratic number of blocks for strong-operator paving.
- Earlier cases. Popa proved paving in ultraproducts of singular maximal abelian subalgebras. Popa and Vaes obtained strong-operator paving with order ε⁻⁴ blocks for type I algebras with separable predual and for Cartan inclusions in amenable algebras or from free ergodic profinite actions, and quadratic bounds for ultraproducts of singular subalgebras; they identified the need to unite the Cartan and singular arguments. Inserting their quartic Cartan bound into their combination result gives order ε⁻⁶.
- The exponent. An L² obstruction in a II₁ factor, due to Popa and Vaes, forces at least order ε⁻² blocks.

The original results

Quadratic strong-operator paving, 25 September 2026. The main theorem of Quadratic Strong-Operator Paving over Arbitrary Maximal Abelian Subalgebras states that for every 0 < ε < 1, every self-adjoint element x of a von Neumann algebra is strong-operator pavable over every maximal abelian subalgebra A with r_ε = ⌈4·10⁸ε⁻²⌉ + ⌈4/ε⌉ + 1 ≤ 5·10⁸ε⁻² projections. For every finite set of vectors and every tolerance there are a partition of the unit into r_ε projections of A, a self-adjoint a in A with ‖a‖ ≤ ‖x‖ and a projection q whose complement is small on the given vectors, such that the compression by q of the pinching of x minus a has norm at most ε‖x‖. No separability or conditional-expectation hypothesis is imposed. The manuscript states that this proves the quadratic strong-operator paving conjecture of Popa and Vaes, and deduces quadratic norm paving in Ocneanu ultrapowers for countably decomposable maximal abelian subalgebras with a normal conditional expectation.
Approximation paving, 25 September 2026. The main theorem of Approximation Paving over Arbitrary Maximal Abelian Subalgebras states that every self-adjoint x is a strong limit of self-adjoint operators y with ‖y‖ ≤ 3‖x‖, each of which admits a norm paving over A with error at most ε‖y‖ and at most Cε⁻⁶ projections, for a universal constant C. It states that this resolves the approximation-paving part of the Popa–Vaes conjecture. When a normal conditional expectation exists, a corollary that uses the companion manuscript gives a quadratic count.
Scope, as stated: neither theorem asserts norm paving of the original operator, which fails for general maximal abelian subalgebras; the operators are self-adjoint; the constants are not optimized, and the approximation theorem claims no quadratic bound without a normal conditional expectation. The quadratic manuscript states that its exponent two is optimal and that the two main proofs are independent.
Method, as described: after reductions that remove the conditional-expectation hypothesis, both proofs split an operator through the algebra generated by the normalizers of A. The Cartan part is paved by a measurable coloring of a nonsingular equivalence relation, built from the polynomial methods of Marcus, Spielman and Srivastava and of Ravichandran and Srivastava, with a Maharam extension to make mass transport available. The remaining part has atomless left–right kernels and is controlled through amalgamated free products and a transfer of moments to actual projections of A. The quadratic manuscript uses a single coloring for both parts.
Sources. Commit adc7f12 of the openai/math repository: Quadratic Strong-Operator Paving over Arbitrary Maximal Abelian Subalgebras and Approximation Paving over Arbitrary Maximal Abelian Subalgebras.
Formalization. The collection lists no Lean scope note or Comparator challenge for this family.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 31 October 2026)
2026-10-07	Paving arbitrary MASAs: strong topology and quadratic bounds, an article of the Latent Seminar blog at lowrank.github.io	Reading, exposition	Explains family 300: diagonal blocks and the strong topology; the two paving statements and their different quantifiers; the normalizer decomposition; a single coloring for both terms; from model colors to actual diagonal projections; clipping, moments and the large projection; removing the central-state hypothesis; the approximation-paving construction; the sharp exponent and the scope of the consequences.	Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs, and that the measured-coloring proofs, the polynomial estimates and the cited structure theorems were not audited. Read on 31 October 2026.
2026-10-16	J. Jardine, Lattice24, referee reviews rank_048 of the approximation manuscript and rank_099 of the quadratic manuscript in JJardine919/openai-math-audit	Review, AI-assisted audit	Both reviews report no gap. The approximation review read everything except one figure and the bibliography, checked the final assembly, the expectation-free reductions and the constants of the polynomial lemmas, and followed two further sections step by step without re-deriving every analytic estimate; as a minor issue, the two corollaries rest on a Popa–Vaes conversion and on the companion manuscript, which it could not check from the source. The quadratic review read all eight sections, checked the main steps and the numerical constants line by line, takes a constant of Ravichandran and Srivastava and an amalgamated free-product construction of Ueda on citation, and finds no circular dependence between the two manuscripts.	Part of the completed Lattice24 audit; the reviews are published under CC BY 4.0.
2026-10-18	AI Proved What?, episode 300 Every MASA, quadratically? The Popa–Vaes paving conjecture, remade version of 23 October 2026	Reading, exposition	Video explainer of the two preprints, 102 pages. It recalls the Kadison–Singer problem, Anderson's paving formulation and the 2013 solution of Marcus, Spielman and Srivastava, and states that Popa and Vaes in 2015 conjectured both weaker forms for subalgebras with a normal conditional expectation, said that arbitrary ones ought to have them too, and called the quadratic count more speculative. It states that the preprints do not claim norm paving of the operator itself, operators that are not self-adjoint or good constants, and compares block counts at ε = 0.1: a lower bound of 100 against 40 billion for the new strong-operator bound.	Episode status, last checked 30 October 2026: posted as preprints, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, no formalization; no expert comment or reported error found. The site states that it is made with Anthropic's Claude. Read on 31 October 2026.

Notes

The background summarizes the manuscripts' own accounts of earlier work.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.