Group Theory

Motivation

Higman's embedding theorem (1961) says that a finitely generated group embeds in a finitely presented group exactly when it is recursively presented, i.e. has a presentation with finitely many generators and a recursively enumerable set of relators. A consequence is that there is a single universal finitely presented group containing every finitely presented group. A natural higher-dimensional question asks whether finiteness can be pushed beyond presentations: finite presentability is the dimension-two case of the topological finiteness properties $F_n$.

This preprint constructs a single group $H$ of type $F_\infty$, i.e. with a classifying space having finitely many cells in every dimension, that contains every finitely presented group. This answers the $F_\infty$ form of the higher-dimensional Higman embedding question posed by Fournier-Facio and Zaremsky.

Background

• 1949. Higman, Neumann and Neumann introduce HNN extensions and embedding theorems for groups.
• 1961. Higman proves his embedding theorem.
• 1974–1975. Bieri and Eckmann, and Brown, develop finiteness properties of groups and homological criteria for them.
• 2018. Leary proves every countable group embeds in a group of type $FP_2$.
• 2026. Fournier-Facio and Zaremsky show that embedding theorems into recursively presented groups of type $FP_n$ would yield embeddings of finitely presented groups into groups of type $F_n$, show that their rope-trick groups fail $FP_3(\mathbb{Q})$ in general, and ask the higher-dimensional Higman embedding question (Question 1.3).
• 2026. The OpenAI preprint A universal group of type $F_\infty$ (dated September 23, 2026) proves the theorem below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A classifying complex for a group $G$ is a connected CW complex with fundamental group isomorphic to $G$ and contractible universal cover; it may be infinite-dimensional. $G$ has type $F_n$ if some classifying complex has finite $n$-skeleton, and type $F_\infty$ if some classifying complex has finitely many cells in every dimension. Type $F_2$ is equivalent to finite presentability. A group is finitely presented if it has a presentation with finitely many generators and relators.

In Lean (OAI.UniversalFInfinity), HasTypeFInfinity G asks for a Hausdorff connected space $X$ with a CW structure on Set.univ having finitely many $n$-cells for every $n$, a basepoint with $\pi_1(X, x) \simeq G$, and a surjective covering map from a contractible space. Finite presentation is Mathlib's Group.IsFinitelyPresented.

Formalization targets

Goal: Theorem 1.1

There exists a group $H$ of type $F_\infty$ such that every finitely presented group admits an injective homomorphism into $H$:

$$\exists H \text{ of type } F_\infty\ \ \forall G \text{ finitely presented}\ \ \exists\, \varphi : G \hookrightarrow H .$$

Significance

The result. Theorem 1.1 gives a universal group with the strongest standard topological finiteness property. Corollary 1.2 follows: the finitely generated subgroups of $H$ are exactly the finitely generated recursively presented groups. No word-problem hypothesis is imposed on the inputs, in contrast with the companion result on simple $F_\infty$ overgroups.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires finite-type CW complexes, classifying spaces and covering theory, Brown's criterion or a direct cell-count argument, Higman's universal finitely presented group, HNN extensions and an ascending-torus theorem (Theorem 5.1), none of which is fully in Mathlib.

Difficulty

Higman's universal group is only finitely presented; type $F_\infty$ requires finite control of relations among relations in every dimension, which is typically destroyed by the embeddings and amalgams used in Higman-type arguments. Fournier-Facio and Zaremsky show that the rope-trick construction fails $FP_3(\mathbb{Q})$, so a different route is needed. The preprint constructs a finitely presented envelope with two families of homomorphisms from the universal group and an ascending HNN-type mapping torus whose finiteness properties can be verified.

Formalization scope

• Universes: $H$ and the quantified finitely presented $G$ live in the same universe Type u; finitely presented groups are countable, so this loses nothing.
• Type $F_\infty$: a CW structure with Finite (cw.cell n) for every $n$, $\pi_1 \simeq H$, and a contractible covering space; no finite-dimensionality is required.
• The universal quantifier is over every Group.IsFinitelyPresented group, not a chosen list of presentations.

The statement cannot be met trivially: a trivial or finite $H$ cannot contain all finitely presented groups, and the type $F_\infty$ requirement is substantive.

Needed infrastructure: CW complexes of finite type, $K(\pi,1)$ spaces, HNN extensions, Higman's embedding theorem. Contributions toward Theorem 5.1 (ascending-torus theorem) or Proposition 6.2 are welcome.

Selected references

• OpenAI, A universal group of type $F_\infty$, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-universal-group-of-type-F-infinity-September-23-2026/paper.pdf
• OpenAI, Simple $F_\infty$ overgroups of groups with decidable word problem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/main/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf
• G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
• G. Higman, B. H. Neumann, H. Neumann, Embedding theorems for groups, J. London Math. Soc. 24 (1949).
• R. Bieri, B. Eckmann, Finiteness properties of duality groups, Comment. Math. Helv. 49 (1974). https://doi.org/10.1007/BF02566720
• K. S. Brown, Homological criteria for finiteness, Comment. Math. Helv. 50 (1975). https://doi.org/10.1007/BF02565740
• I. J. Leary, Subgroups of almost finitely presented groups, Math. Ann. 372 (2018).
• F. Fournier-Facio, M. C. B. Zaremsky, Finiteness properties and Higman's rope trick, preprint, 2026. https://arxiv.org/abs/2607.21727
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002.

Motivation

Thompson's group $F$ consists of the increasing piecewise linear homeomorphisms of $[0,1]$ with finitely many pieces, dyadic rational breakpoints, and slopes that are integer powers of $2$. It is finitely presented, has strong topological finiteness properties, and appears across group theory, dynamics and logic. Whether $F$ is amenable, i.e. whether its bounded functions admit a translation-invariant mean, is one of the best-known open questions about a single explicit group. It is a natural test case because the two classical routes to deciding amenability both fail: $F$ contains no nonabelian free subgroup (Brin–Squier 1985), so the free-subgroup obstruction is unavailable, yet $F$ is not elementary amenable (Cannon–Floyd–Parry 1996, Theorem 4.10). Geoghegan conjectured in 1979 that $F$ is nonamenable. The problem has attracted claimed resolutions in both directions, several later withdrawn or found to contain errors.

This mission asks for a formal proof of nonamenability as stated in an OpenAI preprint dated September 23, 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

• 1929–1957 — Von Neumann and Day develop invariant means and amenability (Fund. Math. 1929; Illinois J. Math. 1957); Følner's criterion (Math. Scand. 1955).
• 1965–1973 — Thompson introduces $F$; an early published construction is McKenzie–Thompson (1973).
• 1979 — Geoghegan conjectures that $F$ is nonamenable (recorded in Cannon–Floyd–Parry 1996, p. 227).
• 1984–1985 — Brown and Geoghegan: $F$ is $\mathrm{FP}_\infty$ (Invent. Math. 1984); Brin and Squier: no nonabelian free subgroups (Invent. Math. 1985).
• 2009–2013 — Shavgulidze's amenability claim (arXiv:0906.0107) and Moore's identification of its errors (arXiv:1102.0747); Moore's tower lower bounds for Følner functions (GGD 2013) and Ramsey characterization of amenability (Fund. Math. 2013); Moore's later amenability manuscript is withdrawn (arXiv:1209.2063).
• 2017 — Haagerup and Olesen: $C^*$-simplicity of $T$ would imply nonamenability of $F$ (JFA 2017).
• 2021–2026 — Akhmedov's nonamenability claim via height functions (arXiv:1310.4395v3); Guba's density estimates (J. Comb. Algebra 2025; J. Algebra 2026).

