Amenability of Thompson's Group $F$

Amenability of Thompson's Group \$F\$

OpenAI's claim

OpenAI presents a counterexample in the selected manuscript. Thompson group $F$ is claimed to be nonamenable.

Mathematical statement of the claimed result

Result 1.

For Thompson's group $F$, consisting of increasing piecewise-linear homeomorphisms of $[0,1]$ with dyadic breakpoints and slopes powers of two, the source claims \[ F\text{ is nonamenable}. \] This is a statement about the standard discrete group $F$.

Outline of the argument

Recursive colors on dyadic partitions are designed to behave under affine transport. Finite averages of these colors give a uniform boundary discrepancy under a fixed set of group moves, contradicting the existence of Følner sets.

Formal verification

For family 248, the documented statement rules out a positive normalized invariant mean for standard dyadic Thompson $F$; it does not specify an explicit expansion constant. The listed Comparator files are ThompsonNonamenability.lean. Named declarations include OAI.ThompsonNonamenability.thompson_F_nonamenable_composition. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, Thompson's group F is nonamenable, 2026-09-23; citation key OAI:Thompsons-group-F-is-nonamenable-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 248: Lean scope.
• Comparator ThompsonNonamenability.json.
• Comparator ThompsonNonamenability.lean.
• OpenAI catalogue entry.

Amenability of Thompson's Group $F$

Definitions and mathematical statement

Thompson's group $F$ consists of increasing piecewise-linear homeomorphisms of $[0,1]$ with finitely many breakpoints, all dyadic rational, and slopes in $\{2^k:k\in{\mathbb{Z}}\}$; its operation is composition. A discrete group is amenable if it has a left-invariant mean: a positive linear functional $m:\ell^\infty(F)\to{\mathbb{R}}$ with $m(1)=1$ and $m(f\circ L_g)=m(f)$ for every $g\in F$. Equivalently, its finite subsets satisfy the Følner criterion \[ \forall E\subset F\text{ finite}\ \forall{\varepsilon}>0\ \exists A\subset F, \quad0<|A|<\infty,\quad |gA\mathbin{\triangle} A|<{\varepsilon}|A|\ (g\in E). \] Determine whether $F$ is amenable. Absence of a nonabelian free subgroup alone is not the definition and would not settle this question.

Formulation and concept references: [S1].

Short English statement

Does Thompson's group admit an averaging operation invariant under all translations, or equivalently finite sets with arbitrarily small translation boundaries?

Research attempt: endpoint quotients, supported copies, and exact boundary counts

Status and source check. This attempt neither constructs Følner sets for all of $F$ nor proves a positive uniform isoperimetric lower bound. The inherited March 2026 primary paper [S1] explicitly retains the amenability issue when discussing $C^*$-simplicity of $F$. Guba's primary account [E1] describes approaches through finite Cayley subgraphs and group-ring equations. These sources were checked on 27 September 2026; their conditional statements are not treated as a resolution.

The work below makes two natural approaches precise. First, the endpoint slope quotient gives an amenable image, but its kernel contains a copy of the original group. Second, finite Cayley subgraphs give an exact numerical criterion, but the needed quantifier ranges over all finite subsets rather than a particular sample family.

Endpoint slopes give a concrete abelian quotient. A map $f\in F$ is affine on a sufficiently small interval at each endpoint. Since it fixes both endpoints, the one-sided derivatives there are powers of two. Define \[ \sigma(f)=\left(\log_2 f'(0+),\log_2 f'(1-)\right)\in\mathbb Z^2. \tag{304.1} \] The chain rule and the fact that every map fixes the endpoints give $\sigma(fg)=\sigma(f)+\sigma(g)$.

Surjectivity can be checked with actual maps. Put \[ x_0(x)= \begin{cases} x/2,&0\leq x\leq1/2,\\ x-1/4,&1/2\leq x\leq3/4,\\ 2x-1,&3/4\leq x\leq1, \end{cases} \] and let $x_1$ be the identity on $[0,1/2]$ and equal to \[ \frac12+\frac12 x_0(2x-1) \quad\text{on }[1/2,1]. \] Both satisfy the defining dyadic and slope conditions. Their endpoint vectors are $(-1,1)$ and $(0,1)$, which generate $\mathbb Z^2$. Hence $304.1$ is onto.

