AI Proved What?

Episode 208, October 2026

Every category finds a floor?

A preprint claims the finite case of the Benson–Etingof–Ostrik conjecture: every finite symmetric tensor category in characteristic p has a fiber functor to some level of the Verlinde tower

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

4:09. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:29The claim
  3. 2:21How the proof goes
  4. 3:24Where it stands

The claim, in plain words

Representations of a group can be added, multiplied by tensor product, and swapped: V ⊗ W is the same as W ⊗ V. A category with these features, finitely many simple pieces, enough projectives, and duals, is a finite symmetric tensor category. Is every such category secretly representations of a group, seen through a fiber functor: a faithful, exact translation into a simpler target that respects the tensor product and the swap? In characteristic zero, Deligne proved in 2002 that super vector spaces are a common target, for all categories of moderate growth.

In characteristic p, new targets are needed: the Verlinde categories. The first, Verp, keeps the Jordan blocks of a cyclic group of order p and throws away the largest one. Our computer checks the rules in characteristic five: two Jordan blocks of size three multiply to blocks of sizes one, three and five; drop the five, and the third simple object squares to the first plus itself. Its Frobenius–Perron dimension is the golden ratio. Benson, Etingof and Ostrik, and independently Coulembier, built a tower of higher Verlinde categories, Verpn, and Benson, Etingof and Ostrik conjectured that every category of moderate growth maps into this tower.

Result 208 is one OpenAI preprint, Fiber functors for finite symmetric tensor categories in positive characteristic (26 pages, dated September 24, 2026). It claims the finite case of that conjecture: for every prime p, including two, every finite symmetric tensor category over an algebraically closed field of characteristic p has a fiber functor to some level Verpn of the tower. The level depends on the category, and no bound on it is given.

What it doesn’t claim

Categories that are not finite (the full conjecture of moderate growth); a functor at a prescribed level; or uniqueness, except in characteristic two, where an earlier theorem already allows at most one. Along the way, the paper proves a conjecture of Coulembier and Flake about tilting modules for SL2, its main new ingredient.

Where it stands

Posted as a preprint
OpenAI, 26 pages, dated September 24, 2026
Peer reviewed
Not yet
Checked in Lean
Main theorem not formalized; an uncatalogued formalization of the key tilting theorem

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. The release lists no Lean for it, but its Lean library holds an uncatalogued formalization of the key tilting theorem (source), about 12,000 lines with no unproved steps; we did not build it. The main theorem is stated there but not proved. The paper is not among those OSVerify reviewed, and we found no expert reaction. Our checks only illustrate small definitions and lemmas.

How the proof goes

  1. Restricted tilting. The new theorem (Theorem 3.1): restrict the Steinberg module to a copy of an elementary abelian group of order pr inside SL2, tensor it with any representation, and the result is the restriction of a tilting module. The proof lifts the representation to a vector bundle on the plane minus the origin, extends it across the origin, and compares fibers. With this, Coulembier and Flake’s higher Frobenius functor becomes symmetric monoidal.
  2. A higher Frobenius functor. The paper takes pr-th tensor powers of objects and reads them through that functor into the category tensored with Verpr, choosing r and the embedding so that the functor is exact (Theorem 6.5).
  3. Squeezing. The Frobenius–Perron dimension never increases along a finite graph of simple objects (Section 7). Iterating finitely many times leaves only a part where earlier results of Etingof with Ostrik, and of Etingof with Gelaki, give a target. Everything lands in one level, Verpn.

The numbers in the video

  • Ver5 (ours): J3 ⊗ J3 = J1 + J3 + J5, so L3 ⊗ L3 = L1 + L3, and the Frobenius–Perron dimension of L3 is 1.618034, the golden ratio.
  • Further checks (ours, not on screen): Verp fusion rules for p = 2, 3, 5, 7 computed two ways (35 pairs agree); the paper’s Lemma 6.2 in 9,595 brute-force tests; Lemma 7.1’s identity in 8 cases. The Lean line count is ours.

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

Representations of a group can be added, multiplied by tensor product, and swapped: V tensor W is the same as W tensor V. A category with these features, finitely many simple pieces, enough projectives, and duals, is a finite symmetric tensor category. A natural question is whether every such category is secretly representations of a group, seen through a fiber functor: a faithful, exact translation into a simpler target that respects the tensor product and the swap. In characteristic zero, Deligne proved in 2002 that super vector spaces are always a common target, for all categories of moderate growth. In characteristic p, that fails, and new targets are needed: the Verlinde categories. The first, Ver_p, keeps the Jordan blocks of a cyclic group of order p, and throws away the largest one. Our computer checks the rules in characteristic five: two Jordan blocks of size three multiply to blocks of sizes one, three and five; drop the five, and the third simple object squares to the first plus itself. Its size, the Frobenius–Perron dimension, is the golden ratio. Benson, Etingof and Ostrik, and independently Coulembier, built a whole tower of higher Verlinde categories, Ver_{p^n}, and Benson, Etingof and Ostrik conjectured that every category of moderate growth maps into this tower.

1:29The claim

Result 208 is one OpenAI preprint, 26 pages, dated September 24, 2026. It claims the finite case of that conjecture: for every prime p, including two, every finite symmetric tensor category over an algebraically closed field of characteristic p has a fiber functor to some level Ver_{p^n} of the tower. The level depends on the category, and no bound on it is given. Not claimed: categories that are not finite, the full conjecture of moderate growth; a functor at any prescribed level; or uniqueness, except in characteristic two, where an earlier theorem already allows at most one. Along the way, the paper proves a conjecture of Coulembier and Flake about tilting modules for two-by-two matrices of determinant one, and that is its main new ingredient.

2:21How the proof goes

The new theorem says: restrict the Steinberg module to a copy of an elementary abelian group of order p^r inside two-by-two matrices, tensor it with any representation, and the result is the restriction of a tilting module. The proof lifts the representation to a vector bundle on the plane minus the origin, extends it across the origin, and compares fibers. With this, Coulembier and Flake’s higher Frobenius functor becomes symmetric monoidal. The paper then takes p^r-th tensor powers of objects of the category and reads them through that functor into the category tensored with Ver_{p^r}. It chooses r and the embedding so that the functor is exact, and shows the Frobenius–Perron dimension never increases along a finite graph of simple objects. Iterating finitely many times leaves only a part where earlier results of Etingof with Ostrik, and of Etingof with Gelaki, give a target. Everything lands in one level, Ver_{p^n}.

3:24Where it stands

The preprint is unrefereed and has not been revised. The release lists no Lean for it, but its Lean library holds an uncatalogued formalization of the key tilting theorem, about 12,000 lines with no unproved steps; we did not build it. The main theorem is stated there but not proved. The paper is not among those OSVerify reviewed, and we found no expert reaction. Our checks only illustrate small definitions and lemmas. If it holds, every finite symmetric tensor category in characteristic p has a fiber functor into some floor of the Verlinde tower, the finite part of a characteristic p analogue of Deligne’s theorem.

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.