Group Theory

Motivation: high-dimensional analogues of expander graphs

An expander graph is a sparse graph in which every set of vertices has a large edge boundary relative to its size. Expanders with bounded degree are a basic tool across combinatorics, computer science and group theory. High-dimensional expanders are simplicial complexes that extend this behavior to faces of every dimension, and coboundary expansion over $\mathbb F_2$ is the strongest of the standard notions: the coboundary of any set of $i$-faces must be large unless the set is already close to a coboundary. Gromov connected such filling inequalities with topological overlap of maps to Euclidean space. The basic existence question is whether there are arbitrarily large complexes of fixed dimension with bounded vertex degree and uniform coboundary expansion in every degree.

Background and timeline

• 2006–2009 — Linial–Meshulam (Combinatorica 2006) and Meshulam–Wallach (Random Struct. Alg. 2009) develop the coisoperimetric viewpoint through random complexes.
• 2010 — Gromov connects cohomological filling inequalities with topological overlap and asks for large complexes with bounded vertex incidence and uniform filling bounds (GAFA 2010, §§2.3–2.5, 2.14).
• 2015 — Lubotzky and Meshulam construct random Latin-square coboundary expanders in dimension two, with bounded codimension-one degree (Adv. Math. 2015).
• 2016 — Kaufman, Kazhdan and Lubotzky prove cosystolic and topological expansion for two-dimensional skeleta of Ramanujan complexes, with bounded vertex degree (GAFA 2016).
• 2019 — Lubotzky, Luria and Rosenthal construct random Steiner-system coboundary expanders in every dimension, again with bounded codimension-one degree but growing vertex degree (Discrete Comput. Geom. 2019).
• 2024 — Evra and Kaufman obtain bounded-degree cosystolic expanders in every dimension (JAMS 2024); cosystolic expansion allows nonzero cohomology.
• 2025 — Chapman and Lubotzky prove existence of bounded-degree two-dimensional coboundary expanders over $\mathbb F_2$ and state the general problem (Adv. Math. 2025, Problem 1.3, Theorem 1.9); Kaufman–Oppenheim–Weinberger (arXiv:2411.02819) prove degree-one coboundary expansion for coset complexes; Oppenheim and Valentiner-Branth prove cosystolic expansion for Kac–Moody–Steinberg complexes (arXiv:2504.05823).
• 2026 — The OpenAI preprint Bounded-degree coboundary expanders in every dimension (OpenAI Math Release, September 24, 2026) claims bounded-degree $\mathbb F_2$ coboundary expanders in every dimension $d\ge3$. It has not been peer reviewed and its theorem is not formally verified.

Setting

A finite simplicial complex $Y$ is a downward-closed family of finite sets (faces) of vertices; $Y(i)$ denotes the faces with $i+1$ vertices. $Y$ is pure of dimension $s$ if it has $s$-faces and every face lies in one. An $i$-cochain is a function $f:Y(i)\to\mathbb F_2$; its coboundary is $(\delta_if)(\tau)=\sum_{\sigma\subset\tau,\,|\sigma|=i+1}f(\sigma)$. Let $B^i(Y)=\operatorname{im}\delta_{i-1}$, with $B^0(Y)$ the constant functions. Faces are weighted by

