Pure Mathematics

Primes in progressions, uniformly in the modulus

Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of $\log x$, and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.

The history is a sequence of partial uniformities:

• 1837. Dirichlet proves that every progression $a \bmod q$ with $(a,q)=1$ contains infinitely many primes, for each fixed $q$, with no rate (Dirichlet's theorem).
• 1896–1899. De la Vallée Poussin proves the prime number theorem with the error term $O(x e^{-c\sqrt{\log x}})$, and extends the zero-free region from $\zeta$ to $L(s,\chi)$, obtaining the prime number theorem in progressions for each fixed $q$ (PNT).
• 1918–1935. Landau and Page isolate the obstruction to uniformity: a single real zero near $s=1$, attached to a quadratic character. Landau shows at most one of two distinct real primitive characters can have such a zero; Page shows at most one modulus below a given bound can, yielding unconditional uniformity for $q$ up to a bounded power of $\log x$ (Page's theorem).
• 1935. Siegel proves $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ for real primitive $\chi$, at the price of an ineffective constant (Siegel).
• 1936. Walfisz combines Siegel's bound with the de la Vallée Poussin machinery and obtains uniformity for every fixed power $q \le (\log x)^A$ (Walfisz).
• 1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes (Vinogradov's theorem).
• 2013. Helfgott removes the "sufficiently large", settling ternary Goldbach for all odd $n > 5$ (arXiv:1312.7748).

Setting

The von Mangoldt function $\Lambda(n)$ equals $\log p$ if $n = p^m$ is a prime power and $0$ otherwise. The Chebyshev function $\psi(x) = \sum_{n \le x} \Lambda(n)$ counts primes with weights; the prime number theorem is the assertion $\psi(x) \sim x$.

A Dirichlet character modulo $q$ is a multiplicative function $\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$, supported on the units and taking root-of-unity values there. The principal character $\chi = 1$ is the indicator of the units; a character is quadratic (real) if $\chi^2 = 1$ and $\chi \neq 1$, and primitive if it is not induced by a character of a proper divisor of $q$. The Dirichlet $L$-function $L(s,\chi) = \sum_{n\ge 1}\chi(n)n^{-s}$, defined for $\operatorname{Re} s > 1$, extends meromorphically to $\mathbb{C}$, entire except for a simple pole at $s = 1$ when $\chi$ is principal.

The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum

$$\psi(N,\chi) = \sum_{n < N} \Lambda(n)\chi(n), \qquad \psi(N;q,a) = \sum_{\substack{n < N \\ n \equiv a\ (q)}} \Lambda(n),$$

related by finite character orthogonality. Write $\delta_\chi = 1$ for $\chi$ principal and $\delta_\chi = 0$ otherwise. A zero $\beta \in (0,1)$ of $L(s,\chi)$ lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given $\chi$ is the exceptional set $E$, which the results below constrain to have at most one element.

Formalization targets

The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.

(1) zero_free_region (§14, pp. 88–96). There is an absolute $c>0$ such that for every $q \ge 1$ and every $\chi \bmod q$,

$$L(s,\chi) \neq 0 \quad\text{for } s \neq 1,\ \operatorname{Re} s \ \ge\ 1 - \frac{c}{\log\big(q(|\operatorname{Im} s| + 2)\big)},$$

with at most one exception, which is real, lies in $(0,1)$, is a simple zero, and can occur only for quadratic non-principal $\chi$.

(2) pnt_dlvp (§18, pp. 111–114). For some $c > 0$ and all $x \ge 2$,

$$\psi(x) = x + O\!\left(x\,e^{-c\sqrt{\log x}}\right).$$

(3) psi_char_of_region (§20, pp. 121–125). For a region constant $c>0$ there are $c_1, c_2 > 0$ such that, whenever $E$ is an exceptional set for $\chi \bmod q$ with respect to $c$ and $q \le \exp(c_2\sqrt{\log N})$,

$$\psi(N,\chi) = \delta_\chi N - \sum_{\beta \in E} \frac{N^\beta}{\beta} + O\!\left(N e^{-c_1\sqrt{\log N}}\right).$$

(4) siegel (§21, pp. 126–131). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,

$$L(1,\chi) > C(\varepsilon)\, q^{-\varepsilon}.$$

(5) siegel_zero (§21, second form). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,

$$L(\sigma,\chi) \neq 0 \quad \text{for all real } \sigma > 1 - C(\varepsilon)q^{-\varepsilon}.$$

(6) siegelWalfisz (§22, pp. 132–134). For every $A > 0$ there are $C, c > 0$ such that for all $q \ge 1$, all $\chi \bmod q$, and all $N \ge 2$ with $q \le (\log N)^A$,

$$\big\lVert \psi(N,\chi) - \delta_\chi N \big\rVert \le C N e^{-c\sqrt{\log N}}.$$

This is literally the platform proposition ThreePrimes.SiegelWalfisz.

A corollary, not a milestone, records the progression form siegel_walfisz_ap: for $(a,q)=1$ and $q \le (\log N)^A$,

$$\psi(N;q,a) = \frac{N}{\varphi(q)} + O_A\!\left(N e^{-c\sqrt{\log N}}\right).$$

Goal (three_primes, §26). There is $N_0$ such that every odd $n \ge N_0$ is a sum of three primes. It follows from milestone (6) by the existing platform theorem deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal leaves $N_0$ unspecified rather than hard-coding a numeric threshold, so it is not invalidated by later improvements to that threshold.

What the result gives, and what remains to be formalized

Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.

Platform status is the reason this mission exists. A complete, machine-checked formalization of the three primes theorem already exists in the namespace ThreePrimes (by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem unconditional, and is the whole content of this mission.

Mathlib contains the analytic continuation of $L(s,\chi)$ (DirichletCharacter.LFunction), its functional equation, the non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$, Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free region for $L(s,\chi)$, the explicit formula for $\psi(x,\chi)$, Siegel's theorem, or Siegel–Walfisz. The platform additionally hosts the PNT+ project contour machinery for $\zeta$ — Borel–Carathéodory, the $3 + 4\cos\theta + \cos 2\theta$ inequality, a zero-free rectangle, and MediumPNT, $\psi(x) = x + O(x\exp(-c(\log x)^{1/10}))$. That is a template for the $L(s,\chi)$ analogues, not a proof of them, and its error term is weaker than the de la Vallée Poussin form milestone (2) asks for.

Where the obvious argument fails

The first idea is to run the $\zeta$ argument character by character. It works for complex $\chi$ and breaks for real ones. The positivity device that pushes zeros off $\operatorname{Re} s = 1$ compares $\chi$, $\chi^2$ and the trivial character at nearby points; when $\chi$ is quadratic, $\chi^2$ is principal and contributes the pole of $L(s,\chi_0)$ at $s = 1$ at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the $N^\beta/\beta$ term present, and milestone (6) is exactly the assertion that for $q \le (\log N)^A$ this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.

A second shortcut, deducing uniformity from Mathlib's non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$ together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in $q$.

Formalization scope

Sums run over $n < N$ with $N \in \mathbb{N}$, matching Vino.vmSumChar and ThreePrimes.SiegelWalfisz; Davenport sums over $n \le x$. The two differ by the single term $\Lambda(N) \le \log N$, negligible against every error term above. Milestone (2) alone uses a real argument, via Mathlib's Chebyshev.psi. $L(s,\chi)$ is Mathlib's DirichletCharacter.LFunction, so no continuation is reconstructed.

The zero-free region is Davenport.InRegion c q s, namely $\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s| + 2))$; the exceptional zero is packaged as IsExceptionalSet c χ E: $E$ is a subsingleton, every element is a real zero of $L(\cdot,\chi)$ in $(0,1)$ and can exist only for quadratic non-principal $\chi$, and $L(s,\chi) \neq 0$ at every $s \neq 1$ of the region outside $E$. Milestone (1) adds simplicity as $L'(\beta,\chi) \neq 0$ for $\beta \in E$.

Milestone (3) takes the region constant $c > 0$ as a parameter rather than importing it from milestone (1), so the milestones can be attempted in any order. For large $c$ the hypothesis IsExceptionalSet c χ E may be unsatisfiable for some $\chi$, making the statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing reading: milestone (1) produces a definite small $c > 0$ with a witness $E$ for every $\chi$, so instantiating milestone (3) at that $c$ discharges the hypothesis rather than voiding it.

Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with the conclusion a lower bound on $\operatorname{Re} L(1,\chi)$; since $L(1,\chi)$ is real for real $\chi$, this is the value itself, not a weakening. The constants in milestones (4), (5) and (6) are ineffective; the statements are plain existentials, so ineffectivity is invisible to Lean, but no numeric constant can be extracted from anything downstream of them.

The principal character is included in the character-form statements, with main term $N$ (if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime number theorem itself and cannot be proved by restricting to non-principal $\chi$. Milestone (6) requires $c > 0$ strictly, which is what makes $Ne^{-c\sqrt{\log N}}$ a genuine saving over the trivial $\psi(N,\chi) \ll N$; with $c = 0$ allowed it would be empty.

Beyond the six milestones, a complete development needs Hadamard factorization for $L(s,\chi)$ as an entire function of order $1$, the zero-counting estimate $N(T,\chi)$ (§16, pp. 101–103), the truncated explicit formula for $\psi(x,\chi)$ (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction $|\psi(N,\chi) - \psi(N,\chi^{*})| \ll (\log q)(\log N)$. All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the $\pi(x;q,a)$ versions, and of sharper constants are welcome.

Selected references

• H. Davenport, Multiplicative Number Theory, 3rd ed., revised by H. L. Montgomery, GTM 74, Springer, 2000. §§14, 18, 20, 21, 22, 26. doi:10.1007/978-1-4757-5927-3
• H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge University Press, 2007. Ch. 11–12 (Theorems 11.3, 11.14, 11.16, 12.10; Corollaries 11.10, 11.12, 11.17, 11.19). doi:10.1017/CBO9780511618314
• R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. Ch. 3. doi:10.1017/CBO9780511470929
• C. L. Siegel, Über die Classenzahl quadratischer Zahlkörper, Acta Arithmetica 1 (1935), 83–86. eudml:205054
• A. Walfisz, Zur additiven Zahlentheorie II, Mathematische Zeitschrift 40 (1936), 592–607. doi:10.1007/BF01218882
• I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akad. Nauk SSSR 15 (1937), 291–294. Vinogradov's theorem
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
• Siegel–Walfisz theorem, Wikipedia. link
• Page theorem, Encyclopedia of Mathematics. link
• A. Kontorovich et al., PrimeNumberTheoremAnd (PNT+), Lean formalization project. github
• Mathlib, Mathlib.NumberTheory.LSeries.DirichletContinuation. docs

Motivation

Polynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.

The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family $\tau(C,\Phi)$ carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.

Setting

Fix $\ell\ge2$ and the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$. The relevant maximal parabolic subalgebra has an abelian nilradical $\mathfrak n$. Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free $U(\mathfrak n)$-module can consequently be modeled on that polynomial ring.

The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar $C\in\mathbb C$ and a polynomial parameter $\Phi$. Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family $\tau(C,\Phi)$ realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.

Formalization targets

Common polynomial-module family

Prove that for every $\ell\ge2$ there is one generator presentation and one family

$$(C,\Phi)\longmapsto \tau(C,\Phi)$$

of $\mathfrak{sp}_{2\ell}(\mathbb C)$-representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that $\tau(C,\Phi)$ is a weight module exactly when $\Phi$ is constant, and the stated simplicity criterion outside the exceptional arithmetic set

$$\left\{\frac{\ell+1}{2}-\frac{n}{2}:n\in\mathbb Z_{>0}\right\}.$$

For exceptional $C$, prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family $\tau$.

Significance

The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.

Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.

Difficulty

The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.

The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.

Formalization scope

The mission works over $\mathbb C$ with natural rank $\ell\ge2$. The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.

The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family $\tau$. Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.

Selected references

• Yang Chen and Haijun Tan, Simple $\mathfrak{sp}_{2\ell}(\mathbb C)$-modules which are free over an abelian nilradical, Journal of Algebra 697 (2026), 341--372, Theorems 1.1--1.3 (formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2). DOI
• G. Shen, foundational work on mixed-product constructions for modules over Lie algebras of Cartan type, cited in the source paper for the Shen--Larsson functor.

The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.

This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.

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

Quantizing a Yang–Mills theory by the Faddeev–Popov procedure requires a gauge condition that picks one representative from each gauge orbit. In the Landau gauge the condition is $\partial_\mu A_\mu^a = 0$. Gribov showed in 1978 that this condition is not ideal: a gauge orbit can meet the surface $\partial_\mu A_\mu = 0$ more than once, so gauge-equivalent configurations — Gribov copies — are still being integrated over (V. N. Gribov, Quantization of non-Abelian gauge theories, Nucl. Phys. B139 (1978) 1). Infinitesimally, a copy of a transverse field $A$ corresponds to a zero mode of the Faddeev–Popov operator $M^{ab}(A) = -\partial_\mu D_\mu^{ab}(A)$, which is Hermitian on transverse configurations.

Gribov's proposed remedy is to restrict the functional integral to the Gribov region $\Omega$, the set of transverse configurations at which $M(A)$ is positive definite. The interest of $\Omega$ is not only that it removes infinitesimal copies: the fact that it is a bounded region of field space is the geometric input of Gribov's confinement scenario, because restricting the integration to a bounded region deforms the gluon propagator in the infrared and produces a mass scale. Whether the restriction to $\Omega$ is the physically correct prescription is still debated; the geometric properties of $\Omega$ themselves are not — they are consequences of the algebraic structure of $M(A)$, and they are what this mission formalizes.

Timeline of the properties at issue, as recorded in §2.2.1 (pp. 188–189) of the review by N. Vandersickel and D. Zwanziger, The Gribov problem and QCD dynamics, Phys. Rep. 520 (2012) 175–251 (doi:10.1016/j.physrep.2012.07.003):

• 1978, Gribov: existence of copies infinitesimally across the horizon $\partial\Omega$ (Nucl. Phys. B139 (1978) 1).
• 1982, D. Zwanziger: $\Omega$ is convex and bounded in every direction (Nucl. Phys. B209 (1982) 336).
• 1982, M. Semenov-Tyan-Shanskii and V. Franke: the variational characterization of $\Omega$ by relative minima of $\|A^U\|^2$, and the fact that $\Omega$ still contains copies.
• 1989, G. Dell'Antonio and D. Zwanziger: $\Omega$ is contained in an ellipsoid (Nucl. Phys. B326 (1989) 333).
• 1991, G. Dell'Antonio and D. Zwanziger: every gauge orbit passes inside $\Omega$ (Comm. Math. Phys. 138 (1991) 291–299).

Setting

Fix a real vector space $V$ of gauge-field configurations (in the physical situation, the transverse fields $A_\mu^a$) and a finite index set $\{1,\dots,n\}$ on which the Faddeev–Popov operator acts (colour index times a finite basis of fluctuation modes $\omega$). The formalization works with the algebraic structure that the Faddeev–Popov operator has, and nothing else:

$$M(A) \;=\; M_0 \;+\; M_2(A),$$

where

• $M_0$ is the field-independent part, $M_0 = -\partial^2$ in the physical setting, taken here to be a fixed symmetric positive definite $n \times n$ real matrix;
• $A \mapsto M_2(A)$ is linear in $A$, and each $M_2(A)$ is a symmetric traceless real $n \times n$ matrix. In the physical setting $M_2(A)^{ab} = \partial_\mu f^{abc} A_\mu^c$, which is traceless already in the colour indices.

The Gribov region is

$$\Omega \;=\; \{\, A \in V \;:\; M(A) \text{ is positive definite} \,\}, \qquad M(A) \text{ positive definite} \iff \forall\, w \neq 0,\ w^{\mathsf T} M(A)\, w > 0 .$$

This is Eq. (2.52) of the review, with positivity as in Eq. (2.54). The boundary $\partial\Omega$ is the first Gribov horizon, where the lowest non-trivial eigenvalue of $M(A)$ vanishes.

Formalization targets

Goal — $\Omega$ is a bounded convex set containing the origin

$$0 \in \Omega, \qquad \Omega \text{ convex}, \qquad \forall A \neq 0\ \exists \lambda_0 > 0\ \forall \lambda \ge \lambda_0:\ \lambda A \notin \Omega, \qquad \Omega \text{ bounded}.$$

The last two clauses are stated under the assumption that $A \mapsto M_2(A)$ is injective, i.e. that distinct configurations give distinct field-dependent parts; without it $\Omega$ contains the whole kernel of $M_2$ as a linear subspace and no boundedness statement can hold.

Supporting statements

$$M(\alpha A_1 + \beta A_2) = \alpha M(A_1) + \beta M(A_2) \quad (\alpha + \beta = 1),$$ $$M \text{ symmetric},\ \operatorname{tr} M = 0,\ M \neq 0 \;\Longrightarrow\; \exists w:\ w^{\mathsf T} M w < 0 .$$

These are Eq. (2.53) and Eq. (2.58) of the review; they are the two ingredients from which convexity and directional boundedness follow.

Significance

What the result gives: $\Omega$ is the region to which Gribov's improved gauge fixing restricts the functional integral, and every subsequent construction in this line of work — the no-pole condition, the horizon function and the local Gribov–Zwanziger action — presupposes that the restriction is to a bounded convex region containing the perturbative point $A = 0$. Convexity is what makes the horizon condition a single well-posed constraint; boundedness in every direction is the property from which the infrared suppression of the gluon propagator, and hence Gribov's mass scale, is read off. Without boundedness there is no geometric mechanism for a mass gap in this scenario.

Status honesty: these statements are proved mathematics, not open problems; the arguments in §2.2.1 of the review are short. What is missing is a machine-checked account. No formalization of the Gribov region in Lean is known to the drafter of this proposal; the platform's existing Gribov material concerns Singer's topological obstruction to continuous gauge fixing, which is a different theorem about a different object.

Difficulty

The statements are elementary once the correct hypotheses are isolated, and the mission is calibrated accordingly: it is a faithfulness exercise rather than a depth exercise. The two places where a naive attempt fails are worth naming. First, directional boundedness does not follow from positivity alone: it needs the tracelessness of $M_2(A)$, which is what forces a direction $w$ with $w^{\mathsf T} M_2(A) w < 0$; a positive semidefinite perturbation would give a region unbounded along that ray. Second, "bounded in every direction" does not imply "bounded" for a general set, and the implication used here rests on convexity together with injectivity of $M_2$ — the argument goes through a limit of rescaled configurations and a closure of the positivity condition, not through a uniform bound extracted directly from the ray statement.

Formalization scope

The mission commits to a finite-dimensional linear-algebra model of the Faddeev–Popov operator, packaged as a structure carrying: the matrix $M_0$ together with a proof that it is positive definite; the linear map $A \mapsto M_2(A)$ together with proofs that each $M_2(A)$ is symmetric and traceless. Configurations live in an arbitrary real vector space $V$, which carries a norm and finite-dimensionality only in the two statements where boundedness is asserted. Positive definiteness is Mathlib's notion for real matrices, which includes symmetry; the region is the set of configurations where it holds strictly, so $\Omega$ is the open region and the horizon is not part of it.

This is a model, not the field-theoretic object: it replaces the operator $-\partial_\mu D_\mu$ acting on transverse fields by its finite-dimensional algebraic shadow, and the reviewer should audit it as such. The properties targeted here are exactly those whose proofs in §2.2.1 use only linearity in $A$, symmetry, tracelessness, and positivity of $-\partial^2$; results that genuinely need the infinite-dimensional setting — that every gauge orbit passes inside $\Omega$, and that $\Omega$ still contains copies on its boundary — are deliberately out of scope, since they cannot be stated in this model.

The model is not vacuous: an instance exists already for $V = \mathbb{R}$, $n = 2$, $M_0 = I$ and $M_2(t) = t\,\mathrm{diag}(1,-1)$, with $M_2$ injective, so none of the statements is satisfied vacuously. Nor is any target trivially true: $\Omega$ is a proper nonempty subset of $V$ in that instance.

Infrastructure needed: Mathlib's positive-definiteness API for matrices, the spectral theorem for real symmetric matrices (for the traceless lemma), and basic convexity and boundedness in finite-dimensional normed spaces. The traceless lemma — a nonzero symmetric traceless matrix has a direction of negative quadratic form — is reusable well beyond this mission. Contributions extending the model towards the infinite-dimensional setting, or supplying the explicit ellipsoidal bound of Dell'Antonio–Zwanziger in place of plain boundedness, are welcome.

Selected references

• N. Vandersickel, D. Zwanziger, The Gribov problem and QCD dynamics, Physics Reports 520 (2012) 175–251. https://doi.org/10.1016/j.physrep.2012.07.003
• V. N. Gribov, Quantization of non-Abelian gauge theories, Nuclear Physics B139 (1978) 1.
• D. Zwanziger, Nonperturbative modification of the Faddeev–Popov formula and banishment of the naive vacuum, Nuclear Physics B209 (1982) 336.
• M. Semenov-Tyan-Shanskii, V. Franke, A variational principle for the Lorentz condition and restriction of the domain of path integration in non-abelian gauge theory, 1982.
• G. Dell'Antonio, D. Zwanziger, Ellipsoidal bound on the Gribov horizon contradicts the perturbative renormalization group, Nuclear Physics B326 (1989) 333.
• G. Dell'Antonio, D. Zwanziger, Every gauge orbit passes inside the Gribov horizon, Communications in Mathematical Physics 138 (1991) 291–299.

Motivation

The third mission in the series formalizing Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) turns to the second main topic of Chapter 1, covering spaces (Section 1.3, pp. 56–78). The first mission used the covering $\mathbb{R}\to S^1$ to compute $\pi_1(S^1)$, and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space $X$: the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of $\pi_1(X)$ (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the classification theorem (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of $X$ and subgroups of $\pi_1(X,x_0)$, together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).

All statements live in the Lean namespace Hatcher used by the earlier missions.

Setting

A covering space of $X$ (p. 56) is a space $\tilde X$ with a map $p:\tilde X\to X$ such that every $x\in X$ has an open neighborhood $U$ whose preimage is a disjoint union of open sets each mapped homeomorphically onto $U$; $p^{-1}(U)$ may be empty, so $p$ need not be surjective. This is Mathlib's IsCoveringMap. For a covering space with basepoints $p:(\tilde X,\tilde x_0)\to(X,x_0)$ we write

$$p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0),\qquad H=p_*\big(\pi_1(\tilde X,\tilde x_0)\big)\le\pi_1(X,x_0)$$

for the induced homomorphism (Hatcher.coverHom) and its image (Hatcher.coverSubgroup).

$X$ is semilocally simply-connected (p. 63, Hatcher.IsSemilocallySimplyConnected) if each $x\in X$ has a neighborhood $U$ such that every loop at $x$ contained in $U$ is null-homotopic in $X$. The bundle Hatcher_Covering also fixes: the structure CoveringSpace X (a total space $\tilde X$ and a covering map $p$) and its pointed version PointedCover X x₀ (with $\tilde x_0\in p^{-1}(x_0)$ and associated subgroup PointedCover.subgroup); isomorphism of covering spaces (p. 67), a homeomorphism $f:\tilde X_1\to\tilde X_2$ with $p_1=p_2f$, with or without preservation of basepoints (IsIsomorphic, IsPointedIsomorphic); the deck transformation group $G(\tilde X)$ (p. 70, deckGroup), the self-homeomorphisms of $\tilde X$ commuting with $p$; normal covering spaces (p. 70, IsNormalCover); Hatcher's condition $(\ast)$ for a covering space action of a group $G$ on $Y$ (p. 72, IsCoveringSpaceAction); and the orbit space $Y/G$ with its quotient map (OrbitSpace, orbitProj).

Formalization targets

Goal (Theorem 1.38, p. 67)

Let $X$ be path-connected, locally path-connected and semilocally simply-connected, with basepoint $x_0$. Then:

1. every subgroup $H\le\pi_1(X,x_0)$ is $p_*\pi_1(\tilde X,\tilde x_0)$ for some path-connected covering space with basepoint;
2. two path-connected covering spaces with basepoints are isomorphic by a basepoint-preserving isomorphism iff their subgroups coincide;
3. two path-connected covering spaces are isomorphic (basepoints ignored) iff their subgroups, at some choice of basepoints over $x_0$, are conjugate in $\pi_1(X,x_0)$.

Together these say that $(\tilde X,\tilde x_0)\mapsto p_*\pi_1(\tilde X,\tilde x_0)$ is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.

Milestones

1. Proposition 1.31 (p. 61), first part: $p_*$ is injective.
2. Proposition 1.31, second part: $p_*\pi_1(\tilde X,\tilde x_0)$ consists of the classes of loops at $x_0$ whose lifts starting at $\tilde x_0$ are loops.
3. Proposition 1.32 (p. 61): for $X,\tilde X$ path-connected, the fibre $p^{-1}(x_0)$ is in bijection with the cosets of $H$, so the number of sheets is the index of $H$.
4. Proposition 1.33 (p. 61), the lifting criterion: for $Y$ path-connected and locally path-connected, $f:(Y,y_0)\to(X,x_0)$ lifts to $(\tilde X,\tilde x_0)$ iff $f_*\pi_1(Y,y_0)\subseteq H$.
5. Proposition 1.34 (p. 62), unique lifting: two lifts of $f:Y\to X$ agreeing at one point agree everywhere if $Y$ is connected.
6. Necessity of semilocal simple connectivity (p. 63): if $X$ has a simply-connected covering space (surjective onto $X$), then $X$ is semilocally simply-connected.
7. Existence of a simply-connected covering space (pp. 63–65): if $X$ is path-connected, locally path-connected and semilocally simply-connected, it has a simply-connected covering space (the universal cover).
8. Proposition 1.36 (p. 66): under the same hypotheses, every subgroup $H\le\pi_1(X,x_0)$ is realized as $p_*\pi_1(X_H,\tilde x_0)$ for a path-connected covering space.
9. Proposition 1.37 (p. 67): for $X$ path-connected and locally path-connected, two path-connected covering spaces with basepoints are basepoint-preservingly isomorphic iff their subgroups are equal.
10. Change of basepoint (pp. 67–68, proof of Theorem 1.38): moving $\tilde x_0$ within $p^{-1}(x_0)$ replaces $H$ by a conjugate, and every conjugate arises this way.
11. Proposition 1.39(a) (p. 71): a path-connected covering space of a path-connected, locally path-connected $X$ is normal iff $H$ is a normal subgroup.
12. Proposition 1.39(b): $G(\tilde X)\cong N(H)/H$, given as a surjective homomorphism $N(H)\to G(\tilde X)$ with kernel $H$.
13. Proposition 1.39, final clause: for the universal cover, $G(\tilde X)\cong\pi_1(X,x_0)$.
14. Proposition 1.40(a) (p. 72): for a covering space action of $G$ on $Y$, the quotient map $Y\to Y/G$ is a normal covering space.
15. Proposition 1.40(b): if moreover $Y$ is path-connected, $G$ is the group of deck transformations of $Y\to Y/G$, via $g\mapsto(y\mapsto gy)$.
16. Proposition 1.40(c): if $Y$ is path-connected and locally path-connected, $G\cong\pi_1(Y/G)/p_*\pi_1(Y)$, given as a surjective homomorphism $\pi_1(Y/G)\to G$ with kernel $p_*\pi_1(Y)$.

Significance

The result itself. The classification theorem is the central structural fact about covering spaces: the connected coverings of $X$ are "the same as" the subgroups of $\pi_1(X)$, with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces ($\pi_1(\mathbb{RP}^n)=\mathbb{Z}/2$, $\pi_1(T^n)=\mathbb{Z}^n$, lens spaces) and is used throughout Hatcher's later chapters.

Formalizing it. Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (IsCoveringMap.liftPath, liftHomotopy), the monodromy action (IsCoveringMap.monodromy), the injectivity of $p_*$ (injective_path_homotopic_map, cited there as Proposition 1.31), the unique-lifting statement (IsCoveringMap.eq_of_comp_eq), and the lifting criterion itself (existsUnique_continuousMap_lifts_of_range_le, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has IsQuotientCoveringMap, with the homomorphism $\pi_1(Y/G)\to G^{\mathrm{op}}$ and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings $X_H$, no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.

Difficulty

The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from $x_0$, the topology is generated by the sets $U_{[\gamma]}$ for $U$ in the basis of path-connected open sets on which $\pi_1$ dies, and one must verify that this is a topology basis, that $p$ is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by $H$ and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.

Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in $N(H)$ to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on $Y/G$ and the evenly covered neighborhoods $p(U)$ from condition $(\ast)$; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.

Formalization scope

• Spaces are arbitrary topological spaces; hypotheses (path-connectedness, local path-connectedness, semilocal simple connectivity, connectedness of the domain in Proposition 1.34) are stated per theorem, exactly where Hatcher assumes them.
• CoveringSpace X bundles a total space in the same universe as $X$ with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings $X_H$ are constructed from paths in $X$, they live in that universe, so nothing is lost.
• "Isomorphic" is the existence of a homeomorphism over $X$ (Hatcher, p. 67), a proposition on pairs of covering spaces; Theorem 1.38 is stated as the three-part conjunction above rather than as a bijection between quotient sets, which avoids forming the set of isomorphism classes of types while asserting exactly the same content.
• Conjugacy is expressed with Mathlib's MulAut.conj; "number of sheets equals the index" is stated as a bijection $p^{-1}(x_0)\simeq\pi_1(X,x_0)/H$ with the coset space.
• The isomorphisms of Propositions 1.39(b) and 1.40(c) are stated as surjective homomorphisms with prescribed kernel, which is how Hatcher proves them and avoids requiring a Normal instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on $Y$ prescribed.
• A covering space action includes continuity of each $y\mapsto gy$ (Hatcher's actions are by homeomorphisms). The orbit space is Mathlib's MulAction.orbitRel.Quotient with the quotient topology.
• Trivializing readings are excluded: path-connected spaces are nonempty, and a nonempty covering space of a path-connected base is surjective; milestone 6 assumes surjectivity explicitly because its base need not be connected.

Contributions welcome: a reusable construction of the space of path classes with its topology, the covering $X_H$, and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.3, pp. 56–72. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• E. H. Spanier, Algebraic Topology, Springer, 1966, Chapter 2 (covering spaces and the classification theorem).
• J. R. Munkres, Topology, 2nd ed., Prentice Hall, 2000, Chapter 13 (classification of covering spaces).
• Mathlib, Mathlib/Topology/Covering/Basic.lean (covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.lean
• Mathlib, Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting, monodromy, the lifting criterion). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean
• Mathlib, Mathlib/Topology/Covering/Quotient.lean (quotient covering maps for group actions). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean

Motivation

Once $\pi_1(S^1)\cong\mathbb{Z}$ is known, the next question in Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) is how to compute fundamental groups of spaces built from pieces. Section 1.2 answers this with van Kampen's theorem (Theorem 1.20, p. 43): if a space is covered by open sets with a common basepoint and path-connected intersections, its fundamental group is the free product of the fundamental groups of the pieces, modulo relations coming from the intersections. It is the main computational tool of Chapter 1: it gives the fundamental groups of wedges of circles, graphs, surfaces, and every CW complex from its 2-skeleton (Propositions 1.26–1.28), and it underlies the classification of covering spaces in Section 1.3.

This is the second mission in the series formalizing Hatcher's book. The first mission established the covering-space lifting properties and $\pi_1(S^1,1)\cong\mathbb{Z}$ in the Lean namespace Hatcher; this one covers the subsection "The van Kampen Theorem" of Section 1.2 (pp. 41–47) together with its warm-up Lemma 1.15 and Proposition 1.14 from Section 1.1 (p. 35).

Setting

Let $X$ be a topological space with a basepoint $x_0$. A path is a continuous map $I=[0,1]\to X$, a loop at $x_0$ is a path with both endpoints $x_0$, and $\pi_1(X,x_0)$ is the group of homotopy classes of loops at $x_0$ under concatenation. A continuous map $\varphi:X\to Y$ with $\varphi(x_0)=y_0$ induces a homomorphism $\varphi_*:\pi_1(X,x_0)\to\pi_1(Y,y_0)$, $[f]\mapsto[\varphi\circ f]$.

Let $(A_\alpha)_{\alpha\in\iota}$ be a family of subsets of $X$, each containing $x_0$, with the subspace topology; write $\pi_1(A_\alpha)$ for $\pi_1(A_\alpha,x_0)$. The inclusions $A_\alpha\hookrightarrow X$ induce

$$j_\alpha:\pi_1(A_\alpha)\to\pi_1(X),$$

which are Hatcher.inclHom, and the inclusions $A_\alpha\cap A_\beta\hookrightarrow A_\alpha$ and $A_\alpha\cap A_\beta\hookrightarrow A_\beta$ induce

$$i_{\alpha\beta}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\alpha),\qquad i_{\beta\alpha}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\beta),$$

which are Hatcher.interHomLeft and Hatcher.interHomRight.

The free product $\ast_\alpha G_\alpha$ of a family of groups is the group of reduced words in the $G_\alpha$ (Hatcher, pp. 41–42); in Lean it is Mathlib's Monoid.CoprodI, here Hatcher.FreeProd. Its universal property extends the $j_\alpha$ to a single homomorphism

$$\Phi:\ast_\alpha\pi_1(A_\alpha)\to\pi_1(X),$$

Hatcher.vanKampenHom. Since $j_\alpha i_{\alpha\beta}=j_\beta i_{\beta\alpha}$ (both are induced by $A_\alpha\cap A_\beta\hookrightarrow X$), the elements

$$i_{\alpha\beta}(\omega)\,i_{\beta\alpha}(\omega)^{-1},\qquad \omega\in\pi_1(A_\alpha\cap A_\beta),$$

lie in the kernel of $\Phi$. Let $N$ be the normal subgroup generated by all of them, Hatcher.vanKampenNormal.

Formalization targets

Goal (Theorem 1.20)

If $X$ is the union of path-connected open sets $A_\alpha$ each containing $x_0$, each $A_\alpha\cap A_\beta$ is path-connected, and each $A_\alpha\cap A_\beta\cap A_\gamma$ is path-connected, then

$$\Phi \text{ is surjective}\qquad\text{and}\qquad \ker\Phi=N .$$

Hence $\Phi$ induces an isomorphism $\pi_1(X)\cong\ast_\alpha\pi_1(A_\alpha)/N$.

Milestones

1. Lemma 1.15 (p. 35). If $X$ is the union of path-connected open sets $A_\alpha$ containing $x_0$ with each $A_\alpha\cap A_\beta$ path-connected, then every loop in $X$ at $x_0$ is homotopic to a product of loops each of which is contained in a single $A_\alpha$.
2. Proposition 1.14 (p. 35). $\pi_1(S^n)=0$ for $n\ge 2$.
3. Theorem 1.20, first part (p. 43). Under the hypotheses of Lemma 1.15, $\Phi$ is surjective.
4. The kernel contains the relators (p. 43). $N\le\ker\Phi$, with no hypotheses on the cover.
5. Theorem 1.20, second part (p. 43). If moreover every triple intersection is path-connected, $\ker\Phi\le N$.
6. Induced isomorphism (p. 43). Under the same hypotheses there is an isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ sending the class of a word to its image under $\Phi$.

Significance

The result itself. Van Kampen's theorem is the gluing law for $\pi_1$. With it Hatcher computes $\pi_1$ of wedge sums (free products), of graphs (free groups), of the closed orientable surfaces (Example 1.26), and shows that attaching $2$-cells kills exactly the attaching loops (Proposition 1.26), so that every group is a fundamental group (Corollary 1.28). The surjectivity half alone gives Proposition 1.14, that spheres of dimension at least two are simply connected, and hence that $\mathbb{R}^2$ is not homeomorphic to $\mathbb{R}^n$ for $n\ne 2$ (Corollary 1.16).

Formalizing it. Mathlib has the fundamental groupoid and fundamental group, induced homomorphisms (FundamentalGroup.map), free products of groups (Monoid.CoprodI) with their universal property, normal closures, and quotient groups. It has no version of van Kampen's theorem for topological spaces (its CategoryTheory/Limits/VanKampen concerns colimits in categories, not fundamental groups), and no computation of $\pi_1(S^n)$ for $n\ge 2$; on the platform, however, the theorem SP4Mission.sphere_simplyConnected (already proved in this environment) states that the unit sphere of $\mathbb{R}^n$ is simply connected for $n\ge 3$, which is Proposition 1.14 with shifted indexing, so that milestone can be closed by a one-line reduction. The mission supplies the statements in Hatcher's form, on Mathlib's $\pi_1$, so that later missions (covering spaces, cell complexes) can use them directly.

Difficulty

Surjectivity is a compactness argument: subdivide $I$ so each piece of the loop lies in one $A_\alpha$, then use path-connectedness of the intersections to connect the subdivision points back to $x_0$. The formal difficulty is bookkeeping: producing the subdivision from an open cover of $[0,1]$ (Mathlib's exists_monotone_Icc_subset_open_cover_unitInterval is the tool) and showing the reparametrised concatenation is homotopic to the original loop.

The kernel computation is the hard part. Hatcher's proof takes a homotopy $F:I\times I\to X$ between two factorizations, subdivides the square into rectangles each mapped into a single $A_\alpha$, perturbs the grid so at most three rectangles meet at a corner (this is where triple intersections enter), and then shows that moving the loop across one rectangle at a time changes the factorization only by the two elementary moves that hold in $\ast_\alpha\pi_1(A_\alpha)/N$. Every step is elementary, but the induction over the grid is long, and each elementary move requires an explicit path-homotopy in a subspace. The naive idea of proving $\ker\Phi\le N$ by an induction on word length does not work: the relation between two factorizations of the same loop is only visible through a homotopy in $X$, not through the words.

Proposition 1.14 is easy given Lemma 1.15 but requires exhibiting the cover of $S^n$ by two complements of antipodal points, showing each is simply connected (homeomorphic to $\mathbb{R}^n$ via stereographic projection, which Mathlib has as stereographic), and showing their intersection is path-connected when $n\ge 2$.

Formalization scope

• The index set $\iota$ and the space $X$ are arbitrary; the $A_\alpha$ are Set X with the subspace topology, and $\pi_1(A_\alpha)$ is Mathlib's FundamentalGroup ↥(A α) ⟨x₀, _⟩. Hypotheses are stated explicitly on each theorem: IsOpen, IsPathConnected, ⋃ α, A α = Set.univ, and path-connectedness of pairwise (and, where Hatcher requires it, triple) intersections.
• $i_{\alpha\beta}$ and $i_{\beta\alpha}$ are both defined on $\pi_1(A_\alpha\cap A_\beta)$ (rather than on $\pi_1(A_\beta\cap A_\alpha)$ for the second), so no identification of $A_\alpha\cap A_\beta$ with $A_\beta\cap A_\alpha$ is needed; the set of relators ranges over all ordered pairs $(\alpha,\beta)$.
• "Product of loops" in Lemma 1.15 is a finite List of loops, each tagged with the index $\alpha$ of the piece it lies in, concatenated right-to-left with the constant loop as empty product (Hatcher.loopProd). Any bracketing gives the same homotopy class.
• The goal is stated as the conjunction "surjective and $\ker\Phi=N$"; the isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ is a separate milestone, stated as the existence of a group isomorphism compatible with $\Phi$ on the quotient, which pins it down uniquely.
• $S^n$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1, and "$\pi_1(S^n)=0$" is Mathlib's SimplyConnectedSpace (path-connected with trivial fundamental group), which is what Hatcher means since $S^n$ is path-connected.
• Trivializing readings are excluded: the cover hypotheses do not force $\iota$ nonempty, but then $X=\bigcup A_\alpha=\varnothing$ contradicts the existence of $x_0$, so the statements are not vacuous in any interesting case, and $\Phi$ is the specific homomorphism induced by the inclusions.

Contributions welcome: the subdivision lemma for loops in an open cover, a reusable treatment of factorizations and their elementary moves, and the two-set special case $\pi_1(X)\cong(\pi_1(A)\ast\pi_1(B))/N$ as a corollary.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.2, pp. 40–49; Lemma 1.15 and Proposition 1.14, p. 35. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• E. R. van Kampen, On the connection between the fundamental groups of some related spaces, American Journal of Mathematics 55 (1933), 261–267. https://doi.org/10.2307/2371128
• H. Seifert, Konstruktion dreidimensionaler geschlossener Räume, Berichte Sächs. Akad. Leipzig 83 (1931), 26–66.
• Mathlib, Mathlib/GroupTheory/CoprodI.lean (free products of groups). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.lean
• Mathlib, Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (fundamental group and induced homomorphisms). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

Motivation

The Hardy--Littlewood circle method is the principal analytic tool for counting solutions to additive equations in integers. Introduced by Hardy and Ramanujan for the partition function and developed by Hardy and Littlewood in their Partitio Numerorum series (1920--1928), it produces asymptotic formulae for the number of representations of a large integer $n$ as a sum of $s$ terms drawn from a prescribed set — $k$-th powers, primes, values of a polynomial.

Its engine is an estimate for exponential sums. If a sum $\sum_{x<N} e(\alpha x^k)$, where $e(\theta)=\exp(2\pi i\theta)$, exhibits cancellation for every $\alpha$ not well approximable by a rational with small denominator, the method delivers an asymptotic formula; if it does not, the method stalls. Weyl's inequality (Weyl 1916) was the first such estimate and remains the standard one for moderate $k$.

A short timeline of the estimate this mission targets. Weyl (1916) proved the inequality below with the exponent $2^{1-k}$, in the course of his work on uniform distribution. Hardy and Littlewood (1920--1928) built the circle method on it, obtaining $G(k)\le (k-2)2^{k-1}+5$ for Waring's problem. Vinogradov (1935) replaced Weyl differencing by his mean value theorem, superior for large $k$, reducing the bound to $O(k\log k)$; Wooley's efficient congruencing (2012) and the Bourgain--Demeter--Guth decoupling theorem (2016) settled the main conjecture of Vinogradov's mean value theorem. For small $k$ — and as the entry point to the subject — Weyl's inequality is still the right tool, and it is the natural first capstone for a formalization of the method.

Setting

For a real number $\theta$ write

$$e(\theta) \;=\; \exp(2\pi i \theta),$$

the standard additive character of $\mathbb{R}/\mathbb{Z}$: it satisfies $e(x+y)=e(x)e(y)$, $|e(x)|=1$, and $e(x)=1$ exactly when $x\in\mathbb{Z}$.

For a real number $\theta$ write $\|\theta\|$ for the distance from $\theta$ to the nearest integer. It is periodic with period $1$, vanishes exactly on $\mathbb{Z}$, satisfies the triangle inequality, and is at most $\tfrac12$.

Given a finite set $A\subseteq\mathbb{Z}$, its generating function is $f_A(\theta)=\sum_{a\in A}e(a\theta)$. The basic identity of the subject is

$$\int_0^1 f_A(\theta)^s\,e(-n\theta)\,d\theta \;=\; \#\{(a_1,\dots,a_s)\in A^s : a_1+\cdots+a_s=n\},$$

a consequence of the orthogonality relation $\int_0^1 e(m\theta)\,d\theta=[\,m=0\,]$.

A Weyl sum of degree $k$ is $\sum_{0\le x<N} e(\alpha x^k)$. The whole difficulty is to bound it for $\alpha$ in the minor arcs — those $\alpha$ admitting no rational approximation $a/q$ with $q$ small.

Target

Fix $k\ge 2$. For every $\varepsilon>0$ there is a constant $C=C(k,\varepsilon)$ such that whenever $(a,q)=1$, $q\ge 1$, and $\left|\alpha-\frac{a}{q}\right|\le \frac{1}{q^2}$,

$$\left|\sum_{0\le x<N} e(\alpha x^{k})\right| \;\le\; C\,N^{1+\varepsilon}\left(\frac{1}{q}+\frac{1}{N}+\frac{q}{N^{k}}\right)^{2^{1-k}}.$$

The intermediate targets, weakest first, are the milestone list: the counting identity, the Weyl differencing (squaring) step, the Farey covering with coprime numerator, the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, Hua's fourth-moment inequality for $k=2$, and the degree-two case of the inequality itself.

Significance

The result itself. Weyl's inequality is what makes the minor arcs negligible. Applied with $q$ in the range $N^{\delta}\le q\le N^{k-\delta}$ it gives a power saving over the trivial bound $N$, and integrating that saving over the minor arcs shows their contribution is smaller than the main term produced by the major arcs. Every classical application of the circle method — the asymptotic formula in Waring's problem, Vinogradov's three primes theorem, the Birch--Davenport theory of forms in many variables — passes through an estimate of this shape. Without it the method produces an identity, not a theorem.

Formalizing it. Mathlib currently contains the analytic prerequisites — Fourier characters on AddCircle, Dirichlet's approximation theorem, Abel summation, Gauss sums — but no circle-method apparatus whatsoever: no Weyl sums, no arc dissection, no singular series, no mean value estimates. This mission supplies the first layer. The foundational tier is already machine-checked: 53 theorems covering the character $e$, the norm $\|\cdot\|$, the geometric sum bound $\left|\sum_{x<N}e(x\theta)\right|\le\min\!\left(N,\frac{1}{2\|\theta\|}\right)$, both orthogonality relations, both forms of Dirichlet's theorem, and the basic theory of $f_A$, are published on the platform with verified proofs and may be imported freely. What remains open is the combinatorial and analytic core listed in the milestones. None of the milestone statements is currently formalized anywhere, to the best of our knowledge.

Difficulty

The obvious approach fails immediately. One would like to sum $\left|\sum_{x<N}e(\alpha x^k)\right|$ by comparing it to the linear case, where the geometric series gives $\min(N,\frac{1}{2\|\alpha\|})$ outright. But for $k\ge2$ the summand is not a geometric progression and there is no closed form.

Weyl's device is to square and difference: $\left|\sum_x e(\phi(x))\right|^2=\sum_{x,y}e(\phi(x)-\phi(y))$, and the substitution $y=x+h$ turns the inner polynomial into one of degree $k-1$ in $x$. Iterating $k-1$ times reduces to a linear sum, at the cost of raising the estimate to the power $2^{1-k}$ — which is why the saving is so weak for large $k$, and why Vinogradov's method eventually supersedes it.

The genuine obstacles in a formalization are: (i) bookkeeping the shifted ranges produced by each differencing step, which are not $[0,N)$ and must be handled uniformly; (ii) the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, needed to count the $h$ for which the resulting linear coefficient is close to an integer, and which is not currently in Mathlib in this form; (iii) tracking the $\varepsilon$-dependent constants through $k-1$ iterations without the informal $\ll$ notation.

Formalization scope

Statements are given over the Prove2Me default environment (Lean v4.30.0, Mathlib c5ea003), in the shared namespace CircleMethod, and build on two published definitions: CircleMethod_char (the character e and the norm nrm) and CircleMethod_genfun (the generating function f).

Conventions this mission commits to:

• $\|\theta\|$ is nrm θ = |θ - round θ|. Mathlib's round breaks ties upwards, so round is not an odd function; the characterisation to use is minimality, nrm θ ≤ |θ - n| for every integer n, which is published as CircleMethod.nrm_le.
• Sums run over Finset.range N, that is $0\le x<N$, and $N$ is a natural number. Hypotheses 0 < N and 0 < q are stated explicitly rather than left implicit.
• Asymptotic notation is eliminated in favour of explicit existential constants: $X\ll_\varepsilon Y$ is rendered as ∀ ε > 0, ∃ C > 0, ∀ …, X ≤ C * Y, with the constant quantified outside the parameters it may depend on and inside nothing else. Solvers should not weaken this by allowing $C$ to depend on $N$, $q$ or $\alpha$.
• Exponents such as $N^{1+\varepsilon}$ and $2^{1-k}$ are real powers (Real.rpow), not natural powers.
• Coprimality is Nat.Coprime a.natAbs q, which is the correct notion for a possibly negative numerator.

One trivialising formalization to rule out: the goal must not be read with $C$ permitted to depend on $N$, since then $C=N$ makes it vacuous. The quantifier order in the Lean statement already forbids this, and solvers should preserve it exactly.

Contributions welcome on any milestone independently; the divisor bound and the Farey covering are self-contained and need no other milestone. Both are reusable well beyond this mission.

Selected references

• H. Weyl, Über die Gleichverteilung von Zahlen mod. Eins, Mathematische Annalen 77 (1916), 313--352. DOI:10.1007/BF01475864
• G. H. Hardy and J. E. Littlewood, Some problems of 'Partitio Numerorum' I--VI, 1920--1928.
• R. C. Vaughan, The Hardy--Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997. (Weyl's inequality is Lemma 2.4; the geometric sum bound is Lemma 2.1.)
• I. M. Vinogradov, New estimates for Weyl sums, Doklady Akademii Nauk SSSR 8 (1935), 195--198.
• T. D. Wooley, Vinogradov's mean value theorem via efficient congruencing, Annals of Mathematics 175 (2012), 1575--1627. DOI:10.4007/annals.2012.175.3.12
• J. Bourgain, C. Demeter and L. Guth, Proof of the main conjecture in Vinogradov's mean value theorem for degrees higher than three, Annals of Mathematics 184 (2016), 633--682. DOI:10.4007/annals.2016.184.2.7