Group Theory

Why bi-Cayley graphs over abelian groups matter

A Cayley graph turns multiplication in a group into adjacency between vertices. Every Cayley graph is vertex transitive: multiplying every vertex by the same group element moves any chosen vertex to any other. A bi-Cayley graph starts with two copies of a group and permits edges both within and between the copies. Its built-in group action is transitive on each copy, but it need not exchange them. This makes bi-Cayley graphs a setting for distinguishing edge, vertex, and arc transitivity. Conder, Zhou, Feng and Zhang study these distinctions and their consequences for graph constructions in Edge-transitive bi-Cayley graphs.

For abelian groups, the paper proves a strong restriction: once a connected bi-Cayley graph is edge transitive, it is also vertex transitive. Its half-arc-transitive examples face additional local restrictions, including a minimum valency of six. The paper exhibits a graph of valency six in Example 4.3, so the numerical bound is attained in its class. The result separates these graphs from semisymmetric graphs, which are edge transitive but not vertex transitive. The claims and example appear in Proposition 1.3 and §4.

Graphs, actions, and terminology

Let $H$ be a finite group and let $R,L,S$ be subsets of $H$. Require $R=R^{-1}$, $L=L^{-1}$, $1\notin R\cup L$, and $|R|=|L|$. The graph $\Gamma=\operatorname{BiCay}(H,R,L,S)$ has vertices $H_0\cup H_1$, two labelled copies of $H$. For $h\in H$, an element $x\in R$ gives an edge from $h_0$ to $(xh)_0$; an element $y\in L$ gives an edge from $h_1$ to $(yh)_1$; and an element $z\in S$ gives an edge from $h_0$ to $(zh)_1$. The inverse closure of $R$ and $L$ makes the within-copy edges undirected. Excluding $1$ from those two sets excludes loops. This is the construction on p. 1.

Every $g\in H$ acts by right multiplication $R(g):h_i\mapsto(hg)_i$. The subgroup $R(H)$ of graph automorphisms has two vertex orbits, $H_0$ and $H_1$. Its normaliser in $\operatorname{Aut}(\Gamma)$ is useful for describing further symmetries. For a group automorphism $\alpha$ and group elements $g,x,y$, the paper defines permutations $\sigma_{\alpha,g}$, which preserve the two copies, and $\delta_{\alpha,x,y}$, which exchange them. Their precise edge-preservation conditions are the sets $F$ and $I$ of equation (2.2). The mission includes those definitions and the relevant part of the normaliser characterization, Proposition 2.2.

A graph is vertex transitive if its full automorphism group can move any vertex to any other, and edge transitive if it can move any undirected edge to any other. Arc transitivity asks the same for ordered adjacent pairs. A graph is half-arc-transitive when it is vertex and edge transitive but not arc transitive. A semisymmetric graph has constant valency, is edge transitive, and is not vertex transitive. These are the paper's definitions on p. 4. Valency means the actual number of neighbours of a vertex.

Formalization targets

The central target is the corrected reading of Proposition 1.3: for connected $\Gamma$ over an abelian $H$,

$$\Gamma\text{ edge transitive}\implies\Gamma\text{ vertex transitive},$$

and, if $\Gamma$ is half-arc-transitive,

$$R\cup L\ne\varnothing,\quad (\forall x\in R\cup L)\ \operatorname{ord}(x)\ne2, \quad |R|=|L|\text{ is even},\quad |S|>2,\quad \deg_{\Gamma}(v)\ge6\quad(v\in V(\Gamma)).$$

The attack path records the normaliser characterization in Proposition 2.2, both parts of Proposition 4.1, its explicit bipartition step, and Proposition 4.2. The companion Corollary 4.4 expresses the absence of connected semisymmetric examples over abelian groups.

What the result establishes

The vertex-transitivity conclusion collapses one apparent possibility in the symmetry classification: an edge-transitive bi-Cayley graph over an abelian group cannot be semisymmetric. For half-arc-transitive graphs, the theorem rules out involutions in the within-copy connection sets, forces even set sizes, and excludes valencies below six. Example 4.3 supplies an attained bound, with $H=C_{28}$ and valency six. These are concrete restrictions on any later classification or construction in this family; they follow from §4.

The mathematical results are proved in the cited paper. The mission asks for machine-checked Lean proofs of their statements and for a reusable finite bi-Cayley graph interface. The setting includes the right regular action, its normaliser, the two families of candidate automorphisms, and the transitivity predicates. The proof obligations are open in this local proposal; a successful development would make the abelian argument and its underlying graph-action lemmas available for later formalizations of bi-Cayley graphs.

The main obstacle

The right multiplication action gives only two known vertex orbits, one for each copy of $H$. Edge transitivity alone does not name an automorphism that swaps them. Inversion is an automorphism of an abelian group, but its induced copy-swapping permutation preserves graph edges directly only in the relevant bipartite case $R=L=\varnothing$. The paper must account for edge-transitive graphs whose connection sets initially allow edges inside the copies. For the valency bound, the absence of arc transitivity restricts how a vertex stabiliser can permute its neighbours; degree counting without those orbit constraints cannot yield $|S|>2$. These are the points at which a proof must use the full automorphism action rather than just the visible right regular subgroup.

Formalization scope

Lean uses the vertex type $H\sqcup H$, with Sum.inl h for $h_0$ and Sum.inr h for $h_1$. The group and graph are finite; the graph is simple and undirected by construction, and every theorem assumes it is connected. The finite sets $R,L,S$ retain the conditions $R=R^{-1}$, $L=L^{-1}$, $1\notin R\cup L$, and $|R|=|L|$. The graph's degree, rather than a separately defined cardinality formula, represents valency. “Involution” means an element of order exactly two. All graph-level transitivity predicates quantify over the full automorphism group; the normaliser appears only in the separate Proposition 2.2 milestone. The paper's exponent notation for group automorphisms is rendered as function application, while $R(g)$ remains right multiplication.

The printed first sentence of Proposition 1.3 says every connected bi-Cayley graph over an abelian group is vertex transitive. That sentence is false: the connected generalized Petersen graph $GP(7,2)$ is a bi-Cayley graph over $C_7$ and is not vertex transitive. Proposition 4.1(b), which the paper uses to establish Proposition 1.3, includes the missing edge-transitivity condition. The Lean goal states that corrected condition explicitly. It does not add an assumption to the half-arc-transitive clause, since half-arc-transitivity already entails edge transitivity. Proposition 4.2 prints two clauses labelled “(a)”; they are treated as distinct clauses while its quotation retains the printed labels.

The definition of the graph keeps $R$ and $L$ inverse closed as data; no graph constructor silently symmetrises arbitrary sets. Transitivity is taken over actual edges or arcs, and the degree bound is checked at every vertex. Contributions to the graph-action lemmas, the normaliser result, Proposition 4.1, and the vertex-stabiliser analysis behind Proposition 4.2 are all within scope. The Cayley-graph isomorphism in Proposition 2.2(b) is outside this mission's stated milestone because it is not used by the target.

Selected references

• M. Conder, J.-X. Zhou, Y.-Q. Feng, and M.-M. Zhang, Edge-transitive bi-Cayley graphs, Journal of Combinatorial Theory, Series B, 2020; arXiv:1606.04625v1; DOI:10.1016/j.jctb.2020.05.006.

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. NIZK proofs are a basic building block of public-key cryptography: chosen-ciphertext secure encryption, signature schemes and secure multi-party computation all use them. Groth, Ostrovsky and Sahai, New Techniques for Noninteractive Zero-Knowledge (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006), built the first NIZK proofs for all of NP that are perfectly sound and the first NIZK arguments that are perfectly zero-knowledge, using bilinear groups.

The construction rests on a single primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys (perfectly binding and perfectly hiding) together with a short non-interactive proof that a commitment contains $0$ or $1$. Section 4 of the paper instantiates this primitive in a bilinear group of composite order $n = pq$, building on the encryption scheme of Boneh, Goh and Nissim (TCC 2005); Section 5 gives a second instantiation in prime-order groups. Theorem 2 states that the composite-order scheme of Figure 1 has all the required properties. This mission formalizes the part of Theorem 2 that is an exact mathematical statement.

Timeline: Boneh, Goh and Nissim (2005) introduced the subgroup decision assumption and the encryption $g^m h^r$ in groups of order $pq$. Groth, Ostrovsky and Sahai (Eurocrypt 2006) used it for perfect NIZK; the simple 0/1 proof $\pi = (g^{2m-1}h^r)^r$ used in Figure 1 is due to an observation of Boyen and Waters (Eurocrypt 2006), as the paper's footnote 7 records. The journal version (2012) presents both instantiations through the abstract notion of a homomorphic proof commitment.

Setting

A BGN bilinear group is a tuple $(p, q, \mathbb G, \mathbb G_T, e, g)$ where $p < q$ are primes, $\mathbb G$ and $\mathbb G_T$ are finite commutative groups of order $n = pq$, $e : \mathbb G \times \mathbb G \to \mathbb G_T$ is bilinear ($e(u^a, v^b) = e(u, v)^{ab}$ for all $u, v \in \mathbb G$, $a, b \in \mathbb Z$), $g$ generates $\mathbb G$, and $e(g, g)$ generates $\mathbb G_T$.

The commitment key is $ck = (n, \mathbb G, \mathbb G_T, e, g, h)$ for an element $h \in \mathbb G$ of one of two kinds:

• a perfectly binding key has $h = g^{px}$ with $x$ a unit modulo $q$, so $h$ has order $q$; the extraction key is $q$;
• a perfectly hiding key has $h = g^x$ with $x$ a unit modulo $n$, so $h$ generates $\mathbb G$; the trapdoor is $x$.

The commitment to a message $m$ with randomizer $r \in \mathbb Z_n$ is $\mathrm{com}(m; r) = g^m h^r$. The trapdoor opening is $\mathrm{Topen}_x(m, r, m') = r - (m'-m)/x \bmod n$. The 0/1 proof for a commitment $c = g^m h^r$ is $\pi = P_{01}(m, r) = (g^{2m-1} h^r)^r$, and the verifier $V_{01}$ accepts $(c, \pi)$ when $e(c, cg^{-1}) = e(h, \pi)$. The extractor $\mathrm{Ext}$ computes $c^q$ and searches for $m$ with $c^q = (g^q)^m$.