$$w_i(\sigma)=\frac{\#\{\tau\in Y(s):\sigma\subseteq\tau\}}{\binom{s+1}{i+1}|Y(s)|},\qquad \|f\|_{i}=\sum_{\sigma:\,f(\sigma)\ne0}w_i(\sigma),$$

so $\|f\|_i$ is the probability that $f$ is nonzero on a random $i$-face of a uniformly random top face, and $\operatorname{dist}_i(f,A)=\min_{a\in A}\|f-a\|_i$.

In Lean (namespace OAI.CoboundaryExpanders), a Complex has vertex set Fin vertexCount, a Finset of faces that is downward closed and contains every singleton; Pure, Connected (connected $1$-skeleton), weight, norm, coboundary, coboundaries and distance follow these definitions, and topDegree X d v counts $d$-faces containing $v$.

Formalization targets

Goal: bounded-degree coboundary expanders (Theorem 1.1)

For every $d\ge3$ there are $D<\infty$, $\varepsilon>0$ and finite connected pure $d$-dimensional complexes $X_m$ with $|X_m(0)|\to\infty$, every vertex in at most $D$ faces of dimension $d$, and

$$\|\delta_if\|_{X_m,i+1}\ \ge\ \varepsilon\,\operatorname{dist}_{X_m,i}\bigl(f,B^i(X_m)\bigr)\qquad(f\in C^i(X_m;\mathbb F_2),\ 0\le i<d),$$

with constants independent of $m$, $i$ and $f$. The Lean goal is published on the platform with status Open.

Significance

The result itself. Together with the classical graph case and the Chapman–Lubotzky two-dimensional theorem, Theorem 1.1 gives bounded-degree $\mathbb F_2$ coboundary expanders in every positive dimension, answering the existence question in the form stated by Chapman and Lubotzky. Earlier bounded-vertex-degree constructions gave cosystolic expansion, which permits nonvanishing cohomology, or degree-one expansion only; earlier coboundary expanders in all dimensions had vertex degrees growing with size. Coboundary expansion in all degrees implies vanishing $\mathbb F_2$-cohomology below the top dimension, the property Gromov related to topological overlap.

Formalizing it. The definitions are elementary finite combinatorics, so the statement is completely precise; the proof combines group-theoretic coset complexes over $\mathrm{SL}_N(k[t])$, congruence quotients and a quantitative cosystolic input. A formal proof would require formalizing that input (Oppenheim–Valentiner-Branth), which is substantial.

Difficulty

Coboundary expansion requires two things at once: a quantitative isoperimetric inequality against cocycles (cosystolic expansion) and exact vanishing of $H^i(X_m;\mathbb F_2)$ for every $i<d$. Random constructions give vanishing cohomology but force growing vertex degree; algebraic bounded-degree constructions (Ramanujan complexes, coset complexes) give the quantitative inequality but typically have nonzero cohomology that cannot be controlled uniformly. A cocycle that is not a coboundary has zero coboundary and positive distance, so any nonzero cohomology class destroys the inequality. The difficulty is a family of bounded-degree complexes whose cohomology vanishes in every degree below $d$, uniformly along the tower.

Formalization scope

• Vertices are Fin vertexCount and every vertex is a face; faces are Finsets, and an $i$-face has exactly $i+1$ vertices.
• Purity requires at least one $d$-face; connectivity is of the $1$-skeleton and requires a nonempty vertex set, so empty or disconnected complexes do not satisfy the hypotheses.
• Cochains are ZMod 2-valued; $B^0$ is the constant cochains (reduced cohomology in degree $0$). Distance is a real sInf over the image of a nonempty finite set, hence a minimum.
• The inequality is required for every $i<d$ and every cochain, with $D$ and $\varepsilon$ chosen before the sequence and depending only on $d$. Only $d\ge3$ is asserted; dimensions $1$ and $2$ are separate known results.
• Needed infrastructure: coset complexes, local spectral expansion and cosystolic expansion theorems, and cohomology of congruence quotients. A library of simplicial cochain complexes over $\mathbb F_2$ would be reusable for many high-dimensional-expansion problems.

Selected references

• N. Linial and R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006). https://doi.org/10.1007/s00493-006-0027-9
• R. Meshulam and N. Wallach, Homological connectivity of random k-dimensional complexes, Random Structures Algorithms 34 (2009). https://doi.org/10.1002/rsa.20238
• M. Gromov, Singularities, expanders and topology of maps. Part 2, Geom. Funct. Anal. 20 (2010), 416–526. https://doi.org/10.1007/s00039-010-0073-8
• A. Lubotzky and R. Meshulam, Random Latin squares and 2-dimensional expanders, Adv. Math. 272 (2015). https://doi.org/10.1016/j.aim.2014.12.015
• T. Kaufman, D. Kazhdan and A. Lubotzky, Isoperimetric inequalities for Ramanujan complexes and topological expanders, Geom. Funct. Anal. 26 (2016). https://doi.org/10.1007/s00039-016-0362-y
• A. Lubotzky, Z. Luria and R. Rosenthal, Random Steiner systems and bounded degree coboundary expanders of every dimension, Discrete Comput. Geom. 62 (2019). https://doi.org/10.1007/s00454-018-9991-2
• S. Evra and T. Kaufman, Bounded degree cosystolic expanders of every dimension, J. Amer. Math. Soc. 37 (2024). https://doi.org/10.1090/jams/1019
• M. Chapman and A. Lubotzky, Stability of homomorphisms, coverings and cocycles II: Examples, applications and open problems, Adv. Math. 463 (2025). https://doi.org/10.1016/j.aim.2025.110117
• T. Kaufman, I. Oppenheim and S. Weinberger, Coboundary expansion of coset complexes, arXiv:2411.02819 (STOC 2025). https://arxiv.org/abs/2411.02819v1
• I. Oppenheim and I. Valentiner-Branth, New cosystolic high-dimensional expanders from KMS groups, arXiv:2504.05823. https://arxiv.org/abs/2504.05823v2
• OpenAI, Bounded-degree coboundary expanders in every dimension, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Bounded-degree-coboundary-expanders-in-every-dimension-September-24-2026/paper.pdf

Motivation

