Wolf: growth of finitely generated solvable groupsResearch Paper
## Motivation
This mission formalizes the group theory of J. A. Wolf's *Growth of finitely generated solvable
groups and curvature of Riemannian manifolds*, J. Differential Geometry 2 (1968) 421–446
([doi:10.4310/jdg/1214428658](https://doi.org/10.4310/jdg/1214428658)), namely its §3 and §4. Wolf
opens with the object of study: "If a group $\Gamma$ is generated by a finite subset $S$, then one
has the 'growth function' $g_S$, where $g_S(m)$ is the number of distinct elements of $\Gamma$
expressible as words of length $\le m$ on $S$" (p. 421). Section 3 proves that a group with a
finitely generated nilpotent subgroup of finite index "is of polynomial growth, and in fact
$c_1m^{E_1(\Delta)} \le g_S(m) \le c_2m^{E_2(\Delta)}$"; section 4 proves that "a polycyclic group,
either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial
growth, or has no such subgroup and is of exponential growth" (p. 421).
Applying Milnor's companion note, which is the complete mission
[Milnor: growth of finitely generated solvable groups](https://prove2.me/missions/Milnor%3A%20growth%20of%20finitely%20generated%20solvable%20groups)
on this platform, Wolf concludes "that a finitely generated solvable group, either is polycyclic and
has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent
subgroup of finite index and is of exponential growth" (p. 421). That is the Milnor–Wolf theorem,
the goal here, and Wolf's Theorem 4.8. It prompted the question Wolf asks on p. 422, "whether every
finitely generated group $\Gamma$, which is not of exponential growth, necessarily has a nilpotent
subgroup of finite index"; Grigorchuk's groups of intermediate growth
([1984](https://doi.org/10.1070/IM1985v025n02ABEH001281)) answered it in the negative, and Gromov
([1981](https://doi.org/10.1007/BF02698687)) proved that polynomial growth alone does force a
nilpotent subgroup of finite index.
## Setting
**Growth.** For a finite subset $S$ of a group $\Gamma$, the **growth function** $g_S(m)$ counts
the elements expressible as words of length $\le m$ on $S$, a word $s_1^{a_1} \cdots s_r^{a_r}$
having length $|a_1| + \cdots + |a_r|$ (p. 426). The published `MilnorWolf.growthFunction S m` takes
this as the size of the ball `Chou.wordBall S m`, the set of products of at most $m$ factors from
$S \cup S^{-1}$. Wolf's two kinds of bound (p. 421) are **polynomial growth of degree $\le E$**,
$g_S(m) \le c \cdot m^E$, and **exponential growth**, $u \cdot v^m \le g_S(m)$ with $v > 1$; the
published predicates are `MilnorWolf.HasPolynomialGrowthOfDegreeLE` and
`Chou.HasExponentialGrowth`, the latter with $u = 1$, which is what Theorem 4.3 actually produces.
Both quantify over some finite generating set, and Wolf shows (p. 427, p. 434) that neither depends
on which one.
**Growth exponents.** For a finitely generated nilpotent $\Delta$ with lower central series
$\Delta = \Delta_0 \supseteq \Delta_1 \supseteq \cdots \supseteq \Delta_{s+1} = \{1\}$, each factor
$\Delta_k/\Delta_{k+1}$ is finitely generated abelian with free part of rank $n_k$; Wolf's (3.3)
sets $E_1(\Delta) = \sum_k (k+1)n_k$ and $E_2(\Delta) = \sum_k 2^kn_k$. These are
`MilnorWolf.growthExponentOne` and `MilnorWolf.growthExponentTwo`.
**Polycyclic groups.** A solvable group is **polycyclic** if it satisfies condition (1) of
Proposition 4.1: "There is a normal series
$\Gamma = A_0 \supset A_1 \supset \cdots \supset A_t = \{1\}$ with every quotient $A_i/A_{i+1}$
finite or infinite cyclic" (p. 433), where a normal series, as in Kurosh, has each term normal in
the preceding one. This is `MilnorWolf.IsPolycyclic`. **Solvable** is Mathlib's
`Group.IsSolvable`.
## Formalization targets
The goal is Wolf's Theorem 4.8 (p. 438): "Let $\Gamma$ be a finitely generated solvable group. If
$\Gamma$ has a nilpotent subgroup $\Delta$ of finite index, then $\Gamma$ is polycyclic and of
polynomial growth of degree $\le E_2(\Delta)$. If $\Gamma$ does not have a nilpotent subgroup of
finite index, then $\Gamma$ is of exponential growth."
The milestones are the results it rests on, in the paper's order. Section 3 climbs from two
rescaling lemmas (3.4, 3.5) and the growth function of a free abelian group (3.6) through generating
sets adapted to the lower central series (3.7) to the polynomial bounds for a finitely generated
nilpotent group (3.2), then passes them to a group with a finite-index subgroup (3.11). Section 4
characterises polycyclic groups (4.1, whose one hard input is Hirsch's theorem, a milestone of its
own) and proves the polycyclic dichotomy (4.3). Milnor's Theorem, already proved on this platform,
appears as a reference milestone: it is what carries 4.3 from polycyclic to solvable, and Wolf notes
on p. 437 that "J. Milnor extended the scope of Theorem 4.3 by proving [10] that a finitely
generated nonpolycyclic solvable group must be of exponential growth."
## Significance
Theorem 4.8 is the first growth dichotomy: within finitely generated solvable groups there is
nothing between polynomial and exponential, and the polynomial side is exactly the almost nilpotent
one. It is the result Gromov's theorem generalises in one direction and Grigorchuk's groups bound in
the other, and the reason a group of intermediate growth can be neither solvable nor elementary
amenable, which is how those groups were first placed outside both classes. Chou's Theorem 3.2, in
the mission
[Chou: elementary amenable groups](https://prove2.me/missions/Chou%3A%20elementary%20amenable%20groups),
extends exactly this statement to elementary amenable groups and cites both halves.
Section 3 also has independent value. The polynomial bounds with the explicit exponents $E_1$ and
$E_2$ from the lower central series are sharper than the usual textbook statement that a finitely
generated nilpotent group has polynomial growth, and the pieces along the way are reusable: the
growth function of $\mathbb Z^n$ in closed form, and the fact that polynomial growth of a given
degree is inherited from a finite-index subgroup.
## Difficulty
The hard milestone is the second half of Theorem 4.3, that a polycyclic group with no nilpotent
subgroup of finite index has exponential growth. Wolf proves it through Proposition 4.4, which
passes to a Malcev completion and reads the eigenvalues of the induced Lie algebra automorphisms;
that machinery is not in Mathlib and is not part of this mission. A route that avoids it: a
polycyclic group acts on a free abelian factor of its chain by integer matrices, so either some
element has an eigenvalue off the unit circle, and then the separation argument of Wolf's p. 437
applies verbatim with that factor in place of the Lie algebra, or every eigenvalue of every element
lies on the unit circle, and then Kronecker's theorem, which Mathlib has, makes them all roots of
unity, so a finite-index subgroup acts unipotently and is nilpotent. Wolf records in the "Added in
Proof" (p. 445) that "B. Hartley recently sent me a manuscript consisting of an alternate proof that
a polycyclic group without nilpotent subgroups of finite index is of exponential growth."
Theorem 3.2 is long rather than deep: the lower bound (3.8) and the upper bound (3.9), (3.10) are
two inductions along the lower central series, each carrying explicit word-length bookkeeping, and
both need the adapted generating sets of Lemma 3.7. Mathlib has no polycyclic groups, so
Proposition 4.1 starts from nothing; it also lacks Hirsch's theorem and P. Hall's finite
presentability results, which is why Hirsch is stated here as its own milestone rather than assumed.
## Formalization scope
No new definitions: every notion is taken from the published bundles `Chou_Growth` and
`MilnorWolf_Growth`, so the statements here are directly comparable with those of the Chou and
Milnor missions. Growth is measured on closed balls, `Chou.wordBall S m` being the products of at
most $m$ letters from $S \cup S^{-1}$ and $g_S(m)$ its cardinality, finite because $S$ is a
`Finset`. "Not of exponential growth" is the negation of an existential, so it is a statement about
every finite generating set.
Conditions (8) to (11) of Proposition 4.1, Proposition 4.4 and the Lie-theoretic apparatus of §4,
and the Riemannian geometry of §2, §5 and §6, are outside this mission; Proposition 4.1 is stated
here with its first seven conditions, which are the ones §4 uses. Hirsch's theorem is cited, not
proved, by Wolf, and appears as a milestone under its own source (Proc. London Math. Soc. 44 (1938)
53–60) rather than as an omission. Cheeger's and Hartley's sharpenings, recorded in Wolf's "Added in
Proof", are not included.
No hypothesis is vacuous: the free abelian groups witness Proposition 3.6 and Theorem 3.2, a
polycyclic group with no nilpotent subgroup of finite index exists (the semidirect product
$\mathbb Z^2 \rtimes_A \mathbb Z$ for a hyperbolic $A \in SL_2(\mathbb Z)$, which is Wolf's own
example of the exponential case), and the lamplighter group $\mathbb Z/2 \wr \mathbb Z$ is finitely
generated solvable and not polycyclic, so Theorem 4.8's second alternative is not empty either.
Contributions welcome: proofs of any milestone, and the general library results they need, such as
polycyclic groups and Hirsch's theorem.
## Selected references
- J. A. Wolf, *Growth of finitely generated solvable groups and curvature of Riemannian manifolds*,
J. Differential Geometry 2 (1968), 421–446.
[doi:10.4310/jdg/1214428658](https://doi.org/10.4310/jdg/1214428658)
- J. Milnor, *Growth of finitely generated solvable groups*, J. Differential Geometry 2 (1968),
447–449. [doi:10.4310/jdg/1214428659](https://doi.org/10.4310/jdg/1214428659)
- J. Milnor, *Problem 5603*, Amer. Math. Monthly 75 (1968), 685–686. The identifier is for the
Advanced Problems section 5600–5609 that contains it:
[doi:10.2307/2313822](https://doi.org/10.2307/2313822)
- K. A. Hirsch, *On infinite soluble groups. I*, Proc. London Math. Soc. 44 (1938), 53–60.
[doi:10.1112/plms/s2-44.1.53](https://doi.org/10.1112/plms/s2-44.1.53)
- A. G. Kurosh, *Theory of groups*, vol. II, 2nd ed., translated by K. A. Hirsch, Chelsea, 1955.
Scanned at
[archive.org/details/a.-g.-kurosh-the-theory-of-groups-volume-2-1960](https://archive.org/details/a.-g.-kurosh-the-theory-of-groups-volume-2-1960).
- A. I. Mal'cev, *On certain classes of infinite solvable groups*, Amer. Math. Soc. Transl. (2) 2
(1956), 1–21. [doi:10.1090/trans2/002/01](https://doi.org/10.1090/trans2/002/01)
- R. G. Swan, *Representations of polycyclic groups*, Proc. Amer. Math. Soc. 18 (1967), 573–574.
[doi:10.1090/S0002-9939-1967-0213442-5](https://doi.org/10.1090/S0002-9939-1967-0213442-5)
- M. Gromov, *Groups of polynomial growth and expanding maps*, Publ. Math. IHÉS 53 (1981), 53–78.
[doi:10.1007/BF02698687](https://doi.org/10.1007/BF02698687)
- R. I. Grigorchuk, *Degrees of growth of finitely generated groups, and the theory of invariant
means*, Math. USSR-Izv. 25 (1985), 259–300 (Russian original 1984).
[doi:10.1070/IM1985v025n02ABEH001281](https://doi.org/10.1070/IM1985v025n02ABEH001281)
- C. Chou, *Elementary amenable groups*, Illinois J. Math. 24 (1980), 396–407.
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)
16 thms1 active userReviewed
Captain: Lucas
Tarcha: Braid Theory and the Artin Presentation with Explicit Half-Twist GeneratorsTextbook
## Motivation
A **braid** on $n$ strands is the everyday object it sounds like: $n$ strings hanging between two
horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned
this picture into algebra in 1925 by showing that braids form a group under concatenation and that
this group has a finite presentation with $n-1$ generators. The braid groups sit at the crossroads
of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of
braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free
and orderable), and of representation theory and mathematical physics through the Burau, Lawrence–
Krammer and Temperley–Lieb representations.
This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander
Andrey Gomes Tarcha's *Um Estudo Introdutório da Teoria de Tranças* (UNESP, Rio Claro), whose
capstone is Teorema 3.15: the braid group on $n$ strands admits Artin's presentation. The
dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9),
shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation
relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two
structural properties: the full twist is central (Proposição 3.16) and $B_m$ embeds in $B_n$ for
$m \le n$ (Proposição 3.17).
## Setting
Work in the plane $E^2 = \mathbb{C}$. The **ordered configuration space**
$$F_{0,n}E^2 = \{(z_1,\dots,z_n) \in \mathbb{C}^n : z_k \neq z_l \text{ for } k \neq l\}$$
carries the subspace topology of $\mathbb{C}^n$, and the symmetric group $\Sigma_n$ acts on it by
permuting coordinates. The **unordered configuration space** $B_{0,n}E^2 = F_{0,n}E^2/\Sigma_n$
carries the quotient topology; its points are the $n$-element subsets of the plane. The base
configuration is $(1,2,\dots,n)$, and $*$ denotes its class in $B_{0,n}E^2$. The **geometric braid
group** is
$$\pi_1\bigl(B_{0,n}E^2, *\bigr),$$
a loop of $n$-point configurations being exactly a geometric braid, and homotopy of loops being
exactly the equivalence by elementary moves used in the dissertation.
The **elementary half-twist** $\sigma_{i+1}$, for $0 \le i \le n-2$, is the loop that rotates the
two base points $i+1$ and $i+2$ by the angle $\pi$ about their midpoint $i + \tfrac32$, leaving the
other $n-2$ points fixed:
$$t \;\longmapsto\; \Bigl\{\, i+\tfrac32 \pm \tfrac12 e^{\pi i t} \,\Bigr\} \;\cup\;
\{\,k+1 : k \neq i,\, i+1 \,\}, \qquad t \in [0,1].$$
It returns to the base configuration at $t = 1$ with the two moving points interchanged, so it is a
loop in $B_{0,n}E^2$ and defines a class in $\pi_1(B_{0,n}E^2,*)$.
The **abstract braid group** $B_n$ is the group presented by 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} \quad (1 \le i \le n-2).$$
## Formalization targets
### Goal — Teorema 3.15, with the isomorphism pinned on generators
$$\exists\, \varphi : B_n \;\xrightarrow{\ \sim\ }\; \pi_1\bigl(B_{0,n}E^2,*\bigr), \qquad
\varphi(\sigma_{i+1}) = \bigl[\text{half-twist}_i\bigr] \ \ (0 \le i \le n-2).$$
This is the statement the dissertation actually proves: the map $\varphi$ of its proof is defined on
generators by $\varphi(x_i) = [\sigma_i]$, and the work consists in showing that it is a
well-defined homomorphism which is surjective and injective. Asking only for an abstract
isomorphism would leave the generators unconstrained; naming their images is what makes the
presentation usable downstream.
### Milestones
$$\langle\,[\text{half-twist}_i]\,\rangle = \pi_1\bigl(B_{0,n}E^2,*\bigr) \qquad \text{(Teorema 3.11)}$$
$$[\text{half-twist}_i][\text{half-twist}_j] = [\text{half-twist}_j][\text{half-twist}_i]\ (|i-j|\ge 2),
\qquad
[\text{ht}_i][\text{ht}_{i+1}][\text{ht}_i] = [\text{ht}_{i+1}][\text{ht}_i][\text{ht}_{i+1}]$$
$$\forall b \in B_2,\ \exists m \in \mathbb{Z},\ b = \sigma_1^m \qquad \text{(Proposição 3.13)}$$
$$\forall b \in B_3,\ b = \sigma_1^{a_1}\sigma_2^{b_1}\cdots\sigma_1^{a_m}\sigma_2^{b_m}
\qquad \text{(Proposição 3.14)}$$
$$(\sigma_1\sigma_2\cdots\sigma_{n-1})^n \in Z(B_n) \qquad \text{(Proposição 3.16)}$$
$$B_m \hookrightarrow B_n \ \ (m \le n) \qquad \text{(Proposição 3.17)}$$
## Significance
Artin's presentation is what makes the braid groups computable: the word problem, the Burau and
Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form
all start from generators and relations, while the topological side supplies the meaning of those
generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute
with a given geometric braid; the version stated here transports each half-twist loop to a
generator word, which is what downstream work needs.
On the formalization side, the geometric model (configuration spaces and their fundamental groups)
and the algebraic model (a presented group) are already available on the platform in this
environment, and the abstract form of Artin's theorem is already stated there as an open problem.
What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in
$B_{0,n}E^2$ — this definition is proved sorry-free here, including the injectivity of the moving
configuration at every time and the continuity of the path; the sharpened goal that fixes the
isomorphism on generators; and the dissertation's supporting results, none of which is currently
on the platform. None of the milestones or the goal has a machine-checked proof yet.
## Difficulty
Surjectivity of $\varphi$ — every braid is a product of half-twists — is a compactness-and-general-
position argument in the dissertation: cut the braid into finitely many slabs in which a single
crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since
"general position" is not available for free: a loop of configurations must be subdivided and each
piece pushed to a standard crossing.
Injectivity is harder and is the step where a naive approach fails. It is not enough to check that
the relations hold; one has to know that they are *all* the relations, i.e. that a word whose braid
is null-homotopic is a consequence of the braid relations. The dissertation follows the classical
route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a
long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with
an induction on $n$; its inductive step needs the exact sequence of the fibration
$F_{0,n}E^2 \to F_{0,n-1}E^2$, which is itself substantial work.
## Formalization scope
The plane is $\mathbb{C}$; configurations are injective tuples indexed by `Fin n`; the unordered
configuration space is the quotient by the coordinate-permutation action with the quotient
topology; the base configuration is $(1,2,\dots,n)$ (not $(0,1,\dots,n-1)$). Braid generators are
indexed by `Fin (n-1)`, the index $i$ standing for the book generator $\sigma_{i+1}$; truncated
natural subtraction means the degenerate values $n = 0, 1$ give the trivial group, and the
statements are asserted for all $n$ including those cases. The abstract braid group is the
presented group on `Fin (n-1)` modulo the normal closure of the commutation and braid relators.
The half-twist rotates counterclockwise. The mirror symmetry $z \mapsto \bar z$ fixes the base
configuration and exchanges the two orientations, so the goal statement does not depend on this
choice; a solver may use either convention internally.
The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the
generators are the prescribed classes of explicit loops, so neither the identity on a presented
group nor an abstract counting argument suffices.
Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the
pure braid group as the kernel of the map to $\Sigma_n$, the exponent-sum homomorphism, and
torsion-freeness of $B_n$. The half-twist definition published with this mission is reusable for
any further work on braids in this environment.
## Selected references
- Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, master's
dissertation, UNESP Rio Claro, 2023. https://repositorio.unesp.br/items/9d2ffbf0-8bd2-4ec7-9e45-e2cee8a1b202
- Emil Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- Joan S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
- Edward Fadell and Lee Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962),
111–118. https://doi.org/10.7146/math.scand.a-10517
42 thms5 active usersReviewed
Captain: Lucas
Faithfulness of the Burau representation of B4Research Paper
## 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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://doi.org/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](https://doi.org/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](https://doi.org/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](https://doi.org/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](https://doi.org/10.2140/gt.1999.3.397).
7 thms2 active usersReviewed
Captain: Lucas
Braids, Links and Mapping Class Groups I: Artin's Presentation of the Braid GroupTextbook
## Motivation
The **braid group** is one of the places where group theory, low-dimensional topology and
knot theory meet. Artin introduced it in 1925 (E. Artin, *Theorie der Zöpfe*, Abh. Math. Sem.
Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard
equipment in the study of links (closed braids and Markov's theorem), of mapping class groups
of punctured surfaces, and of configuration spaces. Birman's *Braids, Links, and Mapping Class
Groups* (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical
reference that develops all three subjects from the braid group outwards, and its Chapter 1
is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the
book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the
mapping class group of the punctured sphere — is phrased in terms of the group
$\pi_1 B_{0,n}E^2$ and of the presentation established here. A mission that fixes faithful Lean
definitions of the configuration spaces and of the abstract braid group therefore fixes the
vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the
characterization of braid automorphisms of a free group; Chow (1948) determined the centre;
Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk
(1962) used them to give the proof of the presentation reproduced by Birman.
## Setting
Write $E^2$ for the Euclidean plane, identified throughout with the complex numbers $\mathbb{C}$.
For $n \ge 0$ let
$$F_{0,n}E^2 = \{\,(z_1,\dots,z_n) \in \mathbb{C}^n : z_i \neq z_j \text{ for } i \neq j\,\}$$
be the **ordered configuration space** of $n$ points in the plane, topologized as a subspace of
$\mathbb{C}^n$. The symmetric group $\Sigma_n$ acts on it by permuting coordinates; the quotient
$$B_{0,n}E^2 = F_{0,n}E^2 / \Sigma_n,$$
with the quotient topology, is the **unordered configuration space**. A point of $B_{0,n}E^2$ is
an unordered set of $n$ distinct points of the plane. The base configuration is
$\bar z^{\,0} = (1,2,\dots,n)$, and all fundamental groups below are taken at $\bar z^{\,0}$ or at
its image.
The **braid group of the plane** is $\pi_1 B_{0,n}E^2$: a loop is a motion of $n$ points of the
plane returning to the same set of points, and homotopy classes of such motions compose as
braids. The **pure braid group** is $P_n = \pi_1 F_{0,n}E^2$, the subgroup of motions returning
each point to its own starting position.
Separately, let $B_n$ denote the abstract group given by 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} \quad (1 \le i \le n-2).$$
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically $\sigma_i$ interchanges the
$i$-th and $(i+1)$-st points along a semicircle.
## Formalization targets
### Goal — Theorem 1.8 (Artin, 1925; Birman p. 18)
$$B_n \;\cong\; \pi_1 B_{0,n} E^2 .$$
The group of motions of $n$ points of the plane is the group with generators
$\sigma_1,\dots,\sigma_{n-1}$ and the two families of relations above: the relations are not only
valid but *defining*.
### Milestones
The milestone list follows the chapter: the covering-space description of the projection
$F_{0,n}E^2 \to B_{0,n}E^2$ (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence
(Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group
(Corollary 1.8.1, p. 24), the faithful representation of $B_n$ by automorphisms of a free group
(Corollary 1.8.3, p. 25), the centre of $B_n$ (Corollary 1.8.4, p. 28, due to Chow), and Artin's
algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
## Significance
Theorem 1.8 is what makes the braid group *computable*: with defining relations in hand one can
combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent
braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2
and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids
into concrete data — a braid is determined by what it does to the generators of a free group —
and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine
behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the
fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid
groups and no configuration spaces: nothing here can be assembled from existing declarations.
The mission therefore produces reusable infrastructure — configuration spaces of the plane, the
symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as
machine-checked proofs of results that are classical but, as far as the mission's search of the
library showed, not yet formalized in Mathlib.
## Difficulty
The generators and relations are easy to write down and easy to verify *in* $\pi_1 B_{0,n}E^2$;
what is hard is completeness, i.e. that no further relations are needed. The naive route —
draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do.
The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on $n$ driven by
the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$: its homotopy exact sequence gives a split extension
of $P_{n-1}$ by a free group, presentations are assembled along the extension, and finally the
covering $F_{0,n}E^2 \to B_{0,n}E^2$ with deck group $\Sigma_n$ transfers the answer from the pure
braid group to the full braid group. Each of those steps needs genuine algebraic topology —
local triviality of the projection, exactness of the homotopy sequence, freeness of
$\pi_1$ of a punctured plane — which is where the formalization work actually lies.
## Formalization scope
The plane is $\mathbb{C}$. $F_{0,n}E^2$ is the subtype of injective functions
$\mathrm{Fin}\,n \to \mathbb{C}$; $B_{0,n}E^2$ is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
$i \mapsto i+1$, i.e. $(1,2,\dots,n)$, and its image. Fundamental groups are Mathlib's
`FundamentalGroup` at those base points. Braid generators are indexed by $\mathrm{Fin}(n-1)$
with $0$-based indices ($i$ stands for $\sigma_{i+1}$), and free-group generators by
$\mathrm{Fin}\,n$; the abstract braid group is a `PresentedGroup` on that index set. Truncated
subtraction makes the generator set empty for $n \le 1$, so $B_0$ and $B_1$ are trivial, as
intended. Two milestones are stated with the shift $n \mapsto n+1$ (i.e. for the projection
$F_{0,n+1}E^2 \to F_{0,n}E^2$) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to
the prose. First, the goal asserts the existence of *some* isomorphism $B_n \cong \pi_1B_{0,n}E^2$;
it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops
are not part of the formal development. Second, Artin's representation is formalized as the
existence of a homomorphism $\xi$ from $B_n$ to the automorphism group of the free group whose
value on each $\sigma_i$ is the explicit endomorphism of equation (1-14), together with its
injectivity; Theorem 1.9 is then stated for an arbitrary such $\xi$, given as a hypothesis, and
is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two
groups that are both defined independently of it, and the degenerate cases $n \le 1$ (both sides
trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of $\pi_1$ of a punctured
plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a
fibration in the range needed, presentations of split extensions, and the transfer of a
presentation along a regular covering. Contributions of any of these as standalone lemmas are
welcome, as is a formalization of the geometric generators (1-9) that would let the goal be
strengthened to pin the isomorphism on $\sigma_i$.
## Selected references
- E. Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- E. Artin, *Theory of braids*, Annals of Mathematics 48 (1947), 101–126.
https://doi.org/10.2307/1969218
- W.-L. Chow, *On the algebraical braid group*, Annals of Mathematics 49 (1948), 654–658.
https://doi.org/10.2307/1969333
- E. Fadell, L. Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962), 111–118.
https://doi.org/10.7146/math.scand.a-10517
- E. Fadell, J. Van Buskirk, *The braid groups of $E^2$ and $S^2$*, Duke Mathematical Journal 29
(1962), 243–257. https://doi.org/10.1215/S0012-7094-62-02925-3
- J. S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
39 thms5 active usersReviewed
Captain: Lucas
The Inverse Galois ProblemOpen Problem
## 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](https://en.wikipedia.org/wiki/Inverse_Galois_problem).
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](https://arxiv.org/abs/2411.07857)) 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
22 thms3 active usersReviewed
Captain: xuanji
230 space groupsTextbook
## 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](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). 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`](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The accompanying [benchmark manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml) 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), $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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean).
## 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), 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](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean); [manifest with historical bibliography](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml).
- Oliver Knill. *Some Fundamental Theorems in Mathematics*, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. [Full text](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). This provides background for the three counts; the exact formal conventions are those of LeanEval above.