Setting

A homeomorphism $f$ of $[0,1]$ is a dyadic PL map if there are dyadic rationals $0=x_0<x_1<\dots<x_k=1$ and integers $e_i$ such that on each $[x_{i-1},x_i]$, $f(x)=f(x_{i-1})+2^{e_i}(x-x_{i-1})$. The group $F$ is the set of increasing dyadic PL homeomorphisms of $[0,1]$, with multiplication $hg=h\circ g$, regarded as a discrete group. Let $\ell^\infty(F;\mathbb R)$ be the bounded real functions on $F$. A left-invariant mean is a linear functional $M:\ell^\infty(F;\mathbb R)\to\mathbb R$ with $M(\mathbf 1)=1$, $M(\varphi)\ge0$ whenever $\varphi\ge0$, and $M(g\mapsto\varphi(hg))=M(\varphi)$ for every $h\in F$. $F$ is amenable if such a mean exists.

Formalization targets

Goal: Theorem 1.1 (p. 1)

Thompson's group $F$ is not amenable: there is no positive, normalized, left-invariant mean on $\ell^\infty(F;\mathbb R)$.

Significance

The result itself. It settles Geoghegan's conjecture and the amenability problem for $F$. Because $F$ has no free subgroups, $F$ becomes a finitely presented, torsion-free example of a nonamenable group without free subgroups. Through companion results the preprint derives that $F$ has uniformly bounded representations that are not unitarizable (Corollary 3.1, p. 7) and that Bernoulli percolation on every Cayley graph of $F$ has a nonuniqueness phase (Corollary 3.2, p. 8). The proof is short (Section 2) and uses an infinite-dimensional fixed-point phenomenon: the Benyamini–Sternfeld theorem that the unit ball of an infinite-dimensional Hilbert space admits a Lipschitz self-map moving every point by at least a fixed $\delta>0$ (Lemma 1.2, p. 2; Proc. AMS 1983).

Formalizing it. Given the length of the published argument, this is a realistic target for a complete formal proof of a result that had been open for over forty years. It needs the dyadic-partition model of $F$, the Følner criterion (forward direction), and a Lipschitz map on a Hilbert ball with no approximate fixed points (Appendix A of the preprint constructs one on $L^2([0,1];\mathbb R^2)$ with $\delta=1/2$). The Følner direction from invariant means to Følner sets is reusable infrastructure for amenability in Mathlib.

Difficulty

Neither standard obstruction applies: there is no free subgroup to produce a paradoxical decomposition, and no structural closure property shows amenability. Følner sets, if they existed, would have to grow extremely fast (Moore's tower bounds), so explicit counting is ineffective. The preprint's argument converts approximate invariance of a finite set $A\subset F$ into an approximate fixed point of a Lipschitz map on a Hilbert ball, via recursively defined Hilbert-valued colours of dyadic partitions. The delicate points are exact covariance of normalized restrictions under the group action (equation (2.2), p. 4) and controlling the diagonal and nested pairs in the correlation expansion, which yields a uniform lower bound on the relative boundary of every finite set (Proposition 2.3, p. 5).

Formalization scope

• UnitInterval is Set.Icc (0:ℝ) 1; an element of F is a homeomorphism of it that is StrictMono and has a DyadicPLWitness: finitely many strictly increasing dyadic knots from $0$ to $1$ and integer exponents with the affine formula on each piece.
• The goal asserts that some group structure on F exists whose multiplication is composition ((h * g) x = h (g x)); since multiplication is fixed, this structure is unique.
• InvariantMean F is a real-linear functional on lp (fun _ : F => ℝ) ∞ that is positive, sends the constant $1$ to $1$, and is invariant under leftPull h, $\varphi\mapsto(g\mapsto\varphi(hg))$; the goal is ¬ Nonempty (InvariantMean F).
• No generating set, Følner constant or boundary bound is fixed in the statement, so the goal is stable under improved constants.

Selected references

• OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thompsons-group-F-is-nonamenable-September-23-2026/paper.pdf
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, Enseign. Math. (2) 42 (1996), 215–256. https://www.imo.universite-paris-saclay.fr/~emmanuel.breuillard/Cannon.pdf
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985), 485–498. https://doi.org/10.1007/BF01388519
• K. S. Brown, R. Geoghegan, An infinite-dimensional torsion-free $\mathrm{FP}_\infty$ group, Invent. Math. 77 (1984), 367–381. https://doi.org/10.1007/BF01388451
• Y. Benyamini, Y. Sternfeld, Spheres in infinite-dimensional normed spaces are Lipschitz contractible, Proc. Amer. Math. Soc. 88 (1983), 439–445. https://doi.org/10.1090/S0002-9939-1983-0699410-7
• E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. https://doi.org/10.7146/math.scand.a-10442
• J. T. Moore, Amenability and Ramsey theory, Fund. Math. 220 (2013), 263–280. https://doi.org/10.4064/fm220-3-6
• J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013), 633–651. https://doi.org/10.4171/GGD/201
• U. Haagerup, K. K. Olesen, Non-inner amenability of the Thompson groups T and V, J. Funct. Anal. 272 (2017), 4838–4852. https://doi.org/10.1016/j.jfa.2017.02.003
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. https://doi.org/10.1215/ijm/1255380675

Motivation: when do partial observations of a permutation force full randomness?

Many random permutations are analysed through what they do to a few labels at a time: the joint positions of $k$ chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most $n-2$ labels, yet it is at total-variation distance $1/2$ from uniform on $S_n$. Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.

Timeline

• 1954 — Frame, Robinson and Thrall prove the hook-length formula for the degrees of irreducible representations of $S_n$ (Canad. J. Math. 1954).
• 1981 — Diaconis and Shahshahani analyse random transpositions by Fourier analysis on $S_n$, establishing the upper-bound-lemma framework (Z. Wahrsch. 1981).
• 2004 — Liebeck and Shalev show that the Witten zeta sums $\sum_{\lambda\vdash n}(f^\lambda)^{-u}$ tend to $2$ for every fixed $u>0$ (J. Algebra 2004).
• 2009, 2013 — Morris uses entropy and trajectory comparison to prove $O((\log n)^4)$ and $O((\log n)^3)$ mixing bounds for the Thorp shuffle (Ann. Probab. 2009; CPC 2013).
• 2014–2015 — Czumaj and Vöcking show that a fixed fraction of the cards randomizes in $O((\log n)^2)$ layers; Czumaj obtains full-permutation sampling by recursively applying partial randomizers on shrinking sets.
• 2026 — The OpenAI preprint From partial permutation information to Fourier bounds (OpenAI Math Release, September 26, 2026) proves that coset caps for complementary blocks control every Fourier matrix (Theorem 1.1). It has not been peer reviewed.

Setting

Let $X$ be a finite set of $n$ labels and $G=\mathrm{Sym}(X)$, acting as maps from initial labels to final positions. For $M\subseteq X$, let $H_M\le G$ be the block subgroup of permutations that fix every label outside $M$. Two permutations have the same images on $X\setminus M$ exactly when they lie in the same left coset $gH_M$, so a bound on the law of those images is a bound on coset masses.