Let $N=\ker\sigma$. If the endpoint slopes of $f$ are one, then its affine formula near $0$, together with $f(0)=0$, makes it the identity there; the same argument applies near $1$. Conversely a map equal to the identity near both endpoints belongs to $N$. Thus $N$ is precisely the subgroup supported away from the endpoints.

Lemma 304.1 (what the amenable quotient reduces to). For this exact sequence \[ 1\longrightarrow N\longrightarrow F\xrightarrow{\sigma}\mathbb Z^2 \longrightarrow1, \] the group $F$ is amenable if and only if $N$ is amenable.

Proof. Amenability passes to subgroups. Here is an explicit mean argument for that fact. For a subgroup $H\leq G$, choose representatives $t$ for the cosets $Ht$. Extend a bounded function $f$ on $H$ to $G$ by $\widetilde f(ht)=f(h)$. This extension is positive, preserves constants, and commutes with left translations by $H$. Composing it with a left invariant mean on $G$ gives such a mean on $H$.

For the converse, amenability is preserved by extensions. Suppose $m_N$ is a left invariant mean on a normal subgroup $N\lhd G$ and $m_Q$ is one on $Q=G/N$. For a bounded function $f$ on $G$, set \[ F_f(gN)=m_N\left(n\mapsto f(gn)\right),\qquad m_G(f)=m_Q(F_f). \] Replacing $g$ by $gn_0$ changes the inner function by left translation on $N$, so $F_f$ is well defined. Positivity and normalization are immediate. Left translation of $f$ by $h$ changes $F_f(gN)$ into $F_f(h^{-1}gN)$, so $m_G$ is left invariant. Finally $\mathbb Z^2$ is amenable, as witnessed by the square boxes $[-M,M]^2\cap\mathbb Z^2$, whose relative boundary under each fixed translation tends to zero. Apply the extension argument to $G=F$. $\square$

The lemma is exact, but it does not make the problem easier unless one can establish amenability of $N$ independently.

Lemma 304.2 (the kernel contains the whole difficulty). For every interval $I=[a,b]\subset(0,1)$ with dyadic endpoints and $a<b$, there is an embedding $\iota_I:F\to N$ supported on $I$.

Proof. Let $\alpha(u)=a+(b-a)u$ and define $\iota_I(f)$ to be $\alpha f\alpha^{-1}$ on $I$ and the identity outside it. The formulas agree at both endpoints. The slopes inside $I$ are exactly the slopes of $f$, because the two affine scaling factors cancel. A dyadic breakpoint $u$ becomes $a+(b-a)u$, which is dyadic, and the two new endpoints are dyadic. Thus the result belongs to $F$ and is the identity near $0$ and $1$. Conjugation preserves composition, and restriction to $I$ recovers $f$, proving injectivity. $\square$

Disjoint intervals yield commuting copies with trivial intersections. More precisely, maps supported in pairwise disjoint interval interiors commute, and if their product is the identity, restriction to each interior forces the corresponding factor to be the identity. Hence $F$ contains a copy of $F^r$ for every finite $r$.

In particular, the assertion that $N$ is amenable already implies amenability of its embedded copy of $F$. The endpoint quotient reduction is therefore a useful structural equivalence, but an argument that simply labels its kernel harmless would be circular. Taking a finite box in $\mathbb Z^2$ and lifting the whole inverse image also fails as a Følner construction: every fiber is infinite. Choosing one representative from each fiber makes a finite set, but multiplication then introduces uncontrolled elements of $N$ between representatives.

Explicit amenable subgroups and their Følner sets. An increasing homeomorphism of an interval has no nontrivial finite order. If $f(x)>x$ at some point, then $f^n(x)$ strictly increases with $n$; if $f(x)<x$, it strictly decreases. Either possibility rules out $f^n=1$. Thus $F$ is torsion-free.