In binary classification the VC dimension decides PAC learnability: a class of $\{0,1\}$-valued functions is learnable from finitely many examples exactly when its VC dimension is finite. Multiclass classification, where a predictor outputs one of many labels, arises whenever the label set is large: language models choosing a next token, image recognition over open vocabularies, structured prediction. For finitely many labels the Natarajan dimension plays the role of the VC dimension (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler and Long 1995). Whether it still characterizes learnability when the label set is infinite stayed open for three decades.

Brukhim, Carmon, Dinur, Moran and Yehudayoff (arXiv:2203.01550, FOCS 2022) settled both directions. Their Theorem A shows that the DS dimension of Daniely and Shalev-Shwartz (COLT 2014, PMLR 35) characterizes multiclass PAC learnability for every label set. Their Theorem 2, the goal of this mission, shows that the Natarajan dimension does not: there is a class whose Natarajan dimension is $1$ and whose DS dimension is infinite.

Timeline:

• 1989: Natarajan introduces his dimension and proves it gives sample-complexity bounds when the label set is finite.
• 1995: Ben-David, Cesa-Bianchi, Haussler and Long show that, for finite label sets, every "reasonable" extension of the VC dimension characterizes learnability.
• 2003: Januszkiewicz and Świątkowski construct, for every dimension, finite simplicial complexes without empty squares from coset complexes of finite groups (Comment. Math. Helv. 78(3), 555–583); the multiclass paper uses this construction for its separation.
• 2014: Daniely and Shalev-Shwartz introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
• 2022: Brukhim et al. prove that finite DS dimension is sufficient and that the Natarajan dimension fails to characterize learnability for infinite label sets.

Setting

A concept class is a set $\mathcal H \subseteq \mathcal Y^{\mathcal X}$ of functions from a domain $\mathcal X$ to a label set $\mathcal Y$, with no finiteness assumption on either. For a sequence $S = (x_1, \dots, x_n) \in \mathcal X^n$, the projection $\mathcal H|_S \subseteq \mathcal Y^n$ is the set of words $(h(x_1), \dots, h(x_n))$, $h \in \mathcal H$.

• $S$ is N-shattered if there are $f, g : [n] \to \mathcal Y$ with $f(i) \ne g(i)$ for every $i$ and $\mathcal H|_S \supseteq \{f(1), g(1)\} \times \dots \times \{f(n), g(n)\}$: the projection contains a copy of the Boolean cube. The Natarajan dimension $d_N(\mathcal H)$ is the largest $n$ for which some $S \in \mathcal X^n$ is N-shattered, or $\infty$.
• A pseudo-cube of dimension $d$ is a non-empty, finite $B \subseteq \mathcal Y^d$ in which every word $h$ has, for every coordinate $i$, an $i$-neighbour: a word $g \in B$ with $g(i) \ne h(i)$ and $g(j) = h(j)$ for $j \ne i$. $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$-dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the largest such $n$, or $\infty$.

Every Boolean cube is a pseudo-cube, so $d_N \le d_{DS}$. The hexagon $\{12, 32, 34, 54, 56, 16\} \subseteq \{1,\dots,6\}^2$ is a 2-dimensional pseudo-cube that contains no Boolean square.

The milestones pass through simplicial complexes: downward-closed families of finite sets. A complex is good if it is finite, pure, has a proper coloring $r$ of its vertices with $\dim(C)+1$ colors, and satisfies replacement (every vertex of every face can be exchanged for a new vertex). A good complex $C$ with coloring $r$ defines the class $B(C, r)$ of its top faces, each written as the word listing its vertices by color. A square is a 4-cycle of distinct vertices in the 1-skeleton; it is empty if neither diagonal is an edge. The coset complex $C_F(H_1, \dots, H_d)$ of subgroups of a group $F$ has the cosets $gH_i$ as vertices and the sets of cosets with a common point as faces.

Formalization targets

Goal: Theorem 2 (p. 4)

$$\exists\, \mathcal X, \mathcal Y,\ \mathcal H \subseteq \mathcal Y^{\mathcal X}:\qquad d_N(\mathcal H) = 1 \quad\text{and}\quad d_{DS}(\mathcal H) = \infty.$$

Milestones

1. Theorem 45 (p. 30; Januszkiewicz–Świątkowski): for every $d > 1$ a finite group $F$ and subgroups $H_1, \dots, H_d$ with $(\bigcap_{j\ne i} H_j) \setminus H_i \ne \emptyset$ for all $i$, whose coset complex has no empty squares.
2. Proposition 46 (p. 31): such a coset complex has dimension $d - 1$, is good and has no empty squares.
3. Proposition 42 (p. 28): a $d$-dimensional good complex with a proper coloring $r$ yields the $(d+1)$-dimensional pseudo-cube $B(C, r)$; conversely every pseudo-cube yields a good complex $C(B)$.
4. Proposition 43 (p. 29): $d_N(B(C,r)) \ge 2$ iff $C$ has a square $v_0 v_1 v_2 v_3$ with $r(v_0) = r(v_2)$ and $r(v_1) = r(v_3)$.
5. Corollary 44 (p. 29): a good complex without empty squares gives $d_N(B(C, r)) \le 1$ for every proper coloring.
6. Proof of Theorem 2 (p. 32): for every $d \ge 1$, a $d$-dimensional pseudo-cube with Natarajan dimension exactly $1$.