For a nonnegative weight $f$ on $G$ and a unitary representation $\rho$ of $G$ on a finite-dimensional complex inner-product space $V$, the Fourier transform is $\widehat f(\rho)=\sum_{g\in G}f(g)\rho(g)$, with $D=\dim V$. The Hilbert–Schmidt norm is unnormalized, $\|A\|_{\mathrm{HS}}^2=\operatorname{tr}(A^*A)$. For $u>0$ the symmetric degree constant is

$$C_u=\sup_{m\ge1}\ \sum_{\lambda\vdash m} D_\lambda^{-u},$$

where $D_\lambda$ ranges over the degrees of the irreducible complex representations of $S_m$.

Formalization targets

Goal: complementary cosets control Fourier matrices (Theorem 1.1)

Partition $X$ into $b\ge1$ nonempty blocks $M_1,\dots,M_b$ and put $H_i=H_{M_i}$. Let $f\ge0$ on $G$ have total mass at most one and satisfy

$$f(gH_i)\le \frac{B}{[G:H_i]}\qquad(g\in G,\ 1\le i\le b).$$

Then for every $u>0$ and every irreducible unitary $\rho$ of degree $D$,

$$\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b} \qquad\text{and}\qquad \|\widehat f(\rho)\|_{\mathrm{op}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b}.$$

No restriction is placed on the block sizes or on multiplicities in the restriction of $\rho$ to $H_1\times\dots\times H_b$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of $S_n$. With $b=8$ and $u=1$ it gives $\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le 8C_1D^{-5/8}$, which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of $7n/8$ labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in $O(\log n)$ shuffles. The statement concerns arbitrary laws on $S_n$ and does not depend on any shuffle.

Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.

Difficulty

The natural approach decomposes $\rho$ restricted to $H_1\times\dots\times H_b$ into tensor products of irreducibles of the blocks and bounds $\widehat f(\rho)$ on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in $D$. The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant $C_u$ is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.

Formalization scope

• $X$ is an arbitrary Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.
• The coset cap is LeftCosetCap f H B: for every $g$, $\sum_{h\in H}f(gh)\le B/[G:H]$, with the index H.index.
• $\rho$ is any irreducible representation on a finite-dimensional complex inner-product space with $\langle\rho(g)x,\rho(g)y\rangle=\langle x,y\rangle$; the Fourier transform is complexFourier ρ f; hsNormSq is $\operatorname{Re}\operatorname{tr}(A^*A)$; the operator norm is that of the associated continuous linear map; $D$ is Module.finrank ℂ V and the exponent is a real power.
• Irreducible representations of $S_m$ are indexed by the isotypic components of the regular representation of Equiv.Perm (Fin m), and $C_u$ is symmetricDegreeConstant u, an sSup over $m\ge1$. The supremum is finite for every $u>0$; a solver must prove this boundedness, since sSup of an unbounded real set would be $0$.
• Needed infrastructure: isotypic decomposition and Schur's lemma for finite groups, degree bounds for $S_m$ (hook-length or tableau counting), and uniform Witten zeta bounds. The degree layer is reusable for any random walk on $S_n$.

Selected references

• J. S. Frame, G. de B. Robinson and R. M. Thrall, The hook graphs of the symmetric group, Canad. J. Math. 6 (1954), 316–324. https://doi.org/10.4153/CJM-1954-030-1
• P. Diaconis and M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981), 159–179. https://doi.org/10.1007/BF00535487
• G. D. James, The Representation Theory of the Symmetric Groups, Lecture Notes in Math. 682, Springer, 1978.
• B. E. Sagan, The Symmetric Group, 2nd ed., Graduate Texts in Math. 203, Springer, 2001. https://doi.org/10.1007/978-1-4757-6804-6
• M. W. Liebeck and A. Shalev, Fuchsian groups, coverings of Riemann surfaces, subgroup growth, random quotients and random walks, J. Algebra 276 (2004), 552–601. https://doi.org/10.1016/S0021-8693(03)00515-5
• E. O. Thorp, Nonrandom shuffling with applications to the game of faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
• B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
• B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
• A. Czumaj and B. Vöcking, Thorp shuffling, butterflies, and non-Markovian couplings, ICALP 2014, LNCS 8572, 344–355. https://doi.org/10.1007/978-3-662-43948-7_29
• A. Czumaj, Random permutations using switching networks, STOC 2015, 703–712. https://doi.org/10.1145/2746539.2746629
• OpenAI, From partial permutation information to Fourier bounds, OpenAI Math Release preprint, September 26, 2026 (source; Theorem 1.1, p. 1–2; Corollary 3.6, p. 9). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/From-partial-permutation-information-to-Fourier-bounds-September-26-2026/main.pdf

Motivation: Kaplansky's zero-divisor conjecture

For a field $K$ and a group $G$, the group algebra $K[G]$ consists of finite formal sums $\sum_g a_g g$ with $a_g\in K$, multiplied by extending the group law bilinearly. If $g\in G$ has finite order $m>1$, then $(1-g)(1+g+\dots+g^{m-1})=0$, so $K[G]$ has zero divisors. Kaplansky's zero-divisor conjecture asserts that this is the only source: if $G$ is torsion-free, $K[G]$ has no nonzero zero divisors. Together with the unit and idempotent conjectures it is one of the central problems connecting ring theory, group theory and topology, and positive answers are known for large classes of groups (elementary amenable groups, groups with the unique-product property, torsion-free 3-manifold groups).

Timeline

• 1940 — Higman's thesis raises the question and proves the domain property for groups in which every nontrivial subgroup maps onto $\mathbb Z$ (Higman, Proc. LMS 1940); the thesis formulation is reproduced by Sandling (1981).
• 1956/1957 — Kaplansky poses the problem (Problem 6 in Problems in the theory of rings, National Research Council, 1957).
• 1987 — Rips and Segev construct torsion-free groups without the unique-product property, removing the standard route to the conjecture (J. Algebra 1987); Steenbock gives a graphical small-cancellation treatment (J. Algebra 2015).
• 1988 — Kropholler, Linnell and Moody prove the conjecture for torsion-free elementary amenable groups (Proc. AMS 1988).
• 2021 — Gardam disproves the related unit conjecture over $\mathbb F_2$ (Ann. of Math. 2021), and later over $\mathbb C$ (arXiv:2312.05240, 2024). A nontrivial unit is not a zero divisor, so the zero-divisor conjecture remained open.
• 2026 — Fisher and Sánchez-Peralta prove the domain conclusion for torsion-free 3-manifold groups and division-ring embeddings for virtually compact special groups (J. Comb. Algebra 2026).
• 2026 — An OpenAI preprint, A Torsion-Free Group Algebra with Zero Divisors (OpenAI Math Release, September 23, 2026), claims a finitely presented torsion-free group $G$ with a finite 2-dimensional classifying space such that $\mathbb F_2[G]$ has nonzero zero divisors. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A group $G$ is torsion-free if $g^n=1$ with $n\ge1$ implies $g=1$. It is finitely presented if it has a presentation with finitely many generators and relations. A classifying space (or $K(G,1)$) for $G$ is a path-connected space $X$ with $\pi_1(X)\cong G$ whose universal cover is contractible; it is finite two-dimensional if it is a finite CW complex with cells only in dimensions $\le 2$. A group with a finite-dimensional classifying space is automatically torsion-free, but the formal goal asks for both properties explicitly.

