AI Proved What?

Episode 327, October 2026

Walks reveal the shape?

An AI preprint claims that nontrivial Markov type forces superreflexivity

Covers result 327 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

3:33. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:04The claim
  3. 1:41How the proof goes
  4. 2:58Where it stands

The claim, in plain words

Run a stationary, reversible random walk on a finite graph and watch it through any map into a Banach space. Markov type p says that after t steps the walk has moved, on average, at most a constant times t^(1/p) times a typical single step. In a Hilbert space, Ball showed in 1992 that p can be two: the walk diffuses. In ℓ₁ it cannot: on the Hamming cube our computer finds the ratio for p = 2 growing past 26 at 128 dimensions, while in Hilbert space it never exceeds 1.

A space is superreflexive when it has an equivalent norm whose unit ball is uniformly round. In 2006 Naor, Peres, Schramm and Sheffield showed that smooth norms give Markov type above 1; with Pisier’s renorming, every superreflexive space has it. In 2012 Naor asked the converse: can a space have Markov type above 1 without such a norm? The question was listed as open, and ordinary Rademacher type is known not to be enough.

Result 327 is one OpenAI paper, 14 pages, dated September 23 and made public October 6, 2026. It claims that every real Banach space with Markov type p for some p above 1 is superreflexive. Together with the known converse, nontrivial Markov type is exactly superreflexivity.

What it doesn’t claim

Not claimed: any relation between the exponents, any explicit constant beyond the proof’s own, or anything about general metric spaces. The walks the proof builds are finite but astronomically large.

Where it stands

Posted as a preprint
OpenAI, 14 pages, dated September 23, 2026
Peer reviewed
Not yet
Formalized in Lean
The full equivalence (docs)

Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Lean formalizes the full equivalence, including the classical inputs, in 207 files and about 27,000 lines, not run by us. Three outside projects re-ran it and it was accepted. We found no public comment from specialists and no reported error. OSVerify has not reviewed it.

How the proof goes

  1. Partial sums that swing between two levels. Suppose a space is not superreflexive. Then it contains, almost isometrically, every finite piece of a norm in which merging neighbouring entries never increases the length, like the size of the largest partial sum. In such a norm, a sum whose partial sums swing many times between two levels a distance l apart has length at least l/6, measured in single steps. The proof needs a reversible walk whose labels do exactly that, with l proportional to the number of steps.
  2. The free group does it. The free group supplies it. A random word of length n keeps, on average, at least half its letters after cancellation; our computer gets 64.75 at 128. Commuting letters would only diffuse. Ping-pong maps let the free group act on the line, and our computer confirms the paper’s two lemmas, for one choice of arcs, on 13,120 reduced words. A finite Ramsey argument lets this motion run inside a finite stationary, reversible walk, and a lattice trick turns edge labels into positions. Then, with probability at least 3/20, the walk moves at least n/24 step lengths, which contradicts Markov type p above 1 for large n.

The numbers in the video

  • Ours, exact: on the Hamming cube, the Markov-type ratio for p = 2 grows to 26.6 at 128 dimensions in ℓ₁ and stays at most 1 in Hilbert space.
  • Ours, exact: a random free-group word of length n keeps on average at least n/2 letters (64.75 at n = 128); commuting letters only diffuse.
  • Ours: the paper’s ping-pong lemmas hold on all 13,120 reduced words of length up to 8, for one choice of arcs.
  • The paper’s constants: the walk moves at least n/24 step lengths with probability at least 3/20.
  • Lean: 207 files and 27,054 lines in the import closure (counted by us; not run by us).

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

Run a stationary, reversible random walk on a finite graph and watch it through any map into a Banach space. Markov type p says that after t steps the walk has moved, on average, at most a constant times t^(1/p) times a typical single step. In a Hilbert space, Ball showed in 1992 that p can be two: the walk diffuses. In ℓ₁ it cannot: on the Hamming cube our computer finds the ratio for p = 2 growing past 26 at 128 dimensions, while in Hilbert space it never exceeds 1. A space is superreflexive when it has an equivalent norm whose unit ball is uniformly round. In 2006 Naor, Peres, Schramm and Sheffield showed that smooth norms give Markov type above 1; with Pisier’s renorming, every superreflexive space has it. In 2012 Naor asked the converse: can a space have Markov type above 1 without such a norm? The question was listed as open, and ordinary Rademacher type is known not to be enough.

1:04The claim

Result 327 is one OpenAI paper, 14 pages, dated September 23 and made public October 6, 2026. It claims that every real Banach space with Markov type p for some p above 1 is superreflexive. Together with the known converse, nontrivial Markov type is exactly superreflexivity. Not claimed: any relation between the exponents, any explicit constant beyond the proof’s own, or anything about general metric spaces. The walks the proof builds are finite but astronomically large.

1:41How the proof goes

Suppose a space is not superreflexive. Then it contains, almost isometrically, every finite piece of a norm in which merging neighbouring entries never increases the length, like the size of the largest partial sum. In such a norm, a sum whose partial sums swing many times between two levels a distance l apart has length at least l/6, measured in single steps. The proof needs a reversible walk whose labels do exactly that, with l proportional to the number of steps. The free group supplies it. A random word of length n keeps, on average, at least half its letters after cancellation; our computer gets 64.75 at 128. Commuting letters would only diffuse. Ping-pong maps let the free group act on the line, and our computer confirms the paper’s two lemmas, for one choice of arcs, on 13,120 reduced words. A finite Ramsey argument lets this motion run inside a finite stationary, reversible walk, and a lattice trick turns edge labels into positions. Then, with probability at least 3/20, the walk moves at least n/24 step lengths, which contradicts Markov type p above 1 for large n.

2:58Where it stands

The paper is unrefereed and unchanged since release. Lean formalizes the full equivalence, including the classical inputs, in 207 files and about 27,000 lines, not run by us. Three outside projects re-ran it and it was accepted. We found no public comment from specialists and no reported error. If it holds, how random walks spread inside a Banach space detects exactly whether it can be given a uniformly round norm, answering Naor’s question.

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.