## 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.
## 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.
## Motivation
Searching an unsorted list of $N$ items for a single marked entry takes $\Theta(N)$ queries
classically — there is no way to do better than checking items one at a time. Grover's algorithm
(Grover 1996) shows that a quantum computer solves the same problem in $\Theta(\sqrt N)$ queries,
a quadratic speedup that applies to any problem expressible as unstructured search over a black-box
oracle (this includes brute-forcing NP-complete problems and inverting one-way functions, which is
why post-quantum cryptography doubles key lengths to compensate). Unlike Shor's algorithm, Grover's
algorithm is provably optimal: Bennett–Bernstein–Brassard–Vazirani (1997) showed $\Omega(\sqrt N)$
queries are necessary for any quantum algorithm solving unstructured search, so the quadratic
speedup is the best any quantum algorithm can achieve on this problem.
## Setting
Model an $N$-item database as the standard basis of $E = \mathbb{C}^N$ (`EuclideanSpace ℂ (Fin N)`),
with inner product $\langle x,y\rangle = \sum_i \overline{x_i}\,y_i$. Fix a **marked index**
$w_0 \in \{0,\dots,N-1\}$. The algorithm starts in the **uniform superposition**
$$|s\rangle = \frac{1}{\sqrt N}\sum_{i} |i\rangle,$$
a unit vector assigning equal amplitude to every item. Two reflections drive the search:
* the **oracle** $O = I - 2|w_0\rangle\langle w_0|$, which flips the sign of the amplitude on the
marked item and leaves every other basis state fixed;
* the **diffusion operator** $D = 2|s\rangle\langle s| - I$ ("inversion about the mean"), the
reflection about $|s\rangle$.
One **Grover iterate** is $G = D\,O$. The algorithm applies $G$ some number of times to $|s\rangle$
and measures; a measurement outcome equal to $w_0$ counts as success.
## Formalization targets
### Milestone — the iterate is an isometry $$\|G x\| = \|x\| \quad \text{for every } x \in E$$
$O$ and $D$ are each reflections about a unit vector, hence isometries; their composition $G$ is
therefore norm-preserving on the whole space, not just at $|s\rangle$ — the minimal fact needed for
$G$ to be a legitimate quantum operation.
### Milestone — the rotation formula $$\langle w_0, G^k s\rangle = \sin\bigl((2k+1)\theta\bigr), \qquad \theta := \arcsin\!\left(\tfrac{1}{\sqrt N}\right)$$
The geometric heart of the algorithm (Nielsen & Chuang, *Quantum Computation and Quantum
Information*, Section 6.1.2): restricted to the real two-dimensional subspace spanned by $|w_0\rangle$
and the component of $|s\rangle$ orthogonal to it, $G$ acts as rotation by a fixed angle $2\theta$.
Each iterate therefore advances the amplitude on the marked state along $\sin((2k+1)\theta)$,
exactly as claimed, with $\theta = \arcsin(1/\sqrt N)$ the rotation's initial offset (since
$\langle w_0, s\rangle = 1/\sqrt N$ at $k=0$).
### Goal $$\exists\, k,\quad 1 - \tfrac1N \;\le\; \bigl|\langle w_0, G^k s\rangle\bigr|^2$$
Some number of iterations drives the probability of measuring the marked item above $1-1/N$. The
goal is stated existentially, without fixing $k$ to a specific rounded formula: the rotation angle
$(2k+1)\theta$ can be made to land within $\theta$ of $\pi/2$ by an appropriate integer $k$, and at
that point $\sin^2((2k+1)\theta) \ge \cos^2\theta = 1-\sin^2\theta = 1 - 1/N$. Pinning $k$ down to
an explicit closed form (e.g. the nearest integer to $\pi/(4\theta) - 1/2$) is one valid strategy,
but is not required by the statement — any correct choice of $k$, and any correct proof it works,
closes the goal.
## Significance
Grover's algorithm is the second landmark quantum algorithm after Shor's, and the one with the
widest applicability: because it treats the search space as a black box, it accelerates any
brute-force search — SAT solving, collision finding, and generic key search among them — which is
the concrete reason NIST's post-quantum cryptography standards double symmetric key lengths rather
than replacing them outright. The mathematics itself has been fully settled since 1996, including
matching optimality lower bounds; nothing here is open. What this mission adds is a **machine-
checked** derivation of the amplitude formula and success bound directly from the definitions of
the oracle and diffusion operators as concrete linear operators on `EuclideanSpace ℂ (Fin N)` —
Mathlib has the finite-dimensional inner product space and rank-one operator machinery this needs
(`InnerProductSpace.rankOne`, `EuclideanSpace.single`), but no existing formalization of the
algorithm itself.
## Difficulty
The obvious first attempt tries to track the full $N$-dimensional state vector through $k$
iterations. This is intractable in general: $G$'s action on an arbitrary basis vector depends on
its overlap with both $|w_0\rangle$ and $|s\rangle$. The move that makes the problem tractable is
recognizing that $G$ preserves the two-dimensional real subspace $\mathrm{span}\{|w_0\rangle,
|s\rangle\}$ — everything orthogonal to this plane is fixed by both $O$ and $D$, and inside the
plane $G$ is *exactly* a rotation matrix by angle $2\theta$. Establishing this invariance and then
tracking only the rotation angle (rather than the full vector) is the standard reduction, and the
one this mission's milestones are built around; skipping it and attempting a direct $N$-dimensional
induction does not scale.
## Formalization scope
Works over a general $N:\mathbb N$ together with a marked index $w_0 : \mathrm{Fin}\,N$ — no
assumption that $N$ is a power of two, since the rotation argument is agnostic to how the $N$ basis
states are physically encoded into qubits (that encoding is a separate, unrelated concern from the
search dynamics proved here). Supplying `w0 : Fin N` already forces $N \ge 1$; no separate
nonemptiness hypothesis is added. The oracle and diffusion operators are built directly from
Mathlib's `InnerProductSpace.rankOne` rather than an ad-hoc pointwise definition, so their
reflection structure (and hence unitarity) is visible from the definition itself. A trivializing
formalization is ruled out explicitly: the goal is stated as an existential over $k$ rather than a
fixed closed-form iteration count, so a correct proof must still exhibit a genuine successful $k$
and establish the bound — it cannot be discharged by an unrelated or degenerate choice. Contributions
extending this to multiple marked items, or proving the matching $\Omega(\sqrt N)$ lower bound
(Bennett–Bernstein–Brassard–Vazirani 1997), are welcome as follow-up missions.
## Selected references
- L. K. Grover, *A fast quantum mechanical algorithm for database search*, STOC 1996.
https://arxiv.org/abs/quant-ph/9605043
- M. A. Nielsen and I. L. Chuang, *Quantum Computation and Quantum Information*, Cambridge
University Press, 2000, Section 6.1.
- C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, *Strengths and Weaknesses of Quantum
Computing*, SIAM J. Comput. 26 (1997). https://arxiv.org/abs/quant-ph/9701001
The Power Method for Eigenvalue ComputationResearch Paper
## Motivation
Finding the eigenvalues of a large matrix or linear operator by computing its characteristic
polynomial is numerically unworkable: the roots of a degree-$n$ polynomial are exponentially
sensitive to small coefficient perturbations, and no closed-form root formula exists once
$n\ge5$. The **power method** avoids the polynomial entirely. Introduced in essentially its
modern form by Müntz (1913) and von Mises and Pollaczek-Geiringer (1929), and analyzed
rigorously alongside its shifted and inverse variants throughout the mid-20th century
(Wilkinson, *The Algebraic Eigenvalue Problem*, 1965), it remains, in the guise of one power
iteration per step, the engine inside PageRank, spectral clustering, and the Lanczos/Arnoldi
methods used to find eigenpairs of matrices too large to diagonalize directly.
## Setting
Let $E$ be a finite-dimensional inner product space over $\mathbb{k}\in\{\mathbb{R},\mathbb{C}\}$,
with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $T:E\to E$ be a
**self-adjoint** (symmetric) linear operator: $\langle Tx,y\rangle=\langle x,Ty\rangle$ for all
$x,y\in E$. The spectral theorem for finite-dimensional self-adjoint operators gives an
orthonormal basis $e_0,\dots,e_{n-1}$ of $E$ ($n=\dim E$) consisting of eigenvectors of $T$,
with real eigenvalues $\lambda_0,\dots,\lambda_{n-1}$ satisfying $Te_i=\lambda_ie_i$.
Call $\lambda_{i_0}$ **dominant** if $|\lambda_j|<|\lambda_{i_0}|$ for every $j\neq i_0$ — it is
then the unique eigenvalue of largest magnitude. Given a starting vector $x_0\in E$ with
coordinates $x_0=\sum_ic_ie_i$ in the eigenbasis, the power iterates are $T^kx_0$ for
$k=0,1,2,\dots$, and the **Rayleigh quotient** of $T$ at a nonzero vector $x$ is
$$R_T(x)=\frac{\operatorname{Re}\langle x,Tx\rangle}{\|x\|^2},$$
which recovers $\lambda_i$ exactly when $x$ is the eigenvector $e_i$.
## Formalization targets
### Iterate expansion $$T^kx_0=\sum_i\bigl(c_i\lambda_i^{\,k}\bigr)\,e_i$$
Rewriting the $k$-th power iterate in the eigenbasis: applying $T$ $k$ times raises each
coordinate's eigenvalue factor to the $k$-th power, since $T$ acts diagonally on the
eigenbasis. This is the algebraic core the rest of the argument rescales and takes limits of.
### Rescaled convergence $$\lambda_{i_0}^{-k}\,T^kx_0\;\longrightarrow\;c_{i_0}\,e_{i_0}\quad(k\to\infty)$$
Given a dominant eigenvalue $\lambda_{i_0}\neq0$ and $c_{i_0}\neq0$, dividing the expansion above
by $\lambda_{i_0}^k$ leaves the $i_0$-th term fixed at $c_{i_0}e_{i_0}$ while every other term is
multiplied by $(\lambda_j/\lambda_{i_0})^k\to0$, since $|\lambda_j/\lambda_{i_0}|<1$ for $j\neq
i_0$. This is the precise sense in which the power iterates "align" with the dominant
eigenvector.
### Goal — Rayleigh quotient convergence $$R_T\bigl(T^kx_0\bigr)\;\longrightarrow\;\lambda_{i_0}\quad(k\to\infty)$$
The practical output of the power method: the Rayleigh quotient of the (unrescaled) iterates
converges to the dominant eigenvalue itself, giving a numerically computable estimator that
needs no knowledge of $\lambda_{i_0}$ in advance. This is the weakest statement that captures
"the power method converges to the dominant eigenvalue" without hard-coding a convergence rate,
so it is the mission's goal.
## Significance
The power method is the template every practical large-scale eigenvalue algorithm departs from:
shifted inverse iteration, Rayleigh quotient iteration (with locally cubic convergence), the
QR algorithm, and Krylov subspace methods (Lanczos, Arnoldi) all begin from the same
diagonal-power argument formalized here, then add a trick — a shift, a change of subspace, an
orthogonalization step — to accelerate or extend it. The result itself is classical and
completely settled mathematically; there is no open question in the convergence theory of the
basic power method under the dominant-eigenvalue hypothesis used here. What this mission
contributes is a **machine-checked** version of that classical argument built directly on
Mathlib's existing finite-dimensional spectral theorem
(`LinearMap.IsSymmetric.eigenvalues`/`eigenvectorBasis`) — as of this writing, Mathlib's
InnerProductSpace/Spectrum.lean and Rayleigh.lean files contain the spectral decomposition
itself, and a Rayleigh quotient for `ContinuousLinearMap`, but not this convergence statement.
## Difficulty
The obvious first attempt is to bound $\|T^kx_0-\lambda_{i_0}^kc_{i_0}e_{i_0}\|$ by a naive
sum of norms and take limits termwise; this works for the *rescaled* sequence (Milestone 2) but
does not by itself give the Rayleigh-quotient limit, because $R_T$ is invariant only under
*nonzero* scalar rescaling, not under limits taken carelessly — one has to first establish that
the limit vector $c_{i_0}e_{i_0}$ is nonzero (using $c_{i_0}\neq0$), then invoke continuity of
$R_T$ away from $0$ to transport the `Tendsto` from the rescaled sequence to
$R_T(T^kx_0)=R_T(\lambda_{i_0}^{-k}T^kx_0)$. Getting the degenerate case $n=1$ right is the
other trap: with only one eigenvalue, the dominance hypothesis is vacuous, and if that
eigenvalue is allowed to be $0$ the rescaling $\lambda_{i_0}^{-k}$ divides by zero and the
rescaled-convergence statement becomes false — the formalization must therefore assume
$\lambda_{i_0}\neq0$ explicitly rather than deriving it from dominance alone.
## Formalization scope
The mission works with a general `RCLike 𝕜` field (real or complex $E$), a `LinearMap.IsSymmetric`
operator on a `FiniteDimensional` inner product space, and Mathlib's own `eigenvalues`/
`eigenvectorBasis` (which already fixes the eigenbasis and a specific, decreasing-by-value
ordering of eigenvalues — the formalization does not re-derive the spectral theorem). Dominance
is stated by magnitude (`|\lambda_j| < |\lambda_{i_0}|`), not by position in Mathlib's ordering,
since the dominant eigenvalue need not be the largest by value (it could be the most negative).
The starting vector $x_0$ is arbitrary subject to $c_{i_0}\neq0$; no normalization ($\|x_0\|=1$)
is imposed, since the Rayleigh quotient and the rescaled limit are both scale-invariant/
scale-equivariant. A trivializing formalization is ruled out explicitly: without both
$\lambda_{i_0}\neq0$ and $c_{i_0}\neq0$, the $n=1$, $T=0$ counterexample above makes the
rescaled-convergence statement false, so these are load-bearing hypotheses, not decoration.
Contributions on the two milestones (the algebraic iterate expansion, and the rescaled-limit
argument) are especially welcome, since they are reusable building blocks for any future mission
on shifted/inverse power iteration or Rayleigh quotient iteration.
## Selected references
- R. von Mises and H. Pollaczek-Geiringer, *Praktische Verfahren der Gleichungsauflösung*,
ZAMM, 1929.
- J. H. Wilkinson, *The Algebraic Eigenvalue Problem*, Oxford University Press, 1965.
- L. N. Trefethen and D. Bau III, *Numerical Linear Algebra*, SIAM, 1997 (Lecture 27: the power
method).
## Motivation
How short can a code for a data source be, if the code must still be uniquely decodable — if every string of concatenated codewords can be unambiguously split back into the original symbols? Shannon's 1948 source coding theorem answers this exactly: the entropy of the source is a hard lower bound on the average codeword length of *any* uniquely decodable code, and it is also achievable up to a one-symbol slack. Entropy is not just a measure of "average surprise" — it is the literal, tight answer to a combinatorial question about how densely symbols can be packed into strings without losing decodability. This is the theorem that gives Shannon's entropy its operational meaning, and it underlies every practical lossless compression scheme (Huffman coding, arithmetic coding, Lempel–Ziv) as the benchmark they approach.
**Timeline.**
- 1948 — Claude Shannon, "A Mathematical Theory of Communication" (*Bell System Technical Journal*), introduces entropy and proves the source coding theorem.
- 1949 — Leon Kraft's MIT master's thesis proves the combinatorial inequality (for prefix codes) that makes the theorem's achievability half constructive.
- 1956 — Brockway McMillan extends Kraft's inequality's necessity direction from prefix codes to the strictly larger class of *uniquely decodable* codes, giving the theorem its full generality.
## Setting
A source has a finite alphabet of symbols $\iota$, with at least two symbols, and probability distribution $p:\iota\to\mathbb R$ ($p_i>0$, $\sum_i p_i=1$). A code assigns to each symbol $i$ a codeword $c(i)$, a finite string over a $D$-ary code alphabet $\alpha$ ($D=|\alpha|\ge 2$); the code is *uniquely decodable* if every finite sequence of codewords is determined by its concatenation. The **entropy** of $p$ in base $D$ is
$$H_D(p) = -\sum_i p_i \log_D p_i.$$
The **expected codeword length** of $c$ under $p$ is $L(c) = \sum_i p_i \, |c(i)|$.
## Formalization targets
### Goal — Shannon's source coding theorem
$$\forall \text{ injective, uniquely decodable } c,\quad H_D(p) \le L(c), \qquad \exists \text{ such } c,\quad L(c) < H_D(p) + 1.$$
(For a source with $|\iota| \ge 2$ symbols — see *Formalization scope* for why the single-symbol case must be excluded.)
## Significance
**The result itself.** This theorem is the reason entropy is called entropy in an information-theoretic sense at all: it converts a quantity defined by an abstract formula ($-\sum p_i\log p_i$) into the exact answer to an operational question (minimum achievable expected code length), with a slack no worse than one symbol. It is the founding theorem of lossless source coding and the benchmark every practical compressor is measured against.
**Formalizing it.** Mathlib recently gained genuine information-theoretic coding content: `InformationTheory.UniquelyDecodable` and the *necessity* direction of the Kraft–McMillan inequality (McMillan's 1956 result: a uniquely decodable code's lengths satisfy $\sum_w D^{-|w|}\le 1$) are already proved, via a counting argument on concatenations of $r$ codewords. This mission builds directly on that foundation rather than duplicating it. What Mathlib does **not** have — and what this mission's milestones supply — is Kraft's original 1949 *sufficiency* direction (existence of a uniquely decodable code realizing any length assignment satisfying the Kraft sum bound), any notion of Shannon entropy for a general finite distribution, and the source coding theorem itself.
## Difficulty
The lower bound ($H_D(p)\le L(c)$) is the easier half: it follows from the Kraft–McMillan inequality (already in Mathlib) via Gibbs'/Jensen's inequality applied to the two probability-like sequences $p_i$ and $D^{-\ell_i}/K$ (where $K=\sum_j D^{-\ell_j}\le1$ is the Kraft sum) — a short, self-contained convexity argument.
The achievability half is the genuine construction. Given the ideal (generally non-integer) lengths $-\log_D p_i$, one rounds up to $\ell_i=\lceil -\log_D p_i\rceil$ (Shannon–Fano–Elias lengths); a one-line estimate shows $D^{-\ell_i}\le p_i$, so the Kraft sum of the rounded lengths is still $\le\sum_i p_i=1$, and the bound $\ell_i<-\log_D p_i+1$ gives $L(c)<H_D(p)+1$ immediately once a code with exactly these lengths is shown to exist. Producing that code is Kraft's sufficiency direction, and it needs an explicit construction: order the lengths, and assign to symbol $i$ the first $\ell_i$ digits of the $D$-ary expansion of the cumulative sum $\sum_{j<i} D^{-\ell_j}$. Verifying this assignment is injective, has the prescribed lengths, and is uniquely decodable (indeed prefix-free) is a careful but standard combinatorial argument — the main open piece of this mission.
## Formalization scope
The source alphabet $\iota$ must have at least two symbols ($|\iota|\ge 2$), not merely be nonempty. A single-symbol source forces $p\equiv 1$ and entropy $H_D(p)=0$, so the achievability conjunct would demand a codeword of length $0$ — but a uniquely decodable code can never contain the empty codeword (`InformationTheory.UniquelyDecodable.epsilon_not_mem`, provable from the definition: the empty string decodes ambiguously as zero or two copies of itself), so no admissible code exists and the theorem would be **false**, not merely hard, at $|\iota|=1$. The same defect breaks Kraft's sufficiency direction (Milestone 2) whenever *any* prescribed length is $0$, independent of $|\iota|$; that milestone accordingly requires every length strictly positive. With $|\iota|\ge2$ and full support, every $p_i<1$ strictly, so the Shannon–Fano lengths $\lceil-\log_D p_i\rceil$ are automatically all $\ge1$, and the achievability construction only ever needs Milestone 2 at positive lengths. The code alphabet $\alpha$ is likewise an arbitrary finite type (matching Mathlib's own `Fintype`/`Nonempty` conventions for the Kraft–McMillan file), with $|\alpha|\ge2$ required to keep `Real.logb` non-degenerate. The source distribution is required strictly positive ($p_i>0$) — the standard simplifying assumption (zero-probability symbols can always be dropped without loss). Unique decodability is stated exactly as Mathlib's `InformationTheory.UniquelyDecodable`, not re-derived from a "prefix code" definition, so the mission's results transport directly onto Mathlib's existing Kraft–McMillan file. A trivializing route to rule out: proving only the lower bound (citing Mathlib's inequality) while leaving the existential achievability half unaddressed would not be Shannon's theorem — the sandwich $H_D(p)\le L^*<H_D(p)+1$ is the theorem's actual content, and the lower bound alone (already essentially free from Mathlib) is not a novel contribution on its own.
Reusable output: the Kraft sufficiency construction (Milestone 2) is directly reusable for any future formalization of Huffman coding optimality, arithmetic coding, or the general "Kraft-inequality-achieving code exists" fact used throughout coding theory. Contributions are welcome starting from Milestone 2 (the open construction) or Milestone 3 (the Gibbs'-inequality lower bound, which only needs Milestone 1, already available via Mathlib).
## Selected references
- C. E. Shannon, "A Mathematical Theory of Communication," *The Bell System Technical Journal* 27 (1948), 379–423, 623–656.
- T. M. Cover and J. A. Thomas, *Elements of Information Theory*, 2nd ed., Wiley, 2006, Chapter 5 ("Data Compression"), §5.2 ("Kraft Inequality") and §5.4 ("Bounds on the Optimal Code Length," Theorem 5.4.1).
- L. G. Kraft, *A Device for Quantizing, Grouping, and Coding Amplitude-Modulated Pulses*, M.S. thesis, MIT, 1949.
- B. McMillan, "Two Inequalities Implied by Unique Decipherability," *IRE Transactions on Information Theory* 2:4 (1956), 115–116.
- Mathlib, `Mathlib.InformationTheory.Coding.UniquelyDecodable` and `Mathlib.InformationTheory.Coding.KraftMcMillan` (2026).
## Motivation and history
The **Collatz conjecture**, also called the **$3x+1$ problem**, asks whether one elementary
iteration rule has the same long-term behavior for every positive integer. It belongs to
number theory and discrete dynamical systems: the rule is deterministic and trivial to
compute for any fixed input, but no argument is known that controls every orbit. The problem
has served as a test case for methods involving congruences, stopping times, probabilistic
models, computation, and arithmetic dynamics. Jeffrey Lagarias's survey, *The $3x+1$ Problem
and Its Generalizations*, organized much of the classical theory and explains why strong
results about large classes of starting values do not settle the universal statement
([Lagarias 1985](https://websites.umich.edu/~lagarias/3x%2B1.html)).
The problem has a long record of partial results. By 1985, the literature already included
results on stopping-time densities, possible cycles, and divergent trajectories, summarized
by Lagarias. In 2019, Terence Tao proved that for every function $f(N)$ tending to infinity,
the minimum value attained by the orbit of $N$ is at most $f(N)$ for almost all positive
integers $N$, where “almost all” is measured using logarithmic density
([Tao 2019](https://arxiv.org/abs/1909.03562)). This is a strong statement about typical
orbits, but it does not cover every starting value. Computational verification has also been
pushed to very large finite ranges; David Barina describes algorithms and verification
methods for this task in *Convergence Verification of the Collatz Problem*
([Barina 2021](https://doi.org/10.1007/s11227-020-03368-x)). A finite verification bound,
regardless of size, leaves all larger starting values outside its scope.
## Setting
For a natural number $n$, define the **Collatz step** $C(n)$ by
$$
C(n)=
\begin{cases}
n/2, & \text{if } n \text{ is even},\\
3n+1, & \text{if } n \text{ is odd}.
\end{cases}
$$
Write $C^m(n)$ for the result of applying $C$ exactly $m$ times, with $C^0(n)=n$.
The forward orbit of $n$ is therefore
$$
n,\ C(n),\ C^2(n),\ C^3(n),\ldots.
$$
The familiar orbit beginning at $6$, for example, starts
$6,3,10,5,16,8,4,2,1$. Reaching $1$ is the relevant event; after that point the
usual map continues around the cycle $1,4,2,1$.
## Formalization target
The mission goal is the universal assertion
$$
\forall n\in\mathbb N,\quad n>0\Longrightarrow
\exists m\in\mathbb N,\quad C^m(n)=1.
$$
The existential index $m$ may be zero, so the case $n=1$ is included directly. The
hypothesis $n>0$ excludes $0$, whose behavior under the total natural-number definition of
$C$ is irrelevant to the conjecture.
The goal is the existing public prove2.me theorem `collatz_conjecture`, rather than a new
copy. Its statement follows the Collatz declaration in the
[Formal Conjectures collection](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean).
## Significance
A proof would classify every positive-integer orbit with respect to reaching $1$. It would
simultaneously rule out an orbit that escapes forever without visiting $1$ and any nontrivial
cycle disjoint from $1$. Partial density results and finite computations establish neither
universal exclusion.
The formalization goal is to make the universal quantifiers, parity split, finite iteration,
and boundary cases explicit in Lean 4. Supporting contributions can isolate reusable facts
about iterates, stopping times, accelerated odd-only maps, residue classes, and finite
certificates. Such components may also support formal work on related piecewise-affine
integer dynamical systems, while every contribution remains tied to a precisely stated
theorem.
## Difficulty
Individual trajectories can be computed, and many families of inputs can be reduced by
elementary parity arguments, but the map combines contraction and expansion. Even steps
halve the current value, while odd steps replace it by the larger value $3n+1$. Local
information about a bounded initial segment of an orbit does not supply a uniform bound on
all later values or on the time required to reach $1$.
Statistical control of most inputs also leaves exceptional inputs unresolved. Likewise,
excluding cycles up to a finite length does not exclude longer cycles, and checking all
inputs below a finite threshold does not constrain every larger input. The mission therefore
requires statements whose quantifiers genuinely cover all positive natural numbers; a large
finite computation or an almost-everywhere theorem cannot by itself close the goal.
## Formalization scope
The existing Lean statement works over `ℕ`. Its local `collatzStep` definition branches on
the proposition that $n$ is even, uses natural-number division by $2$ on the even branch,
and uses $3n+1$ on the odd branch. Iteration is represented by the standard finite function
iterate notation. The theorem quantifies over a positive starting value $n$ and asserts the
existence of a finite iterate index $m$ at which the value is exactly $1$.
The positivity hypothesis is essential: the total function sends $0$ to $0$, so including
$0$ would make the universal statement false. The mission does not replace the universal
quantifier by a fixed numerical bound, and it does not encode a predetermined stopping-time
limit. A complete solution must account for every positive starting value.
Useful supporting formalizations include exact relations between the classical and
accelerated maps, composition laws for finite iteration, stopping-time predicates, cycle
exclusion statements, descent criteria, and checked finite ranges. Each supporting theorem
should state its own hypotheses and trust boundary explicitly. Computational artifacts are
welcome when their finite scope is stated precisely and their result is connected to a Lean
consumer through a checked certificate or another accepted verification boundary.
## Selected references
- Jeffrey C. Lagarias, *The $3x+1$ Problem and Its Generalizations*, American Mathematical
Monthly 92 (1985), 3–23. https://websites.umich.edu/~lagarias/3x%2B1.html
- Terence Tao, *Almost All Orbits of the Collatz Map Attain Almost Bounded Values*, 2019;
published in Forum of Mathematics, Pi 10 (2022). https://arxiv.org/abs/1909.03562
- David Barina, *Convergence Verification of the Collatz Problem*, The Journal of
Supercomputing 77 (2021), 2681–2688. https://doi.org/10.1007/s11227-020-03368-x
- Google DeepMind, *Formal Conjectures: Collatz Conjecture*, Lean 4 statement.
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean
Formalization of the Poincaré ConjectureResearch Paper
**Our goal**
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's [Notes on Perelman's Papers](https://arxiv.org/abs/math/0605667).
**Important references**
[Poincare-Conjecture](https://github.com/frenzymath/Poincare-Conjecture) and [DifferentialGeometry](https://github.com/qinz1yang/differential-geometry) are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
**OpenGA's role**
[OpenGA](https://github.com/MathNetwork/OpenGA) focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The `PoincareConjecture` directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.
Dynamic Programming and Optimal Control IV: LQR and the Riccati EquationTextbook
## Motivation
The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.
## Setting
Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (`BertsekasRiccatiMap`)
$$F(P) = A^\top\big(P - P B (B^\top P B + R)^{-1} B^\top P\big) A + Q.$$
$(A,B)$ is **controllable** if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (`BertsekasControllablePair`); $(A,C)$ is **observable** if $(A^\top, C^\top)$ is controllable (`BertsekasObservablePair`). Separately, $g : \mathbb{R} \to \mathbb{R}$ is **$K$-convex** (`BertsekasKConvex`, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.
## Target
$$\exists\, P \succ 0:\quad F(P) = P,\quad P \text{ unique among } P' \succeq 0,\quad F^{k}(P_0) \to P \ \ \forall P_0 \succeq 0,\quad \rho\big(A + BL\big) < 1,$$
with $L = -(B^\top P B + R)^{-1} B^\top P A$ — `BertsekasDP.riccati_convergence_stability` (goal). Milestones: Lemma 4.2.1(a)–(d) (`kconvex_of_convex`, `kconvex_combination`, `kconvex_expectation`, `kconvex_sS_structure`), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.
## Significance
The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.
## Difficulty
The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.
## Formalization scope
Real matrices over `Fin n`; `Matrix.PosSemidef`/`PosDef`; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via `spectrum ℂ` of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
- R. E. Kalman, Contributions to the theory of optimal control, *Bol. Soc. Mat. Mexicana* 5 (1960), 102–119.
- H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in *Mathematical Methods in the Social Sciences*, Stanford Univ. Press, 1960.
Capped Base-Stock Policies: A 2.33-ApproximationResearch Paper
## A performance guarantee for a simple replenishment rule
When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.
**Capped base-stock policies** combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by [Xin (2021)](https://doi.org/10.1287/opre.2020.2019). The present target is the finite-lead-time guarantee in Linwei Xin's *Capped Base-Stock Policies: A 2.33-Approximation*, specifically the author-supplied manuscript with source label `thm-main`. A [public listing of the paper](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538) identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.
## Demand, stock, and delayed orders
Periods are discrete. **Demand** is a sequence of independent, identically distributed nonnegative real random variables $D_t$ with finite, strictly positive mean $\mu$. The deterministic **lead time** is an integer $L\ge1$. Holding and lost-sales rates are $h>0$ and $p>0$.
At the beginning of period $t$, $I_t$ is on-hand inventory and $x_{1,t},\ldots,x_{L,t}$ are outstanding orders, with $x_{1,t}$ due immediately. That arrival is received, an order $q_t\ge0$ is placed, demand is realized, and costs are charged. The new order arrives $L$ periods later. The equations are
$$I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad x_{i,t+1}=x_{i+1,t}\ (i<L),\qquad x_{L,t+1}=q_t.$$
Here $u^+=\max\{u,0\}$. Unfilled demand is lost rather than backlogged. With $\ell_t=(D_t-I_t-x_{1,t})^+$, the period cost is $hI_{t+1}+p\ell_t$. Initial inventory and every pipeline coordinate are zero. A **nonanticipative policy** chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.
For a policy $\pi$, its **long-run expected average cost** is
$$C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[hI_{t+1}^\pi+p\ell_t^\pi],\qquad \mathrm{OPT}=\inf_{\pi\in\Pi}C(\pi).$$
The capped rule is $q_t=\min\{(S-I_t-\sum_{i=1}^Lx_{i,t})^+,r\}$ for finite $S,r\ge0$. Write $C^*_{\rm CBS}=\inf_{S,r\ge0}C(\pi_{S,r})$. Ordinary base stock is already included by taking $r=S$; no infinite order cap is required.
## Formalization targets
For $0\le r\le\mu$ and $m\ge1$, set
$$I_r^m=\max_{0\le k\le m}\sum_{i=1}^k(r-D_i),\qquad G_m(r,z)=\mathbb E\left[\left(I_r^m+\sum_{i=1}^m(D_i-r)-z\right)^+\right].$$
Empty sums are zero. The **lower certificate** is
$$\underline C=\inf\{hz+p(\mu-r):0\le r\le\mu,\ z\ge0,\ G_L(r,z)\le L(\mu-r),\ G_{L+1}(r,z)\le(L+1)(\mu-r)\}.$$
The pair $(0,0)$ is feasible. Both horizon constraints are retained. With
$$\kappa_L=1+\frac{4L^2}{(L+1)(3L-1)},$$
the goal is Theorem 1's complete assertion:
$$C^*_{\rm CBS}\le\kappa_L\underline C,\qquad C^*_{\rm CBS}\le\kappa_L\mathrm{OPT}\le\frac73\mathrm{OPT}.$$
The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.
Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly $(S,r)=((L+1)r+z,r)$ and $S=(L+1)r+2z$, respectively. Labels accompany the printed numbering so the supplied source is unambiguous.
## What completing the mission establishes
The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At $L=1$ the displayed coefficient is 2, while its uniform upper bound is $7/3$.
The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.
## Where the formal work lies
The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including [Xin and Goldberg (2016)](https://doi.org/10.1287/opre.2016.1514), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.
The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.
## Formalization scope and conventions
Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.
Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.
Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.
## Selected references
- Linwei Xin, *Capped Base-Stock Policies: A 2.33-Approximation*, working paper, 2026. [SSRN listing](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538). Author-supplied LaTeX is authoritative: Theorem 1 (`thm-main`), Proposition 1 (`lemma-lb`), Proposition 2 (`prop-finite-cap-bound`), Lemma 2 (`lem-greedy-window`), Proposition 3 (`prop-base-stock-bound`), Proposition 4 (`lem-two-branch`). Source SHA-256: `f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a`.
- Linwei Xin, *Technical Note—Understanding the Performance of Capped Base-Stock Policies in Lost-Sales Inventory Models*, Operations Research 69(1), 61–70, 2021. [DOI](https://doi.org/10.1287/opre.2020.2019).
- Linwei Xin and David A. Goldberg, *Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models*, Operations Research 64(6), 1556–1565, 2016. [DOI](https://doi.org/10.1287/opre.2016.1514).
## Motivation
Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a **magic state**, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the **stabilizer rank** -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few *unconditional* obstructions to classical simulation available at all.
A timeline of what is established for the standard magic state $|H\rangle$:
- **2016.** Bravyi, Smith and Smolin exhibit a decomposition giving $\chi(|H^{\otimes 6}\rangle)\le 7$, hence $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468n}$, and prove a lower bound of order $\sqrt{n}$.
- **2020.** Huang, Newman and Szegedy show that hardness assumptions stronger than $\mathrm{P}\neq\mathrm{NP}$, such as the exponential time hypothesis, imply $\chi(|H^{\otimes n}\rangle)=2^{\Omega(n)}$ ([arXiv link](https://doi.org/10.1109/TIT.2020.3004427)).
- **2022.** Peleg, Shpilka and Volk improve the unconditional lower bound to $\Omega(n)$ and give the first non-trivial bound for the approximate rank ([arXiv:2106.03214](https://arxiv.org/abs/2106.03214)).
- **2024.** A quadratic lower bound is obtained for the approximate stabilizer rank ([arXiv:2305.10277](https://arxiv.org/abs/2305.10277)).
Between the linear unconditional lower bound and the $2^{0.468n}$ upper bound lies the open problem this mission targets.
## Setting
Index the computational basis of an $n$-qubit system by bit strings $x\in\{0,1\}^n$, so a state is a vector $\psi\in\mathbb{C}^{2^n}$ with coordinates $\psi(x)$.
The **Pauli operators** are $X^aZ^b$ for $a,b\in\{0,1\}^n$, acting by $X^aZ^b|x\rangle=(-1)^{\,b\cdot x}|x\oplus a\rangle$, where $b\cdot x$ counts the coordinates on which both are $1$ and $\oplus$ is bitwise addition; the **Pauli group** is the set of $4\cdot 4^n$ operators $i^cX^aZ^b$. A unitary $U$ is a **Clifford unitary** when $UPU^\dagger$ lies in the Pauli group for every Pauli group element $P$, and a **stabilizer state** is a vector $U|0\cdots0\rangle$ for some Clifford $U$. There are $2^n\prod_{k=1}^{n}(2^k+1)$ of them up to phase -- six for a single qubit.
The **stabilizer rank** $\chi(\psi)$ is the least $r$ admitting coefficients $c_1,\dots,c_r\in\mathbb{C}$ and stabilizer states $\varphi_1,\dots,\varphi_r$ with $\psi=\sum_{j\le r}c_j\varphi_j$.
The **magic state** is $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$, and $|H^{\otimes n}\rangle$ its $n$-fold tensor power, with coordinates $\cos(\pi/8)^{\,n-|x|}\sin(\pi/8)^{\,|x|}$ where $|x|$ is the Hamming weight of $x$.
## Target
The goal is a super-polynomial lower bound: for every exponent $d$ and constant $C$ there exists $n$ with
$$\chi\bigl(|H^{\otimes n}\rangle\bigr)\;>\;C\,n^{d},$$
equivalently, $\chi(|H^{\otimes n}\rangle)$ is not $O(n^d)$ for any fixed $d$.
Stronger statements are expected but are deliberately not the goal. An exponential bound $\chi=2^{\Omega(n)}$ is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.
## Significance
*The result itself.* A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a *polynomial* upper bound on $\chi(|H^{\otimes n}\rangle)$ would imply $\mathrm{BPP}=\mathrm{BQP}$, and via postselection $\mathrm{P}=\mathrm{NP}$. There is also a purely classical payoff -- improving the known bound even to super-*linear* would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over $\mathbb{F}_2$, resolving a separate open question.
*Formalizing it.* The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the $n$-qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.
## Difficulty
Counting settles the problem for *random* states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about $|H^{\otimes n}\rangle$, which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.
The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.
## Formalization scope
State vectors are functions $\{0,1\}^n\to\mathbb{C}$ and are **not** required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of $|0\cdots0\rangle$. The Pauli group is given by the explicit parametrisation $i^cX^aZ^b$ rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by-$H,S,\mathrm{CNOT}$ description. Because $e^{i\theta}U$ normalises the Pauli group whenever $U$ does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.
One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value $0$; if no decomposition existed the rank would be $0$ for every state and the goal would be *false* rather than merely unproved. The milestone $\chi(\psi)\le 2^n$ is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies $C$ over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive $C$.
A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.
## Selected references
- S. Peleg, A. Shpilka, B. L. Volk, *Lower Bounds on Stabilizer Rank*, Quantum 6 (2022) 652; [arXiv:2106.03214](https://arxiv.org/abs/2106.03214).
- S. Bravyi, G. Smith, J. Smolin, *Trading Classical and Quantum Computational Resources*, Phys. Rev. X 6 (2016) 021043; [arXiv:1506.01396](https://arxiv.org/abs/1506.01396).
- C. Huang, M. Newman, M. Szegedy, *Explicit Lower Bounds on Strong Quantum Simulation*, IEEE Trans. Inf. Theory 66(9) (2020) 5585--5600.
- *Quadratic Lower Bounds on the Approximate Stabilizer Rank: A Probabilistic Approach*, STOC 2024; [arXiv:2305.10277](https://arxiv.org/abs/2305.10277).
## Motivation
Quantum query algorithms are known to beat classical ones on problems with algebraic
structure -- period finding, hidden subgroups, forrelation. No such speedup is known for
a problem with no structure at all. **Aaronson and Ambainis** proposed making that
observation into a theorem, and reduced it to a question with no quantum content: a
statement about bounded low-degree polynomials on the Boolean cube
([Aaronson--Ambainis 2009](https://arxiv.org/abs/0911.0996)).
The question has resisted since. A timeline of what is actually established:
- **2009.** Aaronson and Ambainis state the conjecture and prove that it implies
almost-everywhere classical simulation of quantum query algorithms.
- **2012.** Montanaro settles the case of block-multilinear forms whose coefficients all
have the same magnitude.
- **2016.** O'Donnell and Zhao reduce the general conjecture to a restricted class,
the one-block decoupled polynomials.
- **2019.** Aaronson surveys a decade of partial progress
([retrospective](https://scottaaronson.blog/?p=4414)).
- **2022.** Bansal, Sinha and de Wolf prove the conjecture for *completely bounded*
degree-$d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at
constant variance ([arXiv:2203.00212](https://arxiv.org/abs/2203.00212)).
- **2024.** The conjecture is established for a non-negligible fraction of random
restrictions ([arXiv:2402.13952](https://arxiv.org/abs/2402.13952)).
The cases that are settled are settled under structural hypotheses -- block-multilinearity,
complete boundedness, symmetry, Boolean range. The general statement is open.
## Setting
Let $N$ be a positive integer. The **Boolean cube** is $\{0,1\}^N$, carrying the uniform
distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real
multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a
function $f$ on the cube write
$$\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).$$
The **variance** of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$.
Writing $x^{\oplus i}$ for $x$ with its $i$-th bit flipped, the **influence** of coordinate
$i$ on $p$ is
$$\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].$$
These are the combinatorial forms of both quantities, as used in the source; no
Fourier--Walsh expansion is required to state anything below. The **degree** of $p$ is its
total degree as a polynomial. Call $p$ **bounded** when $0\le p(x)\le 1$ at every cube
point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$.
## Target
The goal is the conjecture in the shape stated by its authors: there is an absolute
constant $C$ such that for all $N$, all $d$, every polynomial $p$ of degree at most $d$
that is bounded on the cube, and every $\varepsilon>0$ with
$\operatorname{Var}[p]\ge\varepsilon$, some coordinate $i$ satisfies
$$\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.$$
The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the
entire content: bounds that degrade exponentially in $d$ are already known, and a goal
naming a specific exponent would be superseded by the next improvement.
## Significance
*The result itself.* Aaronson and Ambainis prove that the conjecture implies that the
acceptance probability of any bounded-error $T$-query quantum algorithm on a Boolean input
can be approximated, to small error on all but a small fraction of inputs, by a classical
algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure
in a precise sense. The conjecture also has purely classical content, asserting that
boundedness plus low degree forces variance to concentrate on some single coordinate rather
than spread across all $N$. Without it, no such concentration is known at any rate
polynomial in $1/d$.
*Formalizing it.* The conjecture is open, so this mission does not formalize a known proof
of the goal. What it produces is a machine-checked statement of the conjecture together with
formalizations of the partial results above, each currently existing only on paper. The
milestone chain also yields reusable infrastructure for analysis of Boolean functions, of
which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no
variance on the cube.
## Difficulty
The elementary bound is the Poincare inequality on the cube,
$4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$, which yields a coordinate with
influence at least $4\varepsilon/N$. This is tight for the dictator $p(x)=x_1$ and depends
on $N$, so it says nothing: the conjecture demands a bound free of $N$ entirely.
The natural repair is the route available when $p$ takes only the values $0$ and $1$. A
Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which
immediately produces an influential one. That argument does not survive relaxing the range
to the interval $[0,1]$: a bounded real-valued polynomial of low degree need not depend on
boundedly many coordinates, and every known substitute loses a factor exponential in $d$.
Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and
it is where all of the partial results stop.
## Formalization scope
Polynomials are `MvPolynomial (Fin N) ℝ` and degree is Mathlib's `totalDegree`, so the
statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$
rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping
is `Function.update x i (!x i)`. Boundedness is asserted at cube points only. Variance and
influence are the combinatorial definitions above, published as the definition
`AaronsonAmbainis`.
Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as
an existentially quantified natural number with no leading multiplicative constant, since
admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at
least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the
bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The
hypothesis $\deg p\le d$ is universally quantified over $d$, which is equivalent to the
source's exact-degree form because the smallest admissible $d$ gives the strongest
conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$
fails for a constant polynomial.
A complete development needs, beyond the published definitions, a Fourier--Walsh layer with
Parseval's identity, the level-$k$ machinery used by the partial results, and -- for the
completely bounded case -- operator-space norms on multilinear forms. All of the
Boolean-analysis material is reusable well beyond this mission. Contributions of any
milestone are welcome, as are alternative formalizations of the definitions in
function-level rather than polynomial-level form.
Out of scope: the quantum simulation consequence is not formalized here. Stating it requires
a formal quantum query model, which no Lean library currently provides.
## Selected references
- S. Aaronson, A. Ambainis, *The Need for Structure in Quantum Speedups*, Theory of Computing 10 (2014) 133--166; [arXiv:0911.0996](https://arxiv.org/abs/0911.0996). Conjecture 6.
- N. Bansal, M. Sinha, R. de Wolf, *Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms*, CCC 2022; [arXiv:2203.00212](https://arxiv.org/abs/2203.00212).
- *Aaronson--Ambainis Conjecture Is True For Random Restrictions*, 2024; [arXiv:2402.13952](https://arxiv.org/abs/2402.13952).
- S. Aaronson, *The Aaronson-Ambainis Conjecture (2008-2019)*, [blog retrospective](https://scottaaronson.blog/?p=4414).
- S. Arunachalam, J. Briet, C. Palazuelos, *Quantum query algorithms are completely bounded forms*, SIAM J. Comput. 48 (2019); [arXiv:1711.07285](https://arxiv.org/abs/1711.07285).
- AIM problem list, *Analysis on the hypercube with applications to quantum computing*, [aimpl.org/hypercubequantum](http://aimpl.org/hypercubequantum/1/).