The coefficient field is $\mathbb F_2=\mathbb Z/2$, and $\mathbb F_2[G]$ is Mathlib's MonoidAlgebra (ZMod 2) G.

Formalization targets

Goal: a counterexample to the zero-divisor conjecture (Theorem 1.1)

There exist a group $G$ and $\alpha,\beta\in\mathbb F_2[G]$ such that

$$G\ \text{finitely presented},\quad G\ \text{torsion-free},\quad G\ \text{has a finite 2-dimensional } K(G,1),\quad \alpha\neq0,\ \beta\neq0,\ \alpha\beta=0.$$

This is the full Theorem 1.1 of the source, including its "Moreover" clause. The source proves existence probabilistically; it does not exhibit a concrete presentation. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If correct, the theorem disproves Kaplansky's zero-divisor conjecture over $\mathbb F_2$, a problem open since the 1940s, and shows that torsion-freeness — even together with finite presentability and a 2-dimensional classifying space — does not force $K[G]$ to be a domain. It implies that $G$ fails the unique-product property, and it bears on the implications among the Kaplansky conjectures (zero divisors, units, idempotents) and on approaches through the Atiyah conjecture and division-ring embeddings.

Formalizing it. The claim refutes a long-standing conjecture by an intricate probabilistic and topological construction, which is a strong case for machine verification. A full formal proof needs the probabilistic existence argument, planar separation, and asphericity of a 2-complex — none of which is a routine Mathlib application. Partial contributions (e.g. the characteristic-2 cancellation argument once asphericity and root separation are assumed, or the torsion-freeness of groups with finite-dimensional $K(G,1)$) are welcome. A related machine-checked result exists only for the weaker non-unique-product property of Gardam's $\widetilde A_2$ lattice (Mian–Siddique 2026).

Difficulty

Writing down $\alpha,\beta$ whose product cancels in characteristic two is the easy part; the source does this by a parity argument on a graph of simultaneous steps. The hard part is two safeguards in the quotient group: both factors must remain nonzero (no vertex label other than the root can collapse to the identity), and the group must be torsion-free, which the source obtains by proving the 2-complex is aspherical. Standard tools — small-cancellation or CAT(0) criteria — are not applied; instead the source must exclude spherical arrangements of arbitrarily many paths of arbitrary length, which a union bound over sizes cannot handle.

Formalization scope

• TorsionFree G is the plain group-theoretic notion ($g^n=1$, $n>0$ implies $g=1$); finite presentability is Group.IsFinitelyPresented.
• HasFiniteTwoDimensionalClassifyingSpace G asks for a Hausdorff, path-connected space $X$ with a finite CW structure on all of $X$, no cells above dimension $2$, at least one $2$-cell, a group isomorphism $G\simeq\pi_1(X,x)$, and a surjective covering map from a contractible space onto $X$ (so $X$ is aspherical). Requiring a $2$-cell excludes only the case of free groups, whose group algebras are domains.
• The witnessing group lives in Type and is existentially quantified together with its group structure; the zero divisors are elements of MonoidAlgebra (ZMod 2) G.
• A trivializing reading is excluded because all three group properties and both nonvanishing conditions are required simultaneously.
• Infrastructure needed: CW complexes and covering spaces (partially in Mathlib), the fundamental group of a 2-complex built by attaching cones, Hurewicz/Whitehead-type asphericity arguments, and random graph constructions.

Selected references

• G. Higman, The units of group-rings, Proc. London Math. Soc. (2) 46 (1940). https://doi.org/10.1112/plms/s2-46.1.231
• I. Kaplansky, Problems in the theory of rings, Report of a Conference on Linear Algebras (1956), National Research Council, 1957.
• E. Rips and Y. Segev, Torsion-free group without unique product property, J. Algebra (1987). https://doi.org/10.1016/0021-8693(87)90125-6
• P. H. Kropholler, P. A. Linnell and J. A. Moody, Applications of a new K-theoretic theorem to soluble group rings, Proc. Amer. Math. Soc. (1988). https://doi.org/10.2307/2046771
• M. Steenbock, Rips–Segev torsion-free groups without the unique product property, J. Algebra (2015). https://doi.org/10.1016/j.jalgebra.2015.05.004
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021). https://doi.org/10.4007/annals.2021.194.3.9
• G. Gardam, Non-trivial units of complex group rings, preprint, 2024. https://arxiv.org/abs/2312.05240v2
• S. P. Fisher and P. Sánchez-Peralta, Division rings for group algebras of virtually compact special groups and 3-manifold groups, J. Comb. Algebra (2026). https://doi.org/10.4171/JCA/89
• I. Mian and S. Siddique, A machine-checked proof that Gardam's $\widetilde A_2$ lattice does not have unique products, preprint, 2026. https://arxiv.org/abs/2609.22380v1
• OpenAI, A Torsion-Free Group Algebra with Zero Divisors, 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-Torsion-Free-Group-Algebra-with-Zero-Divisors-September-23-2026/paper.pdf

This mission formalizes A. Erschler and T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155 (doi:10.1007/s00222-019-00922-0). Page and result numbers are those of arXiv:1802.09077v2.

Motivation

The growth function $v_{\Gamma,S}(n)$ of a group $\Gamma$ generated by a finite set $S$ counts the elements of word length at most $n$. A group has polynomial growth, exponential growth, or intermediate growth, strictly between the two. Grigorchuk's groups $G_\omega$ were the first groups of intermediate growth, and for forty years the precise asymptotics of their growth was open, even for the most studied of them, the first Grigorchuk group $G_{\mathbf{012}}$. Erschler and Zheng determine its growth exponent:

$$\lim_{n\to\infty}\frac{\log\log v_{G,S}(n)}{\log n} = \alpha_0,$$

where $\alpha_0 = \log 2/\log\lambda_0 \approx 0.7674$ and $\lambda_0$ is the positive root of $X^3 - X^2 - 2X - 4$. The upper bound was known; the new lower bound comes from random walks.

Timeline.

• 1980: Grigorchuk introduces the first Grigorchuk group, a finitely generated infinite periodic group (doi:10.1007/BF01078416).
• 1983: Kaimanovich and Vershik relate the Poisson boundary of a random walk to its asymptotic entropy (doi:10.1214/aop/1176993497); with Derriennic's work (Astérisque 74, 1980) this is the entropy criterion the lower bound rests on.
• 1984: Grigorchuk defines the family $G_\omega$, proves intermediate growth, and shows $\exp(cn^{1/2}) \le v_{G,S}(n) \le \exp(Cn^{\log_{32}31})$ for $G_{\mathbf{012}}$ (doi:10.1070/IM1985v025n02ABEH001281).
• 1997: Leonov raises the lower exponent to $0.504$ (Mat. Stud. 8 (1997) 192–197; no DOI).
• 1998: Bartholdi proves $v_{G,S}(n) \le \exp(Cn^{\alpha_0})$ (doi:10.1155/S1073792898000622); Muchnik and Pak prove upper bounds of this kind for more general $\omega$ in 2001 (doi:10.1142/S0218196701000450).
• 2001: Bartholdi raises the lower exponent to $0.5157$ (doi:10.1142/S0218196701000395); Brieussel's thesis (2008) reaches $0.5207$.
• 2020: Erschler and Zheng prove $v_{G,S}(n) \ge \exp(c_\epsilon n^{\alpha_0 - \epsilon})$, matching Bartholdi's upper bound.