Formalization targets

Goal: the exact part of Theorem 2

For every BGN bilinear group, the scheme above satisfies:

$$\begin{aligned} &\text{(homomorphic, either key)} && \mathrm{com}(m_1+m_2; r_1+r_2) = \mathrm{com}(m_1; r_1)\,\mathrm{com}(m_2; r_2),\\ &\text{(perfect binding)} && \mathrm{com}(m_1; r_1) = \mathrm{com}(m_2; r_2) \Rightarrow m_1 \equiv m_2 \pmod p,\\ &\text{(trapdoor opening)} && \mathrm{com}(m_2; \mathrm{Topen}_x(m_1, r_1, m_2)) = \mathrm{com}(m_1; r_1),\\ &\text{(opening indistinguishability)} && r_1 \text{ uniform} \Rightarrow \mathrm{Topen}_x(m_1, r_1, m_2) \text{ uniform},\\ &\text{(completeness, either key)} && m \in \{0,1\} \Rightarrow V_{01}(\mathrm{com}(m; r), P_{01}(m, r)),\\ &\text{(soundness)} && V_{01}(c, \pi) \Rightarrow \exists\, m \in \{0,1\}, r : c = \mathrm{com}(m; r),\\ &\text{(witness indistinguishability)} && \mathrm{com}(m; r_0) = \mathrm{com}(1-m; r_1) \Rightarrow P_{01}(m, r_0) = P_{01}(1-m, r_1),\\ &\text{(extractability)} && m \in \{0,1\} \Rightarrow \mathrm{Ext}(\mathrm{com}(m; r)) = m, \end{aligned}$$

with binding, soundness and extractability on binding keys, and trapdoor opening and witness indistinguishability on hiding keys.

Milestones

The milestones follow the proof of Theorem 2 (p. 9) and Figure 1 (p. 10): the homomorphic property; perfect binding; the extraction identity $c^q = (g^q)^m$; the trapdoor identity $g^m h^r = g^{m'} h^{r-(m'-m)/x}$ and the uniqueness of openings on a hiding key; the completeness display $e(c, cg^{-1}) = e(g,g)^{m(m-1)} e(h^r, g^{2m-1}h^r) = e(h, \pi)$; the decomposition of every element as $g^m h^r$ on a binding key; the step "$e(g,g)^{m(m-1)}$ of order $1$ or $q$ implies $m \equiv 0$ or $1 \pmod p$"; perfect soundness; and the uniqueness of the proof on a hiding key, which gives witness indistinguishability.

Significance

Theorem 2 is one of the two instantiations on which every exact result of the paper rests. Plugged into the Circuit-SAT construction of Section 6, the binding-key properties give a perfectly sound NIZK proof and a perfect proof of knowledge for every NP relation, and the hiding-key properties give a perfect zero-knowledge NIZK argument. The same composite-order techniques underlie later pairing-based proof systems, notably the Groth–Sahai proofs.

The paper's proof is about one page of group computations and has, as far as the planning of this series found, no machine-checked counterpart. The mission produces a reusable model of composite-order bilinear groups and of the BGN commitment, and checks details the paper leaves implicit: the message space $\mathbb Z_p$ versus exponents taken modulo $n$, the role of the non-degeneracy of $e$, and the order arguments behind soundness.

Difficulty

Each property is elementary on its own, but soundness is not a plain computation: the verifier only sees $c$ and $\pi$, and the conclusion asks for an opening of $c$ with message in $\{0, 1\}$ from a single pairing equation. An argument that only manipulates the equation symbolically cannot reach it; the statement depends on the orders of elements in $\mathbb G_T$, on $e(g,g)$ generating $\mathbb G_T$ (with a degenerate pairing soundness is false), and on $p$ and $q$ being distinct primes. A second subtlety is that a message is only determined modulo $p$ by a commitment under a binding key, while the conclusion asks for a message that is exactly $0$ or $1$ in $\mathbb Z_n$.

Formalization scope

• $\mathbb G$, $\mathbb G_T$ are finite commutative groups with Fintype.card = p * q; $e$ is a homomorphism G →* G →* GT, which is exactly bilinearity; $g$ generates $\mathbb G$ and $e(g,g)$ generates $\mathbb G_T$ (both as hypotheses of the structure BGNSetup).
• Messages and randomizers are elements of ZMod n; $g^a$ is $g$ to the representative of $a$ in $\{0, \dots, n-1\}$. The paper's message space is $\mathbb Z_p$, but $g^m$ is not well defined for $m \in \mathbb Z_p$ in a group of order $pq$; binding and extraction therefore compare messages modulo $p$.
• Keys are described by the support of the key generators; each "probability $1$ for every adversary" property is stated for every key in that support and every adversary choice. Trapdoor opening indistinguishability is an equality of probability mass functions. The prover is deterministic, so witness indistinguishability is equality of proofs, and non-erasure witness indistinguishability holds with the empty proof randomness.
• Not formalized: the subgroup decision assumption (Definition 1), key indistinguishability, the clause "if the subgroup decision assumption holds", the randomized generator $\mathcal G_{\mathrm{BGN}}$ and its efficiency, and the elliptic-curve example on p. 9.
• A trivializing formalization is ruled out: soundness is stated only for binding keys $h = g^{px}$ with $x$ a unit modulo $q$, with the non-degeneracy of $e$ as a hypothesis, and the extractor is an exhaustive search over $\mathbb Z_p$, not a test that presupposes $m \in \{0,1\}$.
• The model of composite-order bilinear groups is reusable for other BGN-based results. Proofs of any milestone are welcome; the trapdoor and homomorphism identities are good first targets.

Selected references

• J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
• D. Boneh, E.-J. Goh, K. Nissim, Evaluating 2-DNF Formulas on Ciphertexts, TCC 2005, LNCS 3378, pp. 325–341. https://doi.org/10.1007/978-3-540-30576-7_18
• X. Boyen, B. Waters, Compact Group Signatures Without Random Oracles, Eurocrypt 2006, LNCS 4004, pp. 427–444. https://doi.org/10.1007/11761679_26
• T. P. Pedersen, Non-Interactive and Information-Theoretic Secure Verifiable Secret Sharing, Crypto 1991, LNCS 576, pp. 129–140. https://doi.org/10.1007/3-540-46766-1_9
• J. Groth, A. Sahai, Efficient Non-interactive Proof Systems for Bilinear Groups, Eurocrypt 2008, LNCS 4965, pp. 415–432. https://doi.org/10.1007/978-3-540-78967-3_24

Motivation

Norm ultrapowers permit approximations along a free ultrafilter. An explicit algebra excluded from every nuclear target ultrapower tests the limits of this embedding mechanism. The pinned manuscript supplies the research context.

Setting

The group is the stated dyadic semidirect product. Its full group C*-algebra is specified by a universal property, and the ultrapower is bounded sequences modulo norm-null sequences along the ultrafilter.

Formalization target

The selected goal is OAI.NuclearUltrapower.main_no_embedding. Its central assertion is

$$A\not\hookrightarrow B^\omega\quad\text{for every nonzero unital nuclear }B.$$

The theorem states that, working in universe level 0, there exist a nonzero unital complex C*-algebra A and a group homomorphism ι from G into the unitary group of A such that the following hold. Here G is the semidirect product of the additive group of 3-vectors over the dyadic rationals Z[1/2] by SL₃(ℤ) × ℤ, where a matrix acts linearly on the vectors and the integer n acts by multiplication by 2ⁿ. First, (A, ι) is the full group C*-algebra of G: the span of ι(G) is dense in A, and every homomorphism of G into the unitaries of a nonzero unital C*-algebra D extends uniquely to a unital -homomorphism A → D. Second, A is separable as a topological space. Third, for every nonzero unital C-algebra B that is nuclear in the tensor-norm sense (minimal and maximal C*-tensor norms agree on B ⊗ C for every C*-algebra C) and every free ultrafilter ω on ℕ (one containing no finite set), there is no injective unital -homomorphism from A into the norm ultrapower of B, namely bounded B-valued sequences modulo those tending to 0 along ω. Fourth, there exist a nonzero unital C-algebra O and two elements s₀, s₁ of O satisfying the Cuntz relations (each sᵢsᵢ = 1 and s₀s₀ + s₁s₁* = 1), with O universal for these relations, such that for every free ultrafilter ω there is likewise no injective unital *-homomorphism from A into the norm ultrapower of O. The theorem is admitted in the source, not proved.

Significance and status

The goal includes separability, the full group universal property, nonembedding and the Cuntz-algebra corollary in the stated base universe. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

A single source algebra must obstruct all nuclear targets and free ultrafilters. Universal full-group and Cuntz-algebra constructions are part of the target.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, An explicit obstruction to nuclear norm-ultrapower embeddings, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A linear filling inequality captures a form of large-scale negative curvature. The source asks whether a finite aspherical complex with that property must admit a geometric model of local nonpositive curvature. The source is OpenAI's September 2026 manuscript.

Setting

A finite complex has its usual barycentric realization. Asphericity means higher homotopy groups vanish. A linear disk-filling inequality bounds triangular face moves needed to fill an edge loop by a constant times its length.

Formalization targets

$$\exists K:\quad K\text{ finite, connected, aspherical, with linear disk filling},\quad\pi_1K\text{ hyperbolic with no geometric CAT(0) action}.$$

