Pisier’s last question?
An AI preprint claims the cotype–cotype conjecture for spaces with the approximation property
Covers result 326 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:57. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Flip a fair sign on each of n unit vectors and add them up. How long is the random sum on average? For the n basis vectors, it depends on the space. In ℓ₁ it is always n; in a Hilbert space, the √n; in ℓ∞, just one. Type says random sums grow more slowly than in ℓ₁; cotype says they still grow, unlike in ℓ∞. A Hilbert space is the best case of both. For 12 vectors, our computer gets 12, about 3.5, and 1.
A space is K-convex when the projection that keeps only the linear part of functions on the sign cube stays bounded however many signs there are. In ℓ₁ and ℓ∞ it does not: our lower bound already passes 25 at 1,001 signs. Pisier showed that K-convexity is the same as nontrivial type. In 1980 and 1981 Pisier asked, then conjectured for spaces with a basis, that finite cotype of both a space and its dual should force it, and called this the last basic question in the theory of type and cotype. Pisier proved it with a bounded approximation hypothesis and a restriction on the exponents, and showed that without some approximation hypothesis it fails.
Result 326 is one OpenAI paper, 21 pages, dated September 23 and made public October 6, 2026. It claims the conjecture for real Banach spaces with the approximation property: such a space is K-convex exactly when it and its dual both have finite cotype, with any exponents. The approximation property is weaker than the bounded version, and almost every classical space has it.
What it doesn’t claim
Not claimed: anything without the approximation property, where the converse can fail, complex spaces, or explicit constants; the paper says its constants are existential. The easy direction, from K-convexity to cotype, was already known for all spaces.
Where it stands
- Posted as a preprint
- OpenAI, 21 pages, dated September 23, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- The main theorem (docs)
Last checked October 19, 2026. The paper is unrefereed and unchanged since release. The main theorem is formalized in Lean, in 125 files and about 12,000 lines, including Pisier’s classical theorem, not run by us. Three outside projects re-ran it and it was accepted, and a reviewer of a separate formal-conjectures entry found that entry’s statement matches the paper. The corollaries are not formalized. We found no public comment from specialists and no reported error. OSVerify has not reviewed it.
How the proof goes
- Walsh norms: does it decay? The tool is a Walsh norm: apply a map to a family of vectors indexed by binary strings, and mix them with a Hadamard matrix. For a Hilbert space the Walsh norm of the identity halves every two steps; for ℓ₁ or ℓ∞ it stays at 1 forever. Our computer reproduces both patterns. If a space contained good copies of ℓ₁ in every finite dimension, its Walsh norms could not decay.
- From slow decay to a contradiction. Cotype on both sides lets the proof lift vectors to bounded families with prescribed sign-weighted averages. A Fourier lemma on binary matrices then shows these families cannot put all their weight on rank-one patterns, so slow decay would keep Walsh norms large at ever higher dimensions, which a finite-rank map cannot do. That gives uniform decay for every finite-rank map, and the approximation property passes it, through compact maps, to the identity. The constants are huge: even in the best case, the shortest tuple length the paper’s conditions allow is about 2⁷⁴.
The numbers in the video
- Ours, exact: random sign sums of the n basis vectors have average length n in ℓ₁, √n in ℓ₂ and 1 in ℓ∞ (12, 3.46 and 1 at n = 12).
- Ours: a lower bound for the Rademacher projection in ℓ₁ and ℓ∞ grows without bound (25.25 at 1,001 signs); in Hilbert space it is 1.
- Ours: Walsh norms of the identity stay at 1 for ℓ₁ and ℓ∞ and halve every two steps for ℓ₂.
- Ours: in the best case, the shortest tuple length the paper’s conditions allow is about 2⁷⁴.
- Lean: 125 files and 11,759 lines in the import closure (counted by us; not run by us).
Read the source
- The cotype–cotype conjecture under the approximation property (PDF), 21 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 326.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Flip a fair sign on each of n unit vectors and add them up. How long is the random sum on average? For the n basis vectors, it depends on the space. In ℓ₁ it is always n; in a Hilbert space, the √n; in ℓ∞, just one. Type says random sums grow more slowly than in ℓ₁; cotype says they still grow, unlike in ℓ∞. A Hilbert space is the best case of both. For 12 vectors, our computer gets 12, about 3.5, and 1. A space is K-convex when the projection that keeps only the linear part of functions on the sign cube stays bounded however many signs there are. In ℓ₁ and ℓ∞ it does not: our lower bound already passes 25 at 1,001 signs. Pisier showed that K-convexity is the same as nontrivial type. In 1980 and 1981 Pisier asked, then conjectured for spaces with a basis, that finite cotype of both a space and its dual should force it, and called this the last basic question in the theory of type and cotype. Pisier proved it with a bounded approximation hypothesis and a restriction on the exponents, and showed that without some approximation hypothesis it fails.
1:17The claim
Result 326 is one OpenAI paper, 21 pages, dated September 23 and made public October 6, 2026. It claims the conjecture for real Banach spaces with the approximation property: such a space is K-convex exactly when it and its dual both have finite cotype, with any exponents. The approximation property is weaker than the bounded version, and almost every classical space has it. Not claimed: anything without the approximation property, where the converse can fail, complex spaces, or explicit constants; the paper says its constants are existential. The easy direction, from K-convexity to cotype, was already known for all spaces.
2:03How the proof goes
The tool is a Walsh norm: apply a map to a family of vectors indexed by binary strings, and mix them with a Hadamard matrix. For a Hilbert space the Walsh norm of the identity halves every two steps; for ℓ₁ or ℓ∞ it stays at 1 forever. Our computer reproduces both patterns. If a space contained good copies of ℓ₁ in every finite dimension, its Walsh norms could not decay. Cotype on both sides lets the proof lift vectors to bounded families with prescribed sign-weighted averages. A Fourier lemma on binary matrices then shows these families cannot put all their weight on rank-one patterns, so slow decay would keep Walsh norms large at ever higher dimensions, which a finite-rank map cannot do. That gives uniform decay for every finite-rank map, and the approximation property passes it, through compact maps, to the identity. The constants are huge: even in the best case, the shortest tuple length the paper’s conditions allow is about 2⁷⁴.
3:08Where it stands
The paper is unrefereed and unchanged since release. The main theorem is formalized in Lean, in 125 files and about 12,000 lines, including Pisier’s classical theorem, not run by us. Three outside projects re-ran it and it was accepted, and a reviewer of a separate formal-conjectures entry found that entry’s statement matches the paper. The corollaries are not formalized. We found no public comment from specialists and no reported error. If it holds, for spaces with the approximation property, finite cotype of a space and its dual is exactly what rules out good copies of ℓ₁ in every finite dimension, settling Pisier’s question in that setting.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.