This mission formalizes the question whether the group $\mathrm{IET}$ of interval exchange transformations is amenable, Question 1.6 of Juschenko, Matte Bon, Monod and de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, p. 4 (doi:10.1017/etds.2016.32), together with the landmark results of the literature on the question.

Motivation

An interval exchange transformation cuts the circle $\mathbf R/\mathbf Z$ into finitely many arcs and puts them back in a different order. These maps model the dynamics of polygonal billiards with rational angles, and since Katok–Stepin (1967) and Keane (1975) they have been a central object of ergodic theory. Under composition they form a group, $\mathrm{IET}$. Two questions about this group are open: whether it contains a non-abelian free subgroup (Katok's question), and whether it is amenable, that is, whether it carries a finitely additive, translation-invariant probability measure on all of its subsets. Amenability would answer Katok's question in the negative, since an amenable group has no non-abelian free subgroup.

Timeline.

• 1967: Katok and Stepin first consider exchanges of three or more intervals (JMMS, p. 4).
• 1975: Keane introduces interval exchange transformations systematically and the terminology (doi:10.1007/BF01236981).
• 2009: Novak shows that cyclic subgroups of $\mathrm{IET}$ are undistorted (doi:10.3934/jmd.2009.3.379).
• 2013: Dahmani, Fujiwara and Guirardel show that two generic interval exchange transformations do not generate a free group (doi:10.4171/GGD/209).
• 2013: Juschenko and Monod prove that the topological full group of every minimal Cantor system is amenable, which gives the first finitely generated infinite simple amenable groups (doi:10.4007/annals.2013.178.2.7). The technical core is the case $X = \mathbf Z$ of the lamplighter question for the wobbling group below (Juschenko–de la Salle, p. 2).
• 2013: de Cornulier's Bourbaki exposé records that “La question de la moyennabilité du groupe entier IET est ouverte” (p. 1064-04; published 2014, arXiv:2002.09342).
• 2013: Juschenko, Nekrashevych and de la Salle prove that recurrent actions are extensively amenable (arXiv 2013; published 2016, doi:10.1007/s00222-016-0664-6).
• 2013: Juschenko and de la Salle prove that the lamplighter action of the wobbling group of a recurrent metric space of bounded geometry, for instance $\mathbf Z$ or $\mathbf Z^2$, is amenable, and that it is not when the space contains a Lipschitz injective image of the binary tree; the case $\mathbf Z^d$, $d \ge 3$, is left open (arXiv 2013; published 2015, doi:10.36045/bbms/1432840864).
• 2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, show that a subgroup of $\mathrm{IET}$ is amenable if and only if its action on $\mathbf R/\mathbf Z$ is extensively amenable, prove that every subgroup of rational rank at most $2$ is amenable, and show that finitely supported random walks are Liouville in rank $1$ and are not in rank at least $3$ (arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
• 2017: Dahmani, Fujiwara and Guirardel prove that every finitely generated torsion-free solvable subgroup of $\mathrm{IET}$ is virtually abelian (arXiv 2017; published 2020, doi:10.5802/afst.1641).
• 2018: Garban shows that the action of the wobbling group of a bounded degree graph is diffuse-extensively amenable if and only if the graph is recurrent, and conjectures that $W(\mathbf Z^d) \curvearrowright \mathbf Z^d$ is not extensively amenable for $d \ge 3$ (arXiv 2018; published 2020, doi:10.4171/GGD/567).
• 2026: Guelman and Liousse record (p. 2) that “there is no known example of non amenable or torsion-free non virtually abelian finitely generated iet-group” (arXiv:2601.23054). The question remains open as of 2026.

Setting

Write $\mathbf R/\mathbf Z$ for the circle (UnitAddCircle). A permutation $g$ of $\mathbf R/\mathbf Z$ is an interval exchange transformation (IntervalExchange.IsIntervalExchange g) when it is right-continuous, has finitely many points of discontinuity, and has finitely many angles $g(x) - x$. Equivalently, $g$ cuts the circle into finitely many half-open arcs and translates each of them. The group $\mathrm{IET}$ (IntervalExchange.IET) is the subgroup of permutations of $\mathbf R/\mathbf Z$ that they generate; a milestone states that it consists of the interval exchange transformations themselves. For a subgroup $G \le \mathrm{IET}$, the angle group $\Lambda(G)$ (angleGroup G) is the subgroup of $\mathbf R/\mathbf Z$ generated by all angles of elements of $G$, and the rational rank $\mathrm{rk}_{\mathbf Q}$ (rationalRank) of a subgroup of $\mathbf R/\mathbf Z$ is the supremum of the $d$ such that $\mathbf Z^d$ embeds in it. For a subgroup $\Lambda$ of $\mathbf R/\mathbf Z$, $\mathrm{IET}(\Lambda)$ (IETOf Λ) consists of the elements of $\mathrm{IET}$ all of whose angles lie in $\Lambda$.

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$. An action of $G$ on a set $X$ is amenable (IsAmenableAction G X) when $X$ carries a $G$-invariant mean, and extensively amenable (IsExtensivelyAmenable G X) 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$.

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

• A finitely supported probability measure $\mu$ on $G$ drives the left random walk $g_n = h_n \cdots h_1$; the inverted orbit of $x_0 \in X$ is $O_n = \{x_0, g_1^{-1}x_0, \dots, g_n^{-1}x_0\}$. The action is recurrent (IsRecurrentAction) when for every symmetric such $\mu$ and every $x_0$, the induced walk $g_n x_0$ returns to $x_0$ with probability $1$.
• For a functor $F$ from finite sets with injections to amenable groups, $F(X)$ (extend F X) is its extension to an arbitrary set $X$ by direct limits, and an action of $G$ on $X$ gives the semidirect product $F(X) \rtimes G$ (FunctorProduct F G X) acting on $F(X)$. The lamplighter case is $F(X) = (\mathbf Z/2\mathbf Z)^{(X)}$ (Lamplighter G X).
• The wobbling group $W(X)$ (wobbling X) of a metric space $X$ consists of the permutations $g$ of $X$ with $\sup_x d(x, gx) < \infty$.

Formalization targets

Goal

$$\mathrm{IsAmenable}(\mathrm{IET}).$$

The question is open. A proof settles it positively and, through von Neumann's theorem, answers Katok's question in the negative; a disproof shows that $\mathrm{IET}$ is not amenable.

Landmarks

The milestones are results from the literature, stated as their sources state them. From Juschenko–Matte Bon–Monod–de la Salle: $\mathrm{IET}$ is a group (p. 4); Lemmas 2.1 and 2.2 on extensive amenability; Theorem 1.3 and Corollary 1.4, the functorial criterion; Proposition 5.3, that a subgroup of $\mathrm{IET}$ is amenable if and only if its action on $\mathbf R/\mathbf Z$ is extensively amenable; Proposition 4.1 and Lemma 4.3, the inverted-orbit reformulations; Theorem 4.2, recurrence implies extensive amenability; Lemma 5.2 and Theorems 5.1 and 1.9, amenability in rational rank at most $2$; and Theorem 1.10, the Liouville dichotomy, with the steps of its proof: Lemma 5.10, Proposition 5.11 with Lemma 5.13 (realizing $\mathrm{IET}(\Lambda; \Sigma)$ as the topological full group of a minimal subshift of polynomial complexity), and Matte Bon's theorem for virtually cyclic groups. The external results these proofs cite are milestones too: Kesten's criterion for a graph (Woess, Theorem 10.6), Lyons–Peres Theorem 2.17 on rough embeddings, Pólya's theorem (already proved on the platform as MarkovMixing.polya_recurrence), the Baldi–Lohoué–Peyrière comparison lemma, and Matte Bon's Theorem 1.2 on topological full groups of subshifts of slow complexity. From Juschenko–de la Salle: Theorem 1.4 on the wobbling group, with coarse embeddings defined by non-decreasing control functions.

Two further open statements

Garban's question, whether $W(\mathbf Z^d) \curvearrowright \mathbf Z^d$ is extensively amenable for every $d$, and Question 1.11 of Juschenko–Matte Bon–Monod–de la Salle, whether a polynomially growing Schreier graph forces extensive amenability, are stated as open milestones. Each comes with a milestone stating that a positive answer implies the goal.

Significance

The result. A proof would make $\mathrm{IET}$ a natural amenable group containing, by Juschenko–Monod and Juschenko–Matte Bon–Monod–de la Salle, finitely generated infinite simple amenable groups, and would answer Katok's question. A disproof would give the first non-amenable finitely generated group of interval exchange transformations; by Theorem 1.9 it would have rational rank at least $3$.

Formalizing it. The definitions of extensive amenability, of the functorial semidirect products $F(X) \rtimes G$, of inverted orbits and recurrent actions, and of wobbling groups are reusable beyond this mission, as are the external probabilistic results (Kesten's criterion, rough embeddings and recurrence). Pólya's theorem is already formalized and proved on the platform (MarkovMixing.polya_recurrence). None of the other landmarks is formalized.

Difficulty

Every known amenability proof for subgroups of $\mathrm{IET}$ passes through Proposition 5.3 and then needs extensive amenability of the action on the circle. The available criterion for extensive amenability is recurrence of the Schreier graphs, which embed into lattices $\mathbf Z^d$ with $d$ the rational rank; for $d \ge 3$ these graphs can be transient, so recurrence is unavailable. Garban's theorem shows that the natural strengthening of extensive amenability fails for all transient wobbling actions, and Theorem 1.10 shows that the Liouville route fails in rank at least $3$.

Formalization scope

$\mathbf R/\mathbf Z$ is UnitAddCircle, and permutations act on it by evaluation. $\mathrm{IET}$ is defined as the subgroup generated by the interval exchange transformations, so that its group structure needs no proof inside the definitions; a milestone states that nothing else lies in it. The source's precise definition (“a right-continuous permutation $g$ of $\mathbf R/\mathbf Z$ such that the set $\{gx - x, x \in \mathbf R/\mathbf Z\}$, called the set of angles of $g$, is finite”) is read together with its opening phrase, “cutting this circle into finitely many intervals”, so the definition also requires finitely many points of discontinuity: without that requirement a right-continuous permutation with two angles can have infinitely many discontinuities, and the cocycle of Proposition 5.3 would not be finitely supported. Means take values in $[0, \infty]$ and are normalized to total mass $1$. Random walks have finitely supported step distributions $\mu : G \to_0 \mathbf R$ where the sources say “finitely supported”, and probabilities of events of a walk are finite sums over the step sequences. Recurrence of a Markov chain is return to the starting point with probability $1$, expressed through first-return probabilities. Functors $I \to \mathrm{Amen}$ are Mathlib functors from the wide subcategory of FintypeCat on the injective maps to GrpCat with amenable values, extended to a set $X$ by the filtered colimit over its finite subsets.

The goal admits no trivializing reading: $\mathrm{IET}$ contains the irrational rotations and the non-rotation exchanges, and Garrido.IsAmenable is the standard notion. The external milestones (Kesten, Lyons–Peres, Baldi–Lohoué–Peyrière) are cited results, stated in the form the sources apply; proofs of them are welcome contributions in their own right.

Selected references

• K. Juschenko, N. Matte Bon, N. Monod and 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, arXiv:1503.04977.
• K. Juschenko and M. de la Salle, Invariant means for the wobbling group, Bull. Belg. Math. Soc. Simon Stevin 22 (2015) 281–290, doi:10.36045/bbms/1432840864.
• K. Juschenko, V. Nekrashevych and M. de la Salle, Extensions of amenable groups by recurrent groupoids, Invent. Math. 206 (2016) 837–867, doi:10.1007/s00222-016-0664-6.
• K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. 178 (2013) 775–787, doi:10.4007/annals.2013.178.2.7.
• C. Garban, Inverted orbits of exclusion processes, diffuse-extensive-amenability, and (non-?)amenability of the interval exchanges, Groups Geom. Dyn. 14 (2020) 871–897, doi:10.4171/GGD/567.
• Y. de Cornulier, Groupes pleins-topologiques [d'après Matui, Juschenko, Monod, ...], Séminaire Bourbaki, exposé 1064, Astérisque 361 (2014) 183–223, arXiv:2002.09342.
• F. Dahmani, K. Fujiwara and V. Guirardel, Free groups of interval exchange transformations are rare, Groups Geom. Dyn. 7 (2013) 883–910, doi:10.4171/GGD/209.
• F. Dahmani, K. Fujiwara and V. Guirardel, Solvable groups of interval exchange transformations, Ann. Fac. Sci. Toulouse Math. 29 (2020) 595–618, doi:10.5802/afst.1641.
• M. Keane, Interval exchange transformations, Math. Z. 141 (1975) 25–31, doi:10.1007/BF01236981.
• C. F. Novak, Discontinuity-growth of interval-exchange maps, J. Mod. Dyn. 3 (2009) 379–405, doi:10.3934/jmd.2009.3.379.
• R. Lyons and Y. Peres, Probability on Trees and Networks, Cambridge University Press, 2016, doi:10.1017/9781316672815.
• W. Woess, Random Walks on Infinite Graphs and Groups, Cambridge University Press, 2000, doi:10.1017/CBO9780511470967.
• N. Matte Bon, Subshifts with slow complexity and simple groups with the Liouville property, Geom. Funct. Anal. 24 (2014) 1637–1659, doi:10.1007/s00039-014-0293-4.
• P. Baldi, N. Lohoué and J. Peyrière, Sur la classification des groupes récurrents, C. R. Acad. Sci. Paris Sér. A–B 285 (1977) A1103–A1104 (no DOI).
• N. Guelman and I. Liousse, Some elementary amenable subgroups of interval exchange transformations, arXiv:2601.23054 (2026).