Midpoints aren’t enough?

The claim, in plain words

Stand at a unit vector and step a distance t in some direction far out in the space. Does the length grow? A norm is asymptotically uniformly convex if every far-out step gains a definite amount. A weaker property, asymptotic midpoint uniform convexity, asks only that a step and its opposite gain on average. On a tiny tree from the release’s space, our computer shows the gap: one push gains nothing until t reaches 1, while the opposite push grows like the √(1 + t²).

Diamond graphs ask a related question: replace each edge by many two-edge paths, again and again, and see how badly the result must be distorted to fit in a space. In 2017, seven authors showed that midpoint convexity forces the distortion of countably branching diamonds to grow without bound, and noted that a 2016 question was still open: can midpoint convexity always be upgraded to the stronger property by changing the norm? In 2025 a book asked, as Problem 39, whether a reflexive space with no such upgrade must always fit the diamonds with bounded distortion, and its authors suspected yes. On September 18, 2026, Baudier answered the upgrade question no, in a non-reflexive space, with a proof that the note says was generated by an OpenAI model.

Result 331 is seven OpenAI papers, 225 pages in all, dated September 27 and made public October 6, 2026. The headline paper claims a separable reflexive space, built from James’s segment norm on a forest of countably branching trees, that is asymptotically midpoint uniformly convex with an explicit modulus, but has no equivalent asymptotically uniformly convex norm. In the same space, depth-k diamonds need distortion at least √(1 + k/12); a companion paper improves this to √(1 + k/4).

What it doesn’t claim

Not claimed: the first separation of the two properties, which Baudier had already done; optimal constants; or any upper bound on diamond distortion. Some companion spaces are not reflexive.

Where it stands

Posted as preprints

OpenAI, 7 papers, 225 pages, dated September 27, 2026

Peer reviewed

Not yet

Formalized in Lean

The headline theorem in full, plus the companions’ main statements (docs)

Last checked October 19, 2026. The papers are unrefereed and unchanged since release. Lean formalizes the headline theorem in full, along with the companions’ main statements, in seven checks and about 49,000 lines, not run by us. Three outside projects re-ran them and they were accepted. We found no public comment from specialists and no reported error. OSVerify has not reviewed it.

How the proof goes

1. Tall trees defeat every AUC norm. Inside each tree, root paths all have length 1, and stepping to a child is a push in a far-out direction. If some equivalent norm were asymptotically uniformly convex, each step to a far-out child could gain a fixed factor, so a path down a tall enough tree would grow without bound, yet root paths stay bounded. Since the forest has trees of every height, no equivalent norm can be asymptotically uniformly convex.
2. Midpoints force the squared stretch to grow. The midpoint estimate tests the two pushes together, with a correction placed at the first vertices outside a finite head; the correction cancels when the two sides are averaged. Then, for each diamond edge, its many midpoints force the squared stretch to grow by a fixed amount, 1/12, per level, and summing over k levels gives the bound. Our computer tabulates it: √(1 + k/12) reaches 2 at depth 36, while the companion bound reaches 2 at depth 12.

The numbers in the video

• Ours, exact on a tiny tree: one push gives length max(1, t), the opposite push √(1 + t²).
• The bounds: √(1 + k/12) reaches 2 at depth 36; the companion’s √(1 + k/4) reaches 2 at depth 12 (our arithmetic).
• Ours: the diamond distance facts the proof uses hold for branching 2, 3 and 4 up to depth 5.
• Lean: 7 checks; 171 files and 49,376 lines in the import closures (counted by us; not run by us).

Read the source

• Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space (PDF), 12 pages.
• Midpoint lenses in segment spaces (PDF), 74 pages.
• Diamond distortion from midpoint and tree energies (PDF), 39 pages.
• Exact asymptotic moduli in a Daugavet subspace of L1 (PDF), 13 pages.
• Midpoint convexity from bounded tree potentials and path costs (PDF), 53 pages.
• Independent products in real L1: asymptotic midpoint convexity without AUC renormings (PDF), 11 pages.
• Midpoint convexity from two recursive potentials (PDF), 23 pages.
• The Lean formalization notes.
• The collection’s catalog, where this is result 331.

The 7 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

• Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space main paper
• Midpoint lenses in segment spaces companion
• Distortion of countably branching diamonds from midpoint and tree energies companion
• Exact asymptotic moduli in a Daugavet subspace of L1 companion
• Midpoint convexity from bounded tree potentials and path costs companion
• Independent products in real L1: asymptotic midpoint convexity without AUC renormings companion
• Midpoint convexity from two recursive potentials companion

Transcript

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.