Group Theory

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

How large can the order of a single permutation of $n$ objects be? The answer, Landau's function $g(n)$, is a basic invariant of the symmetric group $S_n$: it is the maximum number of times a permutation can be iterated before it returns to the identity. Because the order of a permutation is the least common multiple of its cycle lengths, $g(n)$ is also the largest least common multiple of the parts of a partition of $n$, which ties the question to the distribution of prime numbers.

Timeline.

• 1902–1903. E. Landau proved that $\ln g(n)\sim\sqrt{n\ln n}$.
• 1968. J.-L. Nicolas showed that $g$ is constant on arbitrarily long runs of consecutive integers.
• 1984. J.-P. Massias proved the explicit bound $\ln g(n)\le 1.05313836\sqrt{n\ln n}$ for all $n\ge 1$.
• 1988. Massias, Nicolas and Robin obtained a three-term asymptotic expansion of $\ln g(n)$, its expression through the inverse logarithmic integral, and the equivalence of a one-sided inequality with the Riemann hypothesis.
• 2002. K. Ford's bounds for the Riemann zeta function give the error term $x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$ in the prime number theorem, which can be fed into the 1988 result.

Setting

For a natural number $n$, let $S_n$ be the group of all permutations of an $n$-element set. The order of $\sigma\in S_n$ is the least $k\ge 1$ with $\sigma^k=\mathrm{id}$. Landau's function is

$$g(n)=\max_{\sigma\in S_n}\operatorname{ord}(\sigma).$$

A partition of $n$ is a multiset of positive integers summing to $n$. The prime counting function $\pi(x)$ is the number of primes $p\le x$, the (offset) logarithmic integral is $\mathrm{Li}(x)=\int_2^x\frac{dt}{\ln t}$, and $\mathrm{Li}^{-1}$ is its inverse on $[2,\infty)$. Throughout, $\ln$ is the natural logarithm.

Formalization targets

Goal: Landau's theorem (1902)

$$\lim_{n\to\infty}\frac{\ln g(n)}{\sqrt{n\ln n}}=1.$$

Supporting milestones

1. Partition characterization: $g(n)=\max\{\operatorname{lcm}(\lambda):\lambda\vdash n\}$.
2. Initial values $g(0),\dots,g(8)=1,1,2,3,4,6,6,12,15$.
3. Nicolas (1968): for every $m$ there is $n$ with $g(n)=g(n+1)=\dots=g(n+m)$.
4. Massias–Nicolas–Robin (1988): $\ln g(n)=\sqrt{n\ln n}\Bigl(1+\frac{\ln\ln n-1}{2\ln n}-\frac{(\ln\ln n)^2-6\ln\ln n+9}{8(\ln n)^2}+O\bigl((\tfrac{\ln\ln n}{\ln n})^3\bigr)\Bigr)$.
5. Ford (2002): $\pi(x)-\mathrm{Li}(x)=O\bigl(x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})\bigr)$ for some $c>0$.
6. Massias–Nicolas–Robin (1988): if $\pi(x)-\mathrm{Li}(x)=O(R(x))$ with $R(x)=x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$, then $\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O\bigl(R(\sqrt{n\ln n})\ln n\bigr)$.
7. Riemann hypothesis criterion: $\ln g(n)<\sqrt{\mathrm{Li}^{-1}(n)}$ for all large $n$ $\iff$ RH.
8. $g(n)\le e^{n/e}$ for all $n$, with equality only at $n=0$.
9. Massias (1984): $g(n)\le\exp(1.05314\sqrt{n\ln n})$.

Significance

Landau's theorem pins down the growth rate of the largest element order in $S_n$, which bounds, for example, how long any fixed shuffle of $n$ cards can be repeated before the deck returns to its starting order. The refined statements quantify the second-order behaviour and connect it to the error term in the prime number theorem; the criterion in milestone 7 is one of the known elementary reformulations of the Riemann hypothesis, and is included as a faithful statement of the source, not as an expected deliverable. The other results are proved in the literature; formalizing them requires building the partition/lcm description of element orders in $S_n$ and quantitative prime-counting estimates on top of Mathlib.

Difficulty

The order of a permutation is easy to compute from its cycle type, but maximizing an lcm over all partitions is a non-linear optimization: the optimum uses prime powers whose sizes are dictated by the distribution of primes, so even the leading-order asymptotics need Chebyshev-type or prime number theorem estimates, and the refined milestones need the prime number theorem with an explicit error term.

Formalization scope