The defined proposition MainStatement holds, namely that there exist a finite abstract simplicial complex K on vertices Fin n, with its standard barycentric realization |K| (nonnegative coordinate vectors summing to 1 supported on a face), a basepoint x in |K|, and a real constant C ≥ 0 such that all of the following hold. |K| is connected and aspherical at x, meaning every homotopy group π_{m}(|K|,x) with m ≥ 2 is trivial. K satisfies a linear disk-filling inequality: every closed edge path p that bounds some disk, where a disk is a chain of elementary moves (collapsing a repeated vertex, removing a spur a,b,a, or replacing a,b,c by a,c across a nondegenerate triangular face, which costs one) reducing p to a single vertex, admits such a disk using at most C times (length of p minus 1) triangular faces. The fundamental group G = π₁(|K|,x) is word hyperbolic in the four-point sense: for some finite generating set S and some δ ≥ 0, every a,b,c,d in G satisfy d(a,c)+d(b,d) ≤ max(d(a,b)+d(c,d), d(a,d)+d(b,c)) + 2δ, where d is word distance. G admits no geometric CAT(0) action: there is no proper cocompact isometric action of G on any nonempty proper complete metric space X (in universe u) that is CAT(0), in the sense that segments exist with the squared-distance comparison inequality. Finally, for every finite complex L whose realization is homotopy equivalent to |K|, there is no metric on |L|, inducing its given topology, that is geodesic and locally CAT(−1), meaning each point has a ball that satisfies the hyperbolic-cosine midpoint inequality cosh d(z,m) ≤ (cosh d(z,x)+cosh d(z,y))/(2cosh(d(x,y)/2)) for segment midpoints m.

The goal is OAI.HyperbolicObstruction.main.

Significance

The goal also excludes a finite homotopy-equivalent complex with a compatible geodesic locally CAT(-1) metric. It joins a finite topological model, a group-theoretic obstruction, and a metric-model consequence. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

A large-scale hyperbolicity inequality does not directly construct a local curvature metric. Excluding all geometric actions requires more than finding a defect in the original complex’s chosen metric.

Formalization scope

Word hyperbolicity uses the four-point word-distance condition. Excluded CAT(0) actions are on nonempty proper complete spaces. The final metric must induce the finite realization’s existing topology; changing that topology is not permitted.

The shared definitions are supplied by HyperbolicObstruction. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A hyperbolic group with no geometric CAT(0) action, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.

Setting

A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.

Formalization targets

$$gA_Xg^{-1}\cap hA_Yh^{-1}=kA_Zk^{-1}\quad\text{for some }Z\subseteq S,\ k\in A_M.$$

The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.

The goal is OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• unconditional arbitrary intersections.
• unconditional nonclique dynamics.
• unconditional parabolic closure.

Significance

The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Conjugation obscures the standard generating subsets, so intersecting $X$ and $Y$ alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.

Formalization scope

The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.

The shared definitions are supplied by ArtinParabolicIntersections. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Parabolic intersections in Artin groups, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.

Setting

An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.

Formalization targets

$$\operatorname{ContractibleSpace}(\operatorname{SalvettiCover}(M))\qquad\text{for every Coxeter matrix }M\text{ on finite }S.$$

For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.

The goal is OAI.HarmonicArtin.salvetti_cover_contractible.

Significance

The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.

Formalization scope

SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.

The shared definitions are supplied by HarmonicArtin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Harmonic heights and the Artin K(pi,1) conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Simplicity constrains normal subgroups, amenability provides almost invariant finite sets, and finite presentation gives a finite description by generators and relations. The source seeks an infinite group satisfying all three conditions together. The source is OpenAI's September 2026 manuscript.

Setting

A simple group is nontrivial and has no proper nontrivial normal subgroup. Følner amenability means that every finite collection of translations changes a suitable nonempty finite set by a small relative symmetric difference.

Formalization targets

$$\exists G:\quad |G|=\infty,\quad G\text{ finitely presented and simple},\quad\forall K,\varepsilon>0\ \exists D:\ |gD\triangle D|<\varepsilon|D|\ (g\in K).$$

There exists a group G, with underlying type in the lowest universe, that is infinite, finitely presented, simple, and Følner-amenable. Here FolnerAmenable(G) is the defined proposition that for every finite subset K of G and every real ε>0 there is a nonempty finite subset D of G such that, for every g in K, the symmetric difference between the left translate gD={g·d : d∈D} and D has cardinality strictly less than ε times the cardinality of D. Simple means G is nontrivial and has no normal subgroups other than the trivial one and G itself, and finitely presented means G has a presentation with finitely many generators and finitely many relations.

The goal is OAI.SimpleAmenable.main.

Significance

The target supplies one group with simultaneous infinitude, simplicity, finite presentation, and the specified Følner property. Each condition is part of the conclusion. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Finite generation is weaker than finite presentation, and an amenability argument need not survive an arbitrary quotient or enlargement used to enforce simplicity. The construction must preserve all four properties.

Formalization scope

Finite sets are Finsets and translations act on the left. The Følner witness is nonempty and the inequality is strict for every member of the given finite set. No uniform bound on the number of generators or relators is imposed.

The shared definitions are supplied by SimpleAmenable. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, An infinite finitely presented simple amenable group, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Periodic groups have only finite-order elements, but this local condition does not visibly bound the group’s size. The source asks whether an ordinary finite presentation forces such a group to be finite. The source is OpenAI's September 2026 manuscript.

Setting

A periodic group satisfies: for each element there is some positive power equal to the identity. A Steinberg group is generated by elementary root symbols subject to additive, commuting, and multiplicative commutator relations over a coefficient ring.

Formalization targets

$$\exists R\text{ over }\mathbb F_2:\ \operatorname{St}_{12}(R)\text{ is infinite, finitely presented, and periodic}.$$

Two propositions hold together. For a natural number n and a ring R, a root is an ordered pair (i,j) of distinct indices in {0,…,n−1}, and the Steinberg group St(n,R) is the group generated by symbols x_{ij}(a), one for each root (i,j) and each a in R, subject to three families of relations: x_{ij}(a+b) = x_{ij}(a)x_{ij}(b); the commutator [x_{ij}(a), x_{kl}(b)] = x y x⁻¹ y⁻¹ is trivial whenever j≠k and i≠l; and for pairwise distinct i, j, k, the commutator [x_{ij}(a), x_{jk}(b)] equals x_{ik}(ab). A group is periodic if every element g has some positive integer m with gᵐ = 1. The first statement, MainStatement, asserts that there exist a ring R in the lowest universe, carrying an algebra structure over ZMod 2, such that St(12,R) is infinite, finitely presented, and periodic. The second statement, BurnsideStatement, asserts that there exists an infinite, finitely presented, periodic group G. The theorem asserts the conjunction of these two existence claims, with no bound on the orders of elements.

The goal is OAI.SourceBurnside.thm_main.

Significance

The formal goal includes both this ring-based construction and the general existence of an infinite finitely presented periodic group. It preserves the stronger concrete realization through a Steinberg group. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

A finite collection of torsion generators does not imply that every product has finite order. Conversely, infinitely many torsion relations do not supply an ordinary finite presentation. Both requirements must hold for the same infinite group.

Formalization scope

The orders of elements may vary; no common exponent is asserted. Finite presentation is Mathlib’s group property. The goal does not include the manuscript’s separate nil-algebra, radical-algebra, or unitization conclusions.

The shared definitions are supplied by PeriodicGroup. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, An infinite finitely presented periodic group, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation: recognizing a group from its large-scale geometry

Geometric group theory studies finitely generated groups through their word metrics, which are well defined up to quasi-isometry. A basic question is which algebraic properties are quasi-isometry invariants: if a group $H$ "looks like" a group $P$ from far away, must $H$ share $P$'s algebraic structure? Gromov's polynomial-growth theorem (1981) answers this for virtually nilpotent groups. The next natural class is the virtually polycyclic groups — groups with a finite-index subgroup admitting a finite subnormal series with cyclic factors — which are exactly, up to finite index, the lattices in connected simply connected solvable Lie groups. Eskin, Fisher and Whyte conjectured that this class is quasi-isometrically rigid, and the question had been settled only for special families such as $\mathrm{Sol}$ and certain abelian-by-abelian groups.

Background

• 1981 — Gromov: groups of polynomial growth are virtually nilpotent, which settles the virtually nilpotent case (Publ. IHÉS 1981).
• 2000 — Farb and Mosher pose horizontal-preservation and recognition problems for solvable groups (arXiv:math/0005184).
• 2004 — Shalom proves that a finitely generated group quasi-isometric to an infinite polycyclic group has a finite-index subgroup with infinite abelianization (Acta Math. 2004).
• 2007 — Eskin, Fisher and Whyte formulate the lattice-recognition conjecture and its polycyclic form (Conjecture 1.2) (PAMQ 2007).
• 2010–2013 — Dymarz treats certain diagonalizable models (GAFA 2010); Peng handles nondegenerate unimodular split abelian-by-abelian Lie groups (G&T 2011); Eskin–Fisher–Whyte prove recognition for $\mathrm{Sol}$ by coarse differentiation (Ann. of Math. 2013).
• 2025 — Dymarz, Fisher and Xie prove a Tukia-type theorem and rigidity for SOL-like groups (Adv. Math. 2025); Le Boudec proves recognition under commability (arXiv:2510.24581); Grayevsky and Pallier treat $\mathrm{Sol}_5$ (arXiv:2509.12823).
• 2026 — An OpenAI preprint, Quasi-isometric recognition of virtually polycyclic groups (OpenAI Math Release, September 24, 2026), claims recognition for the full class. The preprint has not been peer reviewed and its theorems are not formally verified.

Setting

