Algebraic Topology

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

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

Motivation

The fundamental group $\pi_1(X, x_0)$ is the first algebraic invariant a student of topology meets, and $\pi_1(S^1)\cong\mathbb{Z}$ is the first computation of it that carries real content. Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; freely available at pi.math.cornell.edu/~hatcher/AT/AT.pdf) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).

This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace Hatcher.

Setting

A path in a topological space $X$ is a continuous map $f : I \to X$, where $I = [0,1]$. A homotopy of paths is a family $f_t : I \to X$, $0 \le t \le 1$, such that the endpoints $f_t(0) = x_0$ and $f_t(1) = x_1$ are independent of $t$ and the associated map $F : I \times I \to X$, $F(s,t) = f_t(s)$, is continuous. A loop at a basepoint $x_0$ is a path with $f(0) = f(1) = x_0$. The set of homotopy classes $[f]$ of loops at $x_0$ is the fundamental group $\pi_1(X, x_0)$; its product is $[f][g] = [f\cdot g]$, where $f\cdot g$ traverses $f$ and then $g$, each at double speed (Hatcher, Proposition 1.3).

The circle $S^1 \subset \mathbb{R}^2$ is realised as the unit circle of $\mathbb{C}$, so the point $(\cos\theta, \sin\theta)$ is $e^{i\theta}$ and the basepoint $(1,0)$ is $1$. Hatcher's map

$$p : \mathbb{R} \to S^1, \qquad p(s) = (\cos 2\pi s, \sin 2\pi s) = e^{2\pi i s}$$

is Hatcher.circleCover. The loops

$$\omega_n(s) = (\cos 2\pi n s, \sin 2\pi n s) = p(ns), \qquad n \in \mathbb{Z},$$

based at $(1,0)$ are Hatcher.omegaLoopN n, and $\omega = \omega_1$ is Hatcher.omegaLoop; its class $[\omega] \in \pi_1(S^1, 1)$ is Hatcher.omegaClass.

A covering space of $X$ is a space $\tilde X$ together with a map $p : \tilde X \to X$ such that every $x \in X$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher's condition $(\ast)$, p. 29; such a $U$ is evenly covered). A lift of a map $f : Y \to X$ is a map $\tilde f : Y \to \tilde X$ with $p \circ \tilde f = f$.

Formalization targets

Goal (Theorem 1.7)

$\pi_1(S^1, 1)$ is an infinite cyclic group generated by $[\omega]$. In the form stated in Lean:

$$\forall\, g \in \pi_1(S^1, 1)\quad \exists!\, n \in \mathbb{Z}:\quad [\omega]^n = g.$$

Surjectivity of $n \mapsto [\omega]^n$ says $[\omega]$ generates; uniqueness of $n$ says the group is infinite cyclic rather than finite.

Milestones on the road to the goal

