This mission formalizes Geoghegan's conjecture that Thompson's group $F$ is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.

Motivation

A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group $F$ the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that $F$ is not amenable; several announced solutions in each direction have not survived.

Timeline.

• 1965: Richard Thompson defines the groups $F$, $T$ and $V$ (Cannon–Floyd–Parry, p. 215).
• 1979: Geoghegan conjectures that $F$ contains no non-abelian free subgroup and is not amenable (Cannon–Floyd–Parry, p. 227).
• 1985: Brin and Squier prove that $F$ contains no non-abelian free subgroup (doi:10.1007/BF01388519).
• 1996: Cannon, Floyd and Parry prove, using Chou's work on elementary amenable groups, that $F$ is not elementary amenable (Theorem 4.10).
• 2009–2014: announced proofs of amenability (Shavgulidze, 2009; Moore, 2012) and of non-amenability (Akhmedov, 2009; Beklaryan, 2011; Wajnryb–Witowicz, 2014) are withdrawn by their authors or found to contain serious errors.
• 2013: Moore proves that if $F$ is amenable, its Følner sets grow at least like a tower of exponentials (doi:10.4171/GGD/201).
• 2013: Monod introduces the groups $H(A)$ of piecewise-projective homeomorphisms of the line, proves that they have no non-abelian free subgroup and are not amenable for every subring $A \ne \mathbf Z$ of $\mathbf R$, and asks whether $H(\mathbf Z)$ is amenable (Problem 12) (doi:10.1073/pnas.1218426110).
• 2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, and prove that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable (Theorem 6.4; arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
• 2017: Kaimanovich proves that random walks on $F$ with finitely supported, strictly non-degenerate step distributions have non-trivial Poisson boundary (doi:10.1017/9781316576571.013).
• 2019: Chornyi shows that $F$ is amenable if and only if its action on the dyadic rationals in $(0,1)$ is extensively amenable (arXiv:1907.01440).
• 2019: Kim, Koberda and Lodha show that large powers of two homeomorphisms of the line with overlapping supports generate a copy of $F$ (doi:10.24033/asens.2397).
• 2021: Stankov records, from Kim–Koberda–Lodha, that $H(\mathbf Z)$ contains a copy of $F$, so that amenability of $H(\mathbf Z)$ would imply amenability of $F$ (doi:10.1017/etds.2019.76).
• 2023: Monod shows that the Thompson group $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in the group $H_{\mathbf Q}(\mathbf Q)$ (doi:10.4171/ggd/883).
• 2023: Guba's survey records that "the famous problem about amenability of $F$ remains open" (doi:10.46298/jgcc.2023.15.1.11315), and it remains open as of 2026.

Setting

Let UI be the unit interval $[0,1]$. Thompson's group $F$ (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational $k/2^n$ and every slope a power of $2$. It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).

A mean on a set $S$ is a function $m$ from the subsets of $S$ to $[0,\infty]$ with $m(\emptyset) = 0$, $m(A \cup B) = m(A) + m(B)$ for disjoint $A, B$, and $m(S) = 1$. A group $G$ is amenable (Garrido.IsAmenable G) when it carries a mean with $m(gA) = m(A)$ for all $g \in G$ and $A \subseteq G$, where $gA = \{ga : a \in A\}$. This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in $[0,1]$.

The milestones use four further notions, defined precisely in the definitions item and in their own statements:

• A finite set $A \subseteq G$ is $\varepsilon$-Følner for a finite $\Gamma \subseteq G$ when $\sum_{\gamma\in\Gamma}|\gamma A \mathbin{\triangle} A| < \varepsilon|A|$; by Følner's criterion, $G$ is amenable exactly when it has such sets for every $\varepsilon > 0$.
• A finitely supported probability measure $\mu$ on $G$ drives a random walk; $\mu$ is strictly non-degenerate when its support generates $G$ as a semigroup, and the walk is Liouville when every bounded $\mu$-harmonic function, $f(g) = \sum_h \mu(h) f(gh)$, is constant.
• An action of $G$ on a set $X$ is extensively amenable when the finite subsets of $X$ carry a $G$-invariant mean that, for each finite $E_0 \subseteq X$, gives full weight to the finite sets containing $E_0$.
• For a subring $A$ of $\mathbf R$, Monod's group $H(A)$ consists of the homeomorphisms of the real line that are piecewise projective, $x \mapsto (ax+b)/(cx+d)$ with $\left(\begin{smallmatrix} a & b \\ c & d \end{smallmatrix}\right) \in \mathrm{SL}_2(A)$, with finitely many breakpoints, each a fixed point of a hyperbolic element of $\mathrm{SL}_2(A)$. $H_B(A)$ allows breakpoints in a set $B$ instead; $H_{\mathbf Q}(\mathbf Z)$ is isomorphic to $F$ (Thurston). A subgroup $K$ of $J$ is co-amenable when $J/K$ carries a $J$-invariant mean.

Formalization targets

Goal: Geoghegan's conjecture

$$\neg\,\mathrm{IsAmenable}(F).$$

The question is open. A proof of this statement proves the conjecture; a disproof shows that $F$ is amenable, and settles the question the other way.

Landmarks

The milestones are results from the literature, stated as their sources state them: $F$ has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of $F$; Kaimanovich's theorem that random walks on $F$ with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of $F$ as extensive amenability of its action on the dyadic rationals; Stankov's embedding of $F$ into Monod's $H(\mathbf Z)$; Monod's theorem that $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in $H_{\mathbf Q}(\mathbf Q)$; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.

A second open statement

Monod's Problem 12 asks whether $H(\mathbf Z)$ is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of $\mathbf R$, namely $\mathbf Z$; this is parallel to the goal. Through Stankov's embedding, a proof of the goal proves it, and a disproof of it disproves the goal. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of $H(\mathbf Z)$ on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of $H(\mathbf Z)$ also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).

Significance

The result. A proof of the conjecture would make $F$ a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make $F$ an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.

Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.

Difficulty

The obstructions to amenability that settle the question for most groups are absent here: $F$ has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of $F$ is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on $F$ are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.

Formalization scope

Lean representation and conventions.

• $F$ is a subgroup of the order isomorphisms of UI; $H(A)$ and $H_B(A)$ are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, $(fg)(x) = f(g(x))$; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.
• Means take values in $[0,\infty]$; total mass $1$ and finite additivity keep every value in $[0,1]$.
• Extensive amenability is stated for an action on $[0,1]$ relative to the set of dyadic rationals in $(0,1)$; the statement of Chornyi's corollary includes that $F$ maps this set to itself.
• The goal cannot be satisfied vacuously: amenability is a single existential statement about means on $F$, and $F$ is a fixed, nontrivial, finitely generated group.

What is left out.

• The Poisson boundary is not formalized: "Liouville" is Kaimanovich's equivalent reformulation through bounded harmonic functions on $\operatorname{sgr}\mu$ (p. 8).
• The "in particular" clause of Moore's Theorem 1.1, on the Følner function, is not stated separately; with Følner's criterion it follows from the stated bound.
• The withdrawn and disputed proofs in the timeline are not formalized.

What a development needs. Thompson's group $F$ and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism $H_{\mathbf Q}(\mathbf Z) \cong F$ (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.

Selected references

• 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
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519
• J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
• V. A. Kaimanovich, Thompson's group F is not Liouville, in Groups, Graphs and Random Walks, LMS Lecture Note Ser. 436 (2017) 300–342. doi:10.1017/9781316576571.013
• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• K. Juschenko, N. Matte Bon, N. Monod, M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219. doi:10.1017/etds.2016.32
• M. Chornyi, Superharmonic functions on the Lamplighter graph of Thompson's group F, preprint (2019). arXiv:1907.01440
• V. Guba, Amenability problem for Thompson's group F: state of the art, J. Groups Complex. Cryptol. 15 (2023), no. 1. doi:10.46298/jgcc.2023.15.1.11315
• S.-h. Kim, T. Koberda, Y. Lodha, Chain groups of homeomorphisms of the interval, Ann. Sci. Éc. Norm. Supér. (4) 52 (2019) 797–820. doi:10.24033/asens.2397
• B. Stankov, Non-triviality of the Poisson boundary of random walks on the group H(ℤ) of Monod, Ergodic Theory Dynam. Systems 41 (2021) 1160–1189. doi:10.1017/etds.2019.76
• N. Monod, Some comments on piecewise-projective groups of the line, Groups Geom. Dyn. 19 (2025) 459–476. doi:10.4171/ggd/883