For finitely generated groups $P,H$ with word metrics, a $(K,C)$-quasi-isometry $F:P\to H$ satisfies $K^{-1}d(x,x')-C\le d(Fx,Fx')\le Kd(x,x')+C$ and has $C$-dense image. For finitely generated groups this is equivalent to a coarse equivalence: maps $f:P\to H$, $g:H\to P$ sending pairs at bounded distance (differences in a fixed finite set) to pairs at bounded distance, with $g\circ f$ and $f\circ g$ at bounded distance from the identities. A uniform lattice in a locally compact group $S$ is a discrete subgroup $\Lambda$ with $S=\Lambda K$ for a compact $K$; a lattice is a discrete subgroup whose coset space carries an $S$-invariant probability measure.

For the height theorem: a connected simply connected Lie group $G$ is real-triangulable if the adjoint representation of its Lie algebra $\mathfrak g$ is simultaneously upper triangular in some real basis, with diagonal characters $\chi_1,\dots,\chi_s$. Put $\mathfrak k=\bigcap_j\ker\chi_j$ and $W=\mathfrak g/\mathfrak k$; the exponential height map $\pi:G\to(W,+)$ is the homomorphism whose differential is the quotient map. $G$ is unimodular if its left Haar measure is right invariant.

Formalization targets

Milestone: uniform bounded height (Theorem 1.4)

Let $G$ be connected, simply connected, real-triangulable and unimodular, with a proper left-invariant metric and a norm on $W$. There is a finite subgroup $\mathcal A_G\le\mathrm{GL}(W)$ such that for all $K\ge1$, $C\ge0$ there is $B$ with: every $(K,C)$ self quasi-isometry $F$ of $G$ has some $A_F\in\mathcal A_G$ with

$$\bigl\|\pi F(g)-\pi F(1)-A_F\,\pi(g)\bigr\|\le B\qquad(g\in G).$$

Milestone: lattice recognition (Corollary 1.2)

If a finitely generated group $H$ is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of $H$ is a uniform lattice in some (possibly different) connected simply connected solvable Lie group.

Goal: quasi-isometric recognition (Theorem 1.1)

Let $P$ be finitely generated and virtually polycyclic and $H$ finitely generated. If $H$ is quasi-isometric to $P$, then

$$H\ \text{is virtually polycyclic},\quad\text{and some finite-index } \Gamma\le H \text{ is isomorphic to a uniform lattice in a connected simply connected solvable Lie group.}$$

The second clause is the classical lattice realization of virtually polycyclic groups (Dekimpe's theorem, used in the source's proof of Corollary 1.2), recorded in the same formal statement. All three statements are published on the platform with status Open: no machine-checked proofs exist yet.

Significance

The result itself. Virtual polycyclicity becomes a quasi-isometry invariant among finitely generated groups, extending Gromov's theorem from nilpotent to solvable lattices and resolving the Eskin–Fisher–Whyte conjecture in its lattice form, where the ambient Lie group may change. The bounded-height theorem is a rigidity statement for quasi-isometries of an entire class of solvable Lie groups: up to bounded error and a finite group of linear symmetries, every quasi-isometry preserves height. This is the kind of control that previously required case-by-case coarse differentiation.

Formalizing it. The proof combines Lie theory, measured couplings, reduced cohomology, volume growth, Gromov's theorem and finiteness/duality results for elementary amenable groups — a long chain in which a machine check would add real confidence. Basic objects (coarse equivalences of groups, polycyclic series, uniform lattices, Lie groups with exponential maps) are reusable across geometric group theory.

Difficulty

Quasi-isometries carry no algebraic structure and can be wild at bounded scales, so the comparison group $H$ cannot be assumed solvable or even amenable a priori. Shalom's argument yields only a nontrivial homomorphism to $\mathbb Z$, not full structure. The geometric core is height rigidity: one must show that a quasi-isometry cannot mix "up" and "down" directions of different exponential rates, uniformly over all quasi-isometries with given constants, and with a bounded (not merely sublinear) error, which is exactly what the later group-theoretic deduction needs.

Formalization scope

• Polycyclicity is encoded by an explicit finite cyclic subnormal series; virtual polycyclicity by a finite-index polycyclic subgroup. Quasi-isometry of finitely generated groups is encoded as GroupCoarseEquivalence, with bornologous maps and errors in finite sets — equivalent to quasi-isometry of word metrics.
• Simply connected solvable Lie groups are bundled as SimplyConnectedSolvableLieModel (finite-dimensional charted Lie group, Hausdorff, second countable, simply connected, solvable). Uniform lattices are discrete subgroups with a compact fundamental cover; finite-covolume lattices carry an invariant probability measure on the coset space.
• In the height theorem, real-triangulability is a TriangularAdjoint basis, $W$ is any normed space linearly isomorphic to the canonical quotient, and $\pi$ is characterized through an exponential map. The metric is any compatible proper left-invariant metric with linear chain bounds — a quasi-isometric generalization of the source's fixed left-invariant Riemannian metric. The finite group $\mathcal A$ is chosen before $K,C$.
• Needed infrastructure: Lie algebras of Lie groups and exponential maps, Haar measure, quasi-isometries, Gromov's theorem, and the theory of elementary amenable groups.

Selected references

• M. Gromov, Groups of polynomial growth and expanding maps, Publ. Math. IHÉS 53 (1981), 53–78. https://doi.org/10.1007/BF02698687
• Y. Shalom, Harmonic analysis, cohomology, and the large-scale geometry of amenable groups, Acta Math. 192 (2004), 119–185. https://doi.org/10.1007/BF02392739
• A. Eskin, D. Fisher and K. Whyte, Quasi-isometries and rigidity of solvable groups, Pure Appl. Math. Q. 3 (2007), 927–947. https://doi.org/10.4310/PAMQ.2007.v3.n4.a3
• A. Eskin, D. Fisher and K. Whyte, Coarse differentiation of quasi-isometries II: Rigidity for Sol and lamplighter groups, Ann. of Math. 177 (2013), 869–910. https://doi.org/10.4007/annals.2013.177.3.2
• I. Peng, Coarse differentiation and quasi-isometries of a class of solvable Lie groups II, Geom. Topol. 15 (2011), 1927–1981. https://doi.org/10.2140/gt.2011.15.1927
• T. Dymarz, Large scale geometry of certain solvable groups, Geom. Funct. Anal. 19 (2010), 1650–1687. https://doi.org/10.1007/s00039-010-0046-y
• T. Dymarz, D. Fisher and X. Xie, A Tukia-type theorem for nilpotent Lie groups and quasi-isometric rigidity of solvable groups, Adv. Math. 468 (2025). https://doi.org/10.1016/j.aim.2025.110202
• K. Dekimpe, Solvable Lie algebras, Lie groups and polynomial structures, Compos. Math. 121 (2000), 183–204. https://doi.org/10.1023/A:1001738932743
• Y. Cornulier and R. Tessera, On the vanishing of reduced 1-cohomology for Banach representations, Ann. Inst. Fourier 70 (2020), 1951–2003. https://doi.org/10.5802/aif.3363
• OpenAI, Quasi-isometric recognition of virtually polycyclic groups, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1 and Corollary 1.2, p. 2; Theorem 1.4, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/quasi-isometric-recognition-of-virtually-polycyclic-groups-September-24-2026/paper.pdf

Motivation

A finitely generated group has decidable word problem if an algorithm decides, for every word in a fixed finite generating set and its inverses, whether it represents the identity. Embedding theorems translate this algorithmic property into algebra: Higman (1961) characterized subgroups of finitely presented groups, and Boone and Higman (1974) showed that decidable word problem is equivalent to embedding in a simple subgroup of a finitely presented group, asking whether the simple group can be finitely presented (the Boone–Higman conjecture).

This preprint proves a stronger statement in the direction of higher finiteness: every finitely generated group with decidable word problem embeds in a simple group of type $F_\infty$, i.e. one with a classifying space having finitely many cells in each dimension. Since type $F_\infty$ implies finite presentation, this implies the Boone–Higman conjecture.

Background

• 1961. Higman's embedding theorem: finitely generated subgroups of finitely presented groups are exactly the recursively presented groups.
• 1974. Boone and Higman characterize decidable word problem by embeddings into simple subgroups of finitely presented groups and pose the conjecture.
• 1975, 1987. Brown gives homological criteria for finiteness and establishes type $F_\infty$ for the Thompson–Higman groups.
• 1980. Thompson shows the simple overgroup can be chosen finitely generated with decidable word problem.
• 2022. Belk and Zaremsky introduce twisted Brin–Thompson groups and construct a simple group of type $F_\infty$ containing all finitely generated right-angled Artin groups.
• 2024–2026. Belk, Hyde and Matucci construct a simple $F_\infty$ group containing every countable abelian group; the Boone–Higman conjecture is verified for hyperbolic groups (Belk, Bleak, Matucci, Zaremsky) and for $\mathrm{Aut}(F_n)$ and mapping class groups (Belk, Fournier-Facio, Hyde, Zaremsky). The survey of Belk, Bleak, Matucci and Zaremsky raises the higher-finiteness question.
• 2026. The OpenAI preprint Simple $F_\infty$ overgroups of groups with decidable word problem (dated September 23, 2026) proves the theorem below, building on the companion preprint Finite algebraic envelopes and the Boone–Higman conjecture. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A classifying space $K(H,1)$ is a connected CW complex with fundamental group $H$ and contractible universal cover. $H$ has type $F_n$ if some $K(H,1)$ has finite $n$-skeleton and type $F_\infty$ if some $K(H,1)$ has finitely many cells in each dimension. Type $F_1$ is finite generation and type $F_2$ is finite presentation. A group is simple if it is nontrivial and has no normal subgroups besides $1$ and itself.

In Lean (OAI.SimpleFInftyOvergroups, definitions SimpleOvergroups), HasDecidableWordProblem G asks for a finite generating tuple with a ComputablePred identity predicate on words; HasTypeFInfty H asks for a Hausdorff connected space $X$ with a CW structure of finite type (Topology.CWComplex.FiniteType), a basepoint with $H \simeq \pi_1(X, x)$, and a surjective covering map from a contractible space.

Formalization targets

Goal: Theorem 1.1

Every finitely generated group $G$ with decidable word problem admits an injective homomorphism $G \hookrightarrow H$ into a nontrivial simple group $H$ of type $F_\infty$.

The input need not be finitely presented and its word-problem algorithm may have arbitrary running time; the classifying space of $H$ may be infinite-dimensional.

Significance

The result. Theorem 1.1 answers the higher-finiteness strengthening of the Boone–Higman conjecture and implies the conjecture itself. With the classical converse (finitely presented simple groups have decidable word problem), it characterizes groups with decidable word problem as the finitely generated subgroups of simple groups of type $F_\infty$.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires CW complexes of finite type, classifying spaces and covering theory (partially in Mathlib), Brown's homological finiteness criterion, Steinberg groups, and twisted Brin–Thompson groups with the Belk–Zaremsky finiteness theorem (Theorem 5.1 in the preprint, from the literature).

Difficulty

Finite presentation already fails to pass to subgroups; higher finiteness additionally requires controlling relations among relations in every dimension. Known families of simple $F_\infty$ groups contain large classes of groups but give no general construction from a word-problem algorithm. The proof needs an oligomorphic faithful action of a group of type $F_\infty$ with stabilizers of type $F_\infty$, built from an algebraic envelope whose Steinberg-group kernel must be annihilated exactly (Theorem 4.6).

Formalization scope

• $G$ and $H$ live in the same universe Type u; $G$ carries [Group.FG G].
• IsSimpleGroup H together with Nontrivial H encodes simplicity.
• Type $F_\infty$ is encoded topologically via a finite-type CW structure on a connected Hausdorff space whose universal cover (a surjective covering with contractible total space) witnesses asphericity.
• The word problem uses ComputablePred on lists of (generator, sign) pairs for a specified generating tuple.

The statement is not vacuous: the hypothesis holds for many groups (e.g. all finitely presented residually finite groups), and the conclusion requires a genuine embedding.

Needed infrastructure: finite-type CW complexes and $K(\pi,1)$ spaces, Brown's criterion, group actions with finiteness properties, Steinberg groups over noncommutative algebras, and twisted Brin–Thompson groups. Contributions toward any of these are welcome.

Selected references

• OpenAI, Simple $F_\infty$ overgroups of groups with decidable word problem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf
• OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/main/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf
• W. W. Boone, G. Higman, An algebraic characterization of groups with soluble word problem, J. Austral. Math. Soc. 18 (1974). https://doi.org/10.1017/S1446788700019108
• G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
• R. J. Thompson, Embeddings into finitely generated simple groups which preserve the word problem, in Word Problems II, 1980. https://doi.org/10.1016/S0049-237X(08)71348-X
• K. S. Brown, Homological criteria for finiteness, Comment. Math. Helv. 50 (1975). https://doi.org/10.1007/BF02565740
• K. S. Brown, Finiteness properties of groups, J. Pure Appl. Algebra 44 (1987). https://doi.org/10.1016/0022-4049(87)90015-6
• J. Belk, M. C. B. Zaremsky, Twisted Brin–Thompson groups, Geom. Topol. 26 (2022). https://doi.org/10.2140/gt.2022.26.1189
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Progress around the Boone–Higman conjecture, 2025. https://arxiv.org/abs/2306.16356
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Hyperbolic groups satisfy the Boone–Higman conjecture, Duke Math. J. 175 (2026). https://doi.org/10.1215/00127094-2025-0055
• J. Belk, J. Hyde, F. Matucci, Finite germ extensions, 2024. https://arxiv.org/abs/2407.03149

Motivation: algebraic versus geometric dimension of groups

Two numbers measure how "large" a discrete group $\Gamma$ is. The cohomological dimension $\operatorname{cd}\Gamma$ is algebraic: the length of the shortest projective resolution of the trivial module $\mathbb Z$ over the group ring $\mathbb Z[\Gamma]$. The geometric dimension $\operatorname{gd}\Gamma$ is topological: the least dimension of a CW complex with fundamental group $\Gamma$ and contractible universal cover (a classifying space or $K(\Gamma,1)$). Cellular chains of a classifying space give a free resolution, so $\operatorname{cd}\Gamma\le\operatorname{gd}\Gamma$. Eilenberg and Ganea proved in 1957 that equality holds whenever $\operatorname{cd}\Gamma\ge3$, and Stallings and Swan settled dimension one. The remaining case — must a group of cohomological dimension two have a two-dimensional classifying space? — is the Eilenberg–Ganea conjecture, closely tied to Whitehead's asphericity conjecture in low-dimensional topology.

Background

• 1941 — Whitehead asks whether every connected subcomplex of an aspherical 2-complex is aspherical (Ann. of Math. 1941).
• 1957 — Eilenberg and Ganea prove $\operatorname{cd}=\operatorname{gd}$ for $\operatorname{cd}\ge3$ and pose the dimension-two question (Ann. of Math. 1957).
• 1968–1969 — Stallings proves that finitely generated groups of cohomological dimension one are free (Ann. of Math. 1968); Swan removes finite generation (J. Algebra 1969).
• 1997 — Bestvina and Brady introduce height kernels of right-angled Artin groups and show that for suitable flag triangulations of a spine of the Poincaré homology sphere at least one of the Eilenberg–Ganea and Whitehead conjectures fails (Invent. Math. 1997, Thm 8.7).
• 1999 — Dicks and Leary give presentations of these kernels (Proc. AMS 1999); Howie studies them via plus constructions (Math. Proc. Camb. Phil. Soc. 1999).
• 2026 — Leary and Petrosyan compare Coxeter and Bestvina–Brady candidates for the problem (arXiv:2605.07853).
• 2026 — An OpenAI preprint, A finitely generated counterexample to the Eilenberg–Ganea conjecture (OpenAI Math Release, September 23, 2026), claims a finitely generated residually finite group with $\operatorname{cd}=2$ and $\operatorname{gd}=3$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

For a finite simplicial graph $\Delta$ with vertex set $V$, the right-angled Artin group is

$$A_\Delta=\bigl\langle a_q\ (q\in V)\ \bigm|\ a_qa_ra_q^{-1}a_r^{-1}=1\ \text{whenever } q,r \text{ are adjacent}\bigr\rangle ,$$

and the height homomorphism $\lambda:A_\Delta\to\mathbb Z$ sends every $a_q$ to $1$. Its kernel is a Bestvina–Brady group.

The specific graph comes from the presentation complex $K$ of $\langle x,y\mid x^2y^{-5},\ x^2(yx^{-1})^{3}\rangle$, which is integrally acyclic and has a nontrivial representation of its fundamental group into $\mathrm{SU}(2)$. Subdivide each of the two loops of $K$ into three edges, cone the boundary of each relator polygon to a new interior vertex (keeping one radial edge per boundary occurrence), and take the order complex of the resulting regular cell structure (7 vertices, 51 edges, 45 triangular sectors). This is a flag triangulation $L$ of $K$; $\Delta$ is its 1-skeleton, i.e. the comparability graph of the cells. The group is $G=\ker\lambda\le A_\Delta$.

A group is residually finite if every nontrivial element survives in some finite quotient.

Formalization targets

Goal: the counterexample (Theorem 1.1)

For the group $G$ above,

$$G\ \text{is finitely generated and residually finite},\qquad \operatorname{cd}G=2,\qquad G \text{ has a 3-dimensional } K(G,1),\qquad G \text{ has no 2-dimensional } K(G,1).$$

In particular $\operatorname{gd}G=3\ne2=\operatorname{cd}G$. The non-existence clause holds for classifying spaces with any number of cells. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem disproves the Eilenberg–Ganea conjecture with a finitely generated (indeed type $\mathrm{FL}$, but not finitely presented) residually finite group, so the conjecture fails even for countable groups with strong finiteness properties. By Bestvina–Brady's dichotomy the Whitehead conjecture is not directly decided by this example, but the gap between the algebraic and geometric dimensions in dimension two is now exhibited concretely.

Formalizing it. The statement is concrete: an explicit finite graph, its Artin group and height kernel, a projective dimension, and existence/non-existence of CW models. The non-existence clause ranges over all CW complexes of arbitrary cardinality, which is exactly the kind of universally quantified topological claim where a machine check is valuable. Groundwork includes classifying spaces in Mathlib's CW-complex framework, projective dimension over group rings, and Bestvina–Brady Morse theory.

Difficulty

The kernel acts freely on an acyclic 2-complex, which gives $\operatorname{cd}G\le2$, but an acyclic complex need not be contractible, and showing that one particular 2-dimensional model fails to be a $K(G,1)$ says nothing about other models. The obstacle is to rule out every hypothetical two-dimensional classifying space, with arbitrarily many cells, and to do so for a group that is not finitely presented. Homological invariants cannot see the difference, since they agree with those of a genuine 2-dimensional model.

Formalization scope

• The seed complex is encoded combinatorially: signed relator words seedWord, rose vertices, circle edges and sectors; seedGraph is the comparability graph of the cell face relation. ArtinGroup is a PresentedGroup on commutators of adjacent vertices, height sends each generator to $1$ in Multiplicative ℤ, and SourceGroup is its kernel.
• cohomologicalDimension is the categorical projective dimension (in WithBot ℕ∞) of the trivial $\mathbb Z[G]$-module in ModuleCat.
• HasClassifyingSpace G n asks for a Hausdorff, path-connected CW complex with no cells above dimension $n$, fundamental group isomorphic to $G$, and a surjective covering map from a contractible space. The positive clause is stated in universe 0; the negative clause is universe-polymorphic, so no restriction on the cardinality of cells is imposed.
• Needed infrastructure: Bestvina–Brady level complexes, presentations of height kernels, residual finiteness of RAAG subgroups, $\mathrm{SU}(2)$ representations and degree arguments.

Selected references

• S. Eilenberg and T. Ganea, On the Lusternik–Schnirelmann category of abstract groups, Ann. of Math. 65 (1957). https://doi.org/10.2307/1970062
• J. H. C. Whitehead, On adding relations to homotopy groups, Ann. of Math. 42 (1941). https://doi.org/10.2307/1968907
• J. R. Stallings, On torsion-free groups with infinitely many ends, Ann. of Math. 88 (1968). https://doi.org/10.2307/1970577
• R. G. Swan, Groups of cohomological dimension one, J. Algebra 12 (1969). https://doi.org/10.1016/0021-8693(69)90030-1
• M. Bestvina and N. Brady, Morse theory and finiteness properties of groups, Invent. Math. 129 (1997). https://doi.org/10.1007/s002220050168
• W. Dicks and I. J. Leary, Presentations for subgroups of Artin groups, Proc. Amer. Math. Soc. 127 (1999). https://doi.org/10.1090/S0002-9939-99-04873-X
• J. Howie, Bestvina–Brady groups and the plus construction, Math. Proc. Cambridge Philos. Soc. 127 (1999). https://doi.org/10.1017/S0305004199003928
• I. J. Leary and N. Petrosyan, Universal structure of graph product kernels, preprint, 2026. https://arxiv.org/abs/2605.07853v1
• OpenAI, A finitely generated counterexample to the Eilenberg–Ganea conjecture, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026/paper.pdf

Motivation

A finitely generated group is (word-)hyperbolic if the geodesic triangles in its Cayley graph are uniformly thin, as in the hyperbolic plane. Such a group has a boundary at infinity $\partial G$, a compact space of asymptotic directions. The fundamental group of a closed hyperbolic 3-manifold is hyperbolic with boundary the 2-sphere. Cannon's conjecture asks for the converse: if a hyperbolic group has boundary homeomorphic to $S^2$, does it act geometrically on hyperbolic three-space $\mathbb H^3$? An affirmative answer characterizes, purely in terms of coarse geometry, which groups arise from closed hyperbolic 3-manifolds; it is one of the central problems of geometric group theory and is closely tied to the geometrization program for 3-manifolds.

Timeline

• 1981, 1980. Sullivan and Tukia show that groups of uniformly quasiconformal maps of the sphere are conjugate to Möbius groups (Sullivan, Stony Brook 1978 proceedings; Tukia, doi:10.5186/aasfm.1980.0530).
• 1989. Pansu introduces conformal dimension of boundaries (doi:10.5186/aasfm.1989.1424).
• 1994. Cannon's combinatorial Riemann mapping theorem recovers quasiconformal coordinates from discrete moduli (doi:10.1007/BF02398434).
• 1998. Cannon and Swenson state the group-boundary conjecture and relate geometric actions to conformality of boundary coverings (doi:10.1090/S0002-9947-98-02107-2).
• 1999. Cannon, Floyd and Parry reduce the problem to bounded discrete moduli of annuli at small scales (Ann. Acad. Sci. Fenn. Math., 1999).
• 2002, 2005. Bonk and Kleiner develop quasisymmetric uniformization of metric spheres and prove the conjecture when the Ahlfors-regular conformal dimension is attained (doi:10.1007/s00222-002-0233-z, doi:10.2140/gt.2005.9.219).
• 2012–2013. Kahn–Marković, Bergeron–Wise, Agol and Marković connect surface subgroups, cubulation and Kleinian realizations (doi:10.4007/annals.2012.175.3.4, doi:10.4171/DM/421, doi:10.1007/s00039-013-0228-5). Bourdon and Kleiner give a combinatorial-modulus criterion for uniformization (doi:10.4171/GGD/177).
• 2015. Haïssinsky proves a virtual Kleinian criterion for cubulated hyperbolic groups with planar boundary (doi:10.1007/s00222-014-0552-x).
• 2026. Groves, Haïssinsky, Manning, Osajda, Sisto and Walsh reduce the residually finite case to the Toral Relative Cannon conjecture (arXiv:2406.14667).

The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.

Setting

Let $G$ be a group with a finite symmetric generating set $S$ and Cayley graph $\Gamma(G,S)$ with graph distance $d$. $G$ is hyperbolic if there is $\delta$ such that every point on a side of a geodesic triangle lies within $d\le\delta$ of the union of the other two sides. A geodesic ray based at $1$ is a sequence $r_0=1,r_1,\dots$ with $d(r_i,r_j)=|i-j|$; two rays are equivalent if $d(r_n,s_n)$ stays bounded. The boundary $\partial G$ is the set of equivalence classes with the quotient of the topology of pointwise convergence.

$\mathbb H^3$ is the upper half-space $\{x\in\mathbb R^3: x_3>0\}$ with distance $\operatorname{arcosh}\bigl(1+|x-y|^2/(2x_3y_3)\bigr)$, and $\operatorname{Isom}(\mathbb H^3)$ is its full isometry group, including orientation-reversing isometries. A homomorphism $\rho:G\to\operatorname{Isom}(\mathbb H^3)$ gives a proper action if $\{g:\rho(g)K\cap K\ne\varnothing\}$ is finite for every compact $K$, and a cocompact action if translates of one compact set cover $\mathbb H^3$.

Formalization targets

Goal: Theorem 1.1

$$G\ \text{hyperbolic},\ \partial G\cong S^2\ \Longrightarrow\ \exists\,\rho:G\to\operatorname{Isom}(\mathbb H^3)\ \text{proper, cocompact, with }\ker\rho\ \text{finite}.$$

The Lean statement OAI.CannonRelease.cannon is open on the platform.

Significance

The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in $\operatorname{Isom}(\mathbb H^3)$. For torsion-free $G$, the quotient $\mathbb H^3/G$ is a closed hyperbolic 3-manifold, possibly nonorientable (Corollary 8.1), and the work of Kahn–Marković, Bergeron–Wise and Agol then gives virtual structure results (Corollary 8.2). It also settles the hypotheses of the reductions of Marković and of Groves et al. in full generality.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would require formal infrastructure for hyperbolic groups and their boundaries, quasiconformal analysis and combinatorial modulus, very little of which is currently in Mathlib.

Difficulty

By the Cannon–Floyd–Parry and Bourdon–Kleiner criteria, the theorem reduces to a uniform upper bound on the combinatorial 2-modulus of curve families at all scales of the boundary. The bound is easy to state but there is no a priori reason why moduli of coverings of a topological sphere should stay bounded; Bonk–Kleiner needed the extra hypothesis that the conformal dimension is attained. A proof must extract analytic control (a nonconstant limit function with controlled oscillation) from a hypothetical sequence of coverings with unbounded modulus and contradict it using only hyperbolicity and the topology of the boundary.

Formalization scope

• CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number $\delta$ working for all geodesic triangles given as walks of length equal to graph distance.
• Rays are ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. $G$ carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.
• $S^2$ is the unit sphere in EuclideanSpace ℝ (Fin 3); $\mathbb H^3$ is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.
• The kernel is only required to be finite, and orientation-reversing elements are allowed, matching the paper.

A complete development needs Gromov hyperbolic groups and visual metrics, approximately self-similar spheres, combinatorial modulus and the Bonk–Kleiner/Bourdon–Kleiner uniformization criterion, and the Sullivan–Tukia straightening of uniformly quasiconformal groups. Contributions formalizing Proposition 2.6 (from a round boundary action to a geometric action on $\mathbb H^3$) or Theorem 2.5 (the uniformization criterion) are welcome.

Selected references

• OpenAI, A Modulus Proof of Cannon's Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Modulus-Proof-of-Cannons-Conjecture-September-23-2026/paper.pdf
• J. W. Cannon, The combinatorial Riemann mapping theorem, Acta Math., 1994. https://doi.org/10.1007/BF02398434
• J. W. Cannon, E. L. Swenson, Recognizing constant curvature discrete groups in dimension 3, Trans. Amer. Math. Soc., 1998. https://doi.org/10.1090/S0002-9947-98-02107-2
• J. W. Cannon, W. J. Floyd, W. R. Parry, Sufficiently rich families of planar rings, Ann. Acad. Sci. Fenn. Math., 1999. https://www.acadsci.fi/mathematica/Vol24/cannon.pdf
• M. Bonk, B. Kleiner, Quasisymmetric parametrizations of two-dimensional metric spheres, Invent. Math., 2002. https://doi.org/10.1007/s00222-002-0233-z
• M. Bonk, B. Kleiner, Conformal dimension and Gromov hyperbolic groups with 2-sphere boundary, Geom. Topol., 2005. https://doi.org/10.2140/gt.2005.9.219
• M. Bourdon, B. Kleiner, Combinatorial modulus, the combinatorial Loewner property, and Coxeter groups, Groups Geom. Dyn., 2013. https://doi.org/10.4171/GGD/177
• V. Marković, Criterion for Cannon's conjecture, Geom. Funct. Anal., 2013. https://doi.org/10.1007/s00039-013-0228-5
• P. Haïssinsky, Hyperbolic groups with planar boundaries, Invent. Math., 2015. https://doi.org/10.1007/s00222-014-0552-x
• D. Groves, P. Haïssinsky, J. F. Manning, D. Osajda, A. Sisto, G. S. Walsh, Drilling hyperbolic groups, preprint, 2026. https://arxiv.org/abs/2406.14667

Motivation

In Bernoulli bond percolation on a graph $G=(V,E)$, each edge is kept (open) independently with probability $p$. As $p$ grows, an infinite connected component of open edges appears at the critical probability $p_c(G)$. The criticality problem asks whether an infinite cluster can already exist at $p_c$. A negative answer means the phase transition is continuous. Benjamini and Schramm (1996) conjectured that, on every graph with a large symmetry group and $p_c<1$, there is no infinite cluster at $p_c$. The question contains the famous open case of $\mathbb Z^3$ and connects percolation to geometric group theory, since Cayley graphs of finitely generated groups are the main examples.

Timeline

• 1957. Broadbent and Hammersley introduce percolation (doi:10.1017/S0305004100032680).
• 1960, 1980. Harris and Kesten settle nearest-neighbour bond percolation on $\mathbb Z^2$, including $\theta(p_c)=0$ (doi:10.1017/S0305004100034241, doi:10.1007/BF01197577).
• 1986–1987. Menshikov and Aizenman–Barsky prove sharpness of the subcritical phase; this does not settle behaviour at $p_c$ (doi:10.1007/BF01212322).
• 1990. Hara and Slade prove mean-field behaviour, including $\theta(p_c)=0$, for $\mathbb Z^d$ in sufficiently high dimension (doi:10.1007/BF02108785).
• 1996. Benjamini and Schramm formulate the conjecture for quasi-transitive graphs with $p_c<1$ (doi:10.1214/ECP.v1-978).
• 1999. Benjamini, Lyons, Peres and Schramm prove it for nonamenable graphs with a unimodular quasi-transitive action (doi:10.1214/aop/1022677450).
• 2006. Timár excludes infinitely many infinite critical clusters on nonunimodular transitive graphs (doi:10.1214/009117906000000494).
• 2016. Hutchcroft proves the conjecture for every quasi-transitive graph of exponential growth (arXiv:1605.05301). Duminil-Copin, Sidoravicius and Tassion treat slabs (doi:10.1002/cpa.21641).
• 2017. Fitzner and van der Hofstad reach nearest-neighbour $\mathbb Z^d$, $d\ge11$ (arXiv:1506.07977).
• 2021. Hermon and Hutchcroft cover certain groups of intermediate growth (arXiv:1809.11112).
• 2024. Kozma and Nitzan reduce the $\mathbb Z^d$ case to a conjectured gluing inequality (arXiv:2401.12397).
• 2026. Public, non-peer-reviewed announcements report AI-assisted proofs for $\mathbb Z^d$, including a reported Lean formalization of the lattice case (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats the remaining subexponential-growth case for all quasi-transitive graphs.

Setting

A graph here has vertex set $V$ and a set $E$ of labelled bonds, each with a pair of endpoints; loops and parallel bonds are allowed. It is locally finite if each vertex lies in finitely many bonds, connected if any two vertices are joined by a path, and quasi-transitive if its automorphism group (bijections of vertices and of bonds respecting endpoints) has finitely many orbits on $V$. Examples include $\mathbb Z^d$ and every Cayley graph of a finitely generated group.

For $p\in[0,1]$, let $\mathbb P_p$ be the law of a random set $\omega\subseteq E$ containing each bond independently with probability $p$. The cluster $C_x(\omega)$ of $x$ is the set of vertices joined to $x$ by a finite path of bonds in $\omega$ (including $x$). Define

$$p_c(G)=\inf\{p\in[0,1]:\ \mathbb P_p(\exists x,\ |C_x|=\infty)>0\}.$$

Formalization targets

Goal: Theorem 1.1

For every infinite, connected, locally finite, quasi-transitive graph $G$,

$$p_c(G)<1\ \Longrightarrow\ \mathbb P_{p_c(G)}\bigl(\exists x\in V:\ |C_x|=\infty\bigr)=0.$$

The hypothesis $p_c<1$ is necessary, since at $p=1$ every infinite connected graph percolates. The Lean statement OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality is open on the platform.

Significance

Theorem 1.1 resolves the Benjamini–Schramm criticality conjecture for Bernoulli bond percolation, and in particular gives $\theta(p_c)=0$ on $\mathbb Z^d$ for every $d\ge2$ (Corollary 10.1, p. 39), including the long-open case $d=3$. With Hutchcroft's exponential-growth theorem, the remaining work is the subexponential case, divided into superpolynomial growth and growth bounded by a polynomial along a sequence of scales. As a consequence the percolation probability is continuous at $p_c$ on every such graph.

The result is proved in an OpenAI preprint that has not been peer reviewed. No machine-checked proof of the general quasi-transitive statement exists; the reported Lean formalization concerns only nearest-neighbour $\mathbb Z^d$. A formal proof would also certify the structural input (Tessera–Tointon's finitary structure theorem) as used here.

Difficulty

The obvious strategy, renormalization from large finite boxes, needs a gluing inequality to connect independently found large clusters, and it needs coordinates: on a general quasi-transitive graph there is no lattice to place boxes in. Planar duality is unavailable, the lace expansion needs high dimension, and Hutchcroft's argument uses exponential growth essentially. In the superpolynomial case one must rule out two large distinct clusters adjacent across an edge; in the polynomial case one needs nilpotent-group coordinates (Gromov, Trofimov, Tessera–Tointon) and a two-direction corridor exploration in which conditional failure probabilities stay uniformly small. Neither uniqueness of the infinite cluster nor independence across coarse blocks can be assumed.

Formalization scope

• BondGraph V E stores ends : E → Sym2 V; loops and parallel bonds are allowed. LocallyFinite counts bonds at each vertex. Clusters use SimpleGraph.fromEdgeSet of the open bonds, so loops are discarded and parallel bonds collapse; reachability includes the zero-length path.
• Aut consists of a vertex bijection and a bond bijection that commute with ends; QuasiTransitive says some finite set of vertices meets every orbit.
• law p is ProbabilityTheory.setBernoulli Set.univ p on Set E: each bond retained independently with probability p : unitInterval.
• criticalProbability is sInf in unitInterval of $\{p:\mathbb P_p(\text{percolates})>0\}$; if the set were empty this would be $1$, which hpc excludes.
• percolates is the event that some cluster is infinite; the conclusion says it has measure $0$ at $p_c$.

A complete development needs Bernoulli product measures, Harris–FKG and conditional correlation inequalities, Hutchcroft's exponential-growth theorem, volume-growth theory of quasi-transitive graphs, and the Gromov–Trofimov–Tessera–Tointon structure theory. Each of these is reusable well beyond this mission. Contributions formalizing Proposition 3.1 (two-cluster bound), Theorem 6.1 (joint gluing), Theorem 7.1 (criticality with a nilpotent quotient action) or Proposition 9.3 (subcritical exploration), or the cited Theorem 2.2 (Hutchcroft), are welcome.

Selected references

• OpenAI, No percolation at criticality on quasi-transitive graphs, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/No-percolation-at-criticality-on-quasi-transitive-graphs-September-24-2026/paper.pdf
• I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$, many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Critical percolation on any nonamenable group has no infinite clusters, Ann. Probab., 1999. https://doi.org/10.1214/aop/1022677450
• T. Hutchcroft, Critical percolation on any quasi-transitive graph of exponential growth has no infinite clusters, C. R. Math., 2016. https://doi.org/10.1016/j.crma.2016.07.013
• J. Hermon, T. Hutchcroft, No percolation at criticality on certain groups of intermediate growth, IMRN, 2021. https://doi.org/10.1093/imrn/rnz265
• R. Tessera, M. C. H. Tointon, A finitary structure theorem for vertex-transitive graphs of polynomial growth, Combinatorica, 2021. https://doi.org/10.1007/s00493-020-4295-6
• G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397
• T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
• H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
• Á. Timár, Percolation on nonunimodular transitive graphs, Ann. Probab., 2006. https://doi.org/10.1214/009117906000000494

Motivation

The Hattori–Stallings trace refines the rank of a finitely generated projective module over a group ring $\mathbb CG$ into one complex number per conjugacy class of $G$. These numbers enter group-ring Euler characteristics, where they retain information that an ordinary numerical Euler characteristic forgets. Bass's trace conjecture (complex group-ring form) predicts that the trace of every projective module vanishes at every conjugacy class of an element of infinite order. For torsion-free groups this forces the trace to be an integer rank, and that in turn implies the Kaplansky idempotent conjecture: a group ring $kG$ of a torsion-free group over a field of characteristic zero has no idempotents other than $0$ and $1$. Both questions date from the 1960s–1970s and were previously known only for restricted classes of groups (linear, elementary amenable, amenable, hyperbolic, or groups satisfying the Farrell–Jones conjecture).

This mission asks for a formal proof of the complex Bass trace conjecture for all discrete groups, with the torsion-free consequences as a milestone, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1965 — Hattori (Nagoya Math. J. 1965) and Stallings (Topology 1965) introduce the rank element of a projective module.
• 1973 — Formanek proves the characteristic-zero idempotent statement for torsion-free groups with the ascending chain condition on subgroups (Canad. J. Math. 1973).
• 1976–1979 — Bass formulates the trace conjectures and proves complex trace vanishing for linear groups (Invent. Math. 1976; Homological Group Theory 1979).
• 1983 — Linnell restricts the possible coefficients of the integral trace (Proc. LMS 1983).
• 1985–1986 — Cyclic homology approaches: Connes (Publ. IHÉS 1985), Burghelea (Comment. Math. Helv. 1985), Eckmann (Comment. Math. Helv. 1986).
• 1998 — Burger and Valette revisit Kaplansky's and Zalesskii's theorems: the canonical trace of an idempotent lies in $[0,1]$ and is rational (J. Lie Theory 1998).
• 2002 — Mineyev–Yu (Invent. Math. 2002) and Puschnigg (Invent. Math. 2002) treat torsion-free hyperbolic groups in $C^*_r(G)$.
• 2003–2008 — Elementary amenable groups (Farrell–Linnell, Math. Ann. 2003); amenable groups (Berrick–Chatterji–Mislin, Math. Ann. 2004); groups satisfying Farrell–Jones (Bartels–Lück–Reich, J. Topol. 2008).
• September 2026 — The OpenAI preprint claims the complex Bass conjecture for every group (Theorem 1.1, p. 3) and the characteristic-zero idempotent conjecture (Corollary 1.2, p. 3).

Setting

Let $G$ be a group and $\mathbb CG$ its complex group ring. $K_0(\mathbb CG)$ is the Grothendieck group of finitely generated projective right $\mathbb CG$-modules. An idempotent matrix $e\in M_q(\mathbb CG)$ represents the module $e(\mathbb CG)^q$; its Hattori–Stallings trace is the class of $\sum_i e_{ii}$ in $\mathbb CG/[\mathbb CG,\mathbb CG]$, extended additively to $K_0$. Identifying this quotient with finitely supported functions on conjugacy classes (sum the coefficients over each class), $\mathrm{HS}_G(x)(C)$ is the coefficient of $x\in K_0(\mathbb CG)$ at the class $C$.

For the corollary: $G$ is torsion-free if its only element of finite order is $1$. The canonical trace is $\tau_G(\sum a_gg)=a_1$, the augmentation is $\epsilon_G(\sum a_gg)=\sum a_g$, $\tau_{G,q}(b)=\sum_i\tau_G(b_{ii})$, and $\epsilon_{G,q}$ applies $\epsilon_G$ entrywise. $\tau_{G,*}:K_0(\mathbb CG)\to\mathbb C$ is the coefficient at $[1]$, and $\mathrm{rk}_\epsilon:K_0(\mathbb CG)\to\mathbb Z$ is the augmentation rank.

Formalization targets

Milestone: Corollary 1.2 (p. 3)

Let $G$ be torsion-free. (i) For every $q\ge1$ and idempotent $e\in M_q(\mathbb CG)$, $\tau_{G,q}(e)=\operatorname{rank}_{\mathbb C}\epsilon_{G,q}(e)$; hence $\tau_{G,*}=\mathrm{rk}_\epsilon$ and $\tau_{G,*}(K_0(\mathbb CG))=\mathbb Z$. (ii) For every commutative unital domain $R$ of characteristic zero, every $e\in RG$ with $e^2=e$ is $0$ or $1$.

Goal: Theorem 1.1 (p. 3)

For every group $G$, every $x\in K_0(\mathbb CG)$ and every $g\in G$ of infinite order,

$$\mathrm{HS}_G(x)([g])=0;$$

equivalently, $\mathrm{HS}_G(x)$ is supported on conjugacy classes of finite-order elements.

Significance

The result itself. Theorem 1.1 holds for arbitrary groups, with no amenability, finiteness, assembly-map or homological-dimension hypothesis. Combined with Linnell's restriction it gives the integral Bass conjecture (Corollary 9.1, p. 29) and, via Berrick–Chatterji–Mislin, statements about homotopy idempotents on manifolds (Corollary 9.2, p. 29). Corollary 1.2 settles Kaplansky's idempotent conjecture in characteristic zero, including over commutative domains rather than only fields. The analytic Kadison–Kaplansky statement in $C^*_r(G)$ and the positive-characteristic idempotent problem are not addressed.

Formalizing it. The statements need only group rings (MonoidAlgebra), matrices, projective modules and conjugacy classes, all in Mathlib, so both are precise algebraic targets. The proof combines finite path sums in the group with a Pfaffian cocycle (Sections 7–8) and a geometric vanishing theorem for sparse simplicial cycles built from separating filtrations, simplicial volume estimates and free actions on Cantor-type spaces (Sections 2–6). None of this exists in Mathlib; the sparse-chain vanishing theorem (Theorem 2.1, p. 6) is of independent interest. No machine-checked proof of either conjecture, even for special group classes, is known.

Difficulty

Previous proofs pass through analytic completions or assembly maps and therefore need hypotheses on the group (amenability, hyperbolicity, Farrell–Jones), or through cyclic homology and need finite homological dimension of the reduced centralizers. The preprint turns an idempotent and an infinite-order element $g$ into simplicial cycles of every even dimension $2m$ with connected supports in one graph of bounded degree, and a cocycle evaluating to $2^{-m}\mathrm{HS}_G(x)([g])$ (Propositions 7.3 and 8.3, pp. 24–27). The difficulty is to show that invariant cocycles vanish on such sparse cycles in high dimension for an arbitrary acting group $H=C_G(g)/\langle g\rangle$, with no bound on its homological dimension (Theorem 2.1, p. 6): naive filling arguments need either amenability or finite dimensionality.

Formalization scope

• $K_0$ of right modules is built in Lean as a quotient of the free abelian group on objects with a finitely generated projective Module (MonoidAlgebra ℂ G)ᵐᵒᵖ structure, by isomorphism and direct-sum relations (ModuleK0); the Hattori–Stallings trace factors through a presentation of each module by an idempotent matrix. Its values are ConjClasses G →₀ ℂ.
• The goal states both the vanishing at infinite-order classes and the support inclusion in finite-order classes.
• The corollary uses an idempotent-matrix presentation of $K_0(\mathbb CG)$ (BassTrace.K0.Group), matrixTrace (sum of identity coefficients of diagonal entries) and augmentedMatrix; part (ii) quantifies over every commutative domain R with CharZero R.
• TorsionFree G is the usual condition (every finite-order element is $1$).
• Neither statement is vacuous: idempotent matrices and projective modules exist for every $G$, and the conclusions are equalities of explicit traces.

Selected references

• OpenAI, The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Bass-trace-conjecture-for-complex-group-rings-September-24-2026/The-Bass-trace-conjecture-for-complex-group-rings-September-24-2026.pdf
• H. Bass, Euler characteristics and characters of discrete groups, Invent. Math. 35 (1976). https://doi.org/10.1007/BF01390137
• H. Bass, Traces and Euler characteristics, Homological Group Theory (1979). https://doi.org/10.1017/CBO9781107325449.003
• A. Hattori, Rank element of a projective module, Nagoya Math. J. (1965). https://doi.org/10.1017/S002776300001148X
• J. Stallings, Centerless groups — an algebraic formulation of Gottlieb's theorem, Topology (1965). https://doi.org/10.1016/0040-9383(65)90060-1
• E. Formanek, Idempotents in Noetherian group rings, Canad. J. Math. (1973). https://doi.org/10.4153/CJM-1973-037-6
• P. A. Linnell, Decomposition of augmentation ideals and relation modules, Proc. London Math. Soc. (1983). https://doi.org/10.1112/plms/s3-47.1.83
• M. Burger, A. Valette, Idempotents in complex group rings: theorems of Zalesskii and Bass, J. Lie Theory (1998). https://doi.org/10.5802/jolt.142
• A. J. Berrick, I. Chatterji, G. Mislin, From acyclic groups to the Bass conjecture for amenable groups, Math. Ann. (2004). https://doi.org/10.1007/s00208-004-0521-6
• F. T. Farrell, P. A. Linnell, Whitehead groups and the Bass conjecture, Math. Ann. (2003). https://doi.org/10.1007/s00208-003-0424-y
• A. Bartels, W. Lück, H. Reich, On the Farrell–Jones Conjecture and its applications, J. Topol. (2008). https://doi.org/10.1112/jtopol/jtm008
• B. Eckmann, Cyclic homology of groups and the Bass conjecture, Comment. Math. Helv. (1986). https://doi.org/10.1007/BF02621911
• H. Alpert, Simplicial volume and 0-strata of separating filtrations, arXiv:2211.06362 (2024). https://arxiv.org/abs/2211.06362v3

Motivation: tensor squares that contain everything

The irreducible complex representations of the symmetric group $S_n$ are indexed by partitions $\lambda\vdash n$ and written $S^\lambda$ (Specht modules). Decomposing a tensor product $S^\lambda\otimes S^\mu$ (with the diagonal action) into irreducibles is governed by the Kronecker coefficients

$$g(\lambda,\mu,\nu)=\dim\operatorname{Hom}_{S_n}\!\big(S^\nu,\,S^\lambda\otimes S^\mu\big),$$

which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.

Timeline

• 2012 — Saxl proposes (UCLA Combinatorics Seminar, 20 March 2012) that the staircase $\rho_m=(m,m-1,\dots,1)$ at triangular degree $n=m(m+1)/2$ has this property; recorded by Pak, Panova and Vallejo.
• 2013 — Heide, Saxl, Tiep and Zalesski conjecture an analogous covering property for alternating simple groups (HSTZ 2013, Rem. 1.3(3)).
• 2013/2016 — Pak, Panova and Vallejo state the tensor square conjecture for $n\ge3$, $n\ne4,9$, and the Saxl conjecture, and give a character-nonvanishing criterion (PPV 2016, Conj. 1.1–1.2, Lemma 1.3).
• 2015 — Ikenmeyer proves the staircase assertion for all $\nu$ comparable with the staircase in dominance order (Ikenmeyer 2015, Thm 2.1).
• 2017 — Luo and Sellke: staircase squares contain almost all partitions, and fourth powers cover everything in large degree (Luo–Sellke 2017).
• 2018 — Bessenrodt: all double-hook constituents (Bessenrodt 2018, Thm 4.10).
• 2021 — Li: the triple-hook case, and a conjectured family for nontriangular degrees (Li 2021).
• 2023 — Harman and Ryba: staircase tensor cubes contain everything (Harman–Ryba 2023, Thm 1.1).
• 2026 — An OpenAI preprint, Universal Tensor Squares for Symmetric Groups (OpenAI Math Release, September 24, 2026), claims the tensor square conjecture for every $n\notin\{2,4,9\}$, building on a companion preprint that proves Saxl's conjecture in a cyclic form. Neither preprint is peer reviewed and the main theorem is not formally verified; its proof uses exact computer calculations for degrees up to $64$.

Setting

For a Young diagram $\lambda$ with $n$ cells, fix a bijection $t$ between $\{0,\dots,n-1\}$ and the cells (a tableau). The Lean development realizes $S^\lambda$ inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$ ($d$ = number of rows), with $S_n$ acting by permuting letters: the polytabloid $e_t$ is the signed sum, over the column group of $t$, of the permuted indicator of the row word of $t$, and Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The Kronecker coefficient kronecker a b t is finrank of the space of $S_n$-intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape $\lambda$.

Formalization targets

Goal: a universal tensor square in every degree $n\notin\{2,4,9\}$

For every positive integer $n$ with $n\ne2,4,9$ there is a partition $\lambda\vdash n$ such that

$$g(\lambda,\lambda,\nu)>0\qquad\text{for every }\nu\vdash n ,$$

so the tensor square $S^\lambda\otimes S^\lambda$ contains every irreducible representation of $S_n$. The Lean statement asserts, for one Young diagram $\lambda$ with $n$ cells: positivity of kronecker for every target diagram $\nu$ with $n$ cells; irreducibility of spechtRep for $\lambda$; and that every finite-dimensional irreducible complex representation of $S_n$ admits an injective intertwining map into $S^\lambda\otimes S^\lambda$. This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.

Significance

The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen $\lambda$ must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of $\mathrm{GL}_n(\mathbb F_q)$ that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.

Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible $n\le64$, and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.

Difficulty

Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and $n=2,4,9$ are genuine exceptions.

Formalization scope

• Partitions are Mathlib YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of $S^\nu$ in the tensor square.
• The third conjunct quantifies over all finite-dimensional complex irreducible representations in a fixed universe; proving it requires that every irreducible of $S_n$ is isomorphic to some Specht module. The second conjunct (irreducibility of $S^\lambda$) is a standard fact the source uses implicitly.
• $n>0$ and $n\ne2,4,9$ match the source; $n=1$ is trivial.
• Needed infrastructure: Specht module theory (irreducibility, completeness), characters and Murnaghan–Nakayama, Littlewood–Richardson branching, verified computation for $n\le 64$. The Specht and Kronecker layer is shared with the companion Saxl mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier, Tensor products of unipotent characters of general linear groups over finite fields, Transform. Groups 18 (2013), 233–262. https://doi.org/10.1007/s00031-013-9211-3
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf
• OpenAI, Universal Tensor Squares for Symmetric Groups, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf

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