Expanders in every dimension?

The claim, in plain words

An expander graph has no bottlenecks: for any set of dots, the edges leaving it are many compared with how far the set is from nothing or everything. A long cycle is a poor expander (two edges cut it in half); a complete graph is a good one, but every dot touches every other. The classical achievement is graphs of any size with a bounded number of edges at each dot that all expand by the same margin. In a simplicial complex (dots, edges, triangles, tetrahedra, and so on), the coboundary of a set of edges is the set of triangles containing an odd number of them, and in general the coboundary of a set of i-faces is the set of (i+1)-faces containing an odd number of them. The star of a dot is the coboundary of that dot, and lights up no triangle. Coboundary expansion asks, at every level, that a set with a small coboundary be close to such a trivial set, a coboundary from one level down, with sizes measured by the paper’s weights (pick a top face at random, then one of its i-faces). Holes spoil this: on our 9-dot torus a ring of edges around the hole has no coboundary yet is not trivial, so the constant is 0. Size spoils it too: on a long sphere with at most 6 triangles at each dot, a crack of marked edges lights only its two ends, so the constant is at most 3/199 at 300 dots (our computation). Complete complexes expand well (10/7 at the edge level on 8 dots, by our computation), but each dot touches more and more triangles.

As the paper recounts, Gromov asked for arbitrarily large complexes with a bounded number of pieces at each vertex and uniform filling bounds; the full coboundary expansion problem also demands that there be no holes (a recent formulation is Chapman and Lubotzky’s Problem 1.3). Random coboundary expanders by Lubotzky and Meshulam (dimension 2) and by Lubotzky, Luria and Rosenthal (every dimension) bound the top faces around faces one level below the top, but their vertex degrees grow. Kaufman, Kazhdan and Lubotzky, and Evra and Kaufman, proved that certain bounded-degree complexes are cosystolic expanders, which measures distance to sets with no coboundary, so holes are allowed. Chapman and Lubotzky settled dimension two over the field with two elements.

Result 177 is one OpenAI preprint, Bounded-degree coboundary expanders in every dimension (14 pages, dated September 24, 2026). Its Theorem 1.1: for every d ≥ 3 there are constants D and ε > 0 and finite, connected, pure d-dimensional complexes X_m with more and more vertices, such that every vertex lies in at most D faces of dimension d and ‖δ_if‖ ≥ ε dist(f, Bⁱ) for every set f of i-faces, for 0 ≤ i < d. “The constants are independent of m, i, and f.” Together with expander graphs and Chapman and Lubotzky’s dimension two, the paper concludes that bounded-degree F₂ coboundary expanders exist in every positive dimension.

What it doesn’t claim

No small or computed constants. The prime q is only “sufficiently large”, partly through a threshold in a cited theorem that the paper does not quantify. Its explicit conditions alone force q ≥ 37 in dimension three, and by our computation that makes the paper’s degree bound D at least about 1.7 × 10³⁴ and the first complex at least about 1.3 × 10⁷⁶ vertices. It gives one growing sequence, not every size, and no algorithm. The coefficients are mod 2 only, and it claims no applications. It is not the first bounded-degree high-dimensional expander: its step is from cocycles to coboundaries, by proving that the holes vanish.

Where it stands

Posted as a preprint

OpenAI, 14 pages, dated September 24, 2026

Peer reviewed

Not yet

Checked in Lean

Formalized by OpenAI in the same form; not run by us

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. OpenAI published a Lean formalization whose comparator statement states the theorem in the same form, with the paper’s weights and mod-2 coefficients. By our count the proof takes 36 files and 33,125 lines, excluding Mathlib (source), with no unproved steps by our search; we have not rebuilt it. The Lean proof assumes none of the paper’s cited results: it proves what it needs itself (the case of the cosystolic inequality it uses, not the general theorem), and by its own notes it avoids the stability theorems. The result is not listed in the repository’s formalization.yaml. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

1. The construction. In an established program of Kac–Moody–Steinberg complexes, take matrices of size 2d+1 with determinant one, entries polynomials in t over the field with q elements (q a large odd prime), upper unitriangular at t = 0. They are generated by 2d+1 simple moves arranged in a cycle; leaving out any one, the others generate a finite group. The cosets of these finite groups are the vertices, and overlapping cosets form faces. Reducing modulo t^m (Oppenheim and Valentiner-Branth’s related construction used other quotients) keeps the finite groups, so every vertex sees the same number of top faces for every m while the complexes grow. These complexes have dimension 2d; the expanders are their d-skeletons.
2. Geometry. The infinite complex is the set of chambers opposite one chamber in an affine twin building. Rebuilding that half of the building layer by layer, each layer’s effect is governed by a spherical piece (an opposition complex) with no mod-2 holes once q is large, and that half is contractible, so the infinite complex, and its group, have no holes below dimension 2d − 1.
3. Algebra. Iwasa’s homological stability theorem, with an input from Morrow, and a transfer argument that works because the finite quotients have odd order, show that the finite complexes have no mod-2 cohomology in degrees 1 to d − 1. This is where the matrix size 2d+1 is needed.
4. Analysis. A theorem of Oppenheim and Valentiner-Branth gives cosystolic expansion with one constant η for every m: a small coboundary means close to a set with no coboundary. With no holes those are all trivial, and comparing weights moves the inequality to the d-skeleton, with ε = η divided by the number of top faces at a vertex of the full 2d-dimensional complex.

The numbers in the video

• Our exact constants with the paper’s weights: cycles on 12 and 24 dots, 1/3 and 1/6; the complete graph on 8 dots, 8/7; the Petersen graph, 2/3.
• Our 3 × 3 torus (9 dots, 18 triangles): the ring of edges between two columns has no coboundary and is not a coboundary, so the coboundary constant is 0 (the cosystolic constant is 3/4).
• Our long spheres made from a tube, at most 6 triangles per dot: constant at most 3/19, 3/99 and 3/199 at 30, 150 and 300 dots.
• Our complete 2-complexes on 5 to 8 dots, edge level: 5/3, 3/2, 7/5 and 10/7, with 6, 10, 15 and 21 triangles per dot.
• Sizes, from the paper’s explicit conditions on q (an odd prime, q ≥ 5, q ≥ 2^2d−1): in dimension 3, q ≥ 37, D ≥ 20 · 37²¹ ≈ 1.7 × 10³⁴, and the first complex has at least 7 · 37⁴⁸ ≈ 1.3 × 10⁷⁶ vertices (our computation; the true q may be larger).
• The Lean count: our count of the import closure.

Read the source

• Bounded-degree coboundary expanders in every dimension (PDF), 14 pages.
• The Lean scope note.
• The collection’s catalog, where this is result 177.

The paper

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

• Bounded-degree coboundary expanders in every dimension

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.