Group Theory

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).

Motivation

In 1935 Werner Burau attached to every braid on $n$ strands a matrix over the ring of Laurent polynomials $\mathbb{Z}[t,t^{-1}]$. The resulting homomorphism $\rho_n : B_n \to \mathrm{GL}_n(\mathbb{Z}[t,t^{-1}])$ is the oldest and most studied linear representation of the braid group, and whether it is faithful — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.

The history is short and sharp:

• 1969 — Magnus and Peluso prove that $\rho_3$ is faithful, by a direct algebraic computation.
• 1991 — Moody proves $\rho_n$ is not faithful for $n \ge 9$.
• 1993 — Long and Paton improve this to $n \ge 6$.
• 1999 — Bigelow settles $n = 5$: $\rho_5$ is not faithful.
• This left exactly one open case, $n = 4$, which appears as Question 3.1 in Margalit's problem list for mapping class groups.
• 2026 — Bharathram, Birman and Brendle prove that $\rho_4$ is faithful (arXiv:2607.05283), closing the last case.

Setting

Let $n \ge 1$. The braid group $B_n$ is taken here in Artin's presentation: generators $\sigma_1,\dots,\sigma_{n-1}$ subject to

$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1}.$$

Let $R = \mathbb{Z}[t,t^{-1}]$. The unreduced Burau representation is the homomorphism

$$\rho_n : B_n \longrightarrow \mathrm{GL}_n(R), \qquad \sigma_i \longmapsto I_{i-1} \oplus \begin{pmatrix} 1-t & t \\ 1 & 0\end{pmatrix} \oplus I_{n-i-1},$$

i.e. the identity matrix altered only in the two rows and columns $i$, $i+1$. That these matrices satisfy the two families of braid relations — so that $\rho_n$ is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block $\begin{pmatrix} 0 & 1 \\ t^{-1} & 1-t^{-1}\end{pmatrix}$).

Equivalently, $\rho_n$ is the action of the mapping class group of the $n$-punctured disk $D_n$ on the relative homology $H_1(\widetilde{D_n}, \{\tilde p_*\})$ of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.

A representation is faithful when it is injective.

Target

The goal of the mission is the Main Theorem of the paper:

$$\rho_4 : B_4 \longrightarrow \mathrm{GL}_4(\mathbb{Z}[t,t^{-1}]) \ \text{ is injective.}$$

The milestones are three supporting results, each of which can be attacked independently:

1. Theorem 4.1 (Magnus–Peluso). $\rho_3$ is injective. The paper gives a new topological proof of this classical statement, and the same argument is the model for the four-strand case.
2. Observation 2.1. If a braid $\Phi \in B_n$ satisfies $\rho_n(\Phi) = I$, then its image under the standard inclusion $B_n \hookrightarrow B_{n+1}$ (add one unbraided strand) satisfies $\rho_{n+1}(\iota(\Phi)) = I$. The paper uses this to move a four-strand braid into $B_5$, where a parity obstruction can be applied.
3. Long's criterion ([Long 1986, Theorem 2.2], quoted in Section 1 of the paper). If $N \trianglelefteq B_n$ is nontrivial and not contained in the centre, and $\rho_n$ is injective on $N$, then $\rho_n$ is injective. This is what reduces the Main Theorem to faithfulness on the Brunnian subgroup $\mathrm{Brun}_4$.

Significance

Faithfulness of $\rho_4$ closes the classification of the faithful Burau representations: $\rho_n$ is faithful exactly for $n \le 4$. It immediately gives faithfulness of the Jones representation of $B_4$ (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of $\rho_n$ for $n \ge 5$ remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.

For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of $\rho_n$ over $\mathbb{Z}[t,t^{-1}]$ (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.

Difficulty

The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for $B_4$ turns injectivity of $\rho_4$ into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how non-faithfulness is proved for $n \ge 5$.

The source argument is topological. To a braid $\Phi$ one associates the arc $\beta = (\beta_*^3)\Phi$ and the sequence of punctured disks cut out by its intersections with a fixed arc $\alpha$; the Moody polynomial $M(\alpha,\beta) \in \mathbb{Z}[t,t^{-1}]$ then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid $\Phi \in K_4$ into $B_5$ and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.

Formalization scope

Conventions fixed by the Lean development:

1. $B_n$ is the abstract group given by Artin's presentation, with generators indexed by $\mathrm{Fin}(n-1)$ using truncated subtraction; the generator of index $i$ is $\sigma_{i+1}$. This is the already-published definition reused by the mission, so results proved here interoperate with other braid-group missions.
2. The representation is the unreduced Burau representation, of size $n \times n$, not the reduced $(n-1)$-dimensional one; the variable is written $t$ and the coefficient ring is $\mathbb{Z}[t,t^{-1}]$.
3. Faithfulness is stated as injectivity of the group homomorphism, not as triviality of the kernel on some subgroup, and it is the genuine homomorphism out of the presented group: the braid relations are verified for the Burau matrices in the definition file, so no statement here is vacuous or conditional on well-definedness.
4. Long's criterion is stated for all $n$; for $n \le 2$ its noncentrality hypothesis cannot be satisfied, so its content is the case $n \ge 3$ that the paper uses.

A complete development will additionally need: point-pushing subgroups and the Brunnian group $\mathrm{Brun}_4$, the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.

Selected references

• V. Bharathram, J. S. Birman, T. E. Brendle, The Burau representation is faithful for n = 4, 2026, arXiv:2607.05283.
• W. Magnus, A. Peluso, On a theorem of V. I. Arnold, Comm. Pure Appl. Math. 22 (1969), 683–692, DOI:10.1002/cpa.3160220508.
• D. D. Long, A note on the normal subgroups of mapping class groups, Math. Proc. Cambridge Philos. Soc. 99 (1986), 79–87, DOI:10.1017/S0305004100063969.
• J. A. Moody, The Burau representation of the braid group $B_n$ is unfaithful for large $n$, Bull. Amer. Math. Soc. 25 (1991), 379–384, DOI:10.1090/S0273-0979-1991-16080-5.
• D. D. Long, M. Paton, The Burau representation is not faithful for $n \ge 6$, Topology 32 (1993), 439–447, DOI:10.1016/0040-9383(93)90030-Y.
• S. Bigelow, The Burau representation is not faithful for $n = 5$, Geom. Topol. 3 (1999), 397–404, DOI:10.2140/gt.1999.3.397.

Motivation

Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is unsolved.

What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.

• Cyclic and, more generally, finite abelian groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
• Symmetric and alternating groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
• Every finite solvable group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219), obtained by solving embedding problems.
• Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — every finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
• Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.

Setting

Fix a field $K$ and a group $G$. A Galois realization of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism

$$G \;\cong\; \mathrm{Gal}(L/K),$$

where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is realizable over $K$, written IsRealizable K G, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.

Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.

Formalization targets

Goal — the inverse Galois problem

$$\text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G.$$

The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.

Milestones — the known partial results

$$G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K,$$ $$G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0),$$ $$G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}.$$