• $S_n$ is Equiv.Perm (Fin n); $g(n)$ is the supremum of orderOf σ over the finite group (a natural number; $g(0)=1$).
• Partitions are Mathlib's Nat.Partition n; the lcm of a partition is the Multiset.lcm of its parts.
• Real logarithms use Real.log (which returns $0$ at $0$ and is defined for negative input); all asymptotic statements are about $n\to\infty$, so the values at small $n$ are irrelevant there. The bounds in milestones 8–9 are stated for every $n$ and are true at $n=0,1$.
• $\pi(x)$ for real $x$ is Nat.primeCounting ⌊x⌋₊; $\mathrm{Li}$ is the offset logarithmic integral $\int_2^x dt/\ln t$; $\mathrm{Li}^{-1}(y)$ is the least $x\ge2$ with $\mathrm{Li}(x)\ge y$, which for $y\ge0$ is the inverse function value. Replacing $\mathrm{Li}$ by the full integral $\mathrm{li}$ changes the inverse by $O(\ln n)$ and does not affect any of the asymptotic statements.
• The Riemann hypothesis is Mathlib's RiemannHypothesis.

Contributions of reusable infrastructure (cycle-type lcm, prime-counting error terms, the logarithmic integral) are welcome.

Selected references

• E. Landau, Über die Maximalordnung der Permutationen gegebenen Grades, Arch. Math. Phys. Ser. 3, vol. 5, 1903.
• J.-L. Nicolas, Sur l'ordre maximum d'un élément dans le groupe $S_n$ des permutations, Acta Arithmetica 14 (1968), 315–332.
• J.-P. Massias, Majoration explicite de l'ordre maximum d'un élément du groupe symétrique, Ann. Fac. Sci. Toulouse Math. (5) 6 (1984), 269–281.
• J.-P. Massias, J.-L. Nicolas, G. Robin, Évaluation asymptotique de l'ordre maximum d'un élément du groupe symétrique, Acta Arithmetica 50 (1988), 221–242.
• K. Ford, Vinogradov's integral and bounds for the Riemann zeta function, Proc. London Math. Soc. 85 (2002), 565–633. https://doi.org/10.1112/S0024611502013655
• W. Miller, The maximum order of an element of a finite symmetric group, Amer. Math. Monthly 94 (1987), 497–506.
• OEIS A000793. https://oeis.org/A000793

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.

Motivation

A graph is symmetric when its automorphism group moves any vertex, edge or arc to any other, and $s$-arc-transitive when it moves any walk of length $s$ without immediate backtracking to any other. Tutte's work on cubic graphs made $s$-arc-transitivity a central measure of symmetry in algebraic graph theory, and most constructions of highly symmetric graphs start from a group acting regularly on vertices (Cayley graphs) or semiregularly with a few orbits.

Bi-Cayley graphs are the case of two orbits: a group $H$ acts semiregularly by right multiplication with exactly two vertex orbits. The Petersen graph, the Gray graph (the smallest cubic semisymmetric graph) and the smallest member of Bouwer's family of half-arc-transitive graphs are all bi-Cayley graphs, and all of them are edge-transitive. Deciding edge-transitivity of a bi-Cayley graph is hard in general, but the subgroup of automorphisms that normalise the semiregular group $R(H)$ is explicitly known, which makes the "normal" version of the question tractable.

C. H. Li asked whether 3-arc-transitive bi-normal Cayley graphs exist and asked for a description of the 2-arc-transitive ones (Li, Proc. Amer. Math. Soc. 133, Question 1.2(a) and Problem 1.3(b), as cited in the paper, p. 2). M. Conder, J.-X. Zhou, Y.-Q. Feng and M.-M. Zhang answered both through their Theorem 1.1 (arXiv:1606.04625v1; J. Combin. Theory Ser. B, 2020). This mission formalizes that theorem and the lemmas its proof uses.

Setting

Let $H$ be a finite group with identity $1$. Let $R, L, S \subseteq H$ with $|R| = |L|$, $1 \notin R = R^{-1}$ and $1 \notin L = L^{-1}$. The bi-Cayley graph $\Gamma = \mathrm{BiCay}(H,R,L,S)$ has vertex set $H_0 \cup H_1$, two disjoint copies of $H$ (the copy of $h$ in $H_i$ is $h_i$), and edges $\{h_0,(xh)_0\}$, $\{h_1,(yh)_1\}$ and $\{h_0,(zh)_1\}$ for $h \in H$, $x \in R$, $y \in L$, $z \in S$. The main theorem concerns $R = L = \emptyset$, where $\Gamma$ is bipartite with parts $H_0$, $H_1$ and every vertex has $|S|$ neighbours.

For $g \in H$, $R(g) : h_i \mapsto (hg)_i$ is an automorphism of $\Gamma$; these form the subgroup $R(H) \le \mathrm{Aut}(\Gamma)$, and