1. $p(s) = e^{2\pi i s}$ is a covering space of $S^1$ (Hatcher, p. 29).
2. Homotopy lifting property (c): for a covering space $p : \tilde X \to X$, a map $F : Y \times I \to X$ and a lift of $F|_{Y \times \{0\}}$ extend uniquely to a lift of $F$ (p. 30).
3. Path lifting property (a): a path $f$ starting at $x_0$ and a point $\tilde x_0 \in p^{-1}(x_0)$ determine a unique lift $\tilde f$ starting at $\tilde x_0$ (p. 29).
4. Lifting homotopies of paths (b): a homotopy of paths $f_t$ starting at $x_0$ lifts uniquely to a homotopy of paths $\tilde f_t$ starting at $\tilde x_0$ (p. 29).
5. Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n \in \mathbb{Z}$ (the reformulation of Theorem 1.7 that Hatcher actually proves, p. 29).
6. $[\omega]^n = [\omega_n]$ for every $n \in \mathbb{Z}$ (Hatcher's remark after Theorem 1.7, p. 29).

Applications (Theorems 1.8–1.10)

$$\text{Every nonconstant } f \in \mathbb{C}[z] \text{ has a root in } \mathbb{C}.$$ $$\text{Every continuous } h : D^2 \to D^2 \text{ has a fixed point.}$$ $$\text{Every continuous } f : S^2 \to \mathbb{R}^2 \text{ satisfies } f(x) = f(-x) \text{ for some } x \in S^2.$$

Significance

The result itself. The computation $\pi_1(S^1) \cong \mathbb{Z}$ assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.

Formalizing it. Mathlib (revision 0df444a) already contains the covering-space infrastructure: IsCoveringMap, path lifting (IsCoveringMap.liftPath, eq_liftPath_iff'), homotopy lifting (IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff'), monodromy, and the fact that Circle.exp is a covering map (Circle.isCoveringMap_exp). It also has FundamentalGroup X x as the endomorphism group of the fundamental groupoid. It does not contain the computation $\pi_1(S^1) \cong \mathbb{Z}$, nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as Complex.exists_root (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.

Difficulty

The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because $\arg$ is discontinuous on $S^1$; the integer has to be produced by lifting the loop through $p$ and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of $n$: this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.

Connecting the concrete loops to Mathlib's abstract $\pi_1$ is its own obstacle. FundamentalGroup Circle 1 multiplies by composing morphisms of the fundamental groupoid, so identifying $[\omega]^n$ with the class of the explicit loop $\omega_n$ (milestone 6) requires reparametrization arguments for concatenated paths, for negative $n$ as well as positive.

For Theorem 1.9 the difficulty is the construction and continuity of the retraction $r : D^2 \to S^1$ from a fixed-point-free map, and then the non-existence of a retraction, which uses that $\pi_1(S^1) \neq 0$. For Theorem 1.10 Hatcher's proof lifts a loop $g(s) = f(\cos 2\pi s, \sin 2\pi s)/\lvert \cdots \rvert$ through $p$ and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.

Formalization scope

• $S^1$ is Circle (the unit circle in $\mathbb{C}$) with basepoint 1; $D^2$ is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1; $S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, with $-x$ the antipodal point.
• A covering space is Mathlib's IsCoveringMap p. This agrees with Hatcher's condition $(\ast)$; neither requires $p$ to be surjective.
• Paths are continuous maps C(I, X) or Mathlib Paths; for homotopies of paths, the square is written I × I with Hatcher's coordinate order $F(s,t) = f_t(s)$: the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is Y × I with $Y$ an arbitrary topological space, as in Hatcher.
• $\pi_1(S^1, 1)$ is Mathlib's FundamentalGroup Circle 1, and $[\omega]$ is FundamentalGroup.fromPath ⟦omegaLoop⟧. Because the goal quantifies over integer powers of a single element, the order of multiplication in FundamentalGroup is immaterial to its truth.
• The goal is stated as $\forall g\, \exists! n,\ [\omega]^n = g$ rather than as an abstract isomorphism with $\mathbb{Z}$, so that the generator is pinned to Hatcher's explicit loop; an isomorphism FundamentalGroup Circle 1 ≃* Multiplicative ℤ sending $[\omega]$ to $1$ is an immediate corollary and a welcome contribution.
• "Nonconstant polynomial" is 0 < f.degree, which excludes both the zero polynomial and nonzero constants.

Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism $\pi_1(S^1,1) \to \mathbb{Z}$ packaged for reuse, and any lemma about concatenation and reparametrization of loops in Circle that later chapters of the series can import.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.1, "The Fundamental Group of the Circle", pp. 29–33. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Mathematische Annalen 71 (1911), 97–115. https://doi.org/10.1007/BF01456931
• K. Borsuk, Drei Sätze über die n-dimensionale euklidische Sphäre, Fundamenta Mathematicae 20 (1933), 177–190. https://doi.org/10.4064/fm-20-1-177-190
• Mathlib, Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting for covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean
• Mathlib, Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (the fundamental group). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

Motivation

How many ways can a closed orientable surface of genus $g$ be "coloured" by a finite group $G$? Precisely: how many group homomorphisms $\pi_1(\Sigma_g)\to G$ are there? The answer is the partition function of two-dimensional Dijkgraaf–Witten theory with gauge group $G$. That theory is the simplest topological quantum field theory (TQFT) in the sense of Atiyah and Segal, and the standard test case for gauge theory with a finite gauge group (Dijkgraaf–Witten 1990, Freed–Quinn 1993). The count has a closed form in terms of the dimensions of the irreducible representations of $G$ alone. It is known as Mednykh's formula.

Timeline. Frobenius (1896) counted pairs with a prescribed commutator, $\#\{(a,b):[a,b]=z\}$, in terms of characters, which is the genus-one case. Frobenius and Schur (1906) treated the non-orientable analogue. Mednykh (1978) proved the formula for every genus using character theory and the standard presentation of $\pi_1(\Sigma_g)$. It was rediscovered in physics as the partition function of 2D and 3D finite-gauge-group TQFTs (Freed–Quinn 1993), and reproved with matrix integrals (Mulase–Yu 2005) and with lattice TQFTs (Snyder 2007). The last paper fixes the form of the statement used here.

Setting

Let $G$ be a finite group. A surface tuple of genus $g$ in $G$ is a family $x=((x_1,y_1),\dots,(x_g,y_g))\in(G\times G)^g$. Its commutator product is

$$\mathrm{commProd}(x)=[x_1,y_1]\,[x_2,y_2]\cdots[x_g,y_g],\qquad [x,y]=xyx^{-1}y^{-1},$$

multiplied left to right. For $z\in G$ let $N_g(z)=\#\{x\in(G\times G)^g:\mathrm{commProd}(x)=z\}$ (commCount G g z). The surface group $\Gamma_g$ (SurfaceGroup g) is the presented group

$$\Gamma_g=\langle a_1,b_1,\dots,a_g,b_g\mid [a_1,b_1]\cdots[a_g,b_g]\rangle,$$

the standard presentation of the fundamental group of the closed orientable surface $\Sigma_g$ of genus $g$, whose Euler characteristic is $\chi(\Sigma_g)=2-2g$.

A complete irreducible family (IrrepFamily G ι) is a finite family $(V_i)_{i\in\iota}$ of finite-dimensional complex representations of $G$ that are irreducible, pairwise non-isomorphic, and such that every irreducible finite-dimensional complex representation is isomorphic to some $V_i$. Write $d_i=\dim_{\mathbb C}V_i$ and $\chi_i(g)=\operatorname{tr}V_i(g)$ for the character.

Formalization targets

Goal: Mednykh's formula

For every finite group $G$, every complete irreducible family and every $g\ge 0$,

$$\sum_{i\in\iota} d_i^{\,2-2g}\;=\;|G|^{\,1-2g}\;\#\operatorname{Hom}(\Gamma_g,G),$$

which is Mulase–Yu, Thm. 1.1 and Snyder, eq. (1) with $\chi(S)=2-2g$. Equivalently, $\#\operatorname{Hom}(\Gamma_g,G)=|G|\sum_i(|G|/d_i)^{2g-2}$. Exponents are integers: at $g=0$ the formula reads $\sum_i d_i^2=|G|$.

Milestones

The milestones follow the algebraic proof of the counting formula recorded in Mulase–Yu 2002, §4, which goes back to Frobenius and Mednykh. Write $(x\star y)(w)=\sum_{\sigma\in G}x(w\sigma^{-1})\,y(\sigma)$ for the convolution of functions on $G$.

• M0. A complete irreducible family exists, with finite index type.
• M1. $\#\operatorname{Hom}(\Gamma_g,G)=N_g(1)$.
• M2. $\sum_i d_i\,\chi_i(z)=|G|$ if $z=1$ and $0$ otherwise.
• M3. For irreducible $V$ of dimension $d$: \sum_{a\in G}\chi_V(axa^{-1}y)=rac{|G|}{d}\chi_V(x)\chi_V(y).
• M4 (Mulase–Yu eq. (4.2)). For irreducible $V,W$: $\chi_V\star\chi_W$ equals rac{|G|}{d_V}\chi_V if $V\cong W$ and $0$ otherwise.
• M5 (Frobenius). $N_1(z)=|G|\sum_i\chi_i(z)/d_i$.
• M6. $N_{g_1+g_2}=N_{g_1}\star N_{g_2}$.
• M7 (Mulase–Yu Thm. 4.1). $N_g(z)=|G|^{2g-1}\sum_i\chi_i(z)\,d_i^{\,1-2g}$ for all $g\ge0$, $z\in G$. Mulase–Yu state it for $g\ge1$; the case $g=0$ is M2.

Significance

The result. The formula says that the number of $G$-coloured genus-$g$ surfaces is a function of the multiset of irreducible dimensions alone. Two groups with the same character degrees (for example $D_4$ and $Q_8$, both with degrees $1,1,1,1,2$) have equally many homomorphisms from every surface group, even though the groups are not isomorphic. In TQFT language the left side is the evaluation $\varepsilon(h^{g})$ of the Frobenius algebra $Z(\mathbb C[G])$, where $h$ is its handle element. The right side is the gauge-theoretic state sum. The identity is the two-dimensional instance of the agreement between the Atiyah–Segal gluing description and the path-integral description of a TQFT. It also gives the volume of the moduli space of flat $G$-bundles on $\Sigma_g$, and it underlies counts of covering spaces of surfaces.

Formalizing it. The theorem is classical and fully proved; to our knowledge it has no machine-checked proof. Mathlib has characters of finite-dimensional representations, their orthonormality (FDRep.char_orthonormal) and Maschke's theorem. It lacks the completeness of irreducible characters, the column orthogonality relation (M2), and any statement linking class sums to characters (M3). These are reusable well beyond this mission. The mission also produces the first formal link between a surface-group presentation and representation theory.

Difficulty

The available orthogonality is the row relation between two irreducible characters. Every step here needs the column relation M2, $\sum_i d_i\chi_i(z)=|G|\delta_{z,1}$. That relation is equivalent to the decomposition of the regular representation $\mathbb C[G]\cong\bigoplus_i V_i^{\oplus d_i}$, and in particular to the finiteness and completeness of the irreducible family. Mathlib has no such decomposition. The convolution identity M4 must also be established in its non-isomorphic case, which the row relation alone does not give in convolution form. The passage from $\operatorname{Hom}(\Gamma_g,G)$ to tuples (M1) depends on the universal property of PresentedGroup and on using one ordering of the commutator product throughout. A proof that bypasses characters by brute counting is not available for general $G$.

Formalization scope

All representations are over $\mathbb C$: FDRep ℂ G with G : Type a Group with [Fintype G]. Characters are FDRep.character and $d_i$ is Module.finrank ℂ (V i). Counts are Nat.card. Powers with exponents depending on $g$ are integer powers (zpow) in $\mathbb C$, so $g=0$ is included and no natural-number truncation occurs. $\Gamma_g$ is PresentedGroup on generators Fin g × Bool, with $a_j=(j,\mathrm{false})$, $b_j=(j,\mathrm{true})$ and the single relator (List.ofFn fun j => ⁅a_j, b_j⁆).prod. This is the standard presentation and stands in for $\pi_1(\Sigma_g)$, since Mathlib has no fundamental groups of closed surfaces. The goal quantifies over every complete irreducible family. M0 shows that such families exist, so the goal is not vacuous. Because the family must be complete and pairwise non-isomorphic, it cannot be chosen to make the sums trivial.

Out of scope: the non-orientable formula of Frobenius–Schur (it needs Frobenius–Schur indicators), positive characteristic, and the bordism-category formulation of TQFTs. Reusable contributions are especially welcome: the decomposition of the regular representation, column orthogonality, and the class-sum Schur lemma.

Selected references

• N. Snyder, Mednykh's formula via lattice topological quantum field theories, arXiv:math/0703073 (2007). https://arxiv.org/abs/math/0703073
• A. D. Mednykh, Determination of the number of nonequivalent coverings over a compact Riemann surface, Dokl. Akad. Nauk SSSR 239 (1978) 269–271; English transl. Soviet Math. Dokl. 19 (1978) 318–320.
• R. Dijkgraaf, E. Witten, Topological gauge theories and group cohomology, Commun. Math. Phys. 129 (1990) 393–429. https://doi.org/10.1007/BF02096988
• D. S. Freed, F. Quinn, Chern–Simons theory with finite gauge group, Commun. Math. Phys. 156 (1993) 435–472. https://arxiv.org/abs/hep-th/9111004
• M. Mulase, J. T. Yu, A generating function of the number of homomorphisms from a surface group into a finite group, arXiv:math/0209008 (2002), §4 (algebraic proof). https://arxiv.org/abs/math/0209008
• M. Mulase, J. T. Yu, Non-commutative matrix integrals and representation varieties of surface groups in a finite group, Ann. Inst. Fourier 55 (2005) 1001–1036. https://arxiv.org/abs/math/0211127
• J. Kock, Frobenius Algebras and 2D Topological Quantum Field Theories, LMS Student Texts 59, Cambridge Univ. Press (2003). https://doi.org/10.1017/CBO9780511615443

Motivation

The Conley–Zehnder index assigns an integer to a path of symplectic matrices that starts at the identity and ends at a matrix without eigenvalue $1$. It is how periodic orbits of Hamiltonian and Reeb flows get graded. In Floer homology it gives the grading of the chain complex, generated by the $1$-periodic orbits of a nondegenerate Hamiltonian (Salamon–Zehnder 1992; Salamon 1999). In contact homology and symplectic field theory it grades Reeb orbits. In the analysis of pseudoholomorphic curves it enters the Fredholm index formula for the linearized Cauchy–Riemann operator through the asymptotic orbits. In three-dimensional Reeb dynamics it defines dynamical convexity (every periodic orbit has index at least $3$), the hypothesis of the Hofer–Wysocki–Zehnder theorem on disk-like global surfaces of section (HWZ 1998).

Timeline. Conley and Zehnder introduced the index in their Morse-type index theory for periodic solutions of Hamiltonian equations (Conley–Zehnder 1984). Salamon and Zehnder gave the definition through a rotation function $\rho : \mathrm{Sp}(2n) \to S^1$ and related it to the Maslov index (SZ92). Robbin and Salamon extended it to arbitrary paths as a half-integer Maslov-type index (Robbin–Salamon 1993). Gutt attributes the properties naturality, homotopy, zero, product, loop, signature, determinant and inverse, and the characterization of the index by homotopy, loop and signature alone, to Salamon's lecture notes (Sal99) and to Audin–Damian (AD14); the statements used here are those of Gutt, Propositions 8–9. Gutt gives a self-contained account with several equivalent formulas, including the normalized complex determinant of the complex-linear part used below (Gutt 2014, §2).

Setting

Write $\mathbb{R}^{2n}$ with coordinates $(q,p)$ and let

$$J_0 = \begin{pmatrix} 0 & -\mathrm{Id} \\ \mathrm{Id} & 0 \end{pmatrix}.$$

The symplectic group $\mathrm{Sp}(2n)$ is the set of real $2n\times 2n$ matrices $A$ with $A J_0 A^{\mathsf T} = J_0$. Let $\mathrm{Sp}^*(2n)$ be the set of $A \in \mathrm{Sp}(2n)$ with $\det(\mathrm{Id} - A) \neq 0$.

$\mathrm{SP}(n)$ is the set of continuous paths $\psi : [0,1] \to \mathrm{Sp}(2n)$ with $\psi(0) = \mathrm{Id}$ and $\psi(1) \in \mathrm{Sp}^*(2n)$. It carries the compact-open topology.

For $A \in \mathrm{Sp}(2n)$, the complex-linear part is $C_A = \tfrac12 (A - J_0 A J_0)$. It commutes with $J_0$, so it has the block form $\begin{pmatrix} X & -Y \\ Y & X\end{pmatrix}$, which is the complex matrix $X + iY$ once $\mathbb{R}^{2n}$ is identified with $\mathbb{C}^n$ by $(x,y) \mapsto x + iy$. Set

$$\hat\rho(A) = \frac{\det_{\mathbb C}(X+iY)}{|\det_{\mathbb C}(X+iY)|} \in S^1.$$

Let $W^+ = -\mathrm{Id}$ and $W^- = \mathrm{diag}(2,-1,\dots,-1,\tfrac12,-1,\dots,-1)$. Each $\psi \in \mathrm{SP}(n)$ extends to a path $\tilde\psi : [0,2] \to \mathrm{Sp}(2n)$ with $\tilde\psi = \psi$ on $[0,1]$, $\tilde\psi(t) \in \mathrm{Sp}^*(2n)$ for $t \geq 1$, and $\tilde\psi(2) \in \{W^+, W^-\}$. The map $\hat\rho^2 \circ \tilde\psi$ is then a loop in $S^1$, and

$$\mu_{CZ}(\psi) = \deg\big(\hat\rho^2 \circ \tilde\psi\big).$$

For a loop $\varphi : [0,1] \to \mathrm{Sp}(2n)$ with $\varphi(0) = \varphi(1) = \mathrm{Id}$, the Maslov index is $\mu(\varphi) = \deg(\hat\rho\circ\varphi)$. For a symmetric matrix $S$, $\mathrm{Sign}(S)$ is the number of positive eigenvalues minus the number of negative eigenvalues.

Formalization targets

Goal: existence and uniqueness

The map $\mu_{CZ} : \mathrm{SP}(n) \to \mathbb{Z}$ has the following three properties, and every map $\mu : \mathrm{SP}(n) \to \mathbb{Z}$ with these properties equals $\mu_{CZ}$:

• Homotopy. $\mu$ is constant on the connected components of $\mathrm{SP}(n)$.
• Loop. $\mu(\varphi\psi) = \mu(\psi) + 2\mu(\varphi)$ for every loop $\varphi$ at $\mathrm{Id}$ and every $\psi \in \mathrm{SP}(n)$.
• Signature. If $S = S^{\mathsf T}$ is nondegenerate and all of its eigenvalues have absolute value $< 2\pi$, then $\mu\big(t \mapsto \exp(tJ_0S)\big) = \tfrac12 \mathrm{Sign}(S)$.

Milestones

1. $\det_{\mathbb C} C_A \neq 0$ for every $A \in \mathrm{Sp}(2n)$.
2. $\deg(\hat\rho^2\circ\tilde\psi)$ exists and does not depend on the extension $\tilde\psi$.
3. $\deg(\hat\rho\circ\varphi)$ is well defined for loops.
4. Naturality. $\mu_{CZ}(\varphi\psi\varphi^{-1}) = \mu_{CZ}(\psi)$ for every path $\varphi$ in $\mathrm{Sp}(2n)$.
5. Homotopy, for $\mu_{CZ}$.
6. Zero. If $\psi(s)$ has no eigenvalue on the unit circle for $s > 0$, then $\mu_{CZ}(\psi) = 0$.
7. Product. $\mu_{CZ}(\psi'\diamond\psi'') = \mu_{CZ}(\psi') + \mu_{CZ}(\psi'')$ under the symplectic block embedding $\mathrm{Sp}(2n')\times\mathrm{Sp}(2n'') \hookrightarrow \mathrm{Sp}(2(n'+n''))$.
8. Loop, for $\mu_{CZ}$.
9. Signature, for $\mu_{CZ}$.
10. Determinant. $(-1)^{n-\mu_{CZ}(\psi)} = \operatorname{sign}\det(\mathrm{Id} - \psi(1))$.
11. Inverse. $\mu_{CZ}(\psi^{-1}) = \mu_{CZ}(\psi^{\mathsf T}) = -\mu_{CZ}(\psi)$.
12. Uniqueness. Homotopy, loop and signature determine $\mu_{CZ}$ on $\mathrm{SP}(n)$.

Significance

The result. The characterization makes the index a canonical invariant: any construction of an integer invariant of nondegenerate symplectic paths that is homotopy invariant and has the correct loop and signature behaviour is the Conley–Zehnder index. In practice this is how different definitions in the literature are identified with one another (rotation function, polar decomposition, complex-linear part, crossing forms, spectral flow of asymptotic operators). The listed properties are used directly to compute indices of concrete orbits, for instance the iterates of orbits of ellipsoids and the orbits of convex energy surfaces.

Formalizing it. All results here are classical and proved. No formalization of the Conley–Zehnder index exists in Mathlib. This mission produces a reusable library for symplectic linear algebra in Lean: the index and the Maslov index of loops as functions on path spaces, together with their computational properties. It is the first stage of a formalization of the Fredholm theory of linearized Cauchy–Riemann operators, whose index formula is stated in terms of Conley–Zehnder indices. It also gives a general-dimension definition against which the two-dimensional winding-interval definitions used in existing dynamical-convexity statements can be compared.

Difficulty

The index is defined through a choice: an extension of the path to $W^\pm$ inside $\mathrm{Sp}^*(2n)$ and a continuous argument of a circle-valued map. Before any property can be stated as a property of a function, the result must be shown independent of these choices. That is not a local computation: it depends on the global topology of the symplectic group and on how the set of matrices with eigenvalue $1$ sits inside it.

The properties themselves are statements about the degree of maps into $S^1$ built from determinants, and $\hat\rho$ is not a homomorphism. So none of the properties follows from a calculation on a single matrix, and loop and product require control of degrees under pointwise products and block sums. The uniqueness statement quantifies over all integer-valued functions on a path space. The argument for it has to use only the three listed properties and the topology of $\mathrm{SP}(n)$.

Formalization scope

• Namespace ConleyZehnder; all definitions are in ConleyZehnder_Setting.
• Matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ. $J_0$ is Mathlib's Matrix.J, and $\mathrm{Sp}(2n)$ is Matrix.symplecticGroup. Paths are C(unitInterval, Mat n) with the compact-open topology. $\mathrm{SP}(n)$ is a Set of such paths, and "connected component" means connectedComponentIn (SP n).
• Index maps are functions $\mu$ on all of C(unitInterval, Mat n). Every property constrains $\mu$ only on $\mathrm{SP}(n)$, and the paths $\varphi\psi\varphi^{-1}$, $\psi^{-1}$, $\psi^{\mathsf T}$, $\psi'\diamond\psi''$ and $\exp(tJ_0S)$ are passed as continuous maps with the stated pointwise values.
• Degree is expressed by continuous real lifts: IsArgLift f θ means $f(t) = e^{i\theta(t)}$. IsCZValue ψ k says that some extension and some lifts give $2\big(\Delta\theta_\psi + \Delta\theta_\chi\big) = 2\pi k$, where $\chi$ is the part of the extension after $t = 1$. czIndex and maslovIndex are defined by choice from these predicates, with fallback value $0$. Milestones 2 and 3 are what make the fallback unreachable. Without them, any property proved for czIndex would say nothing about the actual index.
• The circle-valued map is $\hat\rho$ of Gutt, Corollary 12, formula (9). The rotation function $\rho$ of Salamon–Zehnder (built from eigenvalue multiplicities and Krein signs) is not formalized. Gutt, Proposition 10 and Corollaries 11–12, shows that the degrees agree. The Maslov index of loops is also taken with $\hat\rho$.
• The signature uses Matrix.IsHermitian.eigenvalues; for real matrices, Hermitian means symmetric. The norm bound is stated as $|\lambda| < 2\pi$ for every eigenvalue $\lambda$. The signature property is stated as $2\mu = \mathrm{Sign}(S)$.
• $n = 0$ is allowed: $\mathrm{SP}(0)$ is a single path and every property holds for it.

Contributions welcome: general lemmas on degrees of maps $[0,1]\to S^1$ (existence and uniqueness of lifts, additivity under products and concatenation, homotopy invariance), and the topology of $\mathrm{Sp}(2n)$ and $\mathrm{Sp}^*(2n)$. These are reusable well beyond this mission.

Selected references

• C. Conley, E. Zehnder, Morse-type index theory for flows and periodic solutions for Hamiltonian equations, Comm. Pure Appl. Math. 37 (1984), 207–253. https://doi.org/10.1002/cpa.3160370204
• D. Salamon, E. Zehnder, Morse theory for periodic solutions of Hamiltonian systems and the Maslov index, Comm. Pure Appl. Math. 45 (1992), 1303–1360. https://doi.org/10.1002/cpa.3160451004
• J. Robbin, D. Salamon, The Maslov index for paths, Topology 32 (1993), 827–844. https://doi.org/10.1016/0040-9383(93)90052-W
• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289. https://doi.org/10.2307/120994
• D. Salamon, Lectures on Floer homology, in: Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229. https://doi.org/10.1090/pcms/007/05
• M. Audin, M. Damian, Morse Theory and Floer Homology, Universitext, Springer (2014); French original 2010. https://doi.org/10.1007/978-1-4471-5496-9
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932. https://doi.org/10.5802/afst.1430 (arXiv:1307.7239)

Motivation

Mode-seeking clustering groups data points by the peak of an underlying probability density that they "flow up" to. Methods of this kind (mean-shift, graph-based hill climbing) are widely used, but their output depends heavily on noise: a density estimated from finitely many samples has many spurious local maxima, and each of them becomes a cluster. Chazal, Guibas, Oudot and Skraba (INRIA RR-6968, 2009; journal version J. ACM 60(6), 2013, doi:10.1145/2535927) combine graph-based hill climbing with topological persistence. Persistence measures how prominent each peak is, and peaks of low prominence are merged into their neighbours. The paper's main guarantee says when this algorithm recovers the right number of clusters from random samples. It holds on Riemannian manifolds that may be non-compact, and the clustering method is now known as ToMATo.

Setting

Let $\mathbb X$ be an $m$-dimensional Riemannian manifold, possibly with boundary, with geodesic distance $d_{\mathbb X}$ and $m$-dimensional Hausdorff measure $\mathcal H^m$. The strong convexity radius $\varrho_c(\mathbb X)$ is the infimum over $x$ of the largest $r$ such that any two points of the closed ball $B_{\mathbb X}(x,r)$ are joined by a unique shortest path, and that path stays in the ball. Let $f:\mathbb X\to\mathbb R$ be a probability density with respect to $\mathcal H^m$ that is $c$-Lipschitz, and write $\mathbb F^\alpha=f^{-1}([\alpha,+\infty))$ for its superlevel sets.

Persistence diagram. As $\alpha$ decreases from $+\infty$ to $-\infty$, path components of $\mathbb F^\alpha$ are born at peaks of $f$ and die when they merge into an older component. The 0-th persistence diagram $D_0f$ records each component as a point $(p_x,p_y)$ of the extended plane $\overline{\mathbb R}^2$, with birth $p_x$ and death $p_y\le p_x$; a component that never dies has $p_y=-\infty$. The prominence of the peak is $p_x-p_y$. The diagonal is added with infinite multiplicity. $f$ is tame when this structure is of finite type. For $d_2>d_1\ge0$, $D_0f$ is $(d_1,d_2)$-separated when every off-diagonal point either has prominence $<d_1$ (noise), or has prominence $\ge d_2$ and birth $>d_2$ (signal).

Algorithm. The input is $n$ sample points $x_1,\dots,x_n$, the values $f(x_i)$, the matrix of distances $d_{\mathbb X}(x_i,x_j)$ and parameters $\delta,\tau$. The Rips graph $R_\delta$ joins two points at distance $\le\delta$. The algorithm processes the points by decreasing $f$ and keeps a union-find structure whose entries are rooted at their highest point. When a point is processed, every neighbouring entry whose root is less than $\tau$ higher than the point is merged into the point's entry. The point's own entry is then merged into the neighbouring entry with the highest root, if its own root is less than $\tau$ higher than the point. The output is the set of final entries whose root has value $\ge\tau$.

Sampling quantities. $\mathcal N_r(A)$ is the least number of closed geodesic balls of radius $r$ covering $A$, and $\mathcal V_r(A)=\inf_{x\in A}\mathcal H^m(B_{\mathbb X}(x,r))$.

Formalization targets

Goal: Theorem 4.8 (p. 22)

Assume $\varrho_c(\mathbb X)>0$, $f$ is a tame $c$-Lipschitz density, $D_0f$ is $(d_1,d_2)$-separated, $0<\delta<\min\{\varrho_c(\mathbb X),\frac{d_2-d_1}{5c}\}$ and $\tau\in(d_1+2c\delta,\,d_2-3c\delta)$. Then for $n$ i.i.d. samples from $f$,

$$\Pr\big[\#\text{clusters}\ne\#\{\text{peaks of prominence}\ge d_2\}\big]\le\mathcal N_{\delta/8}(\mathbb F^{c\delta})\,e^{-n\frac34c\delta\,\mathcal V_{\delta/8}(\mathbb F^{c\delta})}.$$

Milestones

1. Lemma 4.3 (p. 17): for $\varepsilon>0$ and $\alpha>c\varepsilon$, the sample is a geodesic $\varepsilon$-sample of $\mathbb F^\alpha$ except with probability at most $\mathcal N_{\varepsilon/2}(\mathbb F^\alpha)e^{-n(\alpha-c\varepsilon)\mathcal V_{\varepsilon/2}(\mathbb F^\alpha)}$.
2. Theorem 4.5 (p. 19): if a finite $L$ is a geodesic $\delta/4$-sample of $\mathbb F^\alpha$, there is a multi-bijection between $D_0f$ and the diagram $D_0\mathcal R^f_\delta(L)$ of the upper-star Rips filtration. Above $\alpha$ it moves points by at most $c\delta$, and in the lower-right quadrant it moves births by at most $c\delta$.
3. Noise image (proof of Thm 4.8, p. 22): the noise points are sent into $\Delta^N_{d_1+2c\delta}\cup\Lambda^W_{d_1+2c\delta}$.
4. Signal image (pp. 22–23): the signal points are sent outside that region.
5. Partition and count (p. 23): for $\tau$ in the range, $D_0\mathcal R^f_\delta(L)$ has exactly as many points in $\Delta^S_\tau\cap\Lambda^E_\tau$ as $D_0f$ has peaks of prominence $\ge d_2$; for the tame $D_0f$ both counts are finite.
6. Algorithm output (p. 23, with §3): for $\tau>0$ the algorithm returns exactly one cluster per point $q$ of the Rips diagram with $q_x-q_y\ge\tau$ and $q_x\ge\tau$.

Significance

The theorem gives a sample-complexity guarantee for a practical clustering algorithm, with an explicit failure probability. It needs neither compactness of the manifold nor a density bounded away from zero; dense sampling of one superlevel set is enough. The separation hypothesis is a signal-to-noise condition, and it tells the user which range of $\tau$ recovers the true number of clusters.

On the formalization side, the paper's results are proved on paper, but nothing about them is machine-checked. Of the steps, the paper proves Lemma 4.3 and the region analysis. Theorem 4.5 rests on the Rips-filtration analysis of Chazal–Guibas–Oudot–Skraba, SODA 2009, the interleaving and stability results of Chazal et al., SoCG 2009, and the paper's Lemma 4.6. The algorithm-output step (milestone 6) is asserted in the paper, not proved. The mission therefore asks for formal proofs of all six steps. A by-product is the first library of 0-dimensional persistence diagrams, multi-bijections and Rips filtrations on the platform.

Difficulty

The probabilistic step is a union bound over a minimal cover, but it has a gap. Covering balls need not be centred in $\mathbb F^\alpha$, while $\mathcal V$ is an infimum over balls centred in $\mathbb F^\alpha$, so the comparison between the two is not justified on a general manifold. Theorem 4.5 is the hardest step. The obvious route, a bottleneck stability theorem, does not apply, because the sample covers only one superlevel set and not $\mathbb X$. This is why the conclusion distinguishes the quadrant above $\alpha$, where both coordinates are controlled, from the quadrant below, where only births are. Milestone 6 is a correctness proof for a union-find procedure with ties: entries are not path components, because prominent entries stay separate after their components meet.

Formalization scope

• Manifold. $\mathbb X$ is a metric space carrying Mathlib's Riemannian manifold structure (IsRiemannianManifold, a ModelWithCorners for the boundary), so $d_{\mathbb X}$ is dist.
• Measures and probability. $\mathcal H^m$ is Mathlib's unnormalized Hausdorff measure of dimension $\dim E$; the statements are invariant under rescaling it. Samples are product measures on Fin n → X. "With probability at least $1-B$" is an upper bound $B\in[0,\infty]$ on the outer measure of the failure event. $e^{-aV}$ uses $e^{-\infty}=0$ and $0\cdot\infty=0$.
• Convexity radius. It is computed in $[0,+\infty]$, with shortest paths as isometric embeddings of $[0,d(y,y')]$.
• Diagrams. A diagram's multiplicities are computed from the rank function of the filtration, so they are not free data.
• Tameness is pinned in a 0-dimensional form: finitely many path components at each level, finitely many critical values, and empty superlevel sets at high levels.
• Multi-bijections are bijections between copies of points, the diagonal contributing countably many copies of each of its points.
• Separation is imposed on off-diagonal points only. On the diagonal the literal definition is unsatisfiable when $d_1=0$.
• Algorithm. It runs Procedures 1–2 with an explicit union-find state, over every processing order compatible with the sort. The upper star of a point is its set of neighbours processed earlier.
• Added hypotheses. $c>0$ in Theorem 4.8 and milestones 3–5 (the paper divides by $c$), and $\tau>0$ in milestone 6.

No formalization in which the number of clusters is defined as a count of diagram points, or in which the diagram is a free parameter, is acceptable: either one empties the goal. The running-time and memory claims of §3, the basin approximation of Theorem 4.9 and the Morse-theoretic material of §2.3 are out of scope. Lemma 4.3 is stated as printed, with covering balls centred anywhere, and its proof gap is an open risk that Theorem 4.8 inherits.

Contributions are welcome on every milestone. The persistence-diagram layer (rank functions, multiplicities, multi-bijections) and the union-find correctness proof are reusable beyond this mission.

Selected references

• F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Persistence-Based Clustering in Riemannian Manifolds, INRIA Research Report RR-6968, 2009. https://inria.hal.science/inria-00389390
• F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Persistence-Based Clustering in Riemannian Manifolds, Journal of the ACM 60(6), 2013. https://doi.org/10.1145/2535927
• F. Chazal, D. Cohen-Steiner, M. Glisse, L. J. Guibas, S. Y. Oudot, Proximity of Persistence Modules and their Diagrams, Proc. 25th ACM Symposium on Computational Geometry, 2009. https://doi.org/10.1145/1542362.1542407
• D. Cohen-Steiner, H. Edelsbrunner, J. Harer, Stability of Persistence Diagrams, Discrete & Computational Geometry 37, 2007. https://doi.org/10.1007/s00454-006-1276-5
• F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Analysis of Scalar Fields over Point Cloud Data, SODA 2009. https://doi.org/10.1137/1.9781611973068.112

Motivation

The homotopy hypothesis relates algebraic higher groupoids to spaces. Elementary expansions provide a concrete test of whether adjoining a higher cell preserves homotopy information. The pinned manuscript supplies the research context.

Setting

C is a globular coherator in the encoded convention, X is a cellular model, and Y is a pushout that attaches an (n+1)-disk along the source-face inclusion of an n-disk.

Formalization target

The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is

$$X\longrightarrow X\amalg_{D_n}D_{n+1}\quad\text{is a weak equivalence}.$$

The theorem states that, for a coherator C (a globular theory, meaning a category of shapes built from globes by iterated gluing, with morphisms preserving the globular pushouts, which has a cellular presentation as a countable-stage colimit of free extensions along admissible pairs of parallel cells and in which every admissible pair is filled by some morphism), the following holds for models of C, i.e. presheaves on C sending globular pushouts to pullbacks. Let X be a cellular model, meaning that it is built from an initial model by a well-ordered transfinite composition in which each successor step attaches cells freely along boundaries of cells of the previous stage. Let n be a natural number, let a be a map from the free model disk(n) on the n-globe to X, and let J_n : disk(n) → disk(n+1) be the map induced by the source-face inclusion of the n-globe into the (n+1)-globe. If Y, together with i : X → Y and b : disk(n+1) → Y, forms a pushout square of a and J_n, then i is a weak equivalence. Here weak equivalence means that i induces a bijection on sets of components (0-cells modulo being joined by a 1-cell) and, for every 0-cell x of X and every n, a bijection on homotopy groups, which are classes of n-loops based at the degenerate cells above x, identified when joined by an (n+1)-cell.

Significance and status

The selected goal is the elementary-expansion theorem. It does not itself assert the complete equivalence between the homotopy theory of spaces and all coherator models. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, The Grothendieck homotopy hypothesis via elementary expansions, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Higman's embedding theorem (1961) says that a finitely generated group embeds in a finitely presented group exactly when it is recursively presented, i.e. has a presentation with finitely many generators and a recursively enumerable set of relators. A consequence is that there is a single universal finitely presented group containing every finitely presented group. A natural higher-dimensional question asks whether finiteness can be pushed beyond presentations: finite presentability is the dimension-two case of the topological finiteness properties $F_n$.

This preprint constructs a single group $H$ of type $F_\infty$, i.e. with a classifying space having finitely many cells in every dimension, that contains every finitely presented group. This answers the $F_\infty$ form of the higher-dimensional Higman embedding question posed by Fournier-Facio and Zaremsky.

Background

• 1949. Higman, Neumann and Neumann introduce HNN extensions and embedding theorems for groups.
• 1961. Higman proves his embedding theorem.
• 1974–1975. Bieri and Eckmann, and Brown, develop finiteness properties of groups and homological criteria for them.
• 2018. Leary proves every countable group embeds in a group of type $FP_2$.
• 2026. Fournier-Facio and Zaremsky show that embedding theorems into recursively presented groups of type $FP_n$ would yield embeddings of finitely presented groups into groups of type $F_n$, show that their rope-trick groups fail $FP_3(\mathbb{Q})$ in general, and ask the higher-dimensional Higman embedding question (Question 1.3).
• 2026. The OpenAI preprint A universal group of type $F_\infty$ (dated September 23, 2026) proves the theorem below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A classifying complex for a group $G$ is a connected CW complex with fundamental group isomorphic to $G$ and contractible universal cover; it may be infinite-dimensional. $G$ has type $F_n$ if some classifying complex has finite $n$-skeleton, and type $F_\infty$ if some classifying complex has finitely many cells in every dimension. Type $F_2$ is equivalent to finite presentability. A group is finitely presented if it has a presentation with finitely many generators and relators.

In Lean (OAI.UniversalFInfinity), HasTypeFInfinity G asks for a Hausdorff connected space $X$ with a CW structure on Set.univ having finitely many $n$-cells for every $n$, a basepoint with $\pi_1(X, x) \simeq G$, and a surjective covering map from a contractible space. Finite presentation is Mathlib's Group.IsFinitelyPresented.

Formalization targets

Goal: Theorem 1.1

There exists a group $H$ of type $F_\infty$ such that every finitely presented group admits an injective homomorphism into $H$:

$$\exists H \text{ of type } F_\infty\ \ \forall G \text{ finitely presented}\ \ \exists\, \varphi : G \hookrightarrow H .$$

Significance

The result. Theorem 1.1 gives a universal group with the strongest standard topological finiteness property. Corollary 1.2 follows: the finitely generated subgroups of $H$ are exactly the finitely generated recursively presented groups. No word-problem hypothesis is imposed on the inputs, in contrast with the companion result on simple $F_\infty$ overgroups.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires finite-type CW complexes, classifying spaces and covering theory, Brown's criterion or a direct cell-count argument, Higman's universal finitely presented group, HNN extensions and an ascending-torus theorem (Theorem 5.1), none of which is fully in Mathlib.

Difficulty

Higman's universal group is only finitely presented; type $F_\infty$ requires finite control of relations among relations in every dimension, which is typically destroyed by the embeddings and amalgams used in Higman-type arguments. Fournier-Facio and Zaremsky show that the rope-trick construction fails $FP_3(\mathbb{Q})$, so a different route is needed. The preprint constructs a finitely presented envelope with two families of homomorphisms from the universal group and an ascending HNN-type mapping torus whose finiteness properties can be verified.

Formalization scope

• Universes: $H$ and the quantified finitely presented $G$ live in the same universe Type u; finitely presented groups are countable, so this loses nothing.
• Type $F_\infty$: a CW structure with Finite (cw.cell n) for every $n$, $\pi_1 \simeq H$, and a contractible covering space; no finite-dimensionality is required.
• The universal quantifier is over every Group.IsFinitelyPresented group, not a chosen list of presentations.

The statement cannot be met trivially: a trivial or finite $H$ cannot contain all finitely presented groups, and the type $F_\infty$ requirement is substantive.

Needed infrastructure: CW complexes of finite type, $K(\pi,1)$ spaces, HNN extensions, Higman's embedding theorem. Contributions toward Theorem 5.1 (ascending-torus theorem) or Proposition 6.2 are welcome.

Selected references

• OpenAI, A universal group of type $F_\infty$, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-universal-group-of-type-F-infinity-September-23-2026/paper.pdf
• OpenAI, Simple $F_\infty$ overgroups of groups with decidable word problem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/main/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf
• G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
• G. Higman, B. H. Neumann, H. Neumann, Embedding theorems for groups, J. London Math. Soc. 24 (1949).
• R. Bieri, B. Eckmann, Finiteness properties of duality groups, Comment. Math. Helv. 49 (1974). https://doi.org/10.1007/BF02566720
• K. S. Brown, Homological criteria for finiteness, Comment. Math. Helv. 50 (1975). https://doi.org/10.1007/BF02565740
• I. J. Leary, Subgroups of almost finitely presented groups, Math. Ann. 372 (2018).
• F. Fournier-Facio, M. C. B. Zaremsky, Finiteness properties and Higman's rope trick, preprint, 2026. https://arxiv.org/abs/2607.21727
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002.