Significance

Theorem 2 shows that the classical generalization of the VC dimension to many labels is the wrong invariant once the label set is infinite: a class can contain no Boolean square at all and still be unlearnable, because it contains pseudo-cubes of every dimension. Combined with the necessity of finite DS dimension, it gives a class that is not PAC learnable although its Natarajan dimension is $1$, and it identifies pseudo-cubes, not Boolean cubes, as the relevant combinatorial obstruction. It also links learning theory to a problem studied in geometric group theory, finite "flag-no-square" complexes.

The paper's proof is complete modulo Theorem 45, which it imports from Januszkiewicz–Świątkowski 2003. None of these results is formalized. A formalization would give machine-checked versions of the dictionary between concept classes and properly colored complexes (Propositions 42–44), of the coset-complex translation (Proposition 46), and of the final disjoint-union argument; Theorem 45 itself, which rests on Coxeter-group and topological arguments, is a separate and substantial formalization target.

Difficulty

Infinite complexes that are pure, properly colored, satisfy replacement and have no empty squares are easy to build: grow a tree of faces indefinitely. The definition of a pseudo-cube demands finiteness, and the difficulty is entirely there: one must "fold" such an infinite object into a finite one without creating an empty square. The obvious finite candidate, the group $(\mathbb Z/2)^d$ with its coordinate subgroups, produces the Boolean cube, whose complex is full of empty squares. Theorem 45 is the input that resolves this, and it is far beyond the rest of the argument.

Formalization scope

All declarations live in the namespace MulticlassDS.NatGap.

• Concept classes are Set (X → Y) with arbitrary types; $[n]$ is Fin n (0-based), and shattering is defined for sequences Fin n → X, as in the paper.
• Both dimensions are ℕ∞-valued suprema, so "infinite DS dimension" is dsDim H = ⊤. An ℕ-valued supremum would silently return $0$ on an unbounded family and would trivialize the goal.
• The goal requires the Natarajan dimension to be exactly $1$; an upper bound alone holds for any class with at most one element.
• Pseudo-cubes are required to be finite (Definition 5). Without finiteness, the tree classes of Example 8 would already have infinite "DS dimension".
• Complexes are Set (Finset V). The dimension is the predicate HasDim C d, not a natural-number subtraction, and colors are Fin (d + 1).
• Replacement is stated with a new vertex $u \notin f$. The page writes "$u \ne v$", but read literally that allows $u \in f$, which makes the condition hold by downward closure and makes Proposition 42 false; the proofs of Propositions 42 and 46 use a new vertex.
• Coset-complex vertices are left cosets as subsets of the group, not pairs (index, coset).
• Proposition 46 states dimension $d - 1$ under $d > 1$, where the subtraction is exact; the converse of Proposition 42 is indexed by $d + 1$ and $d$ to avoid it.
• The proof-of-Theorem-2 milestone says "for every $d$"; it is posed for $d \ge 1$, because at $d = 0$ the only pseudo-cube has Natarajan dimension $0$.

Welcome contributions: proofs of Propositions 42–44 and 46 and of the goal from the milestones, which need only finite combinatorics and elementary group theory; and, separately, a formalization of the Januszkiewicz–Świątkowski construction behind Theorem 45. The definitions of pseudo-cubes, the DS dimension and good complexes are reusable by the companion mission on sample compression and by any later work on multiclass learnability.

Selected references

• N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, arXiv:2203.01550v1, 2022 (FOCS 2022). https://arxiv.org/abs/2203.01550
• T. Januszkiewicz, J. Świątkowski, Hyperbolic Coxeter groups of large dimension, Comment. Math. Helv. 78(3) (2003), 555–583 (reference [Januszkiewicz and Świątkowski 2003] of arXiv:2203.01550v1, p. 33).
• A. Daniely, S. Shalev-Shwartz, Optimal learners for multiclass problems, COLT 2014, PMLR 35, 287–316. https://proceedings.mlr.press/v35/
• B. K. Natarajan, On learning sets and functions, Machine Learning 4 (1989), 67–97. https://doi.org/10.1007/BF00114804
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0,…,n}-valued functions, J. Comput. Syst. Sci. 50(1) (1995), 74–86. https://doi.org/10.1006/jcss.1995.1008