Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns (experimental)
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Is every odd number a sum of k primes? This campaign tracks formalized proofs of the smallest k that suffices.
Schnirelmann (1930) showed some finite k works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved k=5 unconditionally. Helfgott (2013) proved that every odd number greater than 5 is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: 27 is neither prime nor 2 + prime.
Schoolbook matrix multiplication takes n3 operations. The exponent ω is the infimum of all τ such that two n×n matrices can be multiplied in O(nτ) arithmetic operations; trivially ω≥2, and ω=2 is conjectured but open.
Strassen gave the first nontrivial bound, ω<2.81, in 1969, and introduced the laser method in 1986 to reach ω<2.48. Coppersmith and Winograd's 1990 bound of 2.376 stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached ω<2.371339 in 2025, and the current record is ω<2.371177, from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Counterexamples to the Zeng–Pryadko Homological-Distance ConjectureResearch Paper
## Background and main question
The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If $A$ and $B$ are finite based chain complexes over a finite field, their tensor product is graded by total degree,
$$
(A\otimes B)_j=\bigoplus_{i=0}^{j} A_i\otimes B_{j-i}.
$$
Each complex carries a basis-dependent homological distance: $d_j(A)$ is the least Hamming weight of a degree-$j$ cycle that is not a boundary, with $d_j(A)=\infty$ when the degree-$j$ homology vanishes. A natural candidate for the distance of the tensor product is therefore
$$
m_j(A,B)=\min_{0\le i\le j} d_i(A)d_{j-i}(B).
$$
Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has $d_j(A\otimes B)\le m_j(A,B)$. The substantive question is whether this upper bound is always sharp.
In the preprint [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://arxiv.org/abs/1810.01519), posted in 2018 and subsequently [published in *Physical Review Letters*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://prove2.me/missions/Higher-Dimensional%20Quantum%20Hypergraph-Product%20Codes%20with%20Finite%20Rates). The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.
Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), published in 2020. In [the corresponding arXiv preprint](https://arxiv.org/abs/2007.12152), Conjecture 18 asserts the unrestricted equality
$$
d_j(A\otimes B)=m_j(A,B).
$$
The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in $A\otimes B$ need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.
## The counterexample mechanism
The common foundation is recorded in the Prove2Me entry [*Based binary chain complexes and homological distance*](https://prove2.me/theorems/9d65f1ac-c78c-4540-8ac4-38597548a9ff). In particular, the boundary in degree $j$ is a map $\partial_j:A_j\to A_{j-1}$, and
$$
d_j(A)=\inf\{\operatorname{wt}(x):x\in\ker\partial_j,\ x\notin\operatorname{im}\partial_{j+1}\}.
$$
The one-complex result is separately available as [*Eq. (13) — Exact distance with a one-complex*](https://prove2.me/theorems/4f4006fe-af5b-42ba-a936-bb49e92c92b6). The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.
Begin with binary CSS check maps
$$
H_X:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_X},
\qquad
H_Z:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_Z},
$$
assumed surjective and satisfying $H_XH_Z^T=H_ZH_X^T=0$. Suppose there are logical vectors $x,z\in\mathbb F_2^n$ such that
$$
H_Zx=0,\qquad H_Xz=0,\qquad x\cdot z=1.
$$
The check maps determine two dual three-term complexes
$$
A:\quad \mathbb F_2^{r_X}\xleftarrow{H_X}\mathbb F_2^n
\xleftarrow{H_Z^T}\mathbb F_2^{r_Z},
\qquad
B:\quad \mathbb F_2^{r_Z}\xleftarrow{H_Z}\mathbb F_2^n
\xleftarrow{H_X^T}\mathbb F_2^{r_X}.
$$
Their degree-two tensor space has three bidegree summands, corresponding to $(2,0)$, $(1,1)$, and $(0,2)$. Under the natural matrix identifications, consider the element whose three blocks are
$$
(I_{r_Z},I_n,I_{r_X}).
$$
The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly $r_Z+n+r_X$, whereas the componentwise candidate in degree two reduces to
$$
m_2(A,B)=d_1(A)d_1(B).
$$
Consequently, any CSS datum satisfying
$$
r_Z+n+r_X<d_1(A)d_1(B)
$$
produces the strict inequality $d_2(A\otimes B)<m_2(A,B)$. For orientation, a binary quantum Golay CSS presentation with parameters $[[23,1,7]]$ has $r_X=r_Z=11$, giving the numerical comparison $45<49$. The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.
## Formalization objectives
The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element $(I_{r_Z},I_n,I_{r_X})$ is a nontrivial degree-two cycle of weight $r_Z+n+r_X$, and the componentwise minimum is $d_1(A)d_1(B)$.
The second milestone constructs and verifies one explicit CSS datum for which $r_Z+n+r_X<d_1(A)d_1(B)$. This is the step that turns the general mechanism into an actual counterexample.
The capstone packages the construction as the direct existential statement
$$
\exists\,A,B\qquad d_2(A\otimes B)<\min_{0\le i\le 2}d_i(A)d_{2-i}(B).
$$
Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.
## Relation to prior work
The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.
The broader literature also indicates why additional structure matters. [Bravyi and Hastings](https://dl.acm.org/doi/10.1145/2591796.2591870) introduced homological-product codes and analyzed logical representatives in product constructions; [Audoux and Couvreur](https://www.numdam.org/articles/10.4171/aihpd/71/) developed tensor products of CSS codes through chain-complex methods. More recently, [Akhmechet et al.](https://arxiv.org/abs/2410.11252) discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while [Berthusen et al.](https://arxiv.org/abs/2508.04794) restated it as Conjecture 5.1 in their study of automorphism gadgets. [Golowich and Guruswami](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25) obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.
Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.
The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with $\infty$-valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.
## References
- W. Zeng and L. P. Pryadko, [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), *Physical Review Letters* 122, 230501 (2019); [arXiv:1810.01519 (2018), Eq. (13)](https://arxiv.org/abs/1810.01519).
- W. Zeng and L. P. Pryadko, [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), *Physical Review A* 102, 062402 (2020); [arXiv:2007.12152, Conjecture 18](https://arxiv.org/abs/2007.12152).
- S. Bravyi and M. B. Hastings, [*Homological Product Codes*](https://dl.acm.org/doi/10.1145/2591796.2591870), STOC 2014; [arXiv:1311.0885](https://arxiv.org/abs/1311.0885).
- B. Audoux and A. Couvreur, [*On tensor products of CSS codes*](https://www.numdam.org/articles/10.4171/aihpd/71/), *Annales de l'Institut Henri Poincaré D* 6 (2019); [arXiv:1512.07081](https://arxiv.org/abs/1512.07081).
- R. Akhmechet et al., [*Khovanov homology and quantum error-correcting codes*](https://arxiv.org/abs/2410.11252), arXiv:2410.11252 (2024).
- N. Berthusen et al., [*Automorphism gadgets in homological product codes*](https://arxiv.org/abs/2508.04794), arXiv:2508.04794 (2025).
- L. Golowich and V. Guruswami, [*Quantum LDPC Codes of Almost Linear Distance via Iterated Homological Products*](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25), CCC 2025; [full version](https://arxiv.org/abs/2411.03646).
## Motivation
A quantum circuit of depth $d$ built from gates of fan-in at most two cannot let an output
wire depend on more than $2^d$ input wires. The argument is folklore and takes a paragraph on
paper: the *causal cone* of the measured wire grows by at most a factor of two per layer.
Formalizing it exposes a subtlety that the paper argument hides, and that is what this mission
is about.
## The subtlety
Define the backward cone step of a wire set $S$ through a layer $l$ by adjoining the support of
every gate of $l$ that meets $S$. There is a choice here: test each gate against the **incoming**
set $S$, or against the **partially accumulated** cone. Testing against the accumulator
over-approximates, and the doubling bound fails. Testing against the incoming set gives the
bound — but is only *correct* when the gates within a layer act on pairwise disjoint wires.
Without that hypothesis (`LayerOk`) the semantic statement is false, and the counterexample is
small: on three wires, the single layer `[cnot 2 1, cnot 1 0]` has cone $\{0,1\}$ around wire
$0$, yet wire $0$ ends up holding $x_0 \oplus x_1 \oplus x_2$. So the cone under-approximates
the true dependence. This mission's development carries `LayerOk` throughout, and the
counterexample is recorded in the source.
## What is formalized
Layered circuits over $\{H, S, T, \mathrm{CNOT}\}$ on $n$ wires, with states as amplitude
functions on bit-strings and no tensor products anywhere. On top of that:
- the combinatorial half — one layer at most doubles the cone, hence $|\mathrm{cone}| \le 2^{d}\,|S|$;
- norm preservation, so that `acceptProb` is a genuine probability in $[0,1]$;
- the semantic half — inputs agreeing on the causal cone of the output wire are accepted with
*equal probability*.
The semantic half is proved in the Heisenberg picture. The measurement observable is conjugated
backwards through the circuit and its support tracked: a gate meeting the support enlarges it by
that gate's own wires, and a gate missing it **commutes** with the observable and cancels against
its own adjoint. That cancellation is the reason the non-cascading cone step is correct, and it is
why unitarity of the gate set is needed at the $2^n$-dimensional level rather than gate by gate.
Supporting this is a small reusable algebra of local operators: locality is monotone, closed under
adjoint and product, and disjointly supported operators commute.
## The frontier
The published depth bound assumes each input wire lies in the *syntactic* cone of the output. That
is weaker than saying the wire *matters*. Milestone 1 asks for the semantically honest version,
stated in terms of genuine functional dependence; the bridge is the semantic cone theorem already
in the development.
Beyond that, the natural continuations are the same argument for fan-in-$k$ gates
($|\mathrm{cone}| \le k^{d}$), for geometrically local circuits where cone growth is linear
rather than exponential, and ultimately the Bravyi–Gosset–König separation
$\mathrm{QNC}^{0} \not\subset \mathrm{NC}^{0}$ — which needs machinery (non-local games, magic
squares) that this development deliberately does not build.
Oracle-Parameterized Convergence Rates: SPIDER, Q-SPIDER, and the Exact CrossoverResearch Paper
## Motivation
Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.
This mission publishes a Lean 4 development in which **the oracle is a parameter, not an assumption**. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.
The published results it reproduces or corrects:
- **Ghadimi--Lan (2013)**, the $\varepsilon^{-4}$ rate for smooth nonconvex SGD.
- **Fang et al.**, the classical SPIDER variance-reduction schedule and its $\varepsilon^{-3}$ query complexity.
- **Sidford--Zhang**, *Quantum speedups for stochastic optimization* ([arXiv:2308.01582](https://arxiv.org/abs/2308.01582)) — Theorem 6's $\tilde O(\Delta\ell\sigma\sqrt{d}\,\varepsilon^{-3})$ and Theorem 8's $\tilde O(\ell\Delta\sqrt{d\sigma}\,\varepsilon^{-5/2})$, both obtained here from *one* schedule evaluated at two cost exponents.
## Setting
Let $E$ be a real inner-product space, $f:E\to\mathbb{R}$ an objective, and $g:E\to E$ a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality
$$f(y)\;\le\;f(x)+\langle g(x),y-x\rangle+\tfrac{L}{2}\|y-x\|^{2},$$
written $\mathrm{QuadUpper}\,f\,g\,L$; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write $\Delta_0=f(x_0)-f^{\star}$ for the initial gap, $\varepsilon$ for the target accuracy, $\sigma$ for the gradient-noise scale, $\ell$ for the mean-squared smoothness constant, and $d$ for the ambient dimension.
A **cost model** converts a target accuracy into a query count as a power law with exponent $p$. Its $p=2$ member is the classical minibatch bill, scaling as $\sigma^{2}/\varepsilon^{2}$; its $p=1$ member is the quantum mean-estimation bill, scaling as $\sigma/\varepsilon$. That single exponent is where classical and quantum part company.
## Target
The goal theorem is the exact crossover between the two SPIDER bills. Writing $Q$ and $C$ for the dominant terms of the quantum and classical query totals,
$$Q=\frac{64000\,\ell\Delta\sqrt{d}\sqrt{10\sigma}}{\varepsilon^{2}\sqrt{\varepsilon}},\qquad C=\frac{25\,728\,000\,\ell\Delta\sigma}{\varepsilon^{3}},$$
the target asserts, for $\ell,\Delta,\sigma,\varepsilon>0$ and $d\ge0$,
$$Q<C\quad\Longleftrightarrow\quad d\,\varepsilon<16000\,\sigma .$$
Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.
## Significance
*The results.* The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed $d$ the quantum advantage disappears as $\varepsilon\to0$, so the speedup lives at moderate accuracy, not asymptotically; and at fixed $\varepsilon$ the advantage requires $d<16000\sigma/\varepsilon$. Note what cancels — $\ell$, $\Delta$ and the $\varepsilon$-exponent all drop out, leaving only $d\varepsilon$ against $\sigma$.
*The formalization.* Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.
## Difficulty
The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on $f$, will produce the right-looking exponent from the wrong hypotheses.
Two specific places carry real content. Evaluating an error recursion at a **random return time** breaks the unconditional variance bound, because conditioning on $\tau=k$ destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to $\tilde O(\cdot)$ — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.
## Formalization scope
Smoothness is `QuadUpper` on an explicitly supplied `g`; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is $f^{\star}\le f(x_K)$ at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are $p=2$ and $p=1$ of one definition. Half-integer powers are written with `Real.sqrt`, so no real exponentiation appears in any statement. Stochastic results use a genuine `Filtration` and a conditional oracle contract; the tower property is derived, not assumed.
Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.
## Selected references
- S. Bubeck-style descent machinery aside, the rates reproduced here are: S. Ghadimi and G. Lan, *Stochastic first- and zeroth-order methods for nonconvex stochastic programming*, SIAM J. Optim. 23(4) (2013).
- C. Fang, C. J. Li, Z. Lin, T. Zhang, *SPIDER: Near-optimal non-convex optimization via stochastic path-integrated differential estimator*, NeurIPS 2018.
- A. Sidford and C. Zhang, *Quantum speedups for stochastic optimization*, [arXiv:2308.01582](https://arxiv.org/abs/2308.01582).
- Source development: `lean-optrates`, [github.com/shiy1022/lean-optrates](https://github.com/shiy1022/lean-optrates) at commit `4c0b8498`, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace `OptRates` to `ShiOptRates`; no statement or proof is otherwise altered.
Dynamic Programming and Optimal Control VI: Lookahead and RolloutTextbook
## Motivation
When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.
## Setting
Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (`BertsekasDPModel`), its policy cost recursion, and the open-loop cost of a fixed control sequence (`BertsekasDPOpenLoopCost`). For rollout (§6.4.1): a **graph search problem** — a finite digraph with destination set and terminal costs $g(i)$ on destinations (`BertsekasGraphSearch`); a **base heuristic** $\mathcal{H}$ producing from every node a path to a destination (`BertsekasBaseHeuristic`), with projection $p(i)$ and heuristic cost $H(i) = g(p(i))$; the **rollout algorithm** $R\mathcal{H}$ repeatedly moves to a neighbor $j$ minimizing $H(j)$ (`BertsekasIsRolloutRun`). $\mathcal{H}$ is *sequentially consistent* if its paths have the tail property (Def. 6.4.1), *sequentially improving* if $\min_{j \in N(i)} H(j) \le H(i)$ (Def. 6.4.2).
## Target
For sequentially improving $\mathcal{H}$ and any terminating rollout run $(i_1, \dots, i_{\bar m})$:
$$g(i_{\bar m}) \;\le\; H(i_1), \qquad g(i_{\bar m}) \;=\; \min\Big\{ H(i_1),\ \min_{j \in N(i_1)} H(j),\ \dots,\ \min_{j \in N(i_{\bar m - 1})} H(j) \Big\},$$
— `BertsekasDP.rollout_sequential_improvement` (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects $\delta_i$), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).
## Significance
Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.
## Difficulty
The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the `IsLeast` membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.
## Formalization scope
Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets $\bar U_k(x) \subseteq U_k(x)$ per Eq. (6.19); all statements at the level of the Mission I model.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (§6.2–6.4.) http://www.athenasc.com/dpbook.html
- G. Tesauro, G. R. Galperin, On-line policy improvement using Monte-Carlo search, *NIPS* 1996. https://papers.nips.cc/paper/1302
- D. P. Bertsekas, J. N. Tsitsiklis, C. Wu, Rollout algorithms for combinatorial optimization, *J. Heuristics* 3 (1997), 245–262. https://doi.org/10.1023/A:1009635226865
Rothvoß Discrepancy Notes I: Spencer's Theorem via the Entropy MethodTextbook
## Motivation
**Discrepancy theory** asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given $n$ sets over an $n$-element ground set, color each element $+1$ or $-1$ so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy $\Theta(\sqrt{n\log n})$, yet a coloring with discrepancy $O(\sqrt n)$ always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's **entropy method** ([MIT 18.095, "Discrepancy theory"](https://math.mit.edu/classes/18.095/lect6/notes.pdf)), the standard modern presentation of the technique (see also Matoušek, *Geometric Discrepancy*, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.
## Setting
Fix $n\ge 1$ and an $n\times n$ matrix $A$ with entries in $\{0,1\}$, thought of as the incidence matrix of $n$ sets $S_1,\dots,S_n$ over an $n$-element ground set: $A_{ij}=1$ iff element $j$ lies in set $S_i$. A **coloring** is a map $\varepsilon:\{1,\dots,n\}\to\{-1,+1\}$, and the **discrepancy of row $i$ under $\varepsilon$** is $\bigl|\sum_j A_{ij}\varepsilon_j\bigr|$, the signed imbalance of set $S_i$. The **discrepancy of the matrix** is the value achieved by the best coloring, minimizing the worst row.
The entropy method bounds this via the **partial coloring lemma**: rather than coloring all $n$ elements at once, one repeatedly colors a constant fraction of the *currently uncolored* elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into $O(1)$ "shells" of width $\Theta(\sqrt m)$ (where $m$ is the number of active elements); a short computation shows this quantization carries very little **Shannon entropy** $H(Z)=\sum_x \Pr[Z=x]\log_2\frac{1}{\Pr[Z=x]}$ once the shell width exceeds a threshold; subadditivity of entropy across the $n$ rows then bounds the *joint* quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.
## Formalization targets
**Goal.**
$$
\exists\, C\in\mathbb R,\ \forall n\ge 1,\ \forall A\in\{0,1\}^{n\times n},\ \exists\,\varepsilon\in\{-1,1\}^n,\ \forall i,\ \Bigl|\sum_{j=1}^n A_{ij}\varepsilon_j\Bigr|\le C\sqrt n.
$$
This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts $O(\sqrt n)$ discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp $6$, or beyond) refines this theorem rather than invalidating it.
## Significance
The removal of the $\sqrt{\log n}$ factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.
This mission's goal theorem, `spencer_discrepancy_sqrt_n_bound`, is **already proved** (zero `sorry`s), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is `shannonEntropy_shellFin_le` (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma `lemma8_partial_coloring_round`, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (`Komlos.spencer_six_deviations`) targets Spencer's *sharp* constant $6$ via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.
## Difficulty
The obvious argument is: fix a target bound $t=\lambda\sqrt n$, use a Chernoff/Hoeffding bound to show each row fails with probability at most $2e^{-\lambda^2/2}$, union-bound over the $n$ rows, and take a coloring outside the bad event. This works to prove a *single* good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of $n$ that a fixed $\lambda$ cannot always absorb once the active column count $m$ is close to $n$: for the *scaling family* where the row count and the active set shrink together, the naive union bound's failure probability grows *linearly* in $m$, not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the *joint* entropy of all $n$ rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.
## Formalization scope
Matrices are `Fin n → Fin n → ℝ` with an explicit `∀ i j, A i j = 0 ∨ A i j = 1` hypothesis; colorings are represented two ways in this development — `Fin m → Bool` internally (via the platform definition `RSign` converting to $\pm1$) during the entropy/Kleitman argument, and directly as `Fin n → ℝ` constrained to $\{-1,1\}$ pointwise in the goal theorem's statement, matching the usual $\{\pm1\}$-coloring convention. The row-sum shell quantization is the platform definitions `rowSumB`, `shellIdx`, `shellFin` (an integer-valued "round to nearest shell" construction, packaged into a fixed `Fin (2m+3)` type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking `Finset (Fin n)` of the *original* index type throughout, rather than moving between different `Fin m` types round to round, which keeps the induction free of type-level bookkeeping.
Reusable, already-Proved infrastructure this development builds on: `shannonEntropy_pi_le` (subadditivity across independent rows), `shannonEntropy_pigeonhole`, `choose_sum_le_exp_mul_binEntropy`, and `kleitman_diameter`, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is `shannonEntropy_shellFin_le` (Lemma 9): a self-contained Shannon-entropy computation about the `shellFin` quantization that does not depend on anything else in this mission and can be attempted independently.
## Selected references
- J. Spencer, *Six standard deviations suffice*, Trans. Amer. Math. Soc. 289 (1985), 679–706. [DOI](https://doi.org/10.1090/S0002-9947-1985-0784009-0)
- T. Rothvoß, *Discrepancy theory, or: how much balance is possible?*, MIT 18.095 lecture notes. [PDF](https://math.mit.edu/classes/18.095/lect6/notes.pdf)
- J. Matoušek, *Geometric Discrepancy: An Illustrated Guide*, Algorithms and Combinatorics 18, Springer, 1999.
- J. Beck, T. Fiala, *"Integer-making" theorems*, Discrete Appl. Math. 3(1) (1981), 1–8.
Higher-Dimensional Quantum Hypergraph-Product Codes with Finite RatesResearch Paper
## Motivation
Quantum low-density parity-check codes encode quantum information using sparse
parity constraints. A standard way to construct them is to translate binary
chain complexes into Calderbank--Shor--Steane codes and to combine complexes by
tensor product. Homology identifies the logical operators of the resulting
code, while the smallest Hamming weight of a nontrivial homology class controls
one of its distances. Determining how this distance behaves under a tensor
product is therefore a basic structural question, not merely a parameter
calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an
arbitrary finite binary chain complex and the other is the one-complex induced
by a binary matrix. Their paper was published as [“Higher-Dimensional Quantum
Hypergraph-Product Codes with Finite Rates,” *Physical Review Letters* 122,
230501 (2019)](https://doi.org/10.1103/PhysRevLett.122.230501). Its main
distance result is Eq. (13) in the [arXiv version](https://arxiv.org/abs/1810.01519):
for this particular tensor factor, the usual product upper bound is always
exact. The result extends the familiar two-complex setting of quantum
hypergraph-product codes to the local structure occurring in complexes of any
dimension.
## Setting
A **based binary chain complex** consists of finite-dimensional vector spaces
$A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and
linear boundary maps
$$
\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i
\xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots
$$
such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is
$H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The
**homological distance** is measured in the chosen basis:
$$
d_i(\mathcal A)=
\min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus
\operatorname{im}\partial_{i+1}\}.
$$
Following the paper, the minimum of an empty set is $\infty$. Thus
$d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For
an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and
$\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently
$$
d_0(\mathcal A)=\min\{\operatorname{wt}(x):
x\in A_0\setminus\operatorname{im}\partial_1\}
$$
and
$$
d_m(\mathcal A)=\min\{\operatorname{wt}(x):
0\ne x\in\ker\partial_m\}.
$$
For an $r\times c$ binary matrix $P$, the **one-complex**
$\mathcal K(P)$ has $\mathbb F_2^c$ in degree one,
$\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are
$$
d_1(\mathcal K(P))=
\min\{\operatorname{wt}(x):Px=0,\ x\ne0\}
$$
and
$$
d_0(\mathcal K(P))=
\min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.
$$
In particular, $d_0=1$ unless $P$ has full row rank, in which case
$d_0=\infty$. The degree-$j$ chain group of
$\mathcal A\times\mathcal K(P)$ is
$$
(A_j\otimes\mathbb F_2^r)\oplus
(A_{j-1}\otimes\mathbb F_2^c),
$$
with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign
in that boundary has no effect.
## Formalization targets
### Tensor-product upper bound for arbitrary complexes
The first milestone is Eq. (11) for two arbitrary finite-length based binary
chain complexes:
$$
d_j(\mathcal A\times\mathcal B)\le
\min_i d_i(\mathcal A)d_{j-i}(\mathcal B).
$$
### Rank-sensitive lower bound
Let $u=\operatorname{rank}P$ and
$\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including
both of its cases:
$$
u<r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
\min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),
$$
and
$$
u=r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
d_{j-1}(\mathcal A)\delta.
$$
### Exact distance with a one-complex
The goal is Eq. (13):
$$
d_j(\mathcal A\times\mathcal K(P))=
\min\!\left(
d_{j-1}(\mathcal A)d_1(\mathcal K(P)),
d_j(\mathcal A)d_0(\mathcal K(P))
\right).
$$
No full-rank hypothesis is imposed on $P$.
## Significance
The equality determines the product distance exactly from four component
distances. General tensor-product arguments immediately provide the upper
bound, but an exact formula requires ruling out lower-weight homology classes
that mix the two direct-sum blocks. Once established, the formula can be
applied repeatedly to tensor products of one-complexes, which is the step used
in the paper to obtain higher-dimensional quantum hypergraph-product code
families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite
based binary chain data, homological distance valued in
$\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant
tensor-product boundary maps. Mathlib contains Hamming weight and general
homological-algebra infrastructure, while QECLean contains a closely related
based length-three homological-code interface. Neither the selected Mathlib
environment nor the inspected QECLean development currently supplies this
rank-sensitive exact distance theorem.
## Difficulty
The central issue is that Hamming weight depends on the chosen bases and is not
preserved by arbitrary homological isomorphisms. A Künneth isomorphism
describes the product homology and readily produces low-weight representatives,
which is enough for the upper bound, but it does not by itself exclude a still
lighter representative obtained by cancellation between the two tensor
blocks. The lower bound must also remain valid at the endpoints of the complex
and in singular cases where one or more homology groups vanish and the relevant
distance is $\infty$.
The theorem cannot be reduced to a dimension calculation. It must reason
about supports and Hamming weights of based representatives while respecting
the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$
and $\operatorname{rank}P=r$.
## Formalization scope
The Lean development works over `ZMod 2`. A finite basis in degree $i$ is
represented by `Fin (dimension i)`, and a chain group is the function space
from that coordinate type to `ZMod 2`. `BasedBinaryChainComplex` stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and
$\mathcal B$, rather than over a local window or a one-complex specialization.
If the stored length is $m$, the zero-dimensional source in degree $m+1$
makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the
zero-dimensional target below degree zero makes
$\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use `WithTop ℕ`. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with `⊤` produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix $P$ is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree-$j$ product group is indexed by the disjoint union of all coordinate
products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm
is the sum of the weights of all tensor-degree blocks. The product boundary is
the standard signed tensor boundary; its sign disappears over $\mathbb F_2$.
A formal proof verifies that every pair of consecutive product boundaries
composes to zero; the cancellation of the two mixed terms uses characteristic
two. Thus the product distance is taken from an actual chain complex, rather
than from unrelated adjacent linear maps.
A basis-free tensor product or an abstract homology group alone is insufficient
for the target, because either would discard the weight data on which the
statement depends.
The mission does not formalize the asymptotic code-family construction later
in the paper, the transposed cohomological distance, or the CSS-code parameter
translation. Those are natural downstream missions; they should reuse rather
than alter the present based-chain definitions.
## Selected references
- Weilei Zeng and Leonid P. Pryadko, [“Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,”](https://doi.org/10.1103/PhysRevLett.122.230501) *Physical Review Letters* 122, 230501 (2019). [arXiv:1810.01519](https://arxiv.org/abs/1810.01519).
- Benjamin Audoux and Alain Couvreur, [“On Tensor Products of CSS Codes,”](https://arxiv.org/abs/1512.07081) arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
- Jean-Pierre Tillich and Gilles Zémor, [“Quantum LDPC Codes With Positive Rate and Minimum Distance Proportional to the Square Root of the Blocklength,”](https://doi.org/10.1109/TIT.2013.2292061) *IEEE Transactions on Information Theory* 60 (2014), 1193--1202.
Irrationality and transcendence of Euler's constantOpen Problem
## What the constant is
Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm:
$$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$
It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
## What is being asked
For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, **neither is known**. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.
The goal theorem of this mission is transcendence,
$$\gamma \notin \overline{\mathbb{Q}},$$
with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.
## What is actually known
Progress has come in three forms, and the milestones below formalize each.
**Conditional bounds on a putative denominator.** If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go.
**Disjunctive results.** The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant
$$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$
Aptekarev, building on work of Mahler and Shidlovskii, observed that **at least one of $\gamma$ and $\delta$ is irrational**. Rivoal later strengthened this to **at least one of them is transcendental**. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.
**Irrationality criteria.** Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
## Timeline
- **1734** — Euler introduces the constant and computes it to six decimals.
- **1790s–1800s** — Mascheroni computes further digits; the constant acquires its second name.
- **1873** — Hermite proves $e$ transcendental; **1882** — Lindemann does the same for $\pi$. The methods do not reach $\gamma$.
- **1980** — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$.
- **1997** — Papanikolaou: the same denominator exceeds $10^{244663}$.
- **2009** — Aptekarev: at least one of $\gamma$, $\delta$ is irrational.
- **2012** — Rivoal: at least one of $\gamma$, $\delta$ is transcendental.
- **2010s** — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched.
## Formalization notes
Mathlib provides the constant as `Real.eulerMascheroniConstant`, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. `Irrational` and `Transcendental ℚ` are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.
Equational Magmas: E677 → E255 (finite case)Open Problem
## Motivation
An equation for a **magma** constrains a binary operation without assuming that it is associative, commutative, or has an identity. Determining which equations force other equations separates the consequences of a single law from familiar properties that require additional assumptions. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.
The Equational Theories Project studies these implications systematically. Its [December 2025 paper](https://arxiv.org/html/2512.07087v2) reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.
This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.
## Setting
A magma here is a type $A$ with a total binary operation $\diamond:A\times A\to A$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition **E677** means
$$\forall x,y\in A,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$
The condition **E255** means
$$\forall x\in A,\quad x=((x\diamond x)\diamond x)\diamond x.$$
These are the two laws used in [Chapter 13 of the project blueprint](https://teorth.github.io/equational_theories/blueprint/677-chapter.html). For a fixed element $y$, the **left multiplication map** is $L_y(x)=y\diamond x$. A **fixer** for $x$ is an element $y$ satisfying $y\diamond x=x$. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element.
## Formalization targets
The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $A$ satisfying E677, the first supporting statement is
$$\forall y\in A,\quad L_y\text{ is bijective}.$$
The second supporting statement specifies any fixer:
$$\forall x,y\in A,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$
The third supporting statement is the backward recurrence
$$\forall x,y\in A,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$
These supporting statements come from ETP blueprint Lemma 13.1(i)–(iii); local direct proof files accompany their statements. The following universal fixer-existence assertion is retained as an explicit equivalent reformulation:
$$\forall x\in A,\quad\exists y\in A,\quad y\diamond x=x.$$
The mission goal is
$$\forall\text{ finite magmas }A,\quad \operatorname{E677}(A)\ \Longrightarrow\ \operatorname{E255}(A).$$
For finite E677 magmas, fixer existence is equivalent to E255: E255 supplies the fixer $(x\diamond x)\diamond x$, and Lemma 13.1(ii) converts any fixer into E255. Thus it is not presented as a strictly weaker milestone.
The active open milestone is an orbit-local producer statement. For a fixed $x$, if two elements in the forward orbit $x,L_x(x),L_x^2(x),\ldots$ have equal right products by $x$, they must be equal unless $x$ has a fixer. This isolates a genuine structural step without asserting a fixer for every element. None of the displayed statements restricts the cardinality to a tested range.
## Significance
A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.
The formal package provides small, reusable statements of the two laws, the left multiplication property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.
## Difficulty
The left multiplication conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$, with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left multiplication map alone does not state that a fixer exists.
Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.
## Formalization scope
The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a `Fintype` instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.
Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$. Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.
## Selected references
- Matthew Bolan et al., *The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale*, arXiv:2512.07087v2 (December 16, 2025), [paper](https://arxiv.org/html/2512.07087v2).
- The Equational Theories Project contributors, *Equational Theories*, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.2, [chapter](https://teorth.github.io/equational_theories/blueprint/677-chapter.html), accessed September 7, 2026.
## Motivation
This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.
## Setting and goal
For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.
## Relationship to the five-primes mission
The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as [Every Odd Number Greater Than 1 is the Sum of at Most Five Primes](https://prove2.me/missions/Every%20Odd%20Number%20Greater%20Than%201%20is%20the%20Sum%20of%20at%20Most%20Five%20Primes). The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.
## Formalization scope
The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.
## Proof approach
A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.
## Reference
H. A. Helfgott, [The ternary Goldbach conjecture is true](https://arxiv.org/abs/1312.7748), 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.
The Theory of Error-Correcting Codes I: The MacWilliams IdentityTextbook
## Motivation
Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.
The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's [*The Theory of Error-Correcting Codes*](https://books.google.com/books?id=nv6WCJgcjxcC). The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.
This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.
## Setting
Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a **word** be a function $c:\iota\to F$. A **linear code** $C$ is an $F$-linear subspace of the word space. The standard bilinear form is
$$
\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,
$$
and the **dual code** is
$$
C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.
$$
The **Hamming weight** $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial
$$
W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.
$$
Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in `MvPolynomial (Fin 2) ℤ`; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.
## Formalization targets
### Character orthogonality over a code
For a primitive complex additive character $\psi$ of $F$, define
$$
S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).
$$
The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.
### Coordinatewise Hamming transform
For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:
$$
\sum_{v\in F^\iota}
X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)}
\psi(\langle c,v\rangle)
=
\bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)}
(X-Y)^{\operatorname{wt}(c)}.
$$
This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.
### MacWilliams identity
The capstone is the following equality of integer polynomials:
$$
|C|\,W_{C^\perp}(X,Y)
=
W_C\bigl(X+(q-1)Y,\,X-Y\bigr).
$$
This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula
$$
W_{C^\perp}(X,Y)
=
\frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).
$$
## Significance
The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.
The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.
## Difficulty
The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.
The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.
## Formalization scope
The coordinate type is an arbitrary finite type rather than only `Fin n`; its cardinality plays the role of the code length. A word is `CodingTheory.Word F ι := ι → F`, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.
The polynomial `CodingTheory.hammingWeightEnumeratorPolynomial` has coefficients in $\mathbb Z$ and variables indexed by `Fin 2`. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.
The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.
## Selected references
- F. J. MacWilliams and N. J. A. Sloane, [*The Theory of Error-Correcting Codes*](https://books.google.com/books?id=nv6WCJgcjxcC), North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). [Publisher chapter record](https://doi.org/10.1016/S0924-6509(08)70530-0).
- Violetta Weger, [*Coding Theory*](https://home.cit.tum.de/~wvi/CT.pdf), Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
- F. J. MacWilliams, [“A Theorem on the Distribution of Weights in a Systematic Code”](https://doi.org/10.1002/j.1538-7305.1963.tb04003.x), *Bell System Technical Journal* 42 (1963), 79--94.
The Monotonicity Theorem in O-Minimal Geometry 1: Monotonicity TheoremTextbook
## Motivation
An **o-minimal structure** is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the **Monotonicity Theorem**: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces.
The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, *Tame Topology and O-minimal Structures*, Chapter 3 ([Cambridge University Press, 1998](https://doi.org/10.1017/CBO9780511529219)). A concise expository account is given in Mário Edmundo, *O-minimal structures* ([arXiv:math/0012051](https://arxiv.org/abs/math/0012051)). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry.
## Setting
Let $R$ be a type equipped with a **dense linear order without endpoints** $D$: an irreflexive, transitive, trichotomous relation $D.\mathrm{lt}$ in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples $\mathrm{Power}\,R\,n := \mathrm{Fin}\,n \to R$, with coordinate projections, deletion, and append operations defined explicitly.
An **o-minimal structure** $M$ over $D$ is a family $M.S\,n$ of collections of subsets of $\mathrm{Power}\,R\,n$, closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of $M.S\,1$ is a finite union of points and open intervals. A **definable function** $f$ with domain $I$ and codomain $B$ is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of $M$.
For $a < b$ in $\mathrm{Power}\,R\,1$, the **open interval** $(a,b)$ is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing $-\infty$ and $+\infty$. A function is **strictly increasing** (respectively **strictly decreasing**) on $I$ when $x < y$ implies $f(x) < f(y)$ (respectively $f(y) < f(x)$) in the first output coordinate. **Continuity** at a domain point is the graph-based epsilon-delta predicate: $x$ belongs to $\mathrm{ContinuousPoints}\,D\,I\,G$ exactly when the graph $G$ meets every sufficiently small box around $(x, f(x))$ in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings.
## Formalization targets
### Goal — Monotonicity theorem
$$f : I \to B\ \text{definable},\ I\ \text{infinite} \implies \exists\, a = p_0 < p_1 < \cdots < p_k = b\ \text{with each}\ (p_i, p_{i+1})\ \text{good}.$$
An open cell $(p_i, p_{i+1})$ is **good** when $f$ restricted to $I \cap (p_i,p_{i+1})$ is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number $k$ of cut points is finite and depends on $f$, $a$, and $b$; no bound on $k$ is asserted.
### Supporting targets
$$I\ \text{definable and infinite} \implies I\ \text{contains a nonempty open interval}.$$
$$f\ \text{definable} \implies \text{each value fiber}\ f^{-1}(z)\ \text{is definable}.$$
$$\text{Either some value fiber is infinite or every value fiber is finite}.$$
$$f\ \text{definable on infinite}\ I \implies f\ \text{is constant or injective on some subinterval}.$$
$$f\ \text{injective and definable} \implies f\ \text{is strictly monotone on some subinterval}.$$
$$f\ \text{strictly monotone and definable} \implies f\ \text{is continuous on some subinterval}.$$
## Significance
*The result itself.* The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished.
*Formalizing it.* The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets.
## Difficulty
The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber $f^{-1}(z)$ is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it.
## Formalization scope
Lean represents one-dimensional points as functions $\mathrm{Fin}\,1 \to R$, with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate $M.S\,n$, never an informal attribute. Continuity is the graph-based $\mathrm{ContinuousPoints}$ predicate applied to $\mathrm{FunctionGraph}\,f.\mathrm{toFun}$; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points $p : \mathrm{Fin}\,(k+1) \to \mathrm{Power}\,R\,1$ with $p_0 = a$, $p_{\mathrm{last}} = b$, and strict increase at each step; the intervening sets $J$ are the open intervals determined by consecutive finite endpoints.
Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions.
## Selected references
- Lou van den Dries, *Tame Topology and O-minimal Structures*, London Mathematical Society Lecture Note Series 248, Cambridge University Press, 1998, Chapter 3. [DOI](https://doi.org/10.1017/CBO9780511529219).
- Mário J. Edmundo, *O-minimal structures*, 2000. [arXiv:math/0012051](https://arxiv.org/abs/math/0012051).
- P. T. Johnstone, notes on o-minimality and the monotonicity theorem (`monotonicity.tex`), Lemmas 1–3 and the Monotonicity Theorem, as cited in the theorem sources.
## Motivation
A number field $\mathbb{K}$ has a unit group $E = \mathcal{O}(\mathbb{K})^\times$ which, by Dirichlet's unit theorem, is free of $\mathbb{Z}$-rank $r_1 + r_2 - 1$ modulo roots of unity. Fix a prime $p$ and embed the units diagonally into the units of the completions of $\mathbb{K}$ at the primes above $p$. The topological closure of the image is a finite free a $\mathbb{Z}_p$-module modulo roots of unity, and its $\mathbb{Z}_p$-rank can in principle be smaller than $r_1 + r_2 - 1$: units that are independent over $\mathbb{Z}$ may become dependent $p$-adically. **Leopoldt's conjecture** asserts that this never happens.
The conjecture controls how many independent $\mathbb{Z}_p$-extensions a number field has. Iwasawa showed that if $\Omega(\mathbb{K})$ is the maximal $p$-abelian $p$-ramified extension of $\mathbb{K}$, then $\mathrm{Gal}(\Omega(\mathbb{K})/\mathbb{K}) \cong \mathbb{Z}_p^{\,r_2 + 1 + \mathcal{D}_L(\mathbb{K})}$, where $\mathcal{D}_L(\mathbb{K})$ is the defect defined below. So a positive defect means extra $\mathbb{Z}_p$-extensions beyond the ones accounted for by the archimedean places, and for a totally real field it means a non-cyclotomic $\mathbb{Z}_p$-extension exists. Non-vanishing of the $p$-adic regulator is also what makes $p$-adic $L$-functions and $p$-adic class number formulas behave as their complex analogues do.
Timeline of what is actually proved, under which hypotheses:
- **1962** — Leopoldt conjectures non-vanishing of the $p$-adic regulator for abelian fields (H. Leopoldt, *Zur Arithmetik in Abelschen Zahlkörpern*, J. reine angew. Math. 209).
- **1965–1967** — Ax reduces the abelian case to a $p$-adic analogue of Baker's theorem on linear forms in logarithms; Baker proves the archimedean version; Brumer adapts it $p$-adically and proves the conjecture **for abelian extensions of $\mathbb{Q}$** (A. Brumer, *On the units of algebraic number fields*, Mathematika 14, 1967).
- **1976** — Greenberg relates the conjecture to a case of his own conjecture: Leopoldt for totally real fields implies the $T$-part of the relevant Iwasawa module is finite.
- **1981** — Waldschmidt proves the general bound $\mathcal{D}_L(\mathbb{K}) \le r/2$, where $r$ is the $\mathbb{Z}$-rank of the units: at least half of the expected $p$-adic rank is always attained.
- **1984, 1987–2007** — Emsalem–Kisilevsky–Wales settle some small non-abelian Galois groups by representation theory plus Baker theory; Jaulent handles fields of small discriminant.
- **2011–2016** — Mihăilescu posts a claimed proof for **all CM fields at odd $p$** (arXiv:1105.4544). It is currently an unpublished preprint, and its proof invokes a separate preprint asserting the vanishing of Iwasawa's $\mu$-invariant for cyclotomic $\mathbb{Z}_p$-extensions of CM fields, with an appendix that is said to avoid that assumption.
Beyond the abelian case the conjecture is open. This mission takes the CM claim as its target.
## Setting
Let $p$ be a prime and $\mathbb{K}$ a number field with ring of integers $\mathcal{O}(\mathbb{K})$ and units $E = \mathcal{O}(\mathbb{K})^\times$.
Let $P = \{\wp \subset \mathcal{O}(\mathbb{K}) : (p) \subset \wp\}$ be the set of primes above $p$, a finite set. For $\wp \in P$ write $\mathbb{K}_\wp$ for the completion and $\mathcal{O}_\wp$ for its valuation ring. Set
$$U \;=\; \prod_{\wp \in P} \mathcal{O}_\wp^{\times},$$
the group of **semilocal units** at $p$, and let
$$\iota : E \longrightarrow U$$
be the diagonal embedding, whose $\wp$-component is the completion map. Define the **$p$-adic closure of the global units**
$$\bar{E} \;=\; \bigcap_{n > 0} \iota(E) \cdot U^{p^n} \;\subseteq\; U ,$$
where $U^{p^n} = \{u^{p^n} : u \in U\}$ and the product of the two subgroups is taken inside the abelian group $U$. Finally, the **Leopoldt defect** of $\mathbb{K}$ at $p$ is
$$\mathcal{D}_L(\mathbb{K}) \;=\; \mathbb{Z}\text{-rk}(E) \;-\; \mathbb{Z}_p\text{-rk}(\bar{E}),$$
the difference between Dirichlet's unit rank $r_1 + r_2 - 1$ and the free $\mathbb{Z}_p$-rank of $\bar{E}$. The defect is always non-negative, and it is positive exactly when units that are independent over $\mathbb{Z}$ satisfy a $p$-adic relation after the diagonal embedding.
A number field $\mathbb{K}$ is **CM** when it is a totally complex quadratic extension of its maximal real subfield $\mathbb{K}^+$. For CM fields a positive defect is equivalent to the vanishing of the $p$-adic regulator of $\mathbb{K}$.
## Formalization targets
### Goal — Leopoldt's conjecture for CM fields at odd $p$
$$p \text{ odd prime}, \quad \mathbb{K}/\mathbb{Q} \text{ CM} \quad \Longrightarrow \quad \mathcal{D}_L(\mathbb{K}) = 0 .$$
This is Theorem 1 of arXiv:1105.4544. It fixes no constants and no auxiliary choices, so it is stable under any later improvement of the argument.
### Supporting targets
$$\mathcal{D}_L(\mathbb{K}) = 0 \quad \text{for } \mathbb{K}/\mathbb{Q} \text{ abelian} \qquad \text{(Brumer, 1967)}$$
$$\mathcal{D}_L(\mathbb{K}) \le r/2, \quad r = \mathbb{Z}\text{-rk}(E) \qquad \text{(Waldschmidt, 1981)}$$
$$\mathcal{D}_L(\mathbb{F}) > 0 \quad \Longrightarrow \quad \mathcal{D}_L(\mathbb{K}) > 0 \quad \text{for every finite } \mathbb{K}/\mathbb{F}$$
The last is Remark 1.A of the source, attributed there to Laurent: a defect is inherited by finite extensions, because the $p$-adic relations among $\mathbb{Z}$-generators of the units are preserved under the embedding of unit groups.
## Significance
*The result itself.* Leopoldt's conjecture for CM fields would pin down $\mathrm{Gal}(\Omega(\mathbb{K})/\mathbb{K}) \cong \mathbb{Z}_p^{\,r_2+1}$ for every CM field and, via the totally real subfield, would rule out non-cyclotomic $\mathbb{Z}_p$-extensions of the totally real fields underlying them. It would remove a standing hypothesis from results in Iwasawa theory and $p$-adic $L$-functions that are currently stated conditionally on Leopoldt. Without it, the $\mathbb{Z}_p$-rank of the $p$-ramified Galois group is only known to lie in a range.
*Formalizing it.* Nothing in this area is formalized today. Mathlib has Dirichlet's unit theorem, the archimedean regulator, CM fields, and the completions of a number field at its finite places, but no $p$-adic regulator, no $p$-adic logarithm, and no Iwasawa theory. This mission first pins down a machine-checked statement of the conjecture itself — which is where the mathematical content of Theorem 1 sits, since the theorem is one sentence long — and then attacks it. Because the target is an unrefereed argument, a serious attempt to formalize it is also a test of it: a step that cannot be closed localizes a gap, and a milestone that turns out to be unprovable is itself the finding.
## Difficulty
The obvious approach is transcendence theory, and it is the one that works in the abelian case: a $p$-adic relation among units is a vanishing linear form in $p$-adic logarithms of algebraic numbers, and Baker-type lower bounds forbid it. This is exactly Ax's reduction and Brumer's theorem. It stalls immediately beyond abelian fields, because the argument needs units whose Galois structure is explicit — for abelian fields the cyclotomic units supply them, and in general nothing does. Waldschmidt's $\mathcal{D}_L \le r/2$ is the limit of what the transcendence route has delivered in general, and it has not been improved by that route. The source therefore abandons transcendence entirely and argues in Iwasawa theory, constructing a CM $\mathbb{Z}_p$-extension of a field where the conjecture is assumed to fail and deriving a contradiction from the classes of primes that split completely in it. That route needs the structure theory of $\Lambda$-modules, $\mu$- and $\lambda$-invariants, Tate cohomology of class group limits, and the vanishing of $\mu$ — none of which exists in Lean.
## Formalization scope
The development commits to the following conventions, all of them visible in the definition file.
$P$ is the subtype of height-one primes $\wp$ of $\mathcal{O}(\mathbb{K})$ with $p \in \wp$, and carries a `Finite` instance. $U$ is the dependent product over $P$ of the unit groups of the valuation rings `adicCompletionIntegers`, so it is a commutative topological group. $\bar{E}$ is defined by the intersection displayed above rather than as a topological closure: the source gives both descriptions, and the intersection is the one that needs no choice of topology on $\prod_\wp \mathbb{K}_\wp$. The two can differ by a finite subgroup, which does not affect the $\mathbb{Z}_p$-rank.
$\mathbb{Z}_p\text{-rk}(\bar{E})$ is defined as the largest $n \le [\mathbb{K}:\mathbb{Q}]$ for which $\mathbb{Z}_p^n$ admits a **continuous** injective homomorphism into $\bar{E}$. Continuity is not decoration: as abstract groups $\mathbb{Z}_p^n$ embeds into $\mathbb{Z}_p$ for every $n$, so the topological requirement is what makes the rank the intended one; and since $\mathbb{Z}_p^n$ is compact and $U$ is Hausdorff, such an injection is automatically a closed embedding. For a closed subgroup of $U$, which is isomorphic to a finite group times $\mathbb{Z}_p^d$, such injections exist exactly for $n \le d$. The cut-off at $[\mathbb{K}:\mathbb{Q}]$ is carried only so that the supremum ranges over a visibly bounded set of naturals rather than falling back on a junk value; since the $\mathbb{Z}_p$-rank of the whole semilocal unit group $U$ is already $[\mathbb{K}:\mathbb{Q}]$, it never binds.
The defect subtracts in $\mathbb{N}$, hence truncates. Since the $\mathbb{Z}_p$-rank never exceeds the $\mathbb{Z}$-rank, truncation is never triggered and $\mathcal{D}_L(\mathbb{K}) = 0$ is equivalent to the two ranks being equal.
One trivializing formalization is worth ruling out. The goal is not vacuous: it is neither provable nor refutable by unfolding the definitions, and it has genuine content whenever $\mathbb{Z}\text{-rk}(E) > 0$, that is for every CM field other than the imaginary quadratic ones, where Dirichlet's rank is $0$ and the statement is trivially true.
A complete development needs, beyond what Mathlib supplies: the $p$-adic logarithm on the units of a local field and the resulting $p$-adic regulator; the Iwasawa algebra acting on inverse limits of $p$-class groups along a $\mathbb{Z}_p$-extension, with $\mu$- and $\lambda$-invariants and the decomposition of Definition 1 of the source; CM $\mathbb{Z}_p$-extensions; and Tate cohomology of these modules. All of that is reusable well beyond this mission — it is the missing foundation of Iwasawa theory in Lean. Contributions of any of these pieces as definitions, and of the three supporting targets as theorems, are welcome independently of the goal.
## Selected references
- P. Mihăilescu, *On CM $\mathbb{Z}_p$-extensions and the Leopoldt conjecture for CM fields*, arXiv:1105.4544 (2011–2016). https://arxiv.org/abs/1105.4544
- H. Leopoldt, *Zur Arithmetik in Abelschen Zahlkörpern*, J. reine angew. Math. 209 (1962), 54–71. https://doi.org/10.1515/crll.1962.209.54
- A. Brumer, *On the units of algebraic number fields*, Mathematika 14 (1967), 121–124. https://doi.org/10.1112/S0025579300003703
- J. Ax, *On the units of an algebraic number field*, Illinois J. Math. 9 (1965), 584–589. https://doi.org/10.1215/ijm/1256059299
- A. Baker, *Linear forms in the logarithms of algebraic numbers I, II, III*, Mathematika 13–14 (1966–67).
- M. Waldschmidt, *Transcendance et exponentielles en plusieurs variables*, Invent. Math. 63 (1981), 97–127. https://doi.org/10.1007/BF01389194
- M. Emsalem, H. Kisilevsky, D. Wales, *Indépendance linéaire sur $\overline{\mathbb{Q}}$ de logarithmes $p$-adiques de nombres algébriques et rang $p$-adique du groupe des unités d'un corps de nombres*, J. Number Theory 19 (1984), 384–391. https://doi.org/10.1016/0022-314X(84)90040-1
- R. Greenberg, *On the Iwasawa invariants of totally real fields*, Amer. J. Math. 98 (1976), 263–284. https://doi.org/10.2307/2373625
- K. Iwasawa, *On $\mathbb{Z}_\ell$-extensions of number fields*, Ann. of Math. 98 (1973), 246–326. https://doi.org/10.2307/1970784
- M. Laurent, *Rang $p$-adique d'unités et action de groupes*, J. reine angew. Math. 399 (1989), 81–108. https://doi.org/10.1515/crll.1989.399.81
Eilenberg Theorems for Many-Sorted FormationsResearch Paper
## Motivation
Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by **many-sorted algebras**, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of [Climent Vidal and Cosme Llópez, *Eilenberg theorems for many-sorted formations*](https://arxiv.org/abs/1604.04792), published in the *Houston Journal of Mathematics* 45(2), 2019.
The companion manuscript *A Kleene theorem for free many-sorted algebras* develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.
## Setting
Fix a finite type of sorts $S$ and an $S$-sorted signature $\Sigma$. For an $S$-sorted set $X$, write $T_\Sigma(X)$ for the free $\Sigma$-algebra on $X$. A **congruence** $\Phi$ on a many-sorted algebra is a family of equivalence relations $\Phi_s$, one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family
$$
(T_\Sigma(X)_s/\Phi_s)_{s\in S}
$$
is finite. A sorted language $L$ is **$\Phi$-saturated** when membership in $L_s$ is constant on every $\Phi_s$-class. The **syntactic congruence** $\Omega(L)$ is the greatest algebra congruence that saturates $L$, and $L$ is regular when $\Omega(L)$ has finite index.
A **finite-index congruence formation** $\mathfrak F$ selects, for every variable family $X$, a nonempty filter $\mathfrak F(X)$ of finite-index congruences on $T_\Sigma(X)$. The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.
A **regular-language formation** $\mathcal L$ selects regular languages in each $T_\Sigma(X)$. It contains every language saturated by the universal congruence; whenever $L,K\in\mathcal L(X)$ it contains every language saturated by $\Omega(L)\cap\Omega(K)$; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.
The two constructions are
$$
\mathcal L_{\mathfrak F}(X)
=\{L\mid \text{$L$ is saturated by some }\Phi\in\mathfrak F(X)\},
$$
and
$$
\mathfrak F_{\mathcal L}(X)
=\{\Phi\mid \text{$\Phi$ has finite index and every $\Phi$-saturated language lies in $\mathcal L(X)$}\}.
$$
## Formalization targets
The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.
$$
\operatorname{Form}_{\mathrm{Cgr}_{\mathrm{fi}}}(\Sigma)
\cong
\operatorname{Form}_{\mathrm{Lang}_{r}}(\Sigma).
$$
The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities
$$
\mathfrak F_{\mathcal L_{\mathfrak F}}=\mathfrak F,
\qquad
\mathcal L_{\mathfrak F_{\mathcal L}}=\mathcal L.
$$
These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.
## Significance
The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.
Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.
## Difficulty
The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.
The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.
## Formalization scope
The Lean development uses the existing `MSKleene` representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.
Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.
The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.
## Selected references
- Juan Climent Vidal and Enric Cosme Llópez, *Eilenberg theorems for many-sorted formations*, Houston Journal of Mathematics 45(2), 2019, pp. 351–416. [arXiv:1604.04792](https://arxiv.org/abs/1604.04792)
- Samuel Eilenberg, *Automata, Languages, and Machines, Volume B*, Academic Press, 1976.
- Adolfo Ballester-Bolinches, Jean-Éric Pin, and Xaro Soler-Escrivà, *Formations of finite monoids and formal languages: Eilenberg's variety theorem revisited*, Forum Mathematicum 26, 2014, pp. 1737–1761.
The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is $[c_F,\infty)$, where
$$
c_F=\frac{2221564096+283748\sqrt{462}}{491993569}
=4.527829566160879\ldots.
$$
The formalization must establish membership of every real number at least $c_F$, including the endpoint, and show that no half-line starting below $c_F$ is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
### Source material
- [Proof report (PDF)](https://drive.google.com/file/d/13jj7vJy-OtTsJIe_vp4Qd1PaUIeoLt8f/view?usp=sharing) — the complete argument, exact certificate appendices and corrected English translation of Freiman's Russian text. [Download PDF](https://drive.google.com/uc?export=download&id=13jj7vJy-OtTsJIe_vp4Qd1PaUIeoLt8f).
- [Verification package (ZIP)](https://drive.google.com/file/d/18AWfMKCJ0XPfRs2k6c_hf0ovbljaPL2u/view?usp=sharing) — the report, its LaTeX sources, the Russian source, certificate data, verification programs and reproduction instructions. [Download ZIP](https://drive.google.com/uc?export=download&id=18AWfMKCJ0XPfRs2k6c_hf0ovbljaPL2u).
Start with `README.md` and `PROOF_GUIDE.md` in the package. The files `formalization/MISSION.md` and `formalization/MILESTONES.md` describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
Gross–Yellen Graph Theory I: Cayley's Tree FormulaTextbook
## Motivation
Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration
problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of
saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the
same number reappears throughout combinatorics as the number of spanning trees of the
complete graph $K_n$, a special case of Kirchhoff's Matrix–Tree Theorem, and as the base
case against which more refined tree-counting results (trees with a prescribed degree
sequence, forests, spanning trees of general graphs) are measured.
Several independent proofs of the count are known — a direct recursive argument, a
determinant computation via the Matrix–Tree Theorem, a double-counting argument on
increasing trees — and each exposes a different piece of structure. This mission
formalizes the proof via **Prüfer sequences**, due to Prüfer (1918): an explicit,
computable bijection between labeled trees and certain finite sequences, presented here
following Gross and Yellen, *Graph Theory and Its Applications*, 3rd ed. (CRC Press,
2018), Section 3.7, pp. 157–162.
## Setting
Fix $n \geq 2$ and take the vertex set to be $\{1, \dots, n\}$ (formalized as `Fin n`).
A **labeled tree** on $n$ vertices is a simple graph $T$ on this vertex set that is
connected and acyclic (Mathlib's `SimpleGraph.IsTree`). Two labeled trees are the same
exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the
source are both paths but are *different* labeled trees, since the labels sit on
different vertices.
A **Prüfer sequence** of length $n - 2$ is any sequence $(s_1, \dots, s_{n-2})$ of
labels drawn from $\{1, \dots, n\}$, repetitions allowed (so there are $n^{n-2}$ of
them, by the rule of product).
The **encoding** of a tree $T$ (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by
repeating, $n-2$ times: find the leaf (degree-one vertex) with the smallest label among
those not yet removed, record the label of *its* neighbor, then delete that leaf. The
**decoding** of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the
tree edge by edge, at each step joining the smallest label not yet used and not
appearing later in the sequence to the next label in the sequence, finishing by joining
the two labels left over.
## Formalization targets
### Goal — Cayley's Tree Formula (Theorem 3.7.5, p. 162)
$$
\operatorname{Nat.card}\, \{T : \text{SimpleGraph}(\text{Fin } n) \mid T.\text{IsTree}\} = n^{\,n-2}, \qquad n \geq 2.
$$
This is the weakest stable statement: it is exactly the count Cayley identified, phrased
without reference to any particular proof method, so it is not tied to properties of
Prüfer sequences beyond what is needed to establish the count.
## Significance
The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree
Theorem (which computes the analogous count for spanning trees of an arbitrary graph as
a cofactor of its Laplacian) and it appears as an ingredient in random graph theory
(counting spanning trees of $K_n$ bounds the number of ways a random graph process can
build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding
itself is used as a compact serialization of a labeled tree.
The result has been proved by hand for over a century, and its most classical proof (the
one formalized here) has not, to this project's knowledge, appeared as a
machine-checked Lean proof; Mathlib's `Combinatorics.SimpleGraph` library has the tree
and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or
the count itself. Formalizing it here means constructing the encoding and decoding maps
explicitly as computable, total recursive functions, and proving they are mutually
inverse — the mission's four milestones below are exactly the four supporting results
the source uses for this.
## Difficulty
The obvious first attempt is to define the encoding by structural recursion, peeling one
leaf per step, but this immediately runs into a dependent-typing obstacle: after
deleting a vertex, the "remaining graph" naturally lives on a *smaller* vertex type, so
a naive recursive definition changes type at every step and the final sequence's type
(length $n-2$) is not visible to the recursion by construction. The formalization here
sidesteps this by keeping the ambient vertex type fixed at `Fin n` throughout and
tracking the shrinking set of "active" vertices as an ordinary `Finset (Fin n)`
parameter, so the recursion is on a natural number step-counter rather than on the type
itself; the price is that every step's "leaf" and "neighbor" must be picked out by an
explicit `Finset.filter`/`Finset.min` computation whose well-definedness (there is
always a smallest active leaf, and it always has a unique active neighbor) is exactly
the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system
gives for free. The inverse direction has the dual issue in reverse: decoding recurses
structurally on the sequence while tracking a shrinking *label set*, and showing the two
recursions undo each other (Proposition 3.7.4) requires the same induction run in both
directions simultaneously.
## Formalization scope
Trees are `SimpleGraph (Fin n)` satisfying Mathlib's `SimpleGraph.IsTree`; no alternate,
weaker notion of "tree" is used. Prüfer sequences are functions `Fin (n - 2) → Fin n`
(equivalently, by `Fintype.card_fun`, exactly the $n^{n-2}$ count needed) rather than
`List` or `Vector`, so that the final counting step is immediate once the bijection is
established. The encoding and decoding functions (`pruferEncode`, `pruferDecode`) are
supplied as `noncomputable` definitions in `Definitions.Def_GYGraphTheory` — noncomputable
only because Prop-level decidability of a general `SimpleGraph.Adj` is classical, not
because the algorithm is non-constructive; every step is the literal Prüfer procedure,
junk-valued (defaulting to label `0`) outside its intended domain in exactly the way a
hand proof would say "this step is meaningless once fewer than two active vertices
remain." The four milestones give the precise faithful statements of the source's
Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal
theorem is the immediate corollary once all four are in hand, via `Fintype.card_congr`
and `Fintype.card_fun`. A trivializing formalization is not available here: `IsTree` is
Mathlib's standard, non-vacuous notion, and the milestones pin down `pruferEncode`
and `pruferDecode` to the source's specific algorithm rather than leaving the bijection's
existence as a free black box. Beyond the four milestones, a full development needs:
basic `Finset`/`List` manipulation lemmas relating `pruferPeel`'s step-indexed recursion
to `pruferDecodeAux`'s list-indexed recursion (reusable in any future mission touching
Prüfer-style encodings); and the final cardinality argument tying the bijection to
`n ^ (n - 2)`. Contributions connecting this formula to Mathlib's general Matrix–Tree
machinery (if and when it exists) would be a natural, welcome extension but are out of
scope for this mission.
## Selected references
- A. Cayley, *A theorem on trees*, Quart. J. Math. 23 (1889), 376–378.
- H. Prüfer, *Neuer Beweis eines Satzes über Permutationen*, Archiv der Mathematischen
Physik 27 (1918), 742–744.
- J.L. Gross and J. Yellen, *Graph Theory and Its Applications*, 3rd ed., CRC Press,
2018, Section 3.7 "Counting Labeled Trees: Prüfer Encoding", pp. 157–162.
Hatcher Algebraic Topology III: The Classification of Covering SpacesTextbook
## 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](https://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](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](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](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](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean)
## Motivation
An **elliptic curve** over $\mathbb{Q}$ is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group $E(\mathbb{Q})$ (Mordell, 1922), so $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$ for an integer $r \ge 0$, the **rank**. No algorithm is known that decides, for a given curve, whether $r > 0$, i.e. whether there are infinitely many rational points. The **Birch and Swinnerton-Dyer conjecture** predicts $r$ from an analytic object, the Hasse–Weil $L$-function $L(E,s)$: it asserts that $r$ equals the order of vanishing of $L(E,s)$ at $s = 1$. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, [*The Birch and Swinnerton-Dyer Conjecture*](https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf) (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.
**Timeline.**
- 1922: L. Mordell (Proc. Cambridge Phil. Soc. 21) proves that $E(\mathbb{Q})$ is finitely generated, answering a question of Poincaré (1901).
- 1936: H. Hasse proves $|p + 1 - \#E(\mathbb{F}_p)| \le 2\sqrt p$ at primes of good reduction, so the Euler product for $L(E,s)$ converges for $\operatorname{Re} s > 3/2$; he conjectures that $L(E,s)$ continues to an entire function.
- 1965: B. Birch and H. P. F. Swinnerton-Dyer, [*Notes on elliptic curves II*](https://doi.org/10.1515/crll.1965.218.79), state the conjecture, found experimentally on the EDSAC computer.
- 1977: J. Coates and A. Wiles, [*On the conjecture of Birch and Swinnerton-Dyer*](https://doi.org/10.1007/BF01402975): for curves with complex multiplication, $L(E,1) \ne 0$ implies $E(\mathbb{Q})$ finite.
- 1986: B. Gross and D. Zagier, [*Heegner points and derivatives of L-series*](https://doi.org/10.1007/BF01388809): for modular $E$ with $L(E,1) = 0 \ne L'(E,1)$, a Heegner point has infinite order.
- 1989–1990: V. Kolyvagin, [*Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves*](https://doi.org/10.1070/IM1989v032n03ABEH000779): for modular $E$ with $L(E,s)$ vanishing to order at most $1$ at $s=1$, the rank equals that order (with a non-vanishing theorem of Bump–Friedberg–Hoffstein and Murty–Murty).
- 1995–2001: A. Wiles ([Ann. Math. 141](https://doi.org/10.2307/2118559)), R. Taylor and A. Wiles ([Ann. Math. 141](https://doi.org/10.2307/2118560)), and C. Breuil, B. Conrad, F. Diamond and R. Taylor ([J. Amer. Math. Soc. 14](https://doi.org/10.1090/S0894-0347-01-00370-8)): every elliptic curve over $\mathbb{Q}$ is modular, so $L(E,s)$ is entire and Kolyvagin's theorem applies to all $E/\mathbb{Q}$.
- 2000: the Clay Mathematics Institute adopts Wiles' formulation as a Millennium Prize Problem.
- 2014: M. Bhargava, C. Skinner and W. Zhang, [*A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture*](https://arxiv.org/abs/1407.1826): the rank conjecture holds for more than $66\%$ of curves ordered by height. The general case is open.
## Setting
A **Weierstrass equation** over $\mathbb{Q}$ is
$$E :\ y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in \mathbb{Q},$$
with discriminant $\Delta$; in Lean, `WeierstrassCurve ℚ`. It is an **elliptic curve** when $\Delta \ne 0$ (Mathlib's typeclass `IsElliptic`). Its **rational points** $E(\mathbb{Q})$ are the rational solutions $(x,y)$ together with the point at infinity $O$, an abelian group under the chord-and-tangent law (`W.toAffine.Point`). The **rank** is the rank of this group as a $\mathbb{Z}$-module,
$$r = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}) \qquad \text{(`BSD.rank W`)},$$
the $r$ in $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$.
The **Hasse–Weil $L$-series** is built prime by prime. For each prime $p$ take a Weierstrass equation for $E$ that is *minimal at $p$* (integral coefficients, with the $p$-adic valuation of $\Delta$ as small as possible) and reduce it modulo $p$; put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ when the reduction is smooth (**good reduction**). The local factor is
$$L_p(E,s) = \begin{cases} (1 - a_p p^{-s} + p^{1-2s})^{-1} & \text{good reduction,}\\ (1 - p^{-s})^{-1} & \text{split multiplicative reduction,}\\ (1 + p^{-s})^{-1} & \text{non-split multiplicative reduction,}\\ 1 & \text{additive reduction,}\end{cases}$$
and $L(E,s) = \prod_p L_p(E,s) = \sum_{n \ge 1} a_n n^{-s}$, convergent for $\operatorname{Re} s > 3/2$ by Hasse's bound. In Lean this is Mathlib's `WeierstrassCurve.LSeries W s`, defined by exactly this recipe (`WeierstrassCurve.LFunction` is the arithmetic function $n \mapsto a_n$, an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's `LSeries` takes the junk value $0$. This is the complete $L$-series $L^*(C,s)$ of Wiles' Remark 1; it differs from the incomplete product over $p \nmid 2\Delta$ in Wiles' display by finitely many factors holomorphic and non-zero at $s = 1$, so both have the same order of vanishing there.
An **$L$-function of $E$** is an entire function $\Lambda : \mathbb{C} \to \mathbb{C}$ with $\Lambda(s) = L(E,s)$ for $\operatorname{Re} s > 3/2$ (`BSD.IsLFunction W Λ`). By the identity theorem there is at most one; by modularity there is exactly one. The **order of vanishing** of $\Lambda$ at $s = 1$ is the $m$ with $\Lambda(s) = c(s-1)^m + \dots$, $c \ne 0$; in Lean, `analyticOrderAt Λ 1`, valued in $\mathbb{N} \cup \{\infty\}$, with value $\infty$ exactly when $\Lambda$ vanishes identically near $1$.
## Formalization targets
### Goal: the Birch and Swinnerton-Dyer conjecture (`BSD.birch_swinnerton_dyer`)
For every elliptic curve $E$ over $\mathbb{Q}$ there is an entire $\Lambda$ agreeing with $L(E,s)$ on $\operatorname{Re} s > 3/2$ such that
$$\operatorname{ord}_{s=1} \Lambda = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}).$$
This is Wiles' *Conjecture (Birch and Swinnerton-Dyer)*: $L(C,s) = c(s-1)^r + \text{higher order terms}$ with $c \ne 0$ and $r = \operatorname{rank} C(\mathbb{Q})$. Open.
### Weaker target: the weak conjecture (`BSD.weak_birch_swinnerton_dyer`)
There is an $L$-function $\Lambda$ of $E$ with $\Lambda(1) = 0$ if and only if $E(\mathbb{Q})$ is infinite. Wiles: "In particular this conjecture asserts that $L(C,1) = 0 \Leftrightarrow C(\mathbb{Q})$ is infinite." Open.
### Milestones: what Wiles lists as known
1. **Mordell's theorem** (`BSD.mordell`): $E(\mathbb{Q})$ is a finitely generated abelian group.
2. **Convergence of the $L$-series** (`BSD.lSeriesSummable`): $\sum a_n n^{-s}$ converges for $\operatorname{Re} s > 3/2$. Wiles: "this Euler product is then known to converge for $\operatorname{Re}(s) > 3/2$."
3. **Analytic continuation** (`BSD.exists_isLFunction`): $E$ has an $L$-function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.
4. **Gross–Zagier–Kolyvagin** (`BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one`): if an $L$-function of $E$ vanishes to order at most $1$ at $s = 1$, its order equals the rank. Wiles: "If $L(C,s) \sim c(s-1)^m$ with $c \ne 0$ and $m = 0$ or $1$, then the conjecture holds."
A bridging lemma, `BSD.isLFunction_unique`, records that an $L$-function of $E$ is unique when it exists.
## Significance
*The result itself.* The conjecture makes the finiteness of $E(\mathbb{Q})$ decidable from $L(E,1)$ and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of $L$-functions.
*Formalizing it.* None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on $E(\mathbb{Q})$, minimal models and reduction types over discrete valuation rings, and the Hasse–Weil $L$-series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of $L(E,s)$. On this platform, earlier library entries named `birch_swinnerton_dyer` are retired placeholders whose formal statements reduce to trivialities such as $0 = 0$; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own $L$-series. Two published platform results bear directly on the milestones: the descent step `WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex` (finite index of $2E(\mathbb{Q})$ implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and `WeierstrassCurve.modularity_of_semistableModel` from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to `WeierstrassCurve.LSeries` would give milestone 3 for semistable curves.
## Difficulty
Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш$(E)$, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of $E(\mathbb{Q})$, founders on Ш. On the analytic side one can certify $\Lambda(1) \ne 0$ or $\Lambda'(1) \ne 0$ numerically but cannot certify an exact zero, and the only known bridge from $L$-values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order $\le 1$ and the conjecture is not known for a single curve of rank $\ge 2$. Iwasawa theory (Kato, Skinner–Urban) relates $p$-adic $L$-functions to Selmer groups but yields $p$-adic, not Archimedean, orders of vanishing.
The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.
## Formalization scope
- $E$ is any `WeierstrassCurve ℚ` with `IsElliptic` ($\Delta \ne 0$); no minimality or integrality of the model is assumed. Mathlib's $L$-series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.
- The rank is `Module.finrank ℤ W.toAffine.Point`: for a finitely generated abelian group, the $r$ in $\mathbb{Z}^r \oplus T$; for a group of infinite rank Mathlib's `finrank` is $0$, a case milestone 1 excludes.
- The $L$-series is Mathlib's `WeierstrassCurve.LSeries`, with all Euler factors including the bad primes, and junk value $0$ where the Dirichlet series diverges. `BSD.IsLFunction` constrains $\Lambda$ only on $\operatorname{Re} s > 3/2$; milestone 2 shows the series is genuine there, and the bridging lemma shows $\Lambda$ is then unique.
- The order of vanishing is `analyticOrderAt Λ 1 : ℕ∞`; equating it with a natural number asserts in particular that $\Lambda \not\equiv 0$ near $1$.
*No trivializing formalization.* The existential $\Lambda$ cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and $\Lambda \equiv 0$ is excluded by the finite value of the rank. Without `IsElliptic` the statements would concern singular cubics, whose point group is $\mathbb{Q}$ or $\mathbb{Q}^\times$; the hypothesis is required, not decorative.
*Out of scope.* The refined conjecture (the leading coefficient in terms of Ш$(E)$, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш$(E)$, number fields and abelian varieties, and the functional equation of $L(E,s)$.
*Infrastructure needed and welcome contributions.* Heights on $E(\mathbb{Q})$ and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of $a_n$; a bridge from Mathlib's `WeierstrassCurve.LSeries` to the $L$-series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about `WeierstrassCurve.LFunction` (its values at primes, multiplicativity, independence of the model) are welcome.
## Selected references
- A. Wiles, *The Birch and Swinnerton-Dyer Conjecture*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf
- B. J. Birch, H. P. F. Swinnerton-Dyer, *Notes on elliptic curves II*, Journal für die reine und angewandte Mathematik 218 (1965), 79–108. https://doi.org/10.1515/crll.1965.218.79
- L. J. Mordell, *On the rational solutions of the indeterminate equations of the third and fourth degrees*, Proceedings of the Cambridge Philosophical Society 21 (1922), 179–192.
- J. Coates, A. Wiles, *On the conjecture of Birch and Swinnerton-Dyer*, Inventiones Mathematicae 39 (1977), 223–251. https://doi.org/10.1007/BF01402975
- B. H. Gross, D. B. Zagier, *Heegner points and derivatives of L-series*, Inventiones Mathematicae 84 (1986), 225–320. https://doi.org/10.1007/BF01388809
- V. A. Kolyvagin, *Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves*, Mathematics of the USSR-Izvestiya 32 (1989), 523–541. https://doi.org/10.1070/IM1989v032n03ABEH000779
- A. Wiles, *Modular elliptic curves and Fermat's Last Theorem*, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
- R. Taylor, A. Wiles, *Ring-theoretic properties of certain Hecke algebras*, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
- C. Breuil, B. Conrad, F. Diamond, R. Taylor, *On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises*, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
- J. B. Tunnell, *A classical Diophantine problem and modular forms of weight 3/2*, Inventiones Mathematicae 72 (1983), 323–334. https://doi.org/10.1007/BF01389327
- M. Bhargava, C. Skinner, W. Zhang, *A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture*, 2014. https://arxiv.org/abs/1407.1826
- J. H. Silverman, *The Arithmetic of Elliptic Curves*, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. https://doi.org/10.1007/978-0-387-09494-6
Uniform Obstacle Bounds for Planar Graphs (OPG-37357)Open Problem
## Motivation
An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The **obstacle number** asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.
The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$, have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.
## Setting
A finite simple graph $G$ has a **$k$-obstacle drawing** when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that
$$
uv\in E(G)
\quad\Longleftrightarrow\quad
[p(u),p(v)]\text{ meets no obstacle}.
$$
Graph vertices lie outside every obstacle. The **ordinary obstacle number** $\operatorname{obs}(G)$ is the least such $k$. The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.
The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.
## Formalization targets
### The two-part OPG record
The source records both
$$
\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1
$$
and
$$
\exists k\in\mathbb N\ \forall\text{ finite planar }H,
\ \operatorname{obs}(H)\le k.
$$
The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.
### Published first part
A milestone formalizes the stronger published statement
$$
\exists\text{ finite planar }G,
\qquad \operatorname{obs}(G)\le2
\quad\text{and}\quad
\operatorname{obs}(G)\not\le1.
$$
This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.
### Universal bound
The open milestone asks for a single natural number $k$, chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.
## Significance
The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.
Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.
## Difficulty
A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.
Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$.
## Formalization scope
All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.
The repository's fixed-placement polygonization argument and finite arrangement code are `candidate_only`. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.
## Selected references
- L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, *Graphs with Obstacle Number Greater than One*, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
- J. Gimbel, P. Ossona de Mendez, and P. Valtr, *Obstacle Numbers of Planar Graphs*, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
- M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, *Bounding and Computing Obstacle Numbers of Graphs*, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
- Open Problem Garden / UnsolvedMath, *OPG-37357*. https://www.unsolvedmath.com/problems/OPG-37357
Clique Partitions of Chordal Graphs (Erdos Problem 81)Open Problem
## Motivation
An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.
Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the $n^2/6$ scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an $o(n^2)$ gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform $n^2/6+o(n^2)$ milestone. It does not supply the $O(n)$ remainder asked for by the root.
## Setting
A finite simple graph is **chordal** when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.
An **edge partition into cliques** is a finite family $\mathcal P$ of complete vertex sets such that every edge of $G$ belongs to exactly one member of $\mathcal P$. Members may share vertices but may not share edges. Write $\operatorname{cp}(G)$ for the minimum possible number of pieces.
The asymptotic notation
$$
\frac{n^2}{6}+O(n)
$$
means that there are constants $C>0$ and $n_0\ge1$, chosen independently of $G$ and $n$, such that every chordal $n$-vertex graph with $n\ge n_0$ has a clique partition with at most $n^2/6+Cn$ pieces.
## Formalization targets
### Erdős Problem 81
The root theorem is
$$
\exists C>0\ \exists n_0\ge1\ \forall n\ge n_0\
\forall G\text{ chordal on }n\text{ vertices},
\qquad
\operatorname{cp}(G)\le \frac{n^2}{6}+Cn.
$$
The quantifier order is essential: $C$ and $n_0$ are universal and cannot depend on the graph.
### Leading-coefficient milestone
The supporting target records the weaker uniform statement
$$
\forall\varepsilon>0\ \exists n_0\ \forall n\ge n_0\
\forall G\text{ chordal on }n\text{ vertices},
\qquad
\operatorname{cp}(G)\le
\left(\frac16+\varepsilon\right)n^2.
$$
This is the precise $n^2/6+o(n^2)$ form. It is not equivalent to the root: choosing $\varepsilon=1/n$ is invalid because the cutoff may depend on the fixed value of $\varepsilon$.
## Significance
The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient $1/6$. It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.
Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.
## Difficulty
Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses $o(n^2)$ pieces; the root requires that loss to be only $O(n)$.
The dense-packing theorem has quantifiers of the form “for every fixed $\varepsilon>0$ there exists $N(\varepsilon)$.” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its $\varepsilon$ could vary with $n$.
## Formalization scope
Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in $\mathbb R$ so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.
The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is `candidate_only`, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.
## Selected references
- P. Erdős, E. T. Ordman, and Y. Zalcstein, *Clique Partitions of Chordal Graphs*, Combinatorics, Probability and Computing 2(4), 1993. https://doi.org/10.1017/S0963548300000808
- P. E. Haxell and V. Rödl, *Integer and Fractional Packings in Dense Graphs*, Combinatorica 21, 2001. https://doi.org/10.1007/s004930170003
- R. Yuster, *Integer and fractional packing of families of graphs*, 2003. https://arxiv.org/abs/math/0305350
- Erdős Problems, *Problem 81*. https://www.erdosproblems.com/81
Weak Pentagon Colorings of Triangle-Free Cubic Graphs (OPG-434)Open Problem
## Motivation
The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.
Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.
## Setting
Let $G$ be a finite simple triangle-free cubic graph. A **five-edge coloring** here is any symmetric assignment
$$
c:E(G)\longrightarrow\{1,2,3,4,5\}.
$$
It need not be proper or surjective. For a color $i$, delete all edges with label $i$ while retaining every vertex. The coloring is a **weak-pentagon coloring** when each of the five resulting spanning graphs is bipartite.
Equivalently, each color class is an **odd-cycle edge transversal**: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.
A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of $G$ to an adjacent pair in this target.
## Formalization targets
### Weak pentagon conjecture
The root target is
$$
\forall G\text{ finite, simple, triangle-free, and cubic},
\qquad
\exists c:E(G)\to[5]\ \forall i\in[5],
\quad G-c^{-1}(i)\text{ is bipartite}.
$$
No condition is imposed on adjacent edges receiving different labels.
### Odd-cycle equivalence
For every fixed graph and fixed five-edge labeling,
$$
\bigl(\forall i,\ G-c^{-1}(i)\text{ is bipartite}\bigr)
\quad\Longleftrightarrow\quad
\bigl(\forall i,\ c^{-1}(i)\text{ meets every odd cycle of }G\bigr).
$$
This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.
### Sixteen-vertex homomorphism formulation
For every finite simple graph $G$,
$$
G\text{ has a weak-pentagon coloring}
\quad\Longleftrightarrow\quad
G\longrightarrow H_{16},
$$
where $H_{16}$ has vertex set $\{0,1\}^4$ and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.
## Significance
The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.
Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.
## Difficulty
The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.
High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.
## Formalization scope
Colors are `Fin 5`. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.
The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are `candidate_only`; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.
## Selected references
- R. Šámal, *Weak pentagon problem*, Open Problem Garden, 2007. https://www.openproblemgarden.org/op/weak_pentagon_problem
- M. DeVos and R. Šámal, *High-girth cubic graphs are homomorphic to the Clebsch graph*, Journal of Graph Theory 66 (2011), 241–259. https://arxiv.org/abs/math/0602580
- P. Kolman, B. Lidický, and J.-S. Sereni, *On Minimum Fair Odd Cycle Transversal*, 2010. https://kam.mff.cuni.cz/kamserie/clanky/2010/s956.pdf
- Open Problem Garden / UnsolvedMath, *OPG-434*. https://www.unsolvedmath.com/problems/OPG-434
Two Acyclic Colors for Planar Orientations (OPG-169)Open Problem
## Motivation
The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.
Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.
## Setting
Let $G$ be a finite simple planar graph. An **orientation** $D$ assigns exactly one direction to every edge of $G$, with no loops, parallel arcs, or pair of opposite arcs. For $X\subseteq V(D)$, the induced digraph $D[X]$ retains every arc whose two endpoints lie in $X$.
A two-coloring is a map
$$
c:V(D)\longrightarrow\{0,1\}.
$$
It is valid when both induced digraphs $D[c^{-1}(0)]$ and $D[c^{-1}(1)]$ contain no directed cycle. The color classes need not be independent and either color may be unused.
Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.
## Formalization targets
### Two Color Conjecture
The goal is
$$
\forall D\text{ an orientation of a finite simple planar graph},
\qquad
\exists c:V(D)\to\{0,1\},
\quad D[c^{-1}(0)]\text{ and }D[c^{-1}(1)]\text{ are acyclic}.
$$
Disconnected graphs and empty color classes are included.
### Least-order counterexample structure
A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:
$$
D\text{ least-order counterexample}
\quad\Longrightarrow\quad
D\text{ strongly connected and }\delta(U(D))\ge3.
$$
The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.
### Semidegree candidate
A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains `candidate_only`.
## Significance
The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.
The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.
## Difficulty
Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.
Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.
## Formalization scope
A directed graph is a binary relation, coupled to a `SimpleGraph` by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.
The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.
Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.
## Selected references
- Open Problem Garden / UnsolvedMath, *OPG-169: The Two Color Conjecture*. https://www.unsolvedmath.com/problems/OPG-169
- B. Mohar, *Eigenvalues and colorings of digraphs*, Linear Algebra and its Applications, 2010. https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf
- Z. Li and B. Mohar, *Planar digraphs of digirth four are 2-colourable*, Journal of Combinatorial Theory, Series B, 2017. https://arxiv.org/abs/1606.06114
Hatcher Algebraic Topology II: The van Kampen TheoremTextbook
## 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](https://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](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](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](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](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean)
## Motivation
The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, [*Existence and smoothness of the Navier–Stokes equation*](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf) (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.
**Timeline.**
- 1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
- 1934: Jean Leray, [*Sur le mouvement d'un liquide visqueux emplissant l'espace*](https://doi.org/10.1007/BF02547354) (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global *weak* solutions with finite energy always exist. Their smoothness and uniqueness are left open.
- 1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph [*The Mathematical Theory of Viscous Incompressible Flow*](https://archive.org/details/mathematicaltheo0000lady), 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
- 1984: Tosio Kato, [*Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$*](https://doi.org/10.1007/BF01174182) (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$.
- 1976–1998: partial regularity. Scheffer, then [Caffarelli, Kohn and Nirenberg](https://doi.org/10.1002/cpa.3160350604) (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
- 2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.
## Setting
Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$-space with its Euclidean norm $|x|$; in Lean this is `NavierStokes.Vec n`. A **velocity field** assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$. A **pressure** is a real function $p(x,t)$. The **viscosity** $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).
For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the **divergence** is
$$\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},$$
in Lean `NavierStokes.div`, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$. The **Laplacian** $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The **gradient** $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$. Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is `NavierStokes.gradNormSq`.
**Admissible initial data** (Fefferman's condition (4), `NavierStokes.IsInitialData`): a $C^\infty$, divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,
$$|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.$$
In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$-th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.
A **physically reasonable solution** on a set $S$ of times (`NavierStokes.IsSolutionOn`; $S = [0,\infty)$ for `NavierStokes.IsSolution`) is a pair $(u,p)$ such that
1. (Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$, up to the boundary of $S$;
2. (Fefferman (1), $f \equiv 0$) for every $t \in S$ with $t > 0$ and every $x$,
$$\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;$$
3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$;
4. (Fefferman (3)) $u(x,0) = u^0(x)$;
5. (Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$, for some constant $C$.
## Formalization targets
### Goal: Fefferman's statement (A)
Take $\nu > 0$ and $n = 3$. For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$:
$$\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) on } \mathbb{R}^3 \times [0,\infty).$$
This is `NavierStokes.existence_and_smoothness_R3`. It is open; a proof would settle the Millennium Prize Problem in the affirmative.
### Milestones: what Fefferman lists as known
1. **Local existence** (`NavierStokes.local_existence_R3`): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$. Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$, with $T$ depending on the initial data."
2. **Global existence for small data** (`NavierStokes.small_data_global_existence_R3`): there is an absolute constant $c > 0$ such that, for $n = 3$, (A) holds for every admissible $u^0$ with
$$\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.$$
Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$, so Kato's theorem also applies.
3. **The two-dimensional case** (`NavierStokes.existence_and_smoothness_R2`): statement (A) with $n = 2$. Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."
A bridging lemma, `NavierStokes.isInitialData_iff_schwartz`, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.
## Significance
*The result itself.* Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."
*Formalizing it.* None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$, the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.
## Difficulty
The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$, but in three dimensions this control is *supercritical*: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$, so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$, gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$, which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.
The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.
## Formalization scope
- $\mathbb{R}^n$ is `EuclideanSpace ℝ (Fin n)` with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$.
- A velocity field is a function of all real times, but every condition is imposed only on the time set $S$; values at negative times are unconstrained.
- Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's `ContDiffOn` of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$. The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "$t \ge 0$".
- Derivatives are Mathlib's total functions (`fderiv`, `deriv`, `iteratedFDeriv`, `gradient`, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
- The energy is a Lebesgue integral in $[0,\infty]$, equal to $\infty$ when $u(\cdot,t) \notin L^2$, so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
- No normalization is imposed on the pressure, as in Fefferman's text.
*No trivializing formalization.* The zero field solves the equations only for $u^0 = 0$; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.
*Infrastructure needed and welcome contributions.* The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the `NavierStokes` namespace, decompositions of the milestones, and Mathlib lemmas about `ContDiffOn` on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ($\nu = 0$) are out of scope.
## Selected references
- C. L. Fefferman, *Existence and smoothness of the Navier–Stokes equation*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
- J. Leray, *Sur le mouvement d'un liquide visqueux emplissant l'espace*, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
- O. A. Ladyzhenskaya, *The Mathematical Theory of Viscous Incompressible Flow*, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
- T. Kato, *Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$, with applications to weak solutions*, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
- L. Caffarelli, R. Kohn, L. Nirenberg, *Partial regularity of suitable weak solutions of the Navier–Stokes equations*, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
- A. J. Majda, A. L. Bertozzi, *Vorticity and Incompressible Flow*, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
- J. C. Robinson, J. L. Rodrigo, W. Sadowski, *The Three-Dimensional Navier–Stokes Equations: Classical Theory*, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143
Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper
## Motivation
A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.
Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in *Algorithmica* in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune $14$-regular bipartite graph of at least that girth, and it has a perfect matching.
This is therefore a `ResearchPaper` mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.
## Setting
For a finite simple graph $G$ and a vertex set $A\subseteq V(G)$, the associated cut consists of all edges with one endpoint in $A$ and one in $V(G)\setminus A$. The cut is **nontrivial** when both shores are nonempty. It is a **matching cut** when each vertex is incident with at most one crossing edge. A graph is called **immune** in the cited paper when it has no matching cut.
The **girth** is the length of a shortest simple cycle; forests have infinite girth. A graph is $14$-regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A **perfect matching** pairs every vertex with one adjacent partner.
The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, $K_1$ has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.
## Formalization targets
### Lemma 5 — immune high-girth graphs
The main theorem follows the paper's structural lemma:
$$
\forall g\ge3\ \exists G,
\quad G\text{ is finite, connected, bipartite, and $14$-regular},
$$
$$
\operatorname{girth}(G)\ge g,
\qquad
G\text{ has no matching cut},
\qquad
G\text{ has a perfect matching}.
$$
The graph may depend on $g$. The existence quantifier does not request an efficient algorithm or a numerical order bound.
### Negative OPG consequence
A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:
$$
\forall g\ge3\ \exists G,
\qquad
\overline d(G)=14<15,
\quad \operatorname{girth}(G)\ge g,
\quad G\text{ has no matching cut}.
$$
Thus choosing $d=15$ refutes the intended universal assertion that some girth threshold works for every graph of average degree below $d$.
## Significance
The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.
Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every $g\ge3$, Matching Cut is NP-complete even for bipartite graphs of girth at least $g$ and maximum degree at most $60$. Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.
## Difficulty
Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.
A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.
## Formalization scope
Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least $g$ means every such cycle has length at least $g$, so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.
The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the $K_1$ ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.
Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are `candidate_only` and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.
## Selected references
- C. Feghali, F. Lucke, D. Paulusma, and B. Ries, *Matching Cuts in Graphs of High Girth and H-Free Graphs*, Algorithmica 87 (2025), 1199–1221. https://doi.org/10.1007/s00453-025-01318-8
- C. Feghali, F. Lucke, D. Paulusma, and B. Ries, ISAAC 2023 version. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.31
- A. Lubotzky, R. Phillips, and P. Sarnak, *Ramanujan graphs*, Combinatorica 8 (1988), 261–277. https://doi.org/10.1007/BF02126799
- Open Problem Garden, *Matching cut and girth*. https://www.openproblemgarden.org/op/matching_cut_and_girth
A Kleene Theorem for Free Many-Sorted AlgebrasResearch Paper
## Motivation
**Kleene's theorem** (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the **regular** ones — those built from finite languages by union, concatenation, and the Kleene star. **Mezei and Wright** (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra **recognizable** when it is the preimage of a subset of a *finite* algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of **recognizable tree languages** and finite tree automata of **Gécseg and Steinby** (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.
Many computational structures are inherently **many-sorted**: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (**CVCL20**), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the **regular** side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.
## Setting
Fix a finite set of **sorts** $S$. An **$S$-sorted set** $A = (A_s)_{s\in S}$ is a family of sets; it is **finite** when $\coprod_{s\in S} A_s$ is finite. An **$S$-sorted signature** $\Sigma$ assigns to each pair $(\mathbf{s}, s) \in S^\star \times S$ a set $\Sigma_{\mathbf{s},s}$ of operation symbols of **arity** $\mathbf{s}$ and **coarity** $s$. A **$\Sigma$-algebra** $\mathbf{A}$ is an $S$-sorted set $A$ together with, for each $\sigma \in \Sigma_{\mathbf{s},s}$, an operation $\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s$, where $A_{\mathbf s} = \prod_{j} A_{s_j}$. A **homomorphism** commutes with all operations sortwise.
The **free $\Sigma$-algebra** $\mathbf T_\Sigma(X)$ on an $S$-sorted set $X$ of variables has as its sort-$s$ carrier $\mathrm T_\Sigma(X)_s$ the set of **$(X,s)$-terms**; every $S$-sorted map $X \to A$ extends uniquely to a homomorphism $\mathbf T_\Sigma(X) \to \mathbf A$. Following automata-theoretic tradition, subsets of $\mathrm T_\Sigma(X)$ are called **languages**. For a sort $s$, a language $L \subseteq \mathrm T_\Sigma(X)_s$ is **$s$-recognizable** when there are a finite $\Sigma$-algebra $\mathbf N$, a homomorphism $f\colon \mathbf T_\Sigma(X) \to \mathbf N$, and a subset $M \subseteq N_s$ with $L = f_s^{-1}[M]$. Write $\mathrm{Rec}_s(\mathbf T_\Sigma(X))$ for the set of all such $L$.
Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable $z \in X_u$ and a language $L \subseteq \mathrm T_\Sigma(X)_u$, **$z$-substitution** $\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s$ replaces, in every term of an input language of sort $s$, each occurrence of $z$ independently by a term of $L$. The **$z$-iteration** is $L^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}$, where $L^{0\,z} = \{z\}$ and $L^{i+1\,z} = L^{i\,z} \cup \left(\!\begin{smallmatrix}z\\ L^{i\,z}\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s(L)$. For a finite $S$-sorted set $Z$, the **regular signature** $\mathrm{Reg}(S,\Sigma,Z)$ expands $\Sigma$ by an empty constant $\varnothing_s$, a binary sum $+_s$, a unary $z$-iteration $(\cdot)^{\star z}$ for each $z\in Z_s$, and a $z$-substitution operation for each $z\in Z_t$. Its terms are the **regular expressions** over $(S,\Sigma,Z)$; the power algebra $\mathbf T_\Sigma(Z)^\wp$ carries a canonical $\mathrm{Reg}(S,\Sigma,Z)$-algebra structure, and interpreting a regular expression there yields a language $\{R\}^{Z\sharp}_s$. A language $L\subseteq \mathrm T_\Sigma(X)_s$ is **$s$-regular** when $L = \{R\}^{Z\sharp}_s$ for some finite $Z\supseteq X$ and some regular expression $R$ of type $s$; write $\mathrm{Reg}_s(\mathbf T_\Sigma(X))$.
## Formalization targets
### Goal — the many-sorted Kleene theorem
$$\forall\, s\in S,\qquad \mathrm{Rec}_s(\mathbf T_\Sigma(X)) \;=\; \mathrm{Reg}_s(\mathbf T_\Sigma(X)).$$
The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite $S$, every finite $S$-sorted signature $\Sigma$, and every finite $S$-sorted set $X$. It splits into $\mathrm{Reg}_s \subseteq \mathrm{Rec}_s$ (Corollary 4.8) and $\mathrm{Rec}_s \subseteq \mathrm{Reg}_s$ (Proposition 4.10).
## Significance
The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of $\Sigma$, plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a $\mathrm{Reg}$-algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.
The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.
## Difficulty
The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a **sortwise budget**: an $S$-sorted family $K \le N$ recording, for each sort $t$, the set $K_t$ of state values still admissible at internal subterms. The induction is on $\lVert\lVert K\rVert\rVert = \sum_{s\in S} k_s$, and each step removes the top state of *one* chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages $L_u(C,K,l)$ with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).
## Formalization scope
Proposed Lean representation: $S$ a type with `[Fintype S]`; an $S$-sorted set as `S → Type`; a signature as a family `List S → S → Type` with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort-$s$ carrier `Set (T_Σ Z s)`; $s$-recognizability as the existence of a finite $\Sigma$-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: $S$ finite throughout; $\Sigma$ finite and $X$ finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly $\{\varnothing, +, (\cdot)^{\star z}, z\text{-subst}\}$ together with the operations of $\Sigma$ — not an unrestricted Boolean or closure algebra, which would trivialize the statement.
A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and $s$-recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.
## Selected references
- L. Gong, R. Ruiz Mora, N. Sanmartín Vich, E. Cosme Llópez, *A Kleene theorem for free many-sorted algebras*, 2026.
- J. Climent Vidal, E. Cosme Llópez, *Congruence-based proofs of the recognizability theorems for free many-sorted algebras*, Journal of Logic and Computation 30(2) (2020), 561–633. https://arxiv.org/abs/1808.08217
- F. Gécseg, M. Steinby, *Tree Automata*, Akadémiai Kiadó, Budapest, 1984.
- R. McNaughton, H. Yamada, *Regular expressions and state graphs for automata*, IRE Transactions on Electronic Computers EC-9 (1960), 39–47.
- S. C. Kleene, *Representation of events in nerve nets and finite automata*, in *Automata Studies*, Princeton University Press, 1956, 3–42.
- J. Mezei, J. Wright, *Algebraic automata and context-free sets*, Information and Control 11 (1967), 3–29.
- S. Eilenberg, *Automata, Languages, and Machines, Vol. A*, Academic Press, New York, 1974.