$$X = N_{\mathrm{Aut}(\Gamma)}(R(H))$$

is its normaliser. For $\alpha \in \mathrm{Aut}(H)$ (written as an exponent, $h \mapsto h^\alpha$) and $x, y, g \in H$ the paper defines the permutations

$$\delta_{\alpha,x,y} : h_0 \mapsto (xh^\alpha)_1,\ h_1 \mapsto (yh^\alpha)_0, \qquad \sigma_{\alpha,g} : h_0 \mapsto (h^\alpha)_0,\ h_1 \mapsto (gh^\alpha)_1,$$

and the sets $\mathrm{I}$ of those $\delta_{\alpha,x,y}$ with $R^\alpha = x^{-1}Lx$, $L^\alpha = y^{-1}Ry$, $S^\alpha = y^{-1}S^{-1}x$, and $\mathrm{F}$ of those $\sigma_{\alpha,g}$ with $R^\alpha = R$, $L^\alpha = g^{-1}Lg$, $S^\alpha = g^{-1}S$.

An $s$-arc is a sequence $(v_0,\dots,v_s)$ of vertices in which consecutive vertices are adjacent and $v_{i-1} \ne v_{i+1}$. A subgroup $K \le \mathrm{Aut}(\Gamma)$ is transitive on $s$-arcs if any $s$-arc can be mapped to any other by an element of $K$; 1-arcs are arcs. $\Gamma$ is normal edge-transitive if $X$ is transitive on edges, and normal locally arc-transitive if the stabiliser $X_{1_0}$ is transitive on the neighbourhood $\Gamma(1_0)$. $K$ acts semisymmetrically if it is edge-transitive but not vertex-transitive. $\mathrm{Aut}(H,\Delta)$ is the setwise stabiliser of $\Delta \subseteq H$ in $\mathrm{Aut}(H)$.

Formalization targets

Goal: Theorem 1.1

Let $\Gamma = \mathrm{BiCay}(H,\emptyset,\emptyset,S)$ be connected, with $1 \in S$ and $|S| \ge 2$. Then

$$X \text{ is transitive on the 2-arcs of } \Gamma \iff \text{(a)} \wedge \text{(b)} \wedge \text{(c)},$$

where (a) $S^\alpha = S^{-1}$ for some $\alpha \in \mathrm{Aut}(H)$; (b) $\mathrm{Aut}(H, S\setminus\{1\})$ is transitive on $S \setminus \{1\}$; (c) $S^\beta = s^{-1}S$ for some $s \in S\setminus\{1\}$ and $\beta \in \mathrm{Aut}(H)$. Furthermore, if $|S| \ge 3$, $X$ is not transitive on the 3-arcs of $\Gamma$.

Milestones

• Proposition 2.2 (cited by the paper from Zhou and Feng): for connected $\Gamma$, every element of $\mathrm{F}$ and of $\mathrm{I}$ is an automorphism in $X$, and $X = R(H)\,(\mathrm{F} \cup \mathrm{I})$.
• Proposition 2.2(a): for $\delta_{\alpha,x,y} \in \mathrm{I}$, $\langle R(H),\delta_{\alpha,x,y}\rangle$ is vertex-transitive.
• Lemma 3.2: $X_{1_01_1} = \{\sigma_{\alpha,1} \mid \alpha \in \mathrm{Aut}(H,S\setminus\{1\})\}$, and, for $|S| \ge 3$, $X$ is not 3-arc-transitive.
• Proposition 3.3: $\Gamma$ is normal locally arc-transitive iff $\Gamma(1_0)$ is an orbit of $\mathrm{F}$; in that case $X$ is arc-transitive iff $S^\alpha = S^{-1}$ for some $\alpha$, and semisymmetric otherwise.

A companion item, Lemma 3.1, shows that a connected normal edge-transitive $\mathrm{BiCay}(H,R,L,S)$ has $R = L = \emptyset$; it explains why the goal is stated for $\mathrm{BiCay}(H,\emptyset,\emptyset,S)$.

Significance

Combined with Lemma 3.1, Theorem 1.1 reduces 2-arc-transitivity of the normaliser of $R(H)$ to three conditions on $\mathrm{Aut}(H)$ and the single set $S$, all checkable in the group without building the graph. Its second part rules out normal 3-arc-transitive bi-Cayley graphs of valency at least 3, which settles Li's question on 3-arc-transitive bi-normal Cayley graphs negatively. Proposition 3.3 is the arc-transitive versus semisymmetric dichotomy for normal locally arc-transitive bi-Cayley graphs, the starting point of the paper's later constructions of semisymmetric and half-arc-transitive examples.