Setting

$\mathsf T$ is the rooted binary tree, its vertices the finite words over $\{0, 1\}$ and its boundary $\partial\mathsf T$ the infinite rays; automorphisms act on the right, $x \mapsto x \cdot g$. For a string $\omega = \omega_0\omega_1\ldots \in \{\mathbf 0, \mathbf 1, \mathbf 2\}^{\mathbb N}$, the Grigorchuk group $G_\omega$ is generated by certain automorphisms of $\mathsf T$, $S = \{a, b_\omega, c_\omega, d_\omega\}$. The automorphism $a$ changes the first letter of a word, swapping the two subtrees of the root, while $b_\omega, c_\omega, d_\omega$ are defined as follows. They fix $1^\infty$, and on a word $1^k0v$ each of them either changes the first letter of $v$ or does nothing, depending on the letter $\omega_k$ of the string: if $\omega_k = \mathbf 0$, then $b_\omega$ and $c_\omega$ change it and $d_\omega$ does nothing; if $\omega_k = \mathbf 1$, then $b_\omega$ and $d_\omega$ change it and $c_\omega$ does nothing; if $\omega_k = \mathbf 2$, then $c_\omega$ and $d_\omega$ change it and $b_\omega$ does nothing. The string $\omega = (\mathbf{012})^\infty$ gives the first Grigorchuk group.

Assumption $\mathrm{Fr}(D)$ asks that every block $\omega_{kD}\ldots\omega_{kD+D-1}$ contain $\mathbf{201}$ or $\mathbf{211}$; it implies that $G_\omega$ is periodic. $L^\omega_n$ is the sum of the entries of $M_{\omega_0}\cdots M_{\omega_{n-1}}$ for three explicit $3\times 3$ matrices: the lengths of the words the substitutions of §2 produce.

A measure on a group is a function $\mu \ge 0$ of total mass 1. A function $f$ is $\mu$-harmonic if $f(x) = \sum_y f(xy)\mu(y)$, the entropy is $H(\mu) = -\sum_g \mu(g)\log\mu(g)$, and the Poisson boundary of $(\Gamma, \mu)$ is non-trivial when some bounded $\mu$-harmonic function is not constant.

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

For every $\epsilon > 0$ there is $C > 0$ such that for every $\omega$ satisfying $\mathrm{Fr}(D)$ there is a non-degenerate symmetric probability $\mu$ on $G_\omega$ of finite entropy and non-trivial Poisson boundary with, writing $l_S$ for the word length,

$$\mu\{g : l_S(g) > L^\omega_n\} \le C\,2^{-(1-\epsilon)n} \quad (n \ge 1),$$

and hence, for some $c > 0$ depending on $\omega$,

$$v_{G_\omega,S}(L^\omega_n) \ge \exp\bigl(c\,2^{(1-\epsilon)n}\bigr) \quad (n \ge 1).$$

The printed theorem has $n$ in place of $2^n$; that version is weaker and does not give the exponent.

The abstract's headline, that the volume exponent of the first Grigorchuk group is $\alpha_0$, is the last milestone, ErschlerZheng.hasVolumeExponent_firstString_alpha0: Theorem A combined with Bartholdi's upper bound.

Milestones

• §2: the entropy criterion and the Shannon theorem for random walks (Kaimanovich–Vershik, external), the Avez entropy, and Lemma 2.1: a finite-entropy measure with non-trivial boundary forces $v_{\Gamma,S}(n\phi(\varrho_n)) \ge e^{cn}$ for all large $n$.
• §3: germs of the action on $\partial\mathsf T$, the groupoid $\mathcal H(H_o)$, Fact 3.5, and Proposition 3.3: if the walk's germ at $1^\infty$ stabilizes modulo a proper subgroup, the Poisson boundary is non-trivial.
• §§2.4–2.5, 5, 7.1: the groups $G_\omega$ and their substitutions, the Schreier graph of $1^\infty$ and its Gray-code distance, cube independence, Facts 7.3–7.6 and Lemma 7.5.
• §7.2–7.6: the conjugated elements $\tilde g^v_j$ and the measures $\mu_\beta$ (Lemmas 7.7, 7.9), kernel and Green-function bounds (Propositions 7.11, 7.12, 7.18, 7.19, Lemmas 7.15–7.17, 7.21), and Theorem 7.13: $\mu_\beta$ has non-trivial Poisson boundary.
• §8: Lemma 8.1, Corollary 8.2, the goal, and after it Theorem A and the exponent of $G_{\mathbf{012}}$, with Bartholdi's upper bound as an external milestone.

Significance

The result. It answers the growth question for $G_{\mathbf{012}}$: the exponent is $\alpha_0$. It gives near-optimal lower bounds for every $G_\omega$ with $\omega$ satisfying $\mathrm{Fr}(D)$, and its measures are the first examples on these groups of random walks with non-trivial Poisson boundary and power-law tails. The method, building a measure with non-trivial boundary and controlled tail and reading off a volume bound from entropy, applies beyond Grigorchuk groups.

Formalizing it. No machine-checked proof of these results exists; Mathlib has neither Grigorchuk groups nor Poisson boundaries. On this platform the mission builds on the published bundle of the first Grigorchuk group, Garrido_Grigorchuk, from the Garrido Amenable Groups III mission, and on Chou's word balls, Chou_Growth. The general Markov-chain inputs (Cheeger, Faber–Krahn and Nash inequalities, and off-diagonal heat-kernel bounds) are separate standalone theorems.

Difficulty

Lower bounds by anti-contraction of word lengths (Grigorchuk, Leonov, Bartholdi, Brieussel) stall well below $\alpha_0$. The entropy route needs a measure with non-trivial Poisson boundary, but on a group of subexponential growth every finitely supported symmetric measure has trivial boundary. The measure must therefore have heavy tails, and the lower bound it gives is only as good as its tail decay. The difficulty is to make the tails as light as $\alpha_0$ allows while keeping the boundary non-trivial. That needs a non-homogeneous random walk on the Schreier graph of $1^\infty$ to be transient enough to fix the germ at $1^\infty$, and heat-kernel bounds for jump processes that are not translation invariant.

Formalization scope

Tree automorphisms are permutations of finite words (Garrido.BinaryTreeAut), acting on rays on the right by $x \cdot g = g^{-1}(x)$, so that $x \cdot (gh) = (x \cdot g) \cdot h$. A measure is a function $G \to \mathbb R$ summed with tsum; it is symmetric when $\mu(g^{-1}) = \mu(g)$, and non-degenerate when its support generates $G$ as a semigroup. The Poisson boundary is non-trivial (HasNontrivialPoissonBoundary) when some bounded harmonic function is not constant on the submonoid generated by the support of $\mu$; for the non-degenerate measures of the goal this is the criterion of p. 2 (ErschlerZheng.hasNontrivialPoissonBoundary_iff_exists_bounded_isHarmonic_ne_of_isNondegenerate). Growth is evaluated at real radii. The definitions are in the bundles ErschlerZheng_Walks, ErschlerZheng_Germs, ErschlerZheng_Grigorchuk and ErschlerZheng_Construction.