Choose nonidentity maps $f_1,\ldots,f_r$ supported in disjoint dyadic subintervals. They commute, and restriction to supports together with torsion-freeness shows that \[ (n_1,\ldots,n_r)\longmapsto f_1^{n_1}\cdots f_r^{n_r} \] embeds $\mathbb Z^r$ in $F$. In this subgroup use the finite sets \[ A_M=\{f_1^{n_1}\cdots f_r^{n_r}:|n_i|\leq M\}. \] For each generator $f_i$, \[ \frac{|f_iA_M\mathbin{\triangle}A_M|}{|A_M|} =\frac{2}{2M+1}. \tag{304.2} \] Indeed, translation by one in coordinate $i$ removes one face of the integer box and adds the opposite face. These are complete Følner constructions for the displayed subgroups. They do not control translation by elements of $F$ which move or reshape their supporting intervals.

Lemma 304.3 (generator boundary is the exact finite test). Let $S$ be a finite symmetric generating set of a group, and let $A$ be a nonempty finite subset. Define \[ e_S(A)=\#\{(s,a)\in S\times A:sa\in A\}. \] Then \[ \sum_{s\in S}|sA\mathbin{\triangle}A| =2\left(|S|\,|A|-e_S(A)\right). \tag{304.3} \] Moreover, a sequence of finite sets with the left side divided by $|A|$ tending to zero is a Følner sequence for every fixed finite subset of the group.

Proof. Since $|sA|=|A|$, the symmetric difference has size $2(|A|-|sA\cap A|)$. Summing gives $304.3$. If $g=s_1\cdots s_\ell$, repeated use of the triangle inequality for symmetric differences, and invariance of cardinality under translation, gives \[ |gA\mathbin{\triangle}A| \leq\sum_{j=1}^{\ell}|s_jA\mathbin{\triangle}A|. \] For a fixed finite collection of words, their lengths are bounded, so small relative generator boundaries imply small relative boundaries for all of them. $\square$

Thus amenability of $F$ can be proved by finding finite subsets with $e_S(A)/|A|$ arbitrarily close to $|S|$. Nonamenability can be proved by a single positive constant $\eta$ such that \[ |S|\,|A|-e_S(A)\geq\eta|A| \] for every nonempty finite $A\subset F$. The first statement requires an unbounded family approaching zero boundary; the second requires uniformity over all finite sets.

A finite list of poor candidate sets proves neither. A list of increasingly good candidates is also insufficient without a rigorous limiting bound. Conversely, the lack of a free subgroup would not directly give $304.3$ with small boundary: the Følner condition quantifies over finite subsets, and its proof cannot be replaced by checking one particular algebraic obstruction to amenability.

Exact diagnostics. The accompanying script uses rational arithmetic to verify the displayed piecewise-linear maps, their dyadic breakpoints, and their endpoint slope vectors. It checks the box boundary formula $304.2$ and the directed-edge identity $304.3$ in finite samples. These calculations validate the explicit subgroups and the counting criterion. They do not enumerate all elements of $F$ or produce finite subsets approaching the full group's required boundary ratio.

Outcome and first gap. The endpoint quotient, extension argument, supported embeddings, and boundary identity are all proved. They explain why an amenable quotient and many amenable subgroups coexist with an unresolved amenability question for the whole group. The missing step is either a Følner family controlling a generating set of all of $F$, or a uniform positive lower bound valid for every finite subset. Neither is supplied by the current reductions. The selected problem remains unresolved by this attempt.

Sources

• S1 Anna Cascioli, Martin Gilabert Vio, Eduardo Silva, Stationary boundaries on the space of amenable subgroups and C*-simplicity, arXiv:2603.28228 $2026$. https://arxiv.org/abs/2603.28228. Formulation source.
• E1 Victor Guba, Amenability problem for Thompson's group $F$: state of the art, arXiv:2305.07113 $2023$. https://arxiv.org/abs/2305.07113. Primary source consulted 27 September 2026; finite Cayley-subgraph and related approaches are not reported as a resolution.