All results are proved in the paper (Proposition 2.2 by citation). None of them has a machine-checked proof that this mission knows of. Mathlib has simple graphs, graph isomorphisms and normalisers, but no bi-Cayley graphs, no $s$-arcs and no transitivity notions for subgroups of $\mathrm{Aut}(\Gamma)$. A formal proof would supply the first verified description of the normaliser of a semiregular group with two orbits, reusable for any bi-Cayley or bi-circulant result.

Difficulty

The bulk of the work is Proposition 2.2. That $\sigma_{\alpha,g}$ and $\delta_{\alpha,x,y}$ preserve edges exactly under the conditions of (2.2) is a direct computation. The converse is harder: every automorphism normalising $R(H)$ must be one of these permutations composed with some $R(h)$. That needs the conjugation action of $X$ on $R(H)$ to induce an automorphism of $H$, and $X$ to preserve the partition $\{H_0, H_1\}$ into $R(H)$-orbits.

The 3-arc clause looks like a stabiliser count, but it holds only once $1_1$ has at least two neighbours besides $1_0$: for $|S| = 2$ the graph is a cycle of length $2|H|$, the normaliser is the whole dihedral automorphism group, and that group is transitive on 3-arcs. Any proof must use $|S| \ge 3$ at exactly this step.

Formalization scope

The vertex set is H ⊕ H (Sum.inl h $= h_0$, Sum.inr h $= h_1$). The data $(R, L, S)$ is a structure of three Finsets carrying the side conditions $R^{-1} = R$, $L^{-1} = L$, $1 \notin R$, $1 \notin L$ and $|R| = |L|$. Adjacency is given directly by the three edge rules. $\mathrm{Aut}(\Gamma)$ is the group Γ ≃g Γ, $R(H)$ is the subgroup generated by the $R(g)$, and $X$ is its Subgroup.normalizer. Automorphisms of $H$ are MulAut H, and $\Delta^\alpha$ is the image of $\Delta$ under $\alpha$. $\sigma_{\alpha,g}$ and $\delta_{\alpha,x,y}$ are permutations of H ⊕ H, and "$\sigma_{\alpha,g} \in X$" means that some element of $X$ has $\sigma_{\alpha,g}$ as its vertex map. Products are written pointwise to avoid the composition-order convention of the group of graph automorphisms. An $s$-arc is a function on Fin (s+1).

The paper assumes throughout that groups and graphs are finite and graphs connected; each theorem carries Fintype H and connectivity. Three hypotheses are added to the printed Theorem 1.1, each needed for the statement to be true or non-vacuous: $1 \in S$ (the paper's normalisation of a bi-Cayley triple, used by conditions (b) and (c) and by the proof); $|S| \ge 2$ (for $|S| = 1$ the graph is $K_2$, which has no 2-arcs, so 2-arc-transitivity would hold vacuously while (c) fails); and $|S| \ge 3$ for the 3-arc clause (false for cycles). Lemma 3.2 carries the same $1 \in S$ and $|S| \ge 3$, and Proposition 3.3 carries $1 \in S$.

Trivializing formalizations are ruled out in four ways. 2-arc-transitivity is never vacuous, since $|S| \ge 2$ guarantees 2-arcs. $R$ and $L$ are never symmetrised silently, since the side conditions are data rather than repairs. Every transitivity statement is about $X$, not the full $\mathrm{Aut}(\Gamma)$. Valency is the degree in the graph, never a formula in $|S|$.

Contributions are welcome at every level: proofs of the milestones, a general library of bi-Cayley graphs and their normalisers, and lemmas on $s$-arcs and stabilisers in SimpleGraph. The definitions are repeated identically in the companion missions on bi-abelian graphs and bi-dihedrants.

Selected references

• M. Conder, J.-X. Zhou, Y.-Q. Feng and M.-M. Zhang, Edge-transitive bi-Cayley graphs, arXiv:1606.04625v1, 2016; J. Combin. Theory Ser. B, 2020. https://arxiv.org/abs/1606.04625v1, https://doi.org/10.1016/j.jctb.2020.05.006
• J.-X. Zhou and Y.-Q. Feng, The automorphisms of bi-Cayley graphs, J. Combin. Theory Ser. B 116 (2016) 504–532 (reference [55] of the paper; source of Proposition 2.2). https://doi.org/10.1016/j.jctb.2015.10.004
• C. H. Li, Finite s-arc transitive Cayley graphs and flag transitive projective planes, Proc. Amer. Math. Soc. 133 (2005) 31–41 (reference [29] of the paper; Question 1.2(a) and Problem 1.3(b)). https://doi.org/10.1090/S0002-9939-04-07549-5