The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.

Significance

The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group $M_{23}$ show.

Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.

Difficulty

The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover over $\mathbb{Q}$ rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.

A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.

Formalization scope

The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:

• IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.
• The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
• The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
• $\mathrm{Sym}(S)$ is Equiv.Perm S for a finite type $S$, and $A_n$ is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.
• Solvability is Group.IsSolvable.

The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.

Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.

Selected references

• Inverse Galois problem, Wikipedia. https://en.wikipedia.org/wiki/Inverse_Galois_problem
• I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219.
• C. U. Jensen, A. Ledet, N. Yui, Generic Polynomials: Constructive Aspects of the Inverse Galois Problem, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
• G. Malle, B. H. Matzat, Inverse Galois Theory, Springer Monographs in Mathematics, 1999.
• R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, 17T7 is a Galois group over the rationals, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012) gave NIZK proofs for Circuit SAT of size $O(|C|k)$ for a circuit $C$ and security parameter $k$, the first perfect NIZK arguments for all of NP, and the first non-interactive zaps based on a standard cryptographic assumption. These constructions use a single algebraic primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys, together with a short proof that a committed value is $0$ or $1$.

The paper gives two instances of this primitive. One rests on the subgroup decision assumption in composite-order groups. The other, the subject of this mission, rests on the decisional linear assumption of Boneh, Boyen and Shacham (CRYPTO 2004) in prime-order bilinear groups. Prime-order groups are the setting of most later pairing-based proof systems, including the Groth–Sahai proofs (EUROCRYPT 2008), and their decisional-linear instantiation uses commitment keys of the same linear-tuple form as this mission.

Setting

A DLIN bilinear group is a tuple $(p, \mathbb G, \mathbb G_T, e, g)$: $p$ is a prime, $\mathbb G$ and $\mathbb G_T$ are groups of order $p$, $e : \mathbb G \times \mathbb G \to \mathbb G_T$ is bilinear ($e(u^a, v^b) = e(u, v)^{ab}$ for all $u, v \in \mathbb G$, $a, b \in \mathbb Z$), $g$ generates $\mathbb G$, and $e(g, g)$ generates $\mathbb G_T$. A triple $(f^r, h^s, g^{r+s})$ is a linear tuple with respect to $(f, h, g)$.

The scheme (Figure 2 of the paper) works as follows.