Where a statement departs from the print, its milestone description says so: under Correction when the printed claim is false or undefined ((2.3), the substitutions on p. 15, Fact 3.5, the Gray code on p. 34, Fact 7.3, $(\mathbf{012})^\infty \in \mathrm{Fr}(3)$ on p. 59, Lemmas 7.9, 7.17 and 7.21, Propositions 7.12 and 7.18, and the uniform digits on p. 55), and under Formalization note when it reads the print or strengthens it (Lemma 2.1, Proposition 7.19, Corollary 8.2, and the constants $\lambda_0$ and $\alpha_0$). The goal is Theorem 8.3 with the $2^n$ its proof gives, as above.

The goal is not trivial: its measure must be a non-degenerate symmetric probability on $G_\omega$, and the growth bound is about the generating set $S$ itself.

Reusable beyond this mission: Grigorchuk groups $G_\omega$ for every $\omega$ with their substitutions, germ groupoids of group actions, entropy and the Poisson boundary of random walks.

What is left out. Theorems B and C, Corollary 8.4 and the other applications in §8 to general $\omega$, which need the upper bounds of Bartholdi and Erschler (doi:10.5802/aif.2902); the side results of §§4–6 on the first Grigorchuk group (Theorem 5.7 and the critical constant of recurrence); the illustrative Examples 2.4 and 7.10; and the remarks and questions of §9. They are planned for a sequel mission.

Selected references

• A. Erschler, T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155. doi:10.1007/s00222-019-00922-0; arXiv:1802.09077
• R. I. Grigorchuk, Burnside's problem on periodic groups, Funct. Anal. Appl. 14 (1980) 41–43. doi:10.1007/BF01078416
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985) 259–300. doi:10.1070/IM1985v025n02ABEH001281
• V. A. Kaimanovich, A. M. Vershik, Random walks on discrete groups: boundary and entropy, Ann. Probab. 11 (1983) 457–490. doi:10.1214/aop/1176993497
• Y. Derriennic, Quelques applications du théorème ergodique sous-additif, Astérisque 74 (1980) 183–201. numdam
• L. Bartholdi, The growth of Grigorchuk's torsion group, Internat. Math. Res. Notices 1998, no. 20, 1049–1054. doi:10.1155/S1073792898000622
• R. Muchnik, I. Pak, On growth of Grigorchuk groups, Internat. J. Algebra Comput. 11 (2001) 1–17. doi:10.1142/S0218196701000450
• L. Bartholdi, Lower bounds on the growth of a group acting on the binary rooted tree, Internat. J. Algebra Comput. 11 (2001) 73–88. doi:10.1142/S0218196701000395
• M. T. Barlow, A. Grigor'yan, T. Kumagai, Heat kernel upper bounds for jump processes and the first exit time, J. Reine Angew. Math. 626 (2009) 135–157. doi:10.1515/CRELLE.2009.005
• L. Bartholdi, A. Erschler, Groups of given intermediate word growth, Ann. Inst. Fourier 64 (2014) 2003–2036. doi:10.5802/aif.2902

Motivation

Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.

The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).

Setting

Let $\mathcal G$ be a finite Abelian group, written additively, with zero $\bar 0$ and order $D=|\mathcal G|$, and let $\mathcal G^+=\mathcal G-\{\bar 0\}$. For a right-hand side $g_0\in\mathcal G$, the group equation asks for nonnegative integers $t(g)$, $g\in\mathcal G^+$, with

$$\sum_{g\in\mathcal G^+}t(g)\cdot g=g_0 .$$

Its solution set is $T(\mathcal G,g_0)$; when $g_0=\bar 0$, the zero solution is excluded, as stipulated on p. 474. Each solution is a point of $\mathbb R^{\mathcal G^+}$, a space of dimension $n'=D-1$, and the master polyhedron $P(\mathcal G,g_0)$ is the convex hull of $T(\mathcal G,g_0)$. Gomory reads a solution $t$ as a path from $\bar 0$ to $g_0$ that uses the element $g$ exactly $t(g)$ times; with arc lengths $\pi(g)$ its length is $\pi\cdot t=\sum_g\pi(g)t(g)$.

An inequality $\pi\cdot t\ge\pi_0$, written $(\pi,\pi_0)$, is a face of $P(\mathcal G,g_0)$ when $\pi\ne0$, every $t\in T(\mathcal G,g_0)$ satisfies it, and the solutions on the hyperplane $\pi\cdot t=\pi_0$ generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with $\pi\cdot t=\pi_0$ are the minimal paths.

Let $\psi$ be a homomorphism of $\mathcal G$ onto a second finite Abelian group $\mathcal H$, with kernel $\mathcal K=\psi^{-1}(\bar 0)$. A coefficient vector $\pi'$ on $\mathcal H^+$ is lifted to $\mathcal G^+$ by

$$\pi(g)=\pi'(\psi g),\qquad \pi'(\bar 0)=0,$$

so that every element of the kernel gets coefficient $0$.

Formalization targets

Goal: THEOREM 19 (p. 486)

