A mathematical object can be easy to describe and remarkably difficult to understand. Thompson’s group F fits that description almost too well. Its elements stretch and compress an interval according to a short list of rules. Yet a basic question about averaging over those transformations resisted resolution for decades.
OpenAI’s manuscript, dated September 23, 2026, reports an answer: F is nonamenable. Its accompanying Lean documentation states that the formalized result establishes this for the standard group. The paper connects the group’s interval structure to a surprising obstruction from infinite-dimensional geometry.
So, is Thompson’s group F amenable? OpenAI’s reported theorem says no. Assessing that answer requires separating the written argument, its documented formalization, independent verification, and the explicit constructions still being sought.
The interesting story is how almost-invariant averages would force an approximate fixed point that cannot exist. Understanding that mechanism makes the announcement far more useful than another entry on a list of AI breakthroughs.
Table of Contents
1. What Is Thompson’s Group F?
Imagine transformations of the interval from zero to one. Each transformation is continuous, invertible, and increasing, so points keep their order. It consists of finitely many straight-line pieces.
Two restrictions define the group. Breakpoints must be dyadic fractions, such as one-half, three-quarters, or five-eighths. Slopes must be integer powers of two, including one-half, one, two, and four. Negative exponents allow compression.
Composing two valid transformations produces another valid transformation. Together with inverses and the identity transformation, these operations form F. The manuscript treats it as a discrete group, without imposing a topology for the amenability question.
Thompson’s Group F: Key Mathematical Facts and Properties
| Key Fact | What It Means |
|---|---|
| Introduced by Richard Thompson in 1965 | The group predates the current AI research story by decades |
| Infinite but finitely presented | F has infinitely many elements but a finite description using generators and relations |
| No nonabelian free subgroup | A familiar obstruction to amenability cannot be used |
| OpenAI manuscript dated September 23, 2026 | The paper reports that F is nonamenable |
| Main result documented as formalized in Lean | The stated scope covers standard F, without an explicit boundary constant or prescribed generating set |
F belongs to a family with groups T and V. Broadly, T uses circle transformations, while V permits more rearrangement in a binary setting. Their properties should not be silently transferred to F. Related names do not make interchangeable theorems.
2. How Binary Trees Encode the Transformations
Repeatedly splitting an interval into equal halves builds a binary tree. Each leaf represents one interval in the resulting partition. A pair of trees with the same number of leaves describes a transformation by matching source intervals to target intervals in order.
The slope on each piece is the target interval’s length divided by the source interval’s length. Since both lengths are powers of one-half, their ratio is a power of two.
Here is a valid example:
Thompson’s Group F: Source and Target Intervals with Slopes
| Source Interval | Target Interval | Slope |
|---|---|---|
| Zero to one-half | Zero to one-quarter | One-half |
| One-half to three-quarters | One-quarter to one-half | One |
| Three-quarters to one | One-half to one | Two |
This transformation first compresses, then translates, then stretches. The pieces meet continuously, and both endpoints stay fixed.
Multiplication means composition. To combine tree diagrams, refine their adjoining partitions until the subdivisions agree, then compose the mappings. Refinement changes the diagram without changing the transformation. For developers, this distinction resembles two representations of the same program behavior.
3. The Amenability Problem: Can F Support Invariant Averaging?
Finite groups have an obvious averaging rule: add the values of a function over every element and divide by the group’s size. Multiplying all elements by a fixed group element merely reorders the average.
For an infinite group, that recipe has no ordinary finite denominator. Amenability asks whether a suitable replacement exists: a positive, normalized averaging operation on bounded functions that remains unchanged under translation.
This is called an invariant mean. It uses finite additivity, rather than requiring an ordinary countably additive probability distribution over the group.
The Følner criterion gives a finite-set formulation. For every finite collection of translations and every positive tolerance, an amenable group must contain a nonempty finite set A satisfying
\[ \frac{|hA\triangle A|}{|A|}<\varepsilon \]
for every selected translation h. The triangle denotes symmetric difference, the elements belonging to exactly one of the two sets.
For the integers, increasingly long intervals work. Shifting an interval by one changes only its endpoints, while its size keeps growing. Its relative mismatch therefore shrinks.
The amenability problem for Thompson’s group F asks whether finite collections of transformations can achieve this kind of increasingly good invariance.
4. Why the Usual Shortcuts Failed
Groups containing a nonabelian free subgroup cannot be amenable. Free groups provide the familiar picture of branching that defeats invariant averaging.
Brin and Squier established that F contains no such subgroup. The usual shortcut was unavailable.
F is also not elementary amenable. That class grows from finite and abelian groups through specified operations, including extensions and directed unions. But falling outside it does not prove nonamenability. The elementary class does not exhaust all amenable groups.
Neither structural fact settled the question. Even substantial numerical evidence could only examine finite samples or approximations. Poor boundary behavior in the sets one can compute does not exclude much larger sets with better behavior.
The challenge was to rule out every sufficiently invariant finite candidate with a fixed obstruction. That requires a universal argument, rather than a computation that becomes more convincing as it becomes larger.
5. What Earlier Research Established
Justin Tatch Moore proved severe lower bounds on the sizes of possible Følner sets for F. These tower-type bounds explain why a successful finite approximation could lie far beyond comfortable computation. Large lower bounds constrain amenability without disproving it.
Moore also connected amenability to a scalar convex Ramsey property for finite ordered binary trees. This translated an infinite-group problem into a finite combinatorial condition.
Victor Guba developed estimates for finite Cayley subgraphs and restrictions on invariant means. Haagerup and Olesen connected the question to simplicity of the reduced group C\*-algebra of T. These approaches revealed useful structure without supplying the eventual answer claimed here.
The history includes resolution claims in both directions. Moore identified errors in Shavgulidze’s amenability approach. Moore separately withdrew an amenability manuscript after Akhmedov found an error. That withdrawal did not invalidate his published Ramsey characterization.
This history makes careful attribution essential. A paper with an assertive title, an accepted partial result, and an audited proof are different kinds of evidence.
6. What OpenAI’s Theorem Actually Says
The manuscript’s central statement is direct: Thompson’s group F is not amenable. It presents this as confirming Geoghegan’s conjecture, recorded from 1979.
The proof produces a finite collection of translations and a positive lower bound on relative mismatch. Every nonempty finite set fails to be sufficiently invariant under at least one translation in that collection.
That contradicts the Følner requirement and excludes an invariant mean.
The main nonamenability argument is contained in the 13-page manuscript, including its supporting appendix. Two companion papers are invoked for later consequences concerning representations and percolation. They are not dependencies of the central proof. This distinction resolves confusion raised in the public discussion.
7. The Fixed-Point Obstruction Behind the Argument
A fixed point of a function f is a point x satisfying f(x)=x. An approximate fixed point moves only slightly when f is applied.
The paper uses a result of Benyamini and Sternfeld: an infinite-dimensional Hilbert ball admits a Lipschitz map into itself whose displacement stays uniformly positive. Lipschitz means distances can increase by at most a fixed factor L.
There is a positive number δ such that
\[ \|f(x)-x\|\geq\delta \]
throughout the ball. No sequence of points can make this displacement approach zero. The appendix constructs a suitable map with δ equal to one-half.
The infinite-dimensional setting matters. Familiar finite-dimensional fixed-point intuitions depend on hypotheses that do not carry over to this ball.
OpenAI’s proof for Thompson’s group F turns this geometric obstruction into a test of amenability. If sufficiently invariant finite sets existed, the group’s dyadic structure would force the map to have approximate fixed points. The remaining work builds that connection.
8. How Recursive Colors Force the Contradiction
8.1. Build Parent Intervals and Descendants
Choose D small dyadic intervals inside the unit interval, with positive gaps between them. These are the parents. Inside each parent, place a scaled copy of the entire family, creating descendants.
Assign each suitable dyadic partition a vector in the Hilbert ball. This vector is its “color.” Restrict the partition to each parent, stretch that restriction back to the full interval, average the resulting colors, and apply f.
The rule is recursive but well founded. Each proper restriction has fewer cells, so the calculation reduces to simpler partitions. When the required restrictions are unavailable, the color is zero.
For sufficiently fine partitions, a parent color equals f applied to the mean of its descendant colors. This exact identity carries the fixed-point map into the group calculation.
8.2. Compare Colors Through Finite Translations
F can send any ordered pair of separated internal dyadic intervals affinely onto another such pair. Choose finitely many transformations comparing relevant parent and descendant pairs with one reference pair.
Call this collection S. Crucially, S is fixed before choosing the finite candidate A. Otherwise, the obstruction could change with every candidate and fail to contradict amenability.
The partition level may depend on A. It is chosen fine enough to handle every element of A and its selected translates at once. That dependence is permitted and explicitly controlled.
If translating A changes few elements, averages of bounded scalar functions over A change little. Apply this cancellation principle to inner products of interval colors. Inner products measure their alignment, and all separated-pair correlations become close to one shared average.
8.3. Use Variance to Expose the Conflict
Let m be the mean of the parent colors, and let zᵢ be the mean of the descendants inside parent i. Recursion makes m the average of the vectors f(zᵢ). These vectors vary with the group element, and the estimates average over A.
Expand the squared distance between zᵢ and m. The shared correlations cancel. Diagonal pairs and descendants paired with their own parents are exceptions, but they occupy only a fraction 1/D of the relevant sums. Since colors stay in the unit ball, their contribution is bounded.
Writing η for the largest relative mismatch of A under S, the resulting estimate gives
\[ \delta^2\leq L^2\left(\frac{4}{D}+4\left(1-\frac{1}{D}\right)\eta\right). \]
Choose D large enough. Amenability would then permit η small enough to make the right side less than δ². That is impossible.
Equivalently, the manuscript obtains a positive boundary lower bound valid for every A. The proof never needs to exhibit a free subgroup. It makes approximate translation invariance incompatible with the recursive coloring.
9. What the Lean Formalization Establishes
OpenAI’s scope documentation says the Lean proof for Thompson’s group F excludes a positive normalized left-invariant mean for the standard dyadic piecewise-linear group. This identifies the mathematical target, rather than merely describing a related lemma.
The scope does not provide an explicit boundary constant or prescribed generating set. That limitation concerns quantitative output, not a weaker stated nonamenability theorem.
Public discussion also raised a sorry in comparator materials. In Lean, sorry stands in for an omitted proof. Its location matters. A comparator target statement is separate from the implementation intended to establish it. Finding a placeholder in the target file alone does not diagnose a gap in that implementation.
A serious independent check must build the proof, examine dependencies and permitted axioms, and confirm that the encoded definitions match the intended group. Searching a single file for one token cannot replace that process.
Human understanding is another question. André Henriques asked for a record of people who had read and understood the argument. A machine certificate and a clear mathematical explanation contribute different evidence. Neither should be casually substituted for the other.
10. What Nonamenability Changes
For Thompson’s group F, the result settles the averaging question in the direction Geoghegan conjectured. It also makes F a particularly recognizable example of nonamenability without nonabelian free subgroups. That combination was already possible in group theory, so this does not newly disprove the general von Neumann conjecture.
Nonamenability implies the existence of a paradoxical decomposition: pieces of the group can be translated and rearranged into two disjoint copies. This is a statement about infinite sets and group actions, not a physical duplication procedure.
The manuscript also derives consequences for uniformly bounded representations that cannot be made unitary by changing the Hilbert norm, and for multiple infinite clusters in Cayley-graph percolation. Those consequences invoke separate companion theorems. Their assumptions and verification deserve their own attention.
11. What Still Needs to Be Made Explicit?
A theorem proving existence can leave substantial constructive work. Ville Salo’s follow-up asks for an explicit paradoxical decomposition of Thompson’s group F and concrete finite sets supporting it.
The obstacle is quantitative. Extracting manageable sets requires tracking the Lipschitz constant of the auxiliary map, choosing D, and specifying the interval transports. The manuscript supplies relationships between these quantities without tabulating a finished numerical construction.
Salo describes a route through expansion and Hall’s theorem, but reports difficulty extracting the constants. A tentative value suggested by another AI model should not be treated as a checked numerical result.
Three tasks remain distinct: auditing the formal proof, developing shared human understanding, and making its consequences explicit. Work on the latter two does not itself identify a logical gap in the theorem. Conversely, a scope note cannot certify that every proposed extraction or interpretation is correct.
12. The Lesson for AI-Assisted Mathematics
The striking feature of this argument is its connection between familiar dyadic transformations and an infinite-dimensional fixed-point obstruction. Established tools are arranged to turn a hypothetical averaging property into a contradiction.
For researchers and builders following AI mathematics, the useful reading sequence is concrete: identify the exact theorem, understand the mechanism, inspect the formalization scope, then examine what can be extracted or extended. A headline gets attention. That sequence produces understanding.
Thompson’s group F gives Binary Verse AI readers a case where the proof deserves as much attention as the announcement. Follow more research explainers at binaryverseai.com, and keep the next question precise: can we turn this nonamenability argument into explicit constructions that people can inspect and use?
1. What is Thompson’s group F, and what does amenability mean?
Thompson’s group F consists of increasing, piecewise-linear transformations of the unit interval whose breakpoints are dyadic fractions and whose slopes are powers of two. Amenability asks whether the group admits an averaging rule unchanged by translation. The Følner criterion expresses this through finite sets with arbitrarily small relative boundaries.
2. Is Thompson’s group F amenable?
OpenAI’s September 2026 manuscript reports that Thompson’s group F is nonamenable, and its accompanying Lean scope documentation states that the formalized theorem establishes this for the standard group. This reported resolution should be distinguished from earlier disputed claims and from the separate process of independent reproduction and mathematical assessment.
3. How does OpenAI’s proof overcome the previous barrier?
F contains no nonabelian free subgroup, so the familiar free-subgroup obstruction cannot establish its nonamenability. OpenAI instead uses recursive colors on dyadic partitions. Hypothetical Følner sets make averaged correlations nearly invariant, forcing an approximate fixed point of a Lipschitz map constructed to stay a positive distance from every fixed point.
4. Has the proof been independently verified, and does Lean’s sorry indicate a gap?
OpenAI publishes formalization materials, but their availability alone does not establish that an independent reviewer has reproduced and audited the complete proof. The discussed sorry appears in a comparator target statement, which is separate from the proof implementation. Verification requires checking the implementation, dependencies, permitted axioms and correspondence with standard F.
5. Does nonamenability provide an explicit paradoxical decomposition of F?
Nonamenability implies that a paradoxical decomposition exists, but an explicit construction is a further task. The discussion asks for concrete finite translation sets and quantitative bounds extracted from the proof. OpenAI’s formalization scope does not provide an explicit boundary constant or prescribed generating set, so existence and a usable construction should be distinguished.