• Keys. Pick $x, y \in \mathbb Z_p^*$, $r_u, s_v \in \mathbb Z_p$, and put $f = g^x$, $h = g^y$. A perfectly binding key is $ck = (f, h, u, v, w) = (f, h, f^{r_u}, h^{s_v}, g^{r_u+s_v+z})$ with $z \in \mathbb Z_p^*$; its extraction key is $xk = (x, y, z)$. A perfectly hiding key is $(f, h, f^{r_u}, h^{s_v}, g^{r_u+s_v})$, a linear tuple; its trapdoor key is $tk = (r_u, s_v)$.
• Commitment. $\mathrm{com}(m; r, s) = (u^m f^r, v^m h^s, w^m g^{r+s}) \in \mathbb G^3$ for $m \in \mathbb Z_p$, $(r, s) \in \mathbb Z_p^2$.
• Extraction and trapdoor opening. $\mathrm{Ext}_{xk}$ recovers a short $m$ from $c_3 c_1^{-1/x} c_2^{-1/y} = (g^z)^m$. $\mathrm{Topen}_{tk}(m, (r, s), m') = (r - (m'-m)r_u,\ s - (m'-m)s_v)$.
• 0/1 proof. On an opening $(m, r, s)$ with $m \in \{0, 1\}$ and randomness $t \in \mathbb Z_p$, the prover $P_{01}$ outputs six group elements $\pi_{11}, \dots, \pi_{23}$. The verifier $V_{01}$ checks six pairing-product equations in $\mathbb G_T$.

The perfect properties of Section 3 are: homomorphism, perfect binding, perfect extractability, perfect trapdoor opening and its indistinguishability, perfect completeness, perfect soundness, perfect witness indistinguishability (WI), and perfect non-erasure WI. Non-erasure WI asks that a simulator turn the randomness of a proof made with one witness into randomness that explains the same proof under the other witness.

Formalization targets

Goal: Theorem 4, exact part

For every DLIN bilinear group, the scheme of Figure 2 is homomorphic on both kinds of key and perfectly binding and extractable on binding keys. On hiding keys it has perfect trapdoor opening and perfect trapdoor-opening indistinguishability. Its 0/1 proof is perfectly complete on both kinds of key, perfectly sound on binding keys, and perfectly WI and perfectly non-erasure WI on hiding keys. Soundness, for example, reads

$$V_{01}(ck, c, \pi) \text{ accepts} \implies \exists\, m \in \{0,1\},\ r, s \in \mathbb Z_p:\ c = \mathrm{com}(m; r, s).$$

Milestones

The milestones follow the paper's proof:

1. the homomorphism display (p. 11);
2. the trapdoor-opening identity and the extraction display (Figure 2);
3. the unique opening $(m, r, s)$ of every $c \in \mathbb G^3$ on a binding key;
4. completeness;
5. the six exponent equations obtained from an accepted proof;
6. the product identity $(r_0+s_0-t_0)(r_1+s_1-t_1) = 0$;
7. "c or $c \cdot \mathrm{com}(-1; 0, 0)$ is a commitment to 0";
8. the identity $P_{01}(ck, 0, (r_0, s_0); t) = P_{01}(ck, 1, (r_1, s_1); t + r_0 s_1 - s_0 r_1)$ on hiding keys.

Significance

The perfect properties are what the paper's later results consume. Perfect soundness and extractability on binding keys give the perfectly sound NIZK proof of knowledge for Circuit SAT (Theorem 6). Perfect WI, trapdoor opening and non-erasure WI on hiding keys give perfect zero-knowledge (Lemma 8 and Theorem 11) and the adaptive and UC-secure variants of Sections 7 and 8. Theorem 4 transfers all of this to prime-order bilinear groups under the decisional linear assumption.

The theorem is published and its proof is short, but the printed construction contains an error. With the signs of $t$ in $\pi_{12}$ and $\pi_{21}$ as printed in Figure 2, an honest proof fails the fourth and sixth verification equations whenever $2t \ne 0$. A machine-checked proof fixes the corrected construction, under which the paper's own witness-indistinguishability argument goes through. No formalization of this scheme, or of the decisional linear setting, exists on the platform or in Mathlib.

Difficulty

The algebra is modest. The work lies in carrying exponents in $\mathbb Z_p$ through powers in groups of order $p$, and in getting the soundness argument right. An accepted proof only constrains discrete logarithms of the proof elements, so the six pairing equations must first be turned into six equations between exponents. That step is valid only because $f$, $h$ and $e(g, g)$ are nondegenerate. Soundness then needs the observation that the product of two specific linear forms vanishes, and it fails outright on a hiding key ($z = 0$). Witness indistinguishability is an exact identity between proofs, which holds only for the corrected prover.

Formalization scope

• Groups. $\mathbb G$ and $\mathbb G_T$ are finite commutative groups of cardinality $p$, $p$ prime. The pairing is a monoid homomorphism G →* G →* GT, which is equivalent to bilinearity. $g$ generates $\mathbb G$ and $e(g, g)$ generates $\mathbb G_T$.
• Exponents. Exponents are elements of ZMod p, acting through their representative in $\{0, \dots, p-1\}$.
• Keys. The key generators are represented by their supports. A binding key requires $x, y, z \ne 0$ and a hiding key requires $x, y \ne 0$. Without $z \ne 0$ a "binding" key is hiding and soundness is false. Without $x, y \ne 0$ the verification equations degenerate.
• Prover. $P_{01}$ is the corrected prover; the erratum is recorded on every item it affects.
• Probabilities. "For all adversaries, probability 1" is stated for every key in the support and every adversarial choice. "Equal probabilities for all adversaries" is stated as equality of probability mass functions over the uniform proof randomness. For perfect properties both readings are equivalent.
• Dropped. The computational content is out of scope: the efficiency of the algorithms, key indistinguishability, and the decisional linear assumption itself (Definition 3).
• Simulator. The non-erasure simulator is the explicit map $t \mapsto t + r_0 s_1 - s_0 r_1$ that the proof constructs, so the statement cannot be met by an arbitrary unbounded function.
• No trivial readings. A trivializing formalization is ruled out. The verifier's equations are not vacuous ($e(g, g) \ne 1$, $f, h \ne 1$), binding keys have $z \ne 0$, and the definitions are instantiated on a concrete group of order 5 in a local check: the corrected proof is accepted there and the printed one is rejected.
• Contributions. Contributions welcome: proofs of the milestones, and a reusable development of discrete logarithms in groups of prime order.

Selected references

• J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
• D. Boneh, X. Boyen, H. Shacham, Short Group Signatures, CRYPTO 2004, LNCS 3152. https://doi.org/10.1007/978-3-540-28628-8_3
• J. Groth, A. Sahai, Efficient Non-interactive Proof Systems for Bilinear Groups, EUROCRYPT 2008, LNCS 4965. https://doi.org/10.1007/978-3-540-78967-3_24
• D. Boneh, E.-J. Goh, K. Nissim, Evaluating 2-DNF Formulas on Ciphertexts, TCC 2005, LNCS 3378. https://doi.org/10.1007/978-3-540-30576-7_18

Motivation

The word problem for a group with a finite generating set asks whether a given word in the generators and their inverses represents the identity; it is decidable if one algorithm answers this for every word. Since Higman's embedding theorem (1961), a recurring theme in combinatorial group theory has been to characterize algorithmic properties of groups by embeddings into groups with good algebraic properties. Boone and Higman (1974) proved that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group can itself be taken finitely presented. This is the Boone–Higman conjecture.

This preprint states a proof of the conjecture: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.

Background

• 1961. Higman characterizes finitely generated subgroups of finitely presented groups as the recursively presented groups.
• 1974. Boone and Higman prove the characterization $G \le H \le K$ with $H$ simple and $K$ finitely presented, and ask whether $H$ can be finitely presented.
• 1980. Thompson embeds every finitely generated group with decidable word problem into a finitely generated simple group with decidable word problem; a later proof is given by Darbinyan and Steenbock (2022).
• 2022. Belk and Zaremsky introduce twisted Brin–Thompson groups, which embed an acting group in a simple group; Zaremsky (2024) gives a finite-presentation criterion requiring a finitely presented acting group with finitely generated point stabilizers and finitely many orbits on unordered pairs.
• 2023–2026. The conjecture is verified for hyperbolic groups and contracting self-similar groups (Belk, Bleak, Matucci, Zaremsky), Baumslag–Solitar and free-by-cyclic groups (Bux, Llosa Isenrich, Wu), and $\mathrm{Aut}(F_n)$ and mapping class groups of punctured surfaces (Belk, Fournier-Facio, Hyde, Zaremsky); see the survey of Belk, Bleak, Matucci and Zaremsky.
• 2026. The OpenAI preprint Finite algebraic envelopes and the Boone–Higman conjecture (dated September 23, 2026) states a proof of the conjecture in general. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A group $G$ is finitely generated if some finite tuple $g_1, \dots, g_n$ generates it. A word is a finite list of letters $g_i^{\pm1}$; $G$ has decidable word problem if for some finite generating tuple the set of words evaluating to $1$ is computable. A group is finitely presented if it has a presentation with finitely many generators and relations, and simple if it is nontrivial with no normal subgroups other than $1$ and itself. An embedding is an injective homomorphism.

In Lean (OAI.FiniteAlgebraicEnvelopes, definitions BooneHigman), words are List (Fin n × Bool), evalWord multiplies generators or their inverses, HasDecidableWordProblem G asserts a generating tuple whose identity predicate is ComputablePred, and EmbedsInFinitelyPresentedSimpleGroup G asserts a group in the same universe that is Group.IsFinitelyPresented and IsSimpleGroup, with an injective homomorphism from $G$.

Formalization targets

Goal: Theorem 1.1 (Boone–Higman conjecture)

For every finitely generated group $G$,

$$G \text{ has decidable word problem} \iff G \text{ embeds in a finitely presented simple group.}$$

The implication from right to left is classical (a finitely presented simple group has decidable word problem, and the property passes to finitely generated subgroups); the content is the forward implication.

Significance

The result. Theorem 1.1 gives a purely algebraic characterization of decidability of the word problem and settles a question open since 1974. Its intermediate result, Theorem 1.2, embeds every finitely generated group with decidable word problem in a finitely presented group with a faithful two-transitive action on a countably infinite set with finitely generated point stabilizers, which feeds Zaremsky's criterion for twisted Brin–Thompson groups.

Formalizing it. No machine-checked proof exists, and the source is an unrefereed preprint. Formalizing it requires computability of word problems, finite presentations (available in Mathlib as Group.IsFinitelyPresented), Steinberg groups over noncommutative rings, and twisted Brin–Thompson groups, which are not in Mathlib. The proof also uses Zaremsky's finite-presentation theorem (Theorem 2.3) from the literature, which a complete formalization must include.

Difficulty

Finite presentation does not pass to subgroups, so Boone and Higman's simple group $H$ and finitely presented group $K$ cannot simply be merged. Thompson's construction gives a finitely generated simple overgroup but provides no finite presentation. The new route needs a finitely presented group acting faithfully and two-transitively, built from a finitely presented algebra whose simplicity appears only after passing to a direct limit, and an exact calculation removing the kernel of the Steinberg group without assuming it is central.

Formalization scope

• GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.
• Decidability is ComputablePred on words over a specified finite generating tuple (Subgroup.closure (range generators) = ⊤); since the word problem's decidability is independent of the finite generating set, this matches the source.
• IsSimpleGroup includes nontriviality, matching the paper's convention.

The statement is not trivially true: both directions are required for every finitely generated group, including infinitely presented ones.

Needed infrastructure: computable group presentations, Steinberg groups, mapping tori of endomorphisms, twisted Brin–Thompson groups and Zaremsky's criterion. Contributions toward the classical backward implication, or toward Theorem 1.2, are welcome.

Selected references

• OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf
• W. W. Boone, G. Higman, An algebraic characterization of groups with soluble word problem, J. Austral. Math. Soc. 18 (1974). https://doi.org/10.1017/S1446788700019108
• G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
• R. J. Thompson, Embeddings into finitely generated simple groups which preserve the word problem, in Word Problems II, North-Holland, 1980. https://doi.org/10.1016/S0049-237X(08)71348-X
• J. Belk, M. C. B. Zaremsky, Twisted Brin–Thompson groups, Geom. Topol. 26 (2022). https://doi.org/10.2140/gt.2022.26.1189
• M. C. B. Zaremsky, Finite presentability of twisted Brin–Thompson groups, Proc. Roy. Soc. Edinburgh Sect. A (2024). https://doi.org/10.1017/prm.2024.131
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Hyperbolic groups satisfy the Boone–Higman conjecture, Duke Math. J. 175 (2026). https://doi.org/10.1215/00127094-2025-0055
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Progress around the Boone–Higman conjecture, 2025. https://arxiv.org/abs/2306.16356
• K.-U. Bux, C. Llosa Isenrich, X. Wu, On the Boone–Higman conjecture for groups acting on locally finite trees, 2025. https://arxiv.org/abs/2408.05673
• J. Belk, F. Fournier-Facio, J. Hyde, M. C. B. Zaremsky, Boone–Higman embeddings of Aut(F_n) and mapping class groups of punctured surfaces, 2026. https://arxiv.org/abs/2503.21882
• A. Darbinyan, M. Steenbock, Embeddings into left-orderable simple groups, J. London Math. Soc. 105 (2022). https://doi.org/10.1112/jlms.12552

Motivation

The inverse Galois problem asks whether every finite group $G$ occurs as the Galois group of a finite Galois extension of $\mathbb{Q}$. For finite simple groups, a large part of the problem was settled by the rigidity method (Shih, Fried, Belyi, Matzat, Thompson) and its refinements such as the braid-group method. Between 1984 and 1989 this machinery realized 25 of the 26 sporadic simple groups as Galois groups over $\mathbb{Q}$, in fact as Galois groups of regular extensions of $\mathbb{Q}(t)$. The Mathieu group $M_{23}$ was the single exception.

Timeline.

• 1985–1987: Hoyden-Siedersleben and Häfner obtained regular $M_{23}$-extensions of $k(t)$ for $k=\mathbb{Q}(\sqrt{-23})$ and $k=\mathbb{Q}(\sqrt{-7})$, by passing through $M_{24}$.
• 1996: Granboulan constructed a regular $M_{23}$-extension of $k(t)$ for every field $k$ over which a certain conic has a point; that conic has no rational point.
• 2013: Elkies computed the four complex polynomials $P$ of degree 23 with $\mathrm{Gal}(P(x)-t/\mathbb{C}(t))\cong M_{23}$; each is defined over a quartic number field.
• 2026: Huang, Jackson, Lee, Poonen, Pries and Zhang (arXiv:2608.08538) produced an explicit regular $M_{23}$-extension of $\mathbb{Q}(t)$ and explicit degree-23 polynomials over $\mathbb{Q}$ with Galois group $M_{23}$, completing the program for the sporadic groups.

Setting

$S_{23}$ denotes the group of permutations of the 23 points $\{1,\dots,23\}$, acting on the left, so $(\sigma\tau)(x)=\sigma(\tau(x))$. The paper fixes three explicit permutations

$$g_1=(1,11)(2,23)(3,8)(4,16)(5,21)(7,20)(15,19)(18,22),$$ $$g_2=(1,2,11,10,16,9,6,3,23,19,20,14,21,17,4,8,22,5,18,15,13,7,12),$$ $$g_3=(1,2,3,4,10,11,12,7,19,18,8,6,9,16,17,21,22,5,14,20,13,15,23),$$

and the Mathieu group $M_{23}$ is the subgroup of $S_{23}$ generated by $g_1$ and $g_2$. A $G$-extension of a field $k$ is a Galois extension $L/k$ together with an isomorphism $\mathrm{Gal}(L/k)\cong G$. A finite extension $L$ of $\mathbb{Q}(t)$ is regular if it contains no nontrivial algebraic extension of $\mathbb{Q}$.

For a triple of conjugacy classes $(C_1,C_2,C_3)$ of $M_{23}$, the set $\Sigma_c$ consists of triples $(h_1,h_2,h_3)\in C_1\times C_2\times C_3$ with $h_1h_2h_3=1$ that generate $M_{23}$, and the Nielsen class $\mathrm{Ni}_c$ is the set of orbits of $\Sigma_c$ under simultaneous conjugation by $M_{23}$. The paper works with the classes $C_1=2$, $C_2=23A$, $C_3=23B$, represented by $g_1,g_2,g_3$.

Formalization targets

Goal (Theorem 1.1)

$$\exists\ K/\mathbb{Q}\ \text{finite Galois with}\ \mathrm{Gal}(K/\mathbb{Q})\cong M_{23}.$$

Stronger forms

• Theorem 1.3: there is a finite Galois extension $L/\mathbb{Q}(t)$, regular over $\mathbb{Q}$, with $\mathrm{Gal}(L/\mathbb{Q}(t))\cong M_{23}$.
• Examples 1.2 and 3.7: two explicit monic degree-23 polynomials in $\mathbb{Z}[x]$ whose splitting fields are $M_{23}$-extensions of $\mathbb{Q}$, unramified outside $\{2,3,23\}$ and $\{2,7,23\}$ respectively.

Supporting milestones

Facts about $M_{23}$ stated in §3 (order $10{,}200{,}960$, simplicity, 4-transitivity, 17 conjugacy classes), the membership $(g_1,g_2,g_3)\in\Sigma_c$, the count $|\mathrm{Ni}_c|=7$, the Riemann–Hurwitz count of Lemma 3.1, the hyperbolic triangle of Lemma 3.2, and the group-theoretic step of Corollary 3.6 ($M_{23}$ is not normal in any strictly larger subgroup of $S_{23}$).

Significance

Theorem 1.1 removes the last sporadic exception: combined with earlier work, every sporadic simple group is the Galois group of a regular extension of $\mathbb{Q}(t)$ (Corollary 1.4), and hence occurs as a Galois group over every number field, in infinitely many mutually independent ways.

The paper's proof is computer-assisted: Belyi maps were computed numerically and the final claims were certified in Magma and PARI/GP. No machine-checked proof in a proof assistant is known. A formal proof of the explicit-polynomial statements (Examples 1.2 and 3.7) would give an independent, kernel-checked certificate of Theorem 1.1. The group-theoretic milestones (order, simplicity, transitivity, class counts, the Nielsen count) are reusable for any later work on $M_{23}$ or the other Mathieu groups.

Difficulty

The rigidity method fails for $M_{23}$: for every $G_{\mathbb{Q}}$-stable triple of conjugacy classes the Nielsen class has size different from $1$, so no rational point of a Hurwitz space is forced. The smallest positive size, $|\mathrm{Ni}_c|=7$ for $\{2,23A,23B\}$, leaves seven covers, and the fact that one of them has field of moduli $\mathbb{Q}$ was found by explicit computation, with no conceptual explanation. Certifying that a particular degree-23 polynomial has Galois group exactly $M_{23}$ requires both a lower bound (the group contains $M_{23}$, for instance via cycle types and the classification of transitive groups of degree 23) and an upper bound (the group is contained in a conjugate of $M_{23}$, for instance via resolvents or reduction modulo primes). Neither bound is a finite check inside current Mathlib.

Formalization scope

$S_{23}$ is Equiv.Perm (Fin 23). The paper's point $k$ corresponds to k - 1 : Fin 23, and permutations compose as functions, which matches the paper's left-action convention. $M_{23}$ is defined as Subgroup.closure {g₁, g₂}, so it is not described up to isomorphism. Galois groups are groups of field automorphisms, K ≃ₐ[ℚ] K, and a $G$-extension is recorded as a group isomorphism with $M_{23}$. $\mathbb{Q}(t)$ is RatFunc ℚ. "Unramified outside $S$" for a number field is encoded as "every prime dividing the absolute discriminant lies in $S$", which is equivalent by Dedekind's discriminant theorem. The Nielsen class is the set of orbits of $\Sigma_c$ under simultaneous conjugation. Hyperbolic angles in the Poincaré disk are defined through the hyperbolic law of cosines.

The geometric statements Lemma 3.3 and Proposition 3.5 concern the numerically computed curve $X_{\mathbb{C}}$ and the polynomial $F(T,V)$, which the paper does not print, so they are not milestones. Lemma 3.1 enters only through its Riemann–Hurwitz count.

Contributions are welcome on decidable certificates for permutation-group facts in Lean, on Galois-group certification for explicit polynomials, and on Hilbert irreducibility.

Selected references

• X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, The Mathieu group $M_{23}$ is a Galois group over $\mathbb{Q}$, 2026. https://arxiv.org/abs/2608.08538
• G. Malle, B. H. Matzat, Inverse Galois Theory, 2nd ed., Springer, 2018.
• J.-P. Serre, Topics in Galois Theory, Jones and Bartlett, 1992.
• N. D. Elkies, The complex polynomials $P(x)$ with $\mathrm{Gal}(P(x)-t)\cong M_{23}$, ANTS X, Open Book Series 1, 2013.
• M. D. Fried, H. Völklein, The inverse Galois problem and rational points on moduli spaces, Math. Ann. 290 (1991), 771–800.

Motivation: classify three-dimensional periodic symmetry

A space group describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in Oliver Knill’s survey, §94, “Crystallography,” p. 41. Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.

The target is the known classification result selected by LeanEval v1, not an unsolved classification conjecture. Its authoritative specification is the declaration LeanEval.Geometry.SpaceGroupsProblem.space_groups. The accompanying benchmark manifest attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.

Setting: groups, transformations, and orientation

For a natural number $d$, let $E(d)=\mathbb R^d$ with its Euclidean inner product. A Euclidean isometry is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the benchmark’s definitions, $G$ is discrete when, for every point $x$ and every real $\varepsilon>0$, the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.

Such a group is crystallographic when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$. These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called cocompact, its actual content is the existence of these independent translations, not a separately assumed compact quotient.

An affine equivalence between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An orientation-preserving affine equivalence additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The Sohncke subfamily restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the source definitions and notes.

Target: one conjunction, with all three exact counts

Write $C_{\mathrm{OP}}(d)$ for crystallographicCountOP d, $C(d)$ for crystallographicCount d, and $C_{\mathrm{OP,only}}(d)$ for crystallographicCountOPOnly d. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is

$$C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.$$

This is the exact benchmark conjunction, in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.

Significance: exact cardinalities for the underlying groups

The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in Knill, §94; the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.

The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The benchmark source currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.

Difficulty: a catalog is not a completeness theorem

A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the source’s cardinality assertion. The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.

Formalization scope: preserve the benchmark model

The Lean representation is EuclideanSpace ℝ (Fin d), with affine isometries and affine equivalences from Mathlib. The three source counting functions use Set.encard in the extended natural numbers $\mathbb N\cup\{\infty\}$. More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.

One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$. Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.

Selected references

• LeanEval contributors; problem submitted by Kim Morrison. LeanEval v1: 230 space groups, statement revision 1, 2026, repository commit 296b7491ec989d21bcf8636a9a69231a1e5d1d25. Exact Lean source; manifest with historical bibliography.
• Oliver Knill. Some Fundamental Theorems in Mathematics, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. Full text. This provides background for the three counts; the exact formal conventions are those of LeanEval above.

Motivation

Finitely many rotations of the sphere generate a group whose orbits are typically dense. A basic quantitative question is how fast those orbits fill the sphere: after words of length $\ell$ in the generators, how uniformly are the points spread? The answer is controlled by the spectral gap of an averaging operator built from the generators. The question goes back to the Banach–Ruziewicz problem (uniqueness of rotation-invariant finitely additive measures on spheres), was studied by Lubotzky, Phillips and Sarnak in their work on distributing points on $S^2$ (LPS 1987), and was formulated as a conjecture about random generators by Gamburd, Jakobson and Sarnak. It also matters in quantum computing: a spectral gap for a gate set gives efficient approximation of every single-qubit gate by short gate sequences (Sawicki–Karnas 2017).

Timeline.

• 1987 — Lubotzky, Phillips and Sarnak construct explicit rotations with optimal spectral gap using automorphic forms and pose the general question (LPS).
• 2006 — Fisher proves a zero–one law: for $n \ge 3$ generators, either almost every $n$-tuple has a spectral gap or almost every $n$-tuple has none (Fisher, IMRN 2006, arXiv:math/0601050).
• 2008 — Bourgain and Gamburd prove the spectral gap for elements of $SU(2)$ with algebraic entries generating a free group (Invent. Math. 171).
• 2012 — Bourgain and Gamburd extend this to dense subgroups of $SU(d)$, $d \ge 2$, generated by finitely many elements with algebraic entries (JEMS 14, arXiv:1108.6264).

The tuples with algebraic entries form a Haar-null set, so the conjecture for random tuples remains open.

Setting

Let $SU(d)$ be the group of complex $d\times d$ matrices $U$ with $U^*U = UU^* = I$ and $\det U = 1$, a compact group with its normalized Haar measure $\mu_d$ (the unique left-invariant Borel probability measure). For $g_1,\dots,g_n \in SU(d)$ the Hecke operator acts on functions $f : SU(d) \to \mathbb C$ by

$$(z_g f)(x) = \sum_{j=1}^{n} \bigl( f(g_j x) + f(g_j^{-1} x) \bigr).$$

On $L^2(SU(d),\mu_d)$ it is bounded and self-adjoint, constants are eigenfunctions with eigenvalue $2n$, and it preserves the space $L^2_0$ of mean-zero functions. Writing $\lambda_1(z_g)$ for the supremum of the spectrum of $z_g$ on $L^2_0$, one always has $\lambda_1 \le 2n$, and $z_g$ (or the tuple $g$) has a spectral gap when

$$\lambda_1(z_g) < 2n .$$

For $SU(2)$, each $U$ acts on the sphere $S^2$ by rotations, and $z_g$ is the operator $\phi_{U_1} + \phi_{U_1}^{-1} + \dots + \phi_{U_n} + \phi_{U_n}^{-1}$ of the source.

Formalization targets

Goal: the spectral gap conjecture

For every $n > 2$, if $U_1,\dots,U_n$ are chosen independently and uniformly (Haar) at random in $SU(2)$, then with probability $1$

$$\lambda_1\bigl(z_{U_1,\dots,U_n}\bigr) < 2n .$$

Milestones from the literature

1. Fisher's zero–one law (2006, Theorem 1.2): for $n \ge 3$, either almost every $n$-tuple has a spectral gap, or almost every $n$-tuple has none.
2. Bourgain–Gamburd in $SU(2)$ (2008): tuples with algebraic entries (up to simultaneous conjugation) that freely generate a free group of rank $n\ge 2$ have a spectral gap.
3. Bourgain–Gamburd in $SU(d)$ (2012, Theorem 1): for $d \ge 2$, tuples with algebraic entries generating a dense subgroup of $SU(d)$ have a spectral gap.

By Fisher's law, the goal follows once a spectral gap is shown on a set of positive Haar measure.

Significance

A spectral gap for $g$ means that random walks driven by $g_1^{\pm1},\dots,g_n^{\pm1}$ equidistribute in $SU(2)$ (and orbits equidistribute on $S^2$) at an exponential rate, and that the action of the generated group on $S^2$ is strongly ergodic. In quantum computation it says that a universal single-qubit gate set is automatically efficiently universal. The conjecture asserts that this holds for a typical gate set, not just for the arithmetically special ones covered by Bourgain–Gamburd.

On the formal side, the milestones are proved theorems (Fisher; Bourgain–Gamburd) that have, to the knowledge of this proposal, no machine-checked proofs. Formalizing any of them requires substantial new libraries: Haar measure and harmonic analysis on $SU(d)$, ergodicity of $\mathrm{Aut}(F_n)$ on $\mathrm{Hom}(F_n, SU(2))$ (Goldman), and the arithmetic-combinatorial machinery of Bourgain–Gamburd. The goal itself is an open problem.

Difficulty

Spectral gap is not detected by density alone: every tuple generating a dense subgroup gives an ergodic action, but ergodicity only shows $\lambda_1$ is not an eigenvalue, not that it is bounded away from $2n$. Known proofs need either arithmetic structure (automorphic forms, or the algebraic entries used by Bourgain–Gamburd to rule out short relations that come too close to the identity) or rigidity (property (T)). A generic tuple has neither.

Formalization scope

• $SU(d)$ is Matrix.specialUnitaryGroup (Fin d) ℂ with the subspace topology and its Borel σ-algebra; it is shown to be a compact topological group, and haarSU d is the Haar measure normalized to total mass $1$.
• The Hecke operator acts on all functions $f : SU(d) \to \mathbb C$ by the formula above.
• "Spectral gap" is encoded through the quadratic form: there is $\varepsilon > 0$ such that $\operatorname{Re}\langle z_g f, f\rangle \le (2n-\varepsilon)\,\|f\|_2^2$ for every $f \in L^2$ with $\int f\,d\mu = 0$. For a bounded self-adjoint operator this is exactly $\lambda_1 < 2n$ (one-sided gap, as in Fisher and Bourgain–Gamburd).
• "Chosen uniformly at random" is the product Haar measure on $SU(2)^n$; "with probability $1$" is an almost-everywhere statement.
• The goal is stated on $L^2(SU(2))$, as in the source. The operator on $L^2(S^2)$ is the restriction to a subrepresentation, so a gap on $L^2_0(SU(2))$ implies a gap on $L^2_0(S^2)$. Fisher (2006, §1) remarks that the two versions of the conjecture are equivalent.
• Trivializations are ruled out: for $g_1=\dots=g_n=I$ the quadratic form equals $2n\|f\|^2$, so no gap holds, and for $n=0$ the gap fails as well.

Useful reusable contributions include: basic harmonic analysis on compact groups (translation invariance in $L^2$, self-adjointness of $z_g$), the Peter–Weyl decomposition of $L^2(SU(2))$, conjugation invariance of the gap, and monotonicity of the gap in the generating set.

Selected references

• A. Lubotzky, R. Phillips, P. Sarnak, Hecke operators and distributing points on $S^2$. II, Comm. Pure Appl. Math. 40 (1987). https://doi.org/10.1002/cpa.3160400402
• D. Fisher, $\mathrm{Out}(F_n)$ and the spectral gap conjecture, IMRN 2006. https://doi.org/10.1155/IMRN/2006/26028 (arXiv:math/0601050)
• J. Bourgain, A. Gamburd, On the spectral gap for finitely-generated subgroups of $SU(2)$, Invent. Math. 171 (2008). https://doi.org/10.1007/s00222-007-0072-z
• J. Bourgain, A. Gamburd, A spectral gap theorem in $SU(d)$, J. Eur. Math. Soc. 14 (2012). https://doi.org/10.4171/jems/337 (arXiv:1108.6264)
• A. Sawicki, K. Karnas, Criteria for universality of quantum gates, Phys. Rev. A 95 (2017). https://doi.org/10.1103/PhysRevA.95.062303
• Wikipedia, Spectral gap conjecture. https://en.wikipedia.org/wiki/Spectral_gap_conjecture

Motivation

A graph may have enough symmetry for every edge to look the same while its vertices still fall into two distinct classes. Such a graph is semisymmetric when it has constant valency, is edge-transitive, and is not vertex-transitive. Conder, Zhou, Feng and Zhang study this phenomenon among bi-Cayley graphs, graphs equipped with a group acting freely on two vertex orbits. Their dihedral case supplies examples related to questions of Marušič and Potočnik about semisymmetric tetracirculants. It also asks how small the valency of a semisymmetric graph with this specific group action can be. The paper states that six is the minimum and that examples occur at every valency $2k$ with odd $k\ge3$ (Conder et al., Theorem 1.5 and its introduction, p. 3).

The authors develop the bi-Cayley setting and the relevant automorphism actions before reaching the dihedral result. The lower bound appears as Theorem 6.1, while Example 6.2 defines a graph family and Proposition 6.4 gives a semisymmetry criterion for its odd-$k$ members (Conder et al., pp. 11–13). This mission targets those claims within a single formal graph model. The final sentence of Theorem 1.5, concerning an edge-regular family, depends on the separate Theorem 6.5 and is outside this goal.

Setting

Let $H$ be a finite group. Choose subsets $R,L,S\subseteq H$ with $R^{-1}=R$, $L^{-1}=L$, $1\notin R\cup L$, and $|R|=|L|$. The graph $\operatorname{BiCay}(H,R,L,S)$ has two labelled copies of each element of $H$, written $h_0$ and $h_1$. For each $h\in H$, it joins $h_0$ to $(xh)_0$ when $x\in R$, joins $h_1$ to $(yh)_1$ when $y\in L$, and joins $h_0$ to $(zh)_1$ when $z\in S$. These are unoriented edges. Right multiplication by $H$ preserves the graph and acts regularly on each of its two vertex copies (Conder et al., pp. 1 and 4).

A bi-dihedrant is a bi-Cayley graph whose group is dihedral. Write $D_n=\langle a,b\mid a^n=b^2=(ab)^2=1\rangle$ for the dihedral group of degree $n\ge3$. Graph valency is the number of neighbours of a vertex. Connectedness is required throughout the paper. For a semisymmetric graph the common valency exists by definition, but the formal statements quantify over every vertex so that the numerical claims refer to the actual graph degree (Conder et al., definitions on p. 4 and Theorem 6.1 on p. 11).

The constructed family $\Gamma(n,\lambda,2k)$ uses $n\ge5$, $k\ge2$, and a residue $\lambda$ of multiplicative order $2k$ modulo $n$ whose even-power sum vanishes: $\sum_{j=0}^{k-1}\lambda^{2j}=0$. For $0\le i<k$, put $c_i=\sum_{j=0}^{i}\lambda^{2j}$ and $d_i=\lambda c_i$. Set $S(n,\lambda,2k)=\{a^{c_i}:0\le i<k\}\cup\{ba^{d_i}:0\le i<k\}$. Then $\Gamma(n,\lambda,2k)=\operatorname{BiCay}(D_n,\varnothing,\varnothing,S(n,\lambda,2k))$ (Conder et al., Example 6.2, pp. 12–13).

Right multiplication $R(g):h_i\mapsto(hg)_i$ gives a subgroup $R(H)\le\operatorname{Aut}(\Gamma)$, and $X=N_{\operatorname{Aut}(\Gamma)}(R(H))$ is its normaliser. For $\alpha\in\operatorname{Aut}(H)$ and $g,x,y\in H$ the paper's permutations are $\sigma_{\alpha,g}:h_0\mapsto(h^\alpha)_0,\ h_1\mapsto(gh^\alpha)_1$ and $\delta_{\alpha,x,y}:h_0\mapsto(xh^\alpha)_1,\ h_1\mapsto(yh^\alpha)_0$; the sets $\mathrm F$ and $\mathrm I$ of (2.2) collect those that preserve the edge rules. A graph is normal edge-transitive when $X$, not merely $\operatorname{Aut}(\Gamma)$, is transitive on edges (Conder et al., pp. 4–5).

Formalization targets

The milestones, in attack order, are Proposition 2.1(b) (one may assume $1\in S$), Proposition 2.2 (the normaliser $X=R(H)(\mathrm F\cup\mathrm I)$), the opening step of the proof of Theorem 6.1 ($R=L=\varnothing$ for a semisymmetric graph), Theorem 6.1, the claims of Example 6.2, and Proposition 6.4.

Minimum valency

For every connected semisymmetric bi-dihedrant over $D_n$, $n\ge3$, and every vertex $v$,

$$\deg_{\Gamma}(v)\ge6.$$

This is Theorem 6.1 and the first claim of Theorem 1.5. The milestone for the proof's opening step records that semisymmetry forces $R=L=\varnothing$; the theorem itself still ranges over all valid $R,L,S$ (Conder et al., Theorem 6.1, p. 11).

Examples at every odd index

For each odd integer $k\ge3$, there is a connected semisymmetric bi-dihedrant $\Gamma$ such that

$$\deg_{\Gamma}(v)=2k\qquad\text{for every vertex }v.$$

Example 6.2 is the first milestone toward this claim: under its hypotheses $\Gamma(n,\lambda,2k)$ is connected, $|S|=2k$, every vertex has degree $2k$, and $\sigma_{\alpha,b}$ for $\alpha:(a,b)\mapsto(a^\lambda,ba)$ lies in $X$ and permutes the neighbours of $1_0$ cyclically, so the graph is normal edge-transitive (Conder et al., p. 13). Proposition 6.4 is the second: under the defining conditions for $\Gamma(n,\lambda,2k)$, odd $k$ and $\lambda^k=-1$ modulo $n$ imply semisymmetry (Conder et al., Proposition 6.4, p. 13). An auxiliary arithmetic theorem states the parameter existence needed to apply it for every odd $k\ge3$.

Significance

The lower bound excludes semisymmetric bi-dihedrants of valency at most five. The existence assertion says that six is attained and places examples at an infinite sequence of larger valencies. Together these claims distinguish the restrictions imposed by a dihedral bi-Cayley action from edge transitivity alone. The construction also gives a concrete family on which questions about stronger automorphism properties can be posed (Conder et al., §6, pp. 11–14).

The result is proved in the cited paper; this mission seeks a machine-checked version of its first two Theorem 1.5 claims. The definition of a bi-Cayley graph, the precise graph symmetry predicates, and the arithmetic parameter family are reusable beyond this particular lower bound. The statements here are open proof targets in Lean, with their mathematical content fixed before proof development. The edge-regular claim from the theorem's final sentence requires additional source results and remains a separate formalization target.

Difficulty

Edge transitivity alone does not make a graph vertex-transitive: a semisymmetric graph is precisely the regular case where that inference fails. The lower bound therefore cannot be obtained by treating every vertex as lying in one automorphism orbit. In the dihedral case, the proof must account for both the rotations and reflections in the connection set, and for the constraints that connectedness and graph automorphisms impose on low-valency possibilities (Conder et al., proof of Theorem 6.1, pp. 11–12).

The existence statement has a distinct arithmetic requirement. Proposition 6.4 is conditional on $n,\lambda,k$ satisfying Example 6.2 and $\lambda^k=-1$. The paper asserts examples for every odd $k\ge3$ without spelling out parameters for all such $k$. The auxiliary arithmetic statement records that remaining obligation explicitly; a proof of the conditional proposition alone would not establish the quantified existence claim.

Formalization scope

Lean represents the two vertex copies by H ⊕ H and the dihedral group by Mathlib's DihedralGroup n. The graph is a SimpleGraph built from the three edge rules above, with the inverse-closure and loop-exclusion conditions retained in BiCayData. Semisymmetry uses the full graph automorphism group, unoriented edge transitivity, and constant graph degree. The source's standing finite, connected, simple, and undirected conventions are explicit through finite groups, simple graphs, and connectedness hypotheses. The goal and Theorem 6.1 use $n\ge3$, the range of dihedral groups in §6; the existence examples are also required to be connected.

The definitions do not set valency equal to $|S|$, replace a graph degree by a formula, or make an edge-transitivity claim true by ranging over an empty edge set. The setting requires valid inverse-closed side sets rather than silently symmetrising an invalid one. The arithmetic hypothesis uses the multiplicative order in $\mathbb Z/n\mathbb Z$ and enumerates the indices of $\mathbb Z_k$ by $0,\ldots,k-1$. Normal edge-transitivity in Example 6.2 is stated for the subgroup $X$ and semisymmetry for the full group $\operatorname{Aut}(\Gamma)$; the two are not interchanged. The restriction $n\ge3$ in the lower bound is that of Theorem 6.1 and is a disclosed hypothesis of the goal: $D_1$ and $D_2$ are abelian, and the paper treats bi-Cayley graphs over abelian groups separately. The auxiliary parameter statement is not in the paper; it is supplied so that the existence claim has a complete proof path. The third sentence of Theorem 1.5 is not formalized. Contributions establishing the structural lower bound, the family criterion, or the arithmetic existence statement are all within scope.

Selected references

• Marston Conder, Jin-Xin Zhou, Yan-Quan Feng and Mi-Mi Zhang, Edge-transitive bi-Cayley graphs, preprint arXiv:1606.04625v1, 2016; published in Journal of Combinatorial Theory, Series B, 2020. Preprint · DOI.