If $\psi g_0\ne\bar 0$ and $(\pi',\pi_0)$ is a face of $P(\mathcal H,\psi g_0)$ with $\pi_0>0$, then

$$\Big(\pi,\pi_0\Big),\quad \pi(g)=\pi'(\psi g),\quad\text{is a face of } P(\mathcal G,g_0).$$

For instance, the face $t_1\ge1$ of $P(\mathcal G_2,(1))$ lifts through reduction mod 2 to the face $t_1+0t_2+t_3+0t_4+t_5\ge1$ of $P(\mathcal G_6,(5))$ (p. 488).

Milestones

1. Face criterion (p. 469, proof of THEOREM 7). For $\pi_0>0$, $(\pi,\pi_0)$ is a face iff it is valid on $T$ and $n'$ linearly independent solutions satisfy $\pi\cdot t=\pi_0$.
2. Pushing paths forward (p. 486). A solution $t$ for $\mathcal G$ maps to the solution $\tau(h)=\sum_{g\in\psi^{-1}h}t(g)$ for $\mathcal H$ of the same length; hence the lifted inequality is valid.
3. Lifted minimal paths (p. 487). From a minimal path $\tau$ for $\mathcal H$ and a kernel element $k$, the path $T_k(\tau)$ is a minimal path for $\mathcal G$.
4. Rank $D-1$ (pp. 487–488). The lifted inequality has $D-1$ linearly independent minimal paths.

Further result: THEOREM 20 (p. 489)

Conversely, a face $(\pi,\pi_0)$ of $P(\mathcal G,g_0)$ with $\pi_0>0$ and $\pi(g)=0$ for some $g\ne\bar0$ is the lift of a face of $P(\mathcal H,\psi g_0)$ for some $\psi$ of $\mathcal G$ onto a group $\mathcal H$ with $\psi g=\bar 0$.

Significance

THEOREMS 19 and 20 together say that the faces of $P(\mathcal G,g_0)$ with $\pi_0>0$ and a zero coefficient are exactly the faces lifted from proper quotients of $\mathcal G$. A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for $\mathcal G_{2,2}$ and $\mathcal G_{2,2,2}$ every such face is a lift of the single nontrivial face of $P(\mathcal G_2,(1))$, and for a direct sum $\mathcal G=\mathcal K_1\oplus\mathcal K_2$ every face of the polyhedron of a summand not containing $g_0$ extends to a face for $\mathcal G$ (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.

Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.

Difficulty

Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit $D-1$ affinely independent solutions on the hyperplane, while the quotient face only supplies $|\mathcal H|-1$ of them. A solution of the quotient problem does not determine a solution for $\mathcal G$; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.

The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from $\mathcal G$-paths to $\mathcal H$-paths is a linear projection from dimension $D-1$ to $|\mathcal H|-1$ and does not lift independence by itself. It also fails at $\pi_0=0$: with $\mathcal G=\mathbb Z_6$, $\mathcal H=\mathbb Z_3$, $g_0=1$, the face $t(1)\ge0$ of $P(\mathbb Z_3,(1))$ lifts to $t(1)+t(4)\ge0$, which is valid but not a face of $P(\mathbb Z_6,(1))$.

Formalization scope

The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both $\mathcal G$ and $\mathcal H$. It commits to the following readings:

• Vectors are indexed by the subtype $\{g\mid g\ne\bar0\}$, so $\bar0$ has no coordinate and the dimension of T-space is $|\mathcal G|-1$ for each group separately; solutions are $\mathbb N$-valued, nonzero, and cast to $\mathbb R$. When $g_0\ne\bar0$, the group equation already excludes the zero vector.
• "Generated by the points on the hyperplane" means that the affine span of the tight solutions equals the hyperplane $\{x:\pi\cdot x=\pi_0\}$; $\pi\ne0$ is part of the definition and $\pi_0\ge0$ is not (THEOREM 6 proves it).
• Paths are vectors and "minimal path" means a solution with $\pi\cdot t=\pi_0$.
• $\pi'(\bar0)=0$ is built into the lift; "onto" is Function.Surjective ψ, and $g_0\notin\mathcal K$ is $\psi g_0\ne\bar0$.
• Added hypothesis $\pi_0>0$ in THEOREM 19 and the rank milestone: the page omits it, and the $\mathbb Z_6\to\mathbb Z_3$ example above shows the statement is false without it.
• The face criterion is THEOREM 7's "basic feasible solution" unfolded into $n'$ linearly independent tight solutions, stated for the master polyhedron only and for nontrivial groups, where $n'>0$.
• Pushing a path forward uses $\psi g_0\ne\bar0$, the standing hypothesis of THEOREM 19, so the pushed path cannot become the excluded zero solution.
• The lifted path $T_k(\tau)$ puts its closing $1$ on the kernel element $g_0-\sum_{g\notin\mathcal K}t_k(g)\cdot g$ itself, and adds nothing when that element is $\bar0$.
• In THEOREM 20, "nontrivial" is $\pi_0>0$, the printed $(\pi_1,\pi_0)$ is read as $(\pi,\pi_0)$, and the conclusion requires $\psi g=\bar0$ for the given zero coefficient: without it the identity map would satisfy the statement.

A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.

The development needs finite sums over fibres of $\psi$, a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of $T$, $P(\mathcal G,g_0)$ and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. doi:10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proceedings of the National Academy of Sciences 53 (1965), 260–265. doi:10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. doi:10.1007/BF01584976

Motivation

Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.

The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.

Setting

Let $\mathcal G$ be a finite Abelian group with zero $0$, and let $\mathcal G^+=\mathcal G\setminus\{0\}$. For a subset $\mathcal N\subseteq\mathcal G^+$ and a right-hand side $g_0\in\mathcal G$, a group-equation solution is a nonnegative integer vector $t\in\mathbb N^{\mathcal N}$ satisfying

$$\sum_{g\in\mathcal N}t(g)g=g_0.$$

The set of solutions is $T(\mathcal G,\mathcal N,g_0)$, and the group polyhedron $P(\mathcal G,\mathcal N,g_0)$ is their convex hull in the real coordinate space $\mathbb R^{\mathcal N}$. The master polyhedron $P(\mathcal G,g_0)$ uses $\mathcal N=\mathcal G^+$. This mission concerns $g_0\ne0$; Gomory specifies a separate convention at $g_0=0$, excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.

Gomory calls $\pi\cdot x\ge\pi_0$ a face when $\pi\ne0$, all points of $P$ satisfy the inequality, and its tight points generate the entire hyperplane $\pi\cdot x=\pi_0$ by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of $T$, which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.

Formalization targets

The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector $t$ represents a path whose total group displacement is $\sum_g t(g)g$ and whose length is $\pi\cdot t$. The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For $P(\mathcal G,g_0)$, Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.

The target is Theorem 18. Fix $g_0\ne0$ and $\pi_0>0$. With $\pi(0)=0$, system (13) is

$$\begin{aligned} \pi(g_0)&=\pi_0,\\ \pi(g)+\pi(g_0-g)&=\pi_0 &&(g\in\mathcal G^+,\ g\ne g_0),\\ \pi(g)+\pi(h)&\ge\pi(g+h) &&(g,h\in\mathcal G^+),\\ \pi(g)&\ge0 &&(g\in\mathcal G^+). \end{aligned}$$

The goal asserts the full equivalence

$$\pi\cdot x\ge\pi_0\text{ is a face of }P(\mathcal G,g_0) \quad\Longleftrightarrow\quad \pi\text{ is a basic feasible solution of (13).}$$

The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; $\pi_0$ is held fixed. Gomory 1969, pp. 481–483, Theorem 18.

Significance

Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in $|\mathcal G|-1$ coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of $P(\mathcal G,g_0)$ for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.

The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.

Difficulty

Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all $|\mathcal G|-1$ coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.

Formalization scope

Lean uses a finite Abelian group and a Finset $\mathcal N$ of nonzero elements. Its real vectors have coordinates indexed by $\mathcal N$ itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in $\mathcal G$; $P$ is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes $\mathcal N$ nonempty ($n'\ge1$), as the paper does implicitly: with no coordinates every vector would be trivially basic.

Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use $\pi(0)=0$, and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of $|\mathcal G|-1$ variables.

The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for $g_0=0$ and for other sections of the paper are outside this mission's stated domain.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. DOI: 10.1016/0024-3795(69)90017-2.

This mission formalizes Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200 (doi:10.4171/GGD/347; arXiv:1308.4250v3, whose page numbers are used): the group $G_0$ generated by three explicit piecewise projective homeomorphisms of the line is nonamenable and finitely presented, the first torsion-free finitely presented counterexample to the von Neumann–Day problem.

Motivation

A discrete group is amenable when it has a finitely additive invariant probability measure on all its subsets. A group containing a nonabelian free subgroup is not amenable, and von Neumann and Day asked whether the converse holds. The counterexamples found before Monod's work are built from torsion groups by elaborate inductive constructions. Monod (2013) found nonamenable groups without free subgroups among piecewise projective homeomorphisms of the line. Lodha and Moore isolate in Monod's group $H$ a subgroup with three explicit generators and nine explicit relations.

Timeline.

• 1929: von Neumann introduces amenability for groups (Fund. Math. 13, no DOI).
• 1950: Day poses the problem in print, attributing it to von Neumann (doi:10.1090/S0002-9947-1950-0044031-5).
• 1980: Ol'shanskii's counterexample (doi:10.1070/RM1980v035n04ABEH001876); soon after, Adyan shows certain Burnside groups are counterexamples (doi:10.1070/IM1983v021n03ABEH001799).
• 2003: Ol'shanskii and Sapir, the first finitely presented counterexample (doi:10.1007/s10240-002-0006-7); Ivanov gives another in 2005 (doi:10.1007/s10711-004-2826-8). Both are torsion-by-cyclic.
• 2013: Monod's groups $H(A)$ of piecewise projective homeomorphisms, nonamenable without free subgroups (doi:10.1073/pnas.1218426110); formalized on this platform in the Monod mission.
• 2016: Lodha and Moore, a torsion-free finitely presented counterexample (doi:10.4171/GGD/347).
• 2020: Lodha, a nonamenable group of type $F_\infty$ in the same family (doi:10.1112/topo.12172).

Setting

The generators act on the real line: $a(t) = t + 1$, and $b$, $c$ are the piecewise projective maps of p. 2 (aFun, bFun, cFun). As homeomorphisms of the projective line $\mathbb R \cup \{\infty\}$ (a, b, c) they generate $G_0$ (G0), inside the group where the published Monod bundle defines $H$ (Monod.Hpp).

Lodha and Moore move to infinite binary sequences through the continued-fraction map $\Phi$ (Phi), under which $a$, $b$, $c$ become functions $x$, $x_1$, $y_{10}$ of sequences (Proposition 3.1). There $x_s$ and $y_s$ are $x$ and $y$ acting on the sequences that extend $s$. $G$ is the group generated by all $x_s$ and $y_s$, $G_0$ the group generated by the $x_s$ and the $y_s$ with $s$ not constant, and $R$ the five families of relations (1)–(5) among them. Products are taken left to right, as in the paper.

Section 5 rewrites words in the generators by explicit substitutions into standard forms and sufficiently expanded standard forms, and tracks them through strings in $0$, $1$, $y$, $y^{-1}$; these notions form the second definitions bundle.

Formalization targets

Goal: Theorem 1.1

$$\neg\,\text{IsAmenable}(G_0) \ \wedge\ G_0 \text{ is finitely presented}.$$

Milestones

• Nonamenability (§2): Lodha and Moore's definition of a $\mu$-amenable equivalence relation, with its equivalence to amenability (Connes, Feldman and Weiss, whose theorem is published as ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel) as two milestones; Theorems 2.1 (Zimmer) and 2.2 (Carrière and Ghys) as printed; the group $K = \langle t+1, 2t, -1/t\rangle$; and the identities and orbit comparison of p. 4.
• Presentations (§3): Proposition 3.1, the identification of $a$, $b$, $c$ with $x$, $x_1$, $y_{10}$, the relations (1)–(5), the presentation of $F$ they contain, Propositions 3.4 and 3.5, the reduction to a finite presentation, the three-generator presentation of $G_0$, and Theorem 3.3.
• Section 5: Lemmas 5.2, 5.3, 5.4, 5.6, 5.9, 5.10 and 5.11.

Significance

The result. $G_0$ settles the finitely presented von Neumann–Day problem with a group that is torsion-free, has explicit generators and relations, and acts by piecewise projective maps, so its elements can be described by labeled tree diagrams much as those of Thompson's group $F$. It shows that $\langle a, b, c\rangle$ shares the combinatorics of $F$ without its unresolved amenability question.

Formalizing it. Before this mission none of the paper was formalized. The Monod mission's milestones supply the setting, and the case of Carrière and Ghys that Monod uses is already proved there by an elementary argument (Monod.not_isAmenableRel_mob).

Difficulty

Nonamenability is a short reduction to Theorem 2.2, which in general is deep. Finite presentation is the bulk: one must show that every word that evaluates to the identity can be reduced to an $X$-word by the substitutions of §5, through a well-founded ordering on standard forms (Lemma 5.6) and an analysis of how $y$ acts on binary expansions (Lemmas 5.9–5.11).

Formalization scope

Lean representation and conventions.

• Sequences are List Bool (finite) and Stream' Bool (infinite). $x$ is explicit; $y$ and $y^{-1}$ are defined by the recursion of p. 5, digit by digit.
• The groups on sequences are subgroups of the opposite of the permutation group of Stream' Bool, so that products are left to right as in the paper. Statements about $a$, $b$, $c$ take products in the opposite of the homeomorphism group for the same reason.
• a, b, c are the homeomorphisms that agree with the formulas on $\mathbb R$, and toSeqGroup turns a bijection of sequences into a group element. Both fall back to the identity for a function that is not a homeomorphism or a bijection. Every generator is in fact one, so the fallback is never reached, and a trivial group would make the goal false.
• $\phi$ is a limit of finite continued fractions; its defining equations are a milestone.
• $K$ is a subgroup of $\mathrm{PSL}_2(\mathbb R)$ (Matrix.ProjectiveSpecialLinearGroup, with the quotient topology), as on p. 4; a class acts on the projective line by the Möbius map of either of its matrices, through the published Monod bundle.

What is left out, and deviations.

• §4 (labeled tree diagrams) is not formalized: the paper calls it "not essential for understanding the proof", and its claims are left to the reader. Remark 3.2 (history) is left out, as are two remarks in the introduction: Thurston's unpublished result that $\langle a, b\rangle$ is a copy of Thompson's group $F$ (on this platform as Monod's published theorem that $H_{\mathbb Q}(\mathbb Z) \cong F$) and the assertion that $t \mapsto t + 1/2$ and $b$ generate a nonamenable group.
• Lodha and Moore's definition of a $\mu$-amenable relation is read with the action of $\mathbb Z$ Borel; read literally, every equivalence relation with countable classes would be $\mu$-amenable (the note on the definitions explains; CountableOrbit.exists_perm_rel_iff_exists_zpow_eq is the underlying fact).
• In the three-generator presentation of p. 7, the fourth and ninth relations as printed in $a$, $b$, $c$ do not hold in $G_0$ (LodhaMoorePrinted.printed_relations_four_and_nine_ne); the milestone uses the translations of the relations in $x_s$, $y_s$ that they come from.
• The substitutions of p. 9 include the rule for $y_s^{-1}$ that the proof of Lemma 5.2 uses and the paragraph before Lemma 5.6 writes out (without it Lemmas 5.2 and 5.4 fail: it is the only substitution that applies to $y_s^{-1}$, LodhaMoorePrinted.eq_of_step_singleton_y_neg_one), and allow commuting $y_u^i$ and $y_v^j$ for any exponents, as the proof of Lemma 5.6 does (with commuting only for positive exponents, Lemma 5.6 fails: LodhaMoorePosCommute.not_forall_exists_derives_sufficientlyExpanded).
• Theorems 2.1 and 2.2 and the Connes–Feldman–Weiss equivalence are cited results, stated as Lodha and Moore apply them; the direction of the equivalence from their definition to the standard one is the easy one. Both directions assume the setting of Connes, Feldman and Weiss: a $\sigma$-finite measure, quasi-invariant for the relation.

What a development needs. Monod's mission supplies $H$, its lack of free subgroups, the elementary non-amenability argument for $\mathrm{SL}_2(A)$ with $A$ dense, and the passage from an amenable group to an amenable orbit relation. The theorem of Connes, Feldman and Weiss is published and proved (ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel); it gives the hard direction of the equivalence. The presentation of Thompson's group $F$ is published by the Cannon–Floyd–Parry mission on the two presentations of Thompson's group $F$. Proofs of any milestone are welcome.

Selected references

• Y. Lodha, J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200. doi:10.4171/GGD/347
• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
• R. J. Zimmer, Amenable ergodic group actions and an application to Poisson boundaries of random walks, J. Funct. Anal. 27 (1978) 350–372. doi:10.1016/0022-1236(78)90013-7
• Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
• J. Belk, Thompson's group F, PhD thesis, Cornell University, 2004 (no DOI). arXiv:0708.3609
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877