# Thompson's group F is nonamenable The following describes the scope of the Lean formalization related to the following accompanying paper(s): - [Thompson's group $F$ is nonamenable](../../preprints/Thompsons-group-F-is-nonamenable-September-23-2026/paper.pdf) ## Scope The amenability problem for Thompson's group $F$ asks whether it admits a positive normalized left-invariant mean on bounded real functions. The formalized result rules out such a mean for the standard group of dyadic piecewise-linear homeomorphisms of the interval, proving nonamenability. No explicit boundary constant or prescribed generating set is given. ## Comparator links | Result | Comparator statement | | --- | --- | | Nonamenability of Thompson's group $F$ | [ThompsonNonamenability.lean](../ComparatorChallenges/ThompsonNonamenability.lean) |