Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.996001Formalized record

3 provers on it4 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.996001Formalized record

3 provers on it4 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Algebraic Topology Pure Mathematics·Captain: korbonits

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) 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:

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;
two path-connected covering spaces with basepoints are isomorphic by a basepoint-preserving isomorphism iff their subgroups coincide;
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

Proposition 1.31 (p. 61), first part: $p_*$ is injective.
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.
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$ .
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$ .
Proposition 1.34 (p. 62), unique lifting: two lifts of $f:Y\to X$ agreeing at one point agree everywhere if $Y$ is connected.
Necessity of semilocal simple connectivity (p. 63): if $X$ has a simply-connected covering space (surjective onto $X$ ), then $X$ is semilocally simply-connected.
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).
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.
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.
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.
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.
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$ .
Proposition 1.39, final clause: for the universal cover, $G(\tilde X)\cong\pi_1(X,x_0)$ .
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.
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)$ .
Proposition 1.40(c): if $Y$ is path-connected and locally path-connected, $G\cong\pi_1(Y/G)/p_*\pi_1(Y)$ , given as a surjective homomorphism $\pi_1(Y/G)\to G$ with kernel $p_*\pi_1(Y)$ .

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

18 thms1 active userReviewed

Completed

Algebraic Topology Pure Mathematics·Captain: korbonits

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) 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

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$ .
Proposition 1.14 (p. 35). $\pi_1(S^n)=0$ for $n\ge 2$ .
Theorem 1.20, first part (p. 43). Under the hypotheses of Lemma 1.15, $\Phi$ is surjective.
The kernel contains the relators (p. 43). $N\le\ker\Phi$ , with no hypotheses on the cover.
Theorem 1.20, second part (p. 43). If moreover every triple intersection is path-connected, $\ker\Phi\le N$ .
Induced isomorphism (p. 43). Under the same hypotheses there is an isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ sending the class of a word to its image under $\Phi$ .

Significance

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

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

Difficulty

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

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

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

Formalization scope

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

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

Selected references

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

8 thms1 active userReviewed

Completed

Harmonic Analysis Mathematical Physics Probability·Captain: lisamegawatts

Finite Reflection Positivity Methods I: Split Weights and Infrared ModesTextbook

Motivation

Reflection positivity and infrared bounds form a standard finite-volume route from the geometry of a lattice reflection to quantitative control of long wavelength fluctuations. In the classical argument, reflection positivity supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier diagonalization of the lattice Laplacian identifies the free covariance used in the infrared comparison. These ingredients underlie rigorous results on continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's development of infrared bounds and spontaneous symmetry breaking (1976), and the general theory of reflection positivity developed by Fröhlich, Israel, Lieb, and Simon (1978). Related technology appears in Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems and Coulomb gas (1981).

The analytic and model-specific theorems are substantial, but their finite algebraic interface is sharply separable. This mission isolates that interface so later clock, XY, and Gaussian-domination developments can share one checked notion of reflection, one spectral covariance convention, and one treatment of the constant mode.

Setting

Let $X$ be a finite set of configurations on one side of a reflection plane. A full split configuration is a pair $(x,y)\in X\times X$ , and reflection exchanges its two entries. A plus-half observable is a function $F:X\to \mathbb R$ lifted to $X\times X$ through the first coordinate. Its reflected copy therefore depends on the second coordinate.

A split weight is specified by a finite feature index $A$ , real coefficients $c_a$ , and features $\phi_a:X\to\mathbb R$ :

W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y).

For a finite family of plus-half observables $F_i$ , the reflected kernel is

K_{ij}=\sum_{(x,y)\in X\times X} W(x,y)F_i(x)F_j(y).

A real matrix is positive semidefinite here when it is symmetric and its quadratic form is nonnegative on every real coordinate vector.

The spectral side uses a finite mode set $I$ with a distinguished zero mode $0$ . An infrared spectrum consists of a function $\lambda:I\to\mathbb R$ that is nonnegative and vanishes exactly at $0$ . For $\beta>0$ , the free mode covariance is diagonal, equals zero at the constant mode, and has entry

G_{kk}=\frac{1}{\beta\lambda_k}

away from zero. Covariance domination is tested only on source vectors whose zero-mode coordinate vanishes. The concrete spectral fixture is the $4\times4$ periodic square lattice, with tensor-product discrete Fourier modes and the nearest-neighbor graph Laplacian.

Formalization targets

Finite reflection positivity

The first target identifies the split reflection pairing with the explicit double sum over the two halves. Under $c_a\ge0$ , the resulting reflected kernel must be positive semidefinite:

\sum_{i,j}u_iK_{ij}u_j\ge0.

Every such kernel must satisfy the two-observable chessboard inequality

K_{ij}^{2}\le K_{ii}K_{jj}.

Typed finite spectrum

For every Torus-4 frequency $k$ and site $x$ , the registered Fourier mode $\psi_k$ must satisfy the pointwise eigenvalue equation

(\Delta_{\mathrm{T4}}\psi_k)(x)=\lambda_k\psi_k(x).

The eigenvalues must be nonnegative and vanish exactly at the constant mode, and these laws must be packaged as the same spectrum type consumed by the infrared definitions.

Zero-mode-restricted infrared bound

The diagonal free covariance must be positive semidefinite for $\beta>0$ . If an interacting covariance $C$ is quadratically dominated by $G$ on sources with $u_0=0$ , then every nonzero Fourier mode must satisfy

C_{kk}\le\frac{1}{\beta\lambda_k}\qquad(k\ne0).

Two finite counterfixtures are part of the target. They assert that an arbitrary full-vertex reflected two-point matrix need not be positive semidefinite, and that domination restricted away from the zero mode need not extend to full-matrix domination.

Significance

The resulting interface prevents three substitutions that otherwise look notational but change the theorem. Reflection positivity is tested on observables supported on one half rather than on an arbitrary matrix indexed by all vertices. The infrared comparison excludes the constant mode rather than forcing a fluctuating zero mode below a covariance with zero diagonal. The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit pointwise theorem rather than by assigning a function the name laplacianEigenvalue.

Several ingredients already have machine-checked Lean proofs in the LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4 DFT diagonalization and zero-mode theorem, and the diagonal free-covariance calculation. This mission reorganizes those results around a corrected consumer boundary and adds the split-half and off-zero adapters. It does not present the finite statements as new mathematics.

Difficulty

The main difficulty is maintaining the correct domain at each interface. A reflection of lattice sites does not by itself imply positive semidefiniteness of a correlation matrix indexed by every site; the tested observables and their support are part of the assertion. Likewise, a free covariance whose constant-mode entry is defined to be zero cannot dominate an arbitrary covariance on all source vectors. Finally, a Fourier multiplier used for a pseudospectral derivative is not automatically the eigenvalue of the nearest-neighbor graph Laplacian. The formal statements must keep these three objects distinct.

Formalization scope

All configuration, feature, observable, and mode types are finite. Kernels, weights, coefficients, source vectors, and quadratic forms are real. Complex numbers occur only in the explicit discrete Fourier modes. Reflected pairings are unnormalized finite sums; no partition function or probability measure is introduced. The inverse temperature satisfies $\beta>0$ . The distinguished zero mode is part of the spectrum interface, and infrared domination is restricted to source vectors that vanish at that coordinate.

The mission does not assert reflection positivity of a clock or XY Gibbs measure, nonnegative Fourier coefficients of a physical cross-bond weight, Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition, or a universal jump. It also does not identify the Torus-4 graph spectrum with the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are separate future missions requiring additional model and analytic input.

The reusable outputs are the split-weight RP interface, the finite positive-semidefinite kernel API, the typed spectrum object, and the zero-mode-restricted domination predicate. Contributions should preserve the explicit half support and zero-mode restrictions; a proof obtained by adding the desired conclusion as a hypothesis is outside scope.

Selected references

J. Fröhlich, B. Simon, and T. Spencer, Infrared bounds, phase transitions and continuous symmetry breaking, Communications in Mathematical Physics 50 (1976), 79--95. https://doi.org/10.1007/bf01608557
J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, Phase transitions and reflection positivity. I. General theory and long range lattice models, Communications in Mathematical Physics 62 (1978), 1--34. https://doi.org/10.1007/bf01940327
J. Fröhlich and T. Spencer, The Kosterlitz--Thouless transition in two-dimensional Abelian spin systems and the Coulomb gas, Communications in Mathematical Physics 81 (1981), 527--602. https://doi.org/10.1007/bf01208273
LeanProofs, ReflectionPositivityInfraredBound.lean, exact repository snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean

11 thms1 active userReviewed

Completed

Algebra Theoretical Computer Science·Captain: Cosme

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.

32 thms1 active userReviewed

Completed

Quantum Information·Captain: Elsie66

Grover's AlgorithmResearch Paper

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

8 thms1 active user

Completed

Numerical Analysis·Captain: Elsie66

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).

4 thms1 active userReviewed

Completed

Operations Research Optimization Probability·Captain: StellaXin

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). 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 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), 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. 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.
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.

14 thms1 active userReviewed

Completed

Number Theory·Captain: Mayank Kumar

Fundamental Theorem of ArithmeticTextbook

Motivation

Every introductory number theory course opens with the same fact: the integers factor into primes in exactly one way. Euclid's Elements (Book IX, Proposition 14) already proves a form of it for the case of two factorizations sharing no further structure, but the theorem is not stated in full generality — with existence and uniqueness as a single package — until Gauss's Disquisitiones Arithmeticae (1801, Art. 16). Every standard modern treatment restates it as the opening theorem of the subject: Hardy & Wright, An Introduction to the Theory of Numbers (Theorem 2), and Apostol, Introduction to Analytic Number Theory (1976, Theorems 1.9–1.10), both prove it in the first chapter, before anything else is developed. The reason is structural, not pedagogical convenience: gcd, lcm, multiplicative functions, the notion of "the" prime factorization of an integer, and the entire multiplicative structure of $\mathbb{Z}$ depend on it being true. Mathlib itself packages the general statement as UniqueFactorizationMonoid, of which $\mathbb{N}$ is one instance — this mission asks for the classical, elementary argument specific to $\mathbb{N}$ , in the two-part shape every textbook gives it.

Setting

A prime $p \in \mathbb{N}$ is a natural number $p \geq 2$ whose only divisors are $1$ and $p$ (Mathlib's Nat.Prime). A factorization of $n \in \mathbb{N}$ is represented here as a multiset $l$ of natural numbers — an unordered collection that tracks multiplicity but not order, so that two factorizations differing only by a reordering of their factors are already identified as the same multiset, with no separate permutation argument needed. Write $l.\mathrm{prod} = \prod_{p \in l} p$ for the product of the elements of $l$ with multiplicity, under the convention that the empty multiset has product $1$ . The theorem concerns multisets all of whose elements are prime.

Formalization targets

Goal — unique factorization

\forall\, n \neq 0,\quad \exists!\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.

For every nonzero $n$ there is exactly one multiset of primes whose product is $n$ . This is the capstone: existence and uniqueness combined into the single statement every textbook eventually asserts.

Milestone 1 — existence

\forall\, n \neq 0,\quad \exists\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.

Every nonzero natural number is a product of primes (Apostol, Theorem 1.9). This alone says nothing about how many such multisets there might be.

Milestone 2 — uniqueness

\left(\forall p \in l_1,\ p \text{ prime}\right) \wedge \left(\forall p \in l_2,\ p \text{ prime}\right) \wedge l_1.\mathrm{prod} = n = l_2.\mathrm{prod} \ \implies\ l_1 = l_2.

Any two multisets of primes with the same product are equal (Apostol, Theorem 1.10). Combined with Milestone 1, this gives the Goal.

Significance

The result itself. Unique factorization is what makes "the prime factorization of $n$ " a well-defined object rather than a choice. Every downstream elementary and analytic number theory construction leans on it: $\gcd(a,b)$ and $\mathrm{lcm}(a,b)$ computed via shared prime exponents, multiplicative arithmetic functions ( $\varphi$ , $\sigma$ , $\mu$ ) defined by their values on prime powers, the Euler product for $\zeta(s)$ , and $p$ -adic valuations. Without it, none of these constructions are canonical.

Formalizing it. The general statement is already machine-checked in Mathlib as an instance of UniqueFactorizationMonoid (and concretely realized for $\mathbb{N}$ via Nat.factors/Nat.factors_unique), so this is not open mathematics. What this mission asks for is the specific, elementary two-lemma argument — strong induction for existence, Euclid's lemma plus strong induction for uniqueness — spelled out for $\mathbb{N}$ with the Multiset representation used here, rather than a one-line appeal to the packaged Mathlib result. A solution that simply repackages Nat.factors_unique and its companions is a legitimate route (nothing here is designed to block it), but the more valuable contribution is the self-contained classical proof, since that is what a reader of Apostol or Hardy & Wright expects to see reconstructed.

Difficulty

For existence, ordinary induction on $n$ does not immediately work: if $n$ is composite, $n = ab$ with $1 < a, b < n$ , and the inductive hypothesis is needed for both $a$ and $b$ at once, neither of which is simply $n - 1$ . The fix is strong (well-founded) induction on $n$ , splitting into the prime case (trivial single-element multiset) and the composite case (combine the two multisets for $a$ and $b$ ).

For uniqueness, the natural first attempt — "cancel a common prime factor from both sides and recurse" — silently assumes that the same prime appears in both multisets, which is exactly what needs to be proved. The step that actually does the work is Euclid's lemma: if a prime $p$ divides a product $l_2.\mathrm{prod}$ , it divides one of the factors of $l_2$ . This is not a restatement of primality (irreducibility, "no nontrivial divisors") but a genuinely separate fact about $\mathbb{N}$ that requires either Bézout's identity or a well-ordering argument to establish; conflating "prime" with "has this divisibility property" is the standard trap for a first attempt at this proof.

Formalization scope

The statement is specific to $\mathbb{N}$ (not $\mathbb{Z}$ or a general UniqueFactorizationMonoid), and factorizations are represented as Multiset ℕ rather than List ℕ up to permutation — this is a deliberate choice that folds "unique up to reordering" directly into multiset equality. The hypothesis is $n \neq 0$ , not $n > 1$ : the case $n = 1$ is included, and its unique witness is the empty multiset, since the empty product is $1$ and no nonempty multiset of primes (each $\geq 2$ ) can have product $1$ . $n = 0$ is excluded because no multiset of natural numbers has product $0$ under this convention (every prime is $\geq 2$ , and the empty product is $1$ ), so no factorization of $0$ exists to be unique.

No auxiliary platform Definitions are required — the statement is expressed entirely in terms of Nat.Prime and Multiset.prod from Mathlib. Reusable contributions welcome beyond the two milestones: an explicit construction of the canonical sorted List ℕ factorization (Nat.factors-style) connecting this multiset formulation to the more computational list representation, or a generalization of the uniqueness argument to an explicit statement and proof of Euclid's lemma as a standalone milestone.

Selected references

C. F. Gauss, Disquisitiones Arithmeticae, 1801, Art. 16.
G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Theorem 2.
T. M. Apostol, Introduction to Analytic Number Theory, Springer, 1976, Theorems 1.9–1.10.
The Mathlib Community, Mathlib4, Mathlib.RingTheory.UniqueFactorizationDomain, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.html

3 thms1 active userReviewed

Completed

Mathematical Physics·Captain: lisamegawatts

Finite Lattice Vortex Methods I: Green Variational EnergyTextbook

Motivation

Two-dimensional lattice models admit topological defects whose energetic cost competes with their configurational multiplicity. The later stages of a finite vortex argument therefore need a trustworthy bridge from a prescribed vorticity to the least quadratic energy of a compatible field. This mission isolates that bridge. It does not attempt a phase-transition theorem; it establishes only the finite-dimensional variational identity on which a later, model-specific energy estimate can rest.

The algebra belongs to finite discrete Hodge theory. A finite cochain complex supplies a differential from degree one to degree two and an adjoint codifferential in the reverse direction. A normalized Green operator inverts the degree-two Laplacian on realizable vorticities and annihilates the harmonic obstruction. Such finite-complex harmonic methods go back at least to Beno Eckmann's 1944 treatment of harmonic functions and boundary-value problems on complexes. The vortex motivation comes from the energy--entropy mechanism discussed by Kosterlitz and Thouless for two-dimensional systems, but no claim from their thermodynamic analysis is included here.

Setting

Let $C^0,C^1,C^2$ be finite-dimensional real inner-product spaces. A finite Hodge complex consists of linear maps

d_0:C^0\to C^1,\qquad d_1:C^1\to C^2,

together with specified adjoints $\delta_1$ and $\delta_2$ , and the cochain relation $d_1d_0=0$ . The degree-two Laplacian is

L_2=d_1\delta_2.

The vorticity space is $\operatorname{range}(d_1)$ . A normalized degree-two Green owner supplies a unique self-adjoint linear map $G:C^2\to C^2$ satisfying both inverse identities with the orthogonal projector onto that range, taking values in the range, and vanishing on $\ker(\delta_2)$ .

For a realizable source $\omega\in\operatorname{range}(d_1)$ , define the canonical one-cochain

a_\omega=\delta_2G\omega.

The physical vortex normalization scales the prescribed vorticity by $2\pi$ , so the canonical physical field is $2\pi a_\omega$ . For a coupling $J\in\mathbb R$ , the quadratic energy of $a\in C^1$ is

E_J(a)=\frac J2\lVert a\rVert^2.

Formalization targets

Exact Green variational decomposition

For every realizable $\omega$ and every field $a$ satisfying $d_1a=2\pi\omega$ , establish

E_J(a)=2\pi^2J\langle\omega,G\omega\rangle +E_J\bigl(a-2\pi\delta_2G\omega\bigr).

The equality is required for every real $J$ . Its unscaled components assert the exact Poisson equation, closedness and orthogonality of the residual, the Pythagorean norm decomposition, and the identity

\lVert\delta_2G\omega\rVert^2=\langle\omega,G\omega\rangle.

One-sided minimum-energy bound

For $J\ge0$ , conclude

2\pi^2J\langle\omega,G\omega\rangle\le E_J(a).

Two controls are part of the target boundary: zero coupling must not identify a unique minimizer, and zero vorticity must not imply that the underlying field or its positive-coupling energy vanishes.

Significance

The result separates universal finite linear algebra from geometry that depends on a particular lattice. Once a periodic square torus is registered as a finite Hodge complex, a later theorem may specialize the Green quadratic form to dipole charges and investigate its dependence on separation. Entropy can then be compared with a genuine energy inequality without redefining energy through the desired conclusion.

Formalizing this layer provides reusable interfaces for Poisson solvability, orthogonal residuals, exact quadratic energy splitting, and the nonnegative-coupling lower bound. It also makes normalization errors visible: the factor $2\pi$ in the source and the factor $J/2$ in the energy force the coefficient $2\pi^2J$ . The underlying Green-owner infrastructure already has a machine-checked implementation in LeanProofs; the propositions in this mission are new proof obligations derived from that interface.

Difficulty

The central issue is not an asymptotic estimate. It is maintaining the exact relationship among the Laplacian sign, the orthogonal projector, the Green normalization, adjointness, and the physical $2\pi$ scaling. A proof that silently projects a non-realizable source changes the problem. A proof that divides by $J$ loses the $J=0$ case. A proof that treats zero vorticity as a zero-field assertion discards closed and harmonic residuals. Each of these shortcuts is ruled out by the formal target or its controls.

Formalization scope

The Lean development uses arbitrary finite-dimensional real inner-product spaces rather than a concrete torus. All maps are continuous only through finite-dimensional linear structure; there is no measure theory, probability, or limiting process. A source is explicitly required to lie in $\operatorname{range}(d_1)$ . The exact decomposition permits every real $J$ , while the inequality requires $0\le J$ . Existence of a Green owner is supplied as data; this mission neither constructs a second inverse nor changes the existing normalization.

The mission does not define integer charge, torus distance, plaquette winding, or a concrete lattice Laplacian. It proves no logarithmic Green estimate, cosine-energy comparison, entropy bound, Gibbs statement, vortex proliferation result, thermodynamic limit, BKT transition, or universal jump. In particular, the target cannot be satisfied by choosing a convenient torus size or hard-coding a Green kernel: it is group-generic finite-dimensional algebra conditional on the stated Hodge and Green structures.

Contributions are welcome on the independent Poisson, orthogonality, norm, scaling, and control nodes. A later mission can add the square-torus realization and the separate analytic capacity estimate needed for a sharp logarithmic lower bound.

Selected references

Beno Eckmann, Harmonische Funktionen und Randwertaufgaben in einem Komplex, Commentarii Mathematici Helvetici 17 (1944/45), 240--255. https://doi.org/10.1007/BF02566245
J. M. Kosterlitz and D. J. Thouless, Ordering, metastability and phase transitions in two-dimensional systems, Journal of Physics C 6 (1973), 1181--1203. https://doi.org/10.1088/0022-3719/6/7/010
LeanProofs, finite Hodge Green-owner foundation at commit dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/commit/dbf503b2909cc17787d40a21eb75a0c9354cc6ef

10 thms1 active userReviewed

Completed

Operations Research Probability·Captain: viratkota

Coherent Measures of Risk: the axioms, and why Value-at-Risk fails themResearch Paper

Motivation

In 1999 Artzner, Delbaen, Eber and Heath asked what a risk measure ought to satisfy, wrote down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails one of them. The failing axiom is subadditivity: merging two positions should never require more capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear riskier than its parts.

That observation did not stay academic. It is the reason the Basel framework moved its market-risk capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance have had a more direct regulatory consequence, and the mathematics is elementary enough to state completely.

Setting

A position is a payoff X : Fin (n+1) -> R across finitely many equally-weighted states, and a risk measure rho sends it to the capital that must be added to make it acceptable. Following Definition 2.4 of the paper, rho is coherent when it is translation-invariant, subadditive, positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type so the worst case is always attained; no probability measure is needed for these four axioms, which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.

Value-at-Risk is defined here at an integer tolerance k rather than a probability level, which keeps the quantile unambiguous on a finite space: VaR X k is the least capital leaving at most k states in loss, corresponding to level k/(n+1).

The goal

The mission's goal theorem is the negative result: Value-at-Risk is not subadditive. A witness is 25 equiprobable states with X losing 100 in state 0 alone and Y losing 100 in state 1 alone. Each has one losing state in twenty-five, so at tolerance k = 1 both have VaR = 0; their sum loses in two states, exceeding the tolerance, so VaR (X+Y) 1 = 100 > 0 + 0. The witness was checked numerically before this mission was drafted; what is open is the Lean proof.

The milestones establish the positive contrast on the same footing: worst-case risk, the most conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than inherent to risk measurement.

Source

P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of subadditivity for VaR and the diversification consequence are discussed in Section 3.

4 thms1 active userReviewed

Completed

Analysis·Captain: wamlart

Basic Analysis II: Stone–WeierstrassTextbook

Motivation: approximating entire continuous functions

An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. Polynomial approximation on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. Lebl, Theorem 11.7.1.

The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s Basic Analysis, Volume II. Source section.

Setting: function algebras and uniform error

A metric space is a set $X$ with a nonnegative, symmetric distance $d(x,y)$ that vanishes exactly when $x=y$ and satisfies the triangle inequality. It is compact if every cover by open sets has a finite subcover. Let $K$ be either the real numbers $\mathbb R$ or the complex numbers $\mathbb C$ , and write $C(X,K)$ for the continuous functions from $X$ to $K$ . Products, sums, and scalar multiplication of functions are taken pointwise. The notation $K[t]$ denotes polynomials in one indeterminate $t$ with coefficients in $K$ , and $[a,b]=\{x\in\mathbb R:a\le x\le b\}$ for real endpoints $a,b$ .

A non-unital function algebra $A$ contains the zero function and is closed under these three operations. It need not contain the constant function $1$ . It separates points if, whenever $x\ne y$ , some $g\in A$ satisfies $g(x)\ne g(y)$ . It vanishes nowhere if, for each $x$ , some $g\in A$ satisfies $g(x)\ne0$ . The witness may depend on $x$ ; one everywhere nonzero function is not specified. A complex algebra is self-adjoint if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15.

Uniform convergence of $f_n$ to $f$ means

\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall n\ge N\;\forall x\in X, \qquad |f_n(x)-f(x)|<\varepsilon.

Here $|\cdot|$ is real absolute value or complex modulus. On compact $X$ , the closure $\overline A$ in $C(X,K)$ uses this uniform topology; saying that $A$ is dense means $\overline A=C(X,K)$ . Mathlib’s compact-domain convergence interface.

Formalization targets

The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.

Theorem 11.7.1. For $K=\mathbb R$ and for $K=\mathbb C$ , respectively,

f\in C([a,b],K)\Longrightarrow \exists(p_n)_{n\in\mathbb N}\subseteq K[t],\qquad p_n\longrightarrow f\ \text{uniformly on }[a,b].

The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. Source theorem.

Corollary 11.7.4. For $a\ge0$ ,

\exists(p_n)\subseteq\mathbb R[t],\qquad (\forall n,\ p_n(0)=0)\ \land\ p_n\longrightarrow |\cdot|\ \text{uniformly on }[-a,a].

Source corollary.

Proposition 11.7.6. For compact metric $X$ and either scalar field,

A\text{ a non-unital algebra in }C(X,K) \Longrightarrow\overline A\text{ is such an algebra}.

Source proposition.

Proposition 11.7.11. For an arbitrary set $X$ , without topology, let $A\subseteq K^X$ be an algebra separating points and vanishing nowhere. Then

\forall x\ne y\;\forall c,d\in K\;\exists f\in A, \qquad f(x)=c\ \land\ f(y)=d.

Both scalar fields belong to this single target. Source proposition.

Theorem 11.7.12. For compact metric $X$ ,

A\subseteq C(X,\mathbb R)\text{ an algebra separating points and vanishing nowhere} \Longrightarrow\overline A=C(X,\mathbb R).

Source theorem.

Theorem 11.7.16, complex Stone–Weierstrass. For compact metric $X$ ,

\begin{gathered} A\subseteq C(X,\mathbb C)\text{ a self-adjoint algebra},\\ A\text{ separates points and vanishes nowhere} \end{gathered} \Longrightarrow\overline A=C(X,\mathbb C).

Source theorem.

Significance: density without an assumed unit

The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.

These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. Polynomial approximation, Stone–Weierstrass library.

Difficulty: local distinctions do not give uniform control

Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.

Requiring $1\in A$ would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. Library theorem hypotheses.

Formalization scope

Namespace LeblRA uses NonUnitalSubalgebra, ContinuousMap, real and complex polynomials, TendstoUniformly, and topological closure. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise star operation on complex continuous maps.

The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes $a\ge0$ and includes $a=0$ . Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.

Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. Non-unital algebra structures, topological closures.

Selected references

Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume II, author-published open textbook, version 6.3, 2026, §11.7. Section text; edition information.
The Mathlib community, Mathlib, Lean mathematical library, revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. Polynomial approximation, Stone–Weierstrass and zero-preserving continuous maps, non-unital algebra closures.

6 thms1 active userReviewed

Completed

Analysis·Captain: wamlart

Basic Analysis I: Arzelà–AscoliTextbook

Motivation: limits of families of functions

Analysis often produces a sequence of candidate functions rather than a finished function. A useful existence theorem must say when some candidates approach a single limit everywhere with a common error bound. Ordinary boundedness is insufficient: Lebl gives bounded continuous functions on a closed interval with no uniformly convergent subsequence. The missing condition concerns how consistently the functions respond to nearby inputs. Examples 11.6.2–11.6.4.

The Arzelà–Ascoli theorem answers this question for continuous complex-valued functions on a compact metric domain. Its uses include existence questions for differential equations and compactness properties of integral operators, both discussed in the source section. These applications require control of entire functions, not merely convergence at isolated points. Differential-equation application, integral-operator application.

The four targets follow §11.6 of Jiří Lebl’s Basic Analysis, Volume II, a textbook treatment of equicontinuity and compactness for uniform convergence. Author’s book page.

Setting: pointwise control and uniform control

A metric space is a set $X$ with a distance $d(x,y)$ that is nonnegative, symmetric, vanishes exactly when $x=y$ , and satisfies the triangle inequality. It is compact when every cover by open sets has a finite subcover. Here $\mathbb C$ denotes the complex numbers, $|z|$ their absolute value, and $F_n:X\to\mathbb C$ the function at index $n\in\mathbb N$ . Write $C(X,\mathbb C)$ for the continuous functions.

The sequence is pointwise bounded if each input has its own bound, and uniformly bounded if one bound works for every input and index:

\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N, \quad |F_n(x)|\le M_x,

\exists M\in\mathbb R\;\forall n\in\mathbb N\;\forall x\in X, \quad |F_n(x)|\le M.

It is uniformly equicontinuous when

\forall\varepsilon>0\;\exists\delta>0\;\forall x,y\in X\;\forall n\in\mathbb N, \quad d(x,y)<\delta\Longrightarrow |F_n(x)-F_n(y)|<\varepsilon.

Thus $\delta$ cannot depend on the function index or the points. These are the source’s distinct boundedness and common-continuity conditions. Definition 11.6.1, Definition 11.6.6.

A subsequence has the form $F_{\varphi(n)}$ , where $\varphi:\mathbb N\to\mathbb N$ is strictly increasing. Pointwise convergence to $f$ means convergence to $f(x)$ separately for every $x$ . Uniform convergence means that for each $\varepsilon>0$ there is one $N$ such that $|F_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x$ . A subset $D\subseteq X$ is dense if its closure $\overline D$ is all of $X$ .

Formalization targets

The supporting targets distinguish countable domains, a necessary continuity condition, and the density property of compact metric spaces. The final target combines the hypotheses into uniform-convergence compactness; no quantitative rate is prescribed.

Proposition 11.6.5. For an arbitrary countable set $X$ , without any topology or continuity assumption,

F_n\text{ pointwise bounded} \Longrightarrow \exists\varphi,f,\quad \varphi\text{ strictly increasing}\quad\land\quad \forall x\in X,\ F_{\varphi(n)}(x)\longrightarrow f(x).

Source proposition.

Proposition 11.6.7. For compact metric $X$ ,

F_n\in C(X,\mathbb C),\quad F_n\longrightarrow f\text{ uniformly} \Longrightarrow F_n\text{ uniformly equicontinuous}.

Source proposition.

Proposition 11.6.8. Every compact metric space satisfies

\exists D\subseteq X,\quad D\text{ countable}\ \land\ \overline D=X.

Source proposition.

Theorem 11.6.9, Arzelà–Ascoli. Suppose $X$ is compact metric, $F_n\in C(X,\mathbb C)$ , and the sequence is pointwise bounded and uniformly equicontinuous. The complete conclusion is

\left(\exists M\in\mathbb R\;\forall n,x,\ |F_n(x)|\le M\right) \quad\land\quad \left(\exists\varphi:\mathbb N\to\mathbb N\;\exists f\in C(X,\mathbb C),\quad \varphi\text{ strictly increasing},\quad F_{\varphi(n)}\longrightarrow f\text{ uniformly}\right).

Both the global bound and the subsequence conclusion are required. The limit belongs to $C(X,\mathbb C)$ , so its continuity is explicit. Source theorem.

Significance: a compactness criterion with explicit hypotheses

The result supplies a uniform limit under hypotheses that concern individual inputs and a shared continuity condition. It therefore identifies a usable replacement for boundedness alone in a space of functions. The distinction matters downstream: retaining only pointwise convergence would not provide a common error bound across the domain, and assuming uniform boundedness in advance would discard one of the theorem’s conclusions. Lebl, Theorem 11.6.9.

These are established theorems, not open conjectures. Mathlib already contains machine-checked general Arzelà–Ascoli results, compactness and convergent-subsequence infrastructure, and the countable-dense-set interface. The four source-level statements also have ordinary local Lean proofs checked against their exact types. The contribution is a faithful textbook-facing formulation that keeps the distinct hypotheses, quantifier order, arbitrary countable domain, and both capstone conclusions visible. It is not a claim to the first formalization of Arzelà–Ascoli. Mathlib Ascoli development, countable dense subsets.

Difficulty: preserving the quantifier order

Convergence at every point does not automatically mean uniform convergence. A permissible index threshold may depend on the point, and different pointwise limits may require different subsequences. Likewise, separate continuity of every $F_n$ does not give a single $\delta$ valid for all $n$ . Replacing these statements with their uniform versions silently changes the problem. Lebl’s bounded sequence $x\mapsto x^n$ on $[0,1]$ already rules out the naive implication from bounded continuous functions to a uniformly convergent subsequence. Example 11.6.3.

The formal challenge is to retain these distinctions across the representations of functions, convergence, and compactness. In particular, the countable-domain proposition must not acquire a compactness assumption, while the capstone must not acquire global bounds as an extra premise.

Formalization scope

The development uses namespace LeblRA, arbitrary universe-polymorphic domain types, Lean’s complex numbers, and zero-based natural-number indices. Zero-based indexing only reindexes the source’s sequence starting at one. A strictly increasing map is represented by StrictMono; pointwise limits use Tendsto at atTop, uniform limits use TendstoUniformly, and density uses Dense. Finite and empty domains remain allowed.

The boundedness and equicontinuity hypotheses are written as explicit quantifiers, not new custom definitions. No claim may be replaced by a finite-domain special case, a vacuous hypothesis, or a statement that assumes its uniform conclusion.

Reusable infrastructure consists of complex norms, metric and compact spaces, continuous maps, uniform convergence, equicontinuity, and sequence compactness. The pinned environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and explicit equivalences between the raw conditions and library predicates are welcome; applications beyond the four numbered targets are outside this scope. Uniform-convergence interface, sequence compactness.

Selected references

Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume II, author-published open textbook, version 6.3, 2026, §11.6. Section text; edition information.
The Mathlib community, Mathlib, Lean mathematical library, revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. General Ascoli theorems, uniform convergence, topological bases and separability.

4 thms1 active userReviewed

Completed

Number Theory·Captain: wamlart

Elementary Number Theory: Primes, Congruences, and Secrets I: Sums of Two SquaresTextbook

From individual representations to an arithmetic criterion

Writing a positive integer as a sum of two squares is an elementary question with a precise general answer. Some integers have such a representation and others do not; checking a few small inputs does not explain the distinction. A criterion expressed through prime factorization instead decides the question for every positive integer. This project follows Section 5.7 of William Stein's Elementary Number Theory: Primes, Congruences, and Secrets, including the section's supporting statements and one subsequent exercise. The selected material connects divisibility, coprimality, algebraic identities, and rational approximation within a single classical topic. The source is the author-hosted January 2017 text, using its numbering rather than the numbering of earlier drafts.

Integers, representations, and prime exponents

A two-square representation of an integer $n$ consists of integers $x,y$ satisfying $n=x^2+y^2$ . Either coordinate may be zero or negative. A representation is primitive when the greatest common divisor of its coordinates is one; this restricts representations, not the definition of representability itself. For a positive integer $n$ and a prime $p$ , the prime exponent $v_p(n)$ is the exponent of $p$ in the prime factorization of $n$ . The congruence $p\equiv3\pmod4$ means that division of $p$ by four leaves remainder three.

The approximation statement uses a real number $t$ , a positive integer $N$ , and a reduced fraction $a/b$ , where $a$ is an integer, $b$ is a positive integer, and their greatest common divisor is one. These conventions agree with Stein's section and its definition of primitive representations.

Formalization targets

The supporting targets retain their complete source statements. Lemma 5.7.4 concerns every positive integer $n$ with a prime divisor $p\equiv3\pmod4$ :

\nexists x,y\in\mathbb Z:\quad n=x^2+y^2\quad\text{and}\quad\gcd(x,y)=1.

Equation (5.7.1) is the integer identity

(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2.

Lemma 5.7.5 states that, for every real $t$ and positive integer $N$ , some reduced fraction satisfies

0<b\le N,\qquad |t-a/b|\le\frac{1}{b(N+1)}.

The capstone, Theorem 5.7.1, is the complete equivalence

n=x^2+y^2\text{ for some }x,y\in\mathbb Z \quad\Longleftrightarrow\quad \forall\text{ primes }p\mid n,\quad p\equiv3\pmod4\Longrightarrow v_p(n)\text{ is even},

for every positive integer $n$ . Both implications are required. These four statements are located on printed pages 117–120 of the source PDF.

Exercise 5.11, on printed page 122, is an optional downstream target:

\forall n\in\mathbb Z,\ \exists k\in\{0,1,2,3\}:\quad \nexists x,y\in\mathbb Z,\ n+k=x^2+y^2.

It describes gaps among represented integers and is not a prerequisite milestone for the capstone.

What the criterion and its formalization provide

The criterion replaces a search for coordinates with a finite condition on the factorization of an input. It applies to composite integers as well as primes and distinguishes the exponent of a prime divisor from the mere presence of that divisor. The primitive obstruction also explains why a claim about coprime coordinates must not be confused with a claim that excludes all representations. The composition identity supplies an explicit statement of multiplicative closure, while the exercise gives a uniform restriction on consecutive runs. These are the consequences and accompanying results presented in Stein's treatment.

The mathematics is established, not an open research problem. Important formal ingredients already exist in Mathlib: the sum-of-two-squares development includes the arithmetic criterion and primitive obstruction, and the Diophantine approximation development supplies the bounded-denominator result. The work here is a source-aligned collection of exact theorem interfaces and independently checked proofs. Reusing those results does not claim a new proof of the classical mathematics or an exact transcription of Stein's argument.

Why the complete statement matters

A finite list of successful representations cannot establish an assertion about every positive integer. Similarly, a restriction on primitive representations is insufficient to settle general representability, because a nonprimitive pair is still a valid representation. The capstone must account for prime exponents and both directions of the equivalence simultaneously. The approximation result has its own coupled requirements: obtaining a small denominator without the stated error bound, or a good approximation with an uncontrolled denominator, does not meet the target. These distinctions are explicit in the source statements.

Formalization scope

The namespace is SteinENT. Inputs $n,p,N$ use natural numbers, with positivity hypotheses wherever the source uses positive integers. Coordinates and all subtraction in the composition identity use integers. Prime exponents use Nat.factorization; primitivity uses Int.gcd x y = 1. Approximation witnesses use Lean's rational type, whose canonical numerator and positive denominator already express a reduced fraction. The error inequality is an inequality of real numbers. The gap exercise allows every integer starting point, including negative ones.

No hypothesis assumes the desired representation or restricts the capstone to a bounded test range. There is no additional definition that hides a proof obligation, and no separate alias item for primitivity. Standard Mathlib arithmetic, rational approximation, and tactic libraries provide reusable infrastructure. Complete alternative proofs are welcome when they preserve these interfaces, including the explicit positive-input boundary and unrestricted integer coordinates.

Selected references

William Stein, Elementary Number Theory: Primes, Congruences, and Secrets, Undergraduate Texts in Mathematics, Springer, 2008; author-hosted January 2017 version, Section 5.7 and Exercise 5.11. Author's book page.
William Stein, author's source text at commit c4984c7ddb22258674816f8c000b0d8eb485d694, corresponding section and exercises.
The Mathlib Community, Mathlib4 at commit 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, Lean 4 library, pinned formalization environment; number-theory modules linked above.

5 thms1 active userReviewed

Completed

Algebra Number Theory·Captain: tomasz

Senthil Kumar: Weierstrass elliptic and zeta valuesResearch Paper

Arithmetic relations among elliptic-function values

Formalization status, 29 September 2026: the main theorem and all nine linked milestones are Proved, with zero Open leaves. The selected proof uses the now-Proved Philippon Theorem 2.1 and the completed Weierstrass application bridges. The linked statements retain their explicit formalization conventions and intermediate variants.

Algebraic independence measures whether several complex numbers satisfy a polynomial relation with rational coefficients. For two numbers, independence means that no nonzero polynomial in two variables vanishes at that pair. This is stronger than asking that each number separately be transcendental: two transcendental numbers can still satisfy a polynomial relation with each other. The distinction matters when describing the arithmetic information carried jointly by periods, lattice invariants, and values of analytic functions.

The completed target is Theorem 1 of Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions (2026). It concerns ten numbers attached to a complex lattice and two evaluation points. The conclusion selects an algebraically independent pair from those ten entries; it does not specify that the pair must consist of two particular function values. The mathematical result is published, and this mission now supplies its checked Lean proof. A source comparison on 29 September 2026 checked the main theorem’s hypotheses, ten values, full-period quasi-period normalization and pair-independence conclusion. The main statement needs no correction.

A lattice and its canonical functions

Take complex numbers $\omega_1,\omega_2$ that are linearly independent over the real numbers. Their integer linear combinations form the period lattice

\Omega=\mathbb Z\omega_1+\mathbb Z\omega_2.

The formal representation is Mathlib's PeriodPair. Its lattice determines the Weierstrass elliptic function $\wp$ and invariants $g_2,g_3$ , using Mathlib's existing definitions. Thus the lattice, function, and invariants are linked by their construction; they are not unrelated parameters.

The Weierstrass zeta function is fixed by the lattice series

\zeta_\Omega(z)=\frac1z+\sum_{\lambda\in\Omega\setminus\{0\}} \left(\frac1{z-\lambda}+\frac1\lambda+\frac{z}{\lambda^2}\right).

This is the normalization in DLMF equation 23.2.5. For a lattice element $\omega$ , its quasi-period is represented by

\eta_\Omega(\omega)=\zeta_\Omega(\omega_1/2+\omega)-\zeta_\Omega(\omega_1/2).

Both arguments lie outside the lattice. Relating this fixed increment to the increment at an arbitrary regular point is part of the established analytic infrastructure. The normalization concerns the full period $\omega$ ; references using half-periods require the corresponding factors of two, as in DLMF equation 23.2.11.

Formalization targets

Theorem 1: an algebraically independent pair

Let $\omega\ne0$ belong to $\Omega$ . Suppose $u_1,u_2,\omega$ are linearly independent over $\mathbb Q$ and

(\mathbb Z u_1+\mathbb Z u_2)\cap\Omega=\{0\}.

Define the indexed tuple

V=(g_2,g_3,\omega,\eta_\Omega(\omega),u_1,u_2, \wp(u_1),\zeta_\Omega(u_1),\wp(u_2),\zeta_\Omega(u_2)).

The proved conclusion is

\exists i,j\in\{0,\ldots,9\},\quad i\ne j\quad\text{and}\quad (V_i,V_j)\text{ is algebraically independent over }\mathbb Q.

These are the hypotheses and conclusion of the paper's Theorem 1. No algebraicity assumption is imposed on $g_2$ or $g_3$ , and the conclusion does not assert independence of all ten entries.

Equations (5) and (6): supporting addition identities

The initial supporting targets are the two identities used in §4 of the paper. For $z,v,z+v\notin\Omega$ , write $\Delta=\wp(v)-\wp(z)$ . They assert

2\Delta\zeta_\Omega(z+v) =2(\zeta_\Omega(z)+\zeta_\Omega(v))\Delta+\wp'(v)-\wp'(z),

and

4\Delta^2\wp(z+v) =-4(\wp(z)+\wp(v))\Delta^2+(\wp'(v)-\wp'(z))^2.

The statements preserve the paper's multiplied-out forms. They do not require $\Delta\ne0$ . These targets supply reusable identities; proving them alone does not establish the arithmetic conclusion of Theorem 1.

Nine completed milestones

Milestone	Linked result
Equation (5) — zeta addition identity	Proved
Equation (6) — elliptic addition identity	Proved
Lemma 6 — entire regularization and interpolation bounds	Proved
Lemma 8 — bounded auxiliary polynomial (formal-grid variant)	Proved
Appendix A.2 — Weierstrass model realization (application bridge)	Proved
Appendix A.2 / Lemma A.1 — subgroup degrees (application bridge)	Proved
Proposition A.1 — zero estimate on the mission’s rank-one grid	Proved
Lemma 9 — bounded-order nonvanishing on the enlarged grid	Proved
Lemma 10 — nonzero small arithmetic elements (linear-degree variant)	Proved

The grid and degree variants are described in the linked statements. The two application bridges identify the Weierstrass objects with the general group-theoretic objects used by Philippon’s theorem.

What the completed formalization establishes

The completed goal certifies that every period pair and every triple satisfying the stated hypotheses yields an independent pair in the precise ten-entry tuple. In particular, a proof must handle arbitrary complex lattice invariants and arbitrary admissible evaluation points. A result for a preferred lattice, algebraic arguments, or a predetermined choice of indices would leave the requested statement unresolved.

The definitions provide a reusable interface for elliptic zeta values: a canonical series, a fixed quasi-period convention, and an explicit finite-family independence predicate. The main theorem and all nine milestones have checked proofs; the theorem pages record their accepted submissions and dependencies.

Analytic identities and arithmetic independence

The central difficulty in the proof is passing from identities of analytic functions to exclusion of rational polynomial relations among selected complex values. Periodicity and the addition identities describe how values are related, but do not by themselves rule out algebraic dependence. Consequently, finishing the elementary function interface is only one part of the development.

The development also addresses a concrete analytic obligation in the chosen representation. An infinite-sum expression is a total Lean term even before summability is proved. Using it as the canonical analytic zeta function requires the appropriate convergence and differentiation results. The classical convergence statement is recorded in DLMF §23.2(ii); it is not introduced as an extra hypothesis of the main theorem.

Formalization scope and conventions

All custom declarations use the namespace WeierstrassEllipticZeta. The lattice intersection is an equality of $\mathbb Z$ -submodules of $\mathbb C$ . Rational linear independence and real linear independence have different roles: the first constrains the three inputs to the theorem, while the second is built into the period pair. Neither is replaced by numerical noncollinearity checks or approximate arithmetic.

The ten values form a Fin 10 family. The selected pair uses Mathlib's AlgebraicIndependent over $\mathbb Q$ , so repeated numerical values cannot supply an independent pair merely by occupying different indices. The existing assumptions imply that both evaluation points are outside the lattice; no extra exclusion hypothesis is needed for the goal. Supporting addition identities state their pole exclusions explicitly because Lean's totalized division also assigns values at zero denominators.

The linked intermediate targets identify the variants sufficient for the completed main proof: Lemma 8 uses the stated formal-grid formulation; Proposition A.1 concerns the mission’s rank-one grid; and Lemma 10 uses linear coordinate-degree bounds rather than the source’s sharper O(N/log N) bounds. These distinctions are explicit in the milestone statements. They do not add assumptions to the main theorem. Further contributions can simplify the checked proofs, improve these intermediate bounds, or extend the general results beyond the existing mission target.

Extensions beyond the paper

Theorem 1 with only individual pole exclusions is an Open follow-up target. It retains the same nonzero period, rational linear independence, and ten-entry algebraic-independence conclusion, while replacing the lattice-intersection hypothesis with $u_1,u_2\notin\Omega$ .

This extension is an additional deduction to formalize, not a numbered result of the paper, and no mathematical novelty is claimed. Its planned proof combines the completed Theorem 1 with a separate Chudnovsky period theorem and an arithmetic lemma recovering the quasi-period of an integer combination. These additional dependencies remain to be formalized. The mission's completed main goal and nine paper-related milestones continue to record the original scope.

Selected references

Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society, published online 17 June 2026, pp. 1–33. DOI. Target: Theorem 1; supporting identities: §4, equations (5) and (6).
NIST Digital Library of Mathematical Functions, Chapter 23, §23.2: Definitions and Periodic Properties, accessed 4 September 2026. Zeta normalization: equation 23.2.5; quasi-period convention: equation 23.2.11.
Mathlib contributors, Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, pinned revision 0df444a360eaa60ab8c11dca51a86af692955474 (Lean 4.33.1).

473 thms1 active userReviewed

Completed

Machine Learning Probability Statistics·Captain: willma

Don't Label Twice: Game, Set, MatchOpen Problem

The problem

(a) In a tennis match, you are the favorite, and win each point independently with probability $q\in(1/2,1)$ . Let $n,m$ be odd positive integers greater than $1$ . You have the choice between playing a best-of- $nm$ (i.e., you play $nm$ points and whoever wins the majority of points wins the match), or a best-of- $n$ of best-of- $m$ 's (i.e., the match is won by winning the majority of $n$ "sets", and each "set" is won by winning the majority of $m$ points). Prove that your probability of winning the match is strictly greater by playing the best-of- $nm$ .

(b) We now consider two generalizations: $m_1,\ldots,m_k$ are odd positive integers, while $n$ is any positive integer, with all integers being greater than $1$ . You have the choice between playing a best-of- $nm_1\cdots m_k$ , or a best-of- $n$ of "sets", which are best-of- $m_1$ 's of "games", …, which are best-of- $m_k$ 's of "points". In both cases, now that $n$ may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of- $nm_1\cdots m_k$ .

(c) We consider a further generalization where each completed "set" counts toward the match score in an independently random way:

with probability $a$ , the winner gains $1$ in the match score, as usual;
with probability $b$ , the set is ignored and does not count toward the match score;
with probability $c$ , the loser gains $1$ in the match score;

with $a+b+c=1$ and $a>c$ , so players are still incentivized to win sets (previously we had $a=1$ , $b=c=0$ ). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of- $nm_1\cdots m_k$ , then each individual point counts as a set and is subject to the same randomness with probabilities $a,b,c$ . Prove that your probability of winning the match is still strictly greater by playing the best-of- $nm_1\cdots m_k$ (the fair-coin-on-ties convention continues).

(d) Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming $b\ge1/2$ , prove that your probability of winning the match is strictly greater by playing the best-of- $nm_1\cdots m_k$ .

Source and connection to Dorner–Hardt

Florian E. Dorner and Moritz Hardt, Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget, ICML 2024. arXiv:2402.02249 (v3, 8 April 2026).

The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.

Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language. A point is a single crowdworker label being correct ( $q$ is the label accuracy); a set is a data point, whose test label is the majority of its $m$ labels; and the scoring rule is what the two classifiers do with that label. Writing $p$ for the worse classifier's accuracy and $p+\epsilon$ for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:

a=(p+\epsilon)(1-p),\qquad c=p(1-p-\epsilon),\qquad b=1-a-c,

so that $a-c=\epsilon>0$ , and $b\ge1/2$ always holds because two classifiers of accuracy at least $1/2$ agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: $\Pr(+1)=q\epsilon+p(1-p-\epsilon)$ , $\Pr(-1)=(1-q)\epsilon+p(1-p-\epsilon)$ . The paper's inequality also allows $n=1$ and $q=1$ , which parts (c)–(d) exclude only because the inequality can fail to be strict at $b=0$ there; for $b\ge1/2$ the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is not claimed here.

Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate $b$ . The hypothesis $b\ge1/2$ in part (d) cannot be dropped: with one level, $(a,b,c)=(0.9,0.1,0)$ , $q=0.6$ , $m=3$ , $n=1$ , the single best-of-3 finishes strictly ahead with probability $0.5832$ while three single points do so with probability $0.5761$ .

Timeline

Feb 2024 — arXiv v1; ICML 2024. Asymptotic theorem via Cramér; finite-sample statement conjectured; ~5·10⁹-configuration numerical sweep.
Oct 2024 — arXiv v2.
Apr 2026 — arXiv v3; conjecture still stated as open.
Aug 2026 — private proof of the Section 3 inequality (strict win, $b\ge1/2$ , one level) via exponential tilting of the tie probability.
Sep 2026 — private proof of the fair-coin version with no constraint on $b$ (Bernstein degree elevation and a hypergeometric parity argument), then of the full four-part statement via a pairing lemma for player-symmetric rules. This mission formalizes that proof.

Conventions in the formal statement

"Greater than $1$ " is read as $n\ge2$ and each $m_i\ge3$ odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions $\mathbb Z\to\mathbb R$ and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.

39 thms1 active userReviewed

Completed

Number Theory Pure Mathematics·Captain: tabbott

The Hardy-Littlewood Method I: Weyl's InequalityTextbook

Motivation

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

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

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

Setting

For a real number $\theta$ write

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

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

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

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

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

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

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

Target

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

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

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

Significance

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

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

Difficulty

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

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

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

Formalization scope

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

Conventions this mission commits to:

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

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

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

Selected references

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

15 thms1 active userReviewed

Completed

Convex Optimization Functional Analysis Optimization·Captain: Shuze Chen

Vector Space Methods IV: Hahn–Banach and Minimum Norm DualityTextbook

Motivation

Chapter 5 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) carries the minimum norm theory of Chapter 3 (Mission I of this series) from Hilbert space to arbitrary real normed spaces. The inner product is gone, so orthogonal projection is no longer available; its role is taken over by the Hahn–Banach theorem, in two classical forms. The extension form generalizes the projection theorem and yields a duality principle equating a minimum norm problem in a space $X$ with a maximization problem in its dual $X^*$ ; the geometric form (separating hyperplanes) extends that duality from subspaces to convex sets. These duality theorems are the backbone of the optimization theory in the remainder of the book — conjugate functionals (Ch. 7) and Lagrange duality (Ch. 8) both trace back to them.

Setting

Throughout, $X$ is a real normed linear space. A linear functional $f$ on $X$ is bounded if $|f(x)| \le M\|x\|$ for some constant $M$ and all $x$ ; the least such $M$ is the norm $\|f\|$ . The (normed) dual $X^*$ is the space of bounded (equivalently, continuous) linear functionals with this norm; $\langle x, x^*\rangle$ denotes $x^*(x)$ . A functional $p : X \to \mathbb{R}$ is sublinear when $p(x+y) \le p(x) + p(y)$ and $p(\alpha x) = \alpha\, p(x)$ for $\alpha > 0$ . Vectors $x \in X$ and $x^* \in X^*$ are aligned when $\langle x, x^*\rangle = \|x^*\|\,\|x\|$ , and orthogonal when $\langle x, x^*\rangle = 0$ ; for $S \subseteq X$ , the complement $S^\perp \subseteq X^*$ consists of the functionals vanishing on $S$ , and for $U \subseteq X^*$ , ${}^\perp U \subseteq X$ consists of the vectors annihilated by every member of $U$ . A hyperplane is a maximal proper linear variety; closed hyperplanes are the level sets $\{x : \langle x, x^*\rangle = c\}$ of nonzero bounded functionals. The support functional of a convex set $K$ is $h(x^*) = \sup_{k \in K}\, \langle k, x^*\rangle$ .

Formalization targets

The goal is §5.13 Theorem 1 (Minimum Norm Duality): if $x_1 \in X$ has distance $d > 0$ from a convex set $K$ with support functional $h$ , then

d \;=\; \inf_{x \in K} \|x - x_1\| \;=\; \max_{\|x^*\| \le 1}\ \big[\langle x_1, x^*\rangle - h(x^*)\big],

the maximum on the right being achieved by some $x_0^*$ ; and if the infimum is achieved by $x_0 \in K$ , then $-x_0^*$ is aligned with $x_0 - x_1$ .

The milestones trace the chapter's route there: boundedness $\Leftrightarrow$ continuity (§5.2); the Hahn–Banach theorem in sublinear form (§5.4 Theorem 1) with its norm-preserving extension and norming-functional corollaries; the annihilator identity ${}^\perp(M^\perp) = M$ for closed subspaces (§5.7 Theorem 1); the two subspace duality theorems and the alignment characterization of best approximations (§5.8 — the chapter's principal results); and the geometric form: Mazur's separation theorem, the support theorem, and Eidelheit's separation theorem (§5.12).

Significance

The §5.8 duality theorems are the exact normed-space analogue of the projection theorem: existence transfers to the dual problem (minimum norm problems should be formulated in a dual space to guarantee solutions — the chapter's methodological moral), orthogonality becomes alignment, and infinite-dimensional problems with finitely many constraints reduce to finite-dimensional dual problems. The geometric form underpins all of convex duality.

All results are classical and proved in the source. Mathlib contains the Hahn–Banach extension theorem and point/convex separation theorems, so several milestones are exercises in connecting Luenberger's formulations to existing library lemmas; the two §5.8 duality theorems, the alignment corollary, and the §5.13 convex duality theorem have no direct Mathlib counterpart and are the mission's genuinely new content.

Difficulty

Degenerate cases are the trap throughout. In §5.8 Corollary 1 the "only if" direction fails literally when $M$ is dense and $x \in M$ (then $M^\perp = \{0\}$ and no nonzero aligned functional exists); the formalization therefore carries the hypothesis $x \notin \overline{M}$ . In the separation theorems the strict inequality holds only on the interior of the convex set — on the set itself only $\le$ survives — and nonemptiness hypotheses (of the interior, of $K_2$ , of the variety) are what make the "nonzero functional" claims true; dropping any of them creates false statements in trivial spaces. In §5.13 the support functional may take the value $+\infty$ , so the dual maximum is formalized by two quantified inequalities (the witness achieves $d$ ; no admissible functional exceeds $d$ ) rather than by a real-valued supremum. The infimum in the primal problems need not be attained — attainment appears only as a hypothesis in the alignment clauses.

Formalization scope

Real scalars throughout. The dual space is represented concretely as continuous linear maps X →L[ℝ] ℝ, and annihilators are written as explicit quantified conditions rather than named subspaces. Five notions the chapter needs and Mathlib lacks are published as definitions and used by the statements rather than inlined: alignment ( $\langle x, x^*\rangle = \|x^*\|\,\|x\|$ ), the support functional ( $h(x^*) = \sup_{k \in K} \langle k, x^*\rangle$ , valued in the extended reals since it may be infinite), the total variation of a function on an interval, the normalized space $NBV[a,b]$ , and the Riemann–Stieltjes integral (defined relationally, so that no existence claim is built into the definition). The Minkowski functional needed for Mazur's theorem is Mathlib's gauge. Minimum distances are infima ⨅ over coerced sets or submodules; in §5.8 Theorem 2 the dual-side supremum is a real sSup over $\{\langle x, x^*\rangle : x \in M,\ \|x\| \le 1\}$ , which is nonempty and bounded. Sublinearity in §5.4 is hypothesized exactly as in the source (subadditivity plus positive homogeneity plus continuity). Linear varieties are parametrized as $x_0 + M$ with $M$ a Submodule ℝ X. No completeness of $X$ is assumed anywhere — the chapter's results are genuinely about normed spaces, and Hahn–Banach needs no completeness. The concrete dual of $C[a,b]$ (§5.5) is in scope, and carries most of the mission's new infrastructure: Mathlib has the property of bounded variation (eVariationOn) but no total-variation norm, no normalized space $NBV[a,b]$ , and no Riemann–Stieltjes integral — its StieltjesFunction is the different object of a monotone right-continuous function inducing a Borel measure, and its Riesz–Markov–Kakutani development represents positive functionals on $C_c(X)$ by measures, not bounded functionals on $C[a,b]$ by functions of bounded variation. This mission therefore publishes those notions as definitions and states the representation theorem in both directions. §5.3 (the Riesz–Fréchet theorem, i.e. self-duality of Hilbert space) is the one omission: Mathlib's InnerProductSpace.toDual already provides it. §5.6 (second dual, reflexivity) is definitional and likewise present in Mathlib.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 5, pp. 103–142. ISBN 0-471-55359-X.
H. Hahn, Über lineare Gleichungssysteme in linearen Räumen, J. Reine Angew. Math. 157 (1927), 214–229; S. Banach, Sur les fonctionnelles linéaires II, Studia Math. 1 (1929), 223–239.
S. Mazur, Über konvexe Mengen in linearen normierten Räumen, Studia Math. 4 (1933), 70–84.

17 thms1 active userReviewed

Completed

Functional Analysis Operations Research Optimization+2·Captain: Shuze Chen

Vector Space Methods II: Gauss–Markov EstimationTextbook

Motivation

Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical Gauss–Markov theorem: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator $(W^\top Q^{-1} W)^{-1} W^\top Q^{-1} y$ has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.

Setting

Measurements are modeled as $y = W\beta + \varepsilon$ , where $y$ is an $m$ -dimensional data vector, $W$ a known $m \times n$ matrix ( $n < m$ ) with linearly independent columns, $\beta$ an unknown $n$ -dimensional parameter vector, and $\varepsilon$ a random $m$ -vector of measurement errors with $E\varepsilon = 0$ and covariance $E[\varepsilon\varepsilon^\top] = Q$ , positive definite. A linear estimate is $\hat\beta = Ky$ for a constant $n \times m$ matrix $K$ ; it is unbiased when $E\hat\beta = \beta$ for every $\beta$ , which holds iff $KW = I$ . The optimality criterion is the error second moment $E\|\hat\beta - \beta\|^2$ , and the book's key observation (p. 85) is that the problem splits into $n$ independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.

Formally, randomness is carried by an abstract probability space: a measure space $(\Omega, \mu)$ with $\mu$ a probability measure, random vectors as functions $\Omega \to \mathbb{R}^m$ with explicit integrability hypotheses for all first and second moments, and $E[\cdot] = \int \cdot \, d\mu$ .

Formalization targets

The goal is §4.4 Theorem 1 (Gauss–Markov): with $K_0 = (W^\top Q^{-1} W)^{-1} W^\top Q^{-1}$ ,

K_0 W = I, \qquad E\big[(K_0 y - \beta)_i^2\big] \le E\big[(K y - \beta)_i^2\big] \quad \text{for every } i \text{ and every } K \text{ with } KW = I,

with error covariance

E\big[(K_0 y - \beta)(K_0 y - \beta)^\top\big] = (W^\top Q^{-1} W)^{-1}.

Milestones: the deterministic least-squares estimate $\hat\beta = (W^\top W)^{-1} W^\top y$ (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of $KQK^\top$ subject to $KW = I$ (p. 85); the minimum-variance estimate $\hat\beta = E[\beta y^\top] (E[y y^\top])^{-1} y$ for random $\beta$ (§4.5 Theorem 1); and the information-form identities $RW^\top(WRW^\top + Q)^{-1} = (W^\top Q^{-1}W + R^{-1})^{-1}W^\top Q^{-1}$ and $R - RW^\top(WRW^\top+Q)^{-1}WR = (W^\top Q^{-1}W + R^{-1})^{-1}$ (§4.5 Corollary 2).

Significance

The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance $R$ ; the information-form identities connect the two and exhibit Gauss–Markov as the limit $R^{-1} \to 0$ . Mission III builds the recursive (Kalman) estimator directly on these results.

All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with MeasureTheory.integral alone.

Difficulty

The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint $KW = I$ (the book proves the equivalence with $E\hat\beta = \beta$ for all $\beta$ ); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of $Q$ enters through invertibility of $W^\top Q^{-1} W$ , which itself needs the linear independence of the columns of $W$ — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.

Formalization scope

Random vectors are plain functions Ω → Fin m → ℝ on a MeasurableSpace Ω with a probability measure μ; second moments are hypotheses of the form ∫ ω, ε ω i * ε ω j ∂μ = Q i j with explicit Integrable assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are Matrix (Fin m) (Fin n) ℝ with Mathlib's Matrix.PosDef, nonconstructive inverse ⁻¹, and mulVec. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear ( $\hat\beta = Ky$ , no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 4, pp. 78–102. ISBN 0-471-55359-X.
A. C. Aitken, On least squares and linear combination of observations, Proc. Roy. Soc. Edinburgh 55 (1935), 42–48 (the weighted-least-squares form of Gauss–Markov).

8 thms1 active userReviewed

Completed

Functional Analysis Operations Research Optimization·Captain: Shuze Chen

Vector Space Methods I: Minimum Norm Problems in Hilbert SpaceTextbook

Motivation

Luenberger's Optimization by Vector Space Methods (Wiley, 1969) organizes a large part of optimization theory around a single geometric idea: minimum norm problems in inner product spaces, solved by orthogonal projection. Chapter 3 is the technical heart of that program. Its projection theorem and normal equations underlie least-squares data fitting, Fourier approximation, minimum-energy control, and the whole statistical estimation theory of Chapter 4 — which Missions II and III of this series formalize on top of the present one.

Setting

Throughout, spaces are real. A pre-Hilbert space is a real vector space $X$ with an inner product $\langle\cdot,\cdot\rangle$ inducing the norm $\|x\| = \langle x,x\rangle^{1/2}$ ; a Hilbert space $H$ is a complete pre-Hilbert space. Vectors $x, y$ are orthogonal when $\langle x, y\rangle = 0$ ; for a subset $S$ , the orthogonal complement $S^\perp$ is the set of vectors orthogonal to every element of $S$ . Given $y_1,\dots,y_n \in H$ , their Gram matrix is $G(y_1,\dots,y_n)_{ij} = \langle y_i, y_j\rangle$ and its determinant $g(y_1,\dots,y_n)$ is the Gram determinant. A linear variety is a translate $x + M$ of a subspace $M$ .

Formalization targets

The goal is §3.10 Theorem 2, the dual approximation problem: for linearly independent $y_1,\dots,y_n \in H$ and constants $c_1,\dots,c_n$ , among all $x \in H$ satisfying the constraints

\langle x, y_i\rangle = c_i, \qquad i = 1,\dots,n,

there is a unique vector of minimum norm, and it has the form

x_0 = \sum_{i=1}^n \beta_i\, y_i, \qquad \text{where} \qquad \sum_{j=1}^n \beta_j \langle y_j, y_i\rangle = c_i .

The milestone list follows the chapter's own development: the projection theorem in its pre-Hilbert form (§3.3 Theorem 1) and classical form (§3.3 Theorem 2), the orthogonal decomposition $H = M \oplus M^\perp$ with $M^{\perp\perp} = M$ (§3.4 Theorem 1), the normal equations and Gram matrices (§3.6), the Gram determinant formula $\delta^2 = g(y_1,\dots,y_n,x)/g(y_1,\dots,y_n)$ for the minimum distance (§3.6 Theorem 1), best approximation by Fourier sums over orthonormal families (§3.7, §3.9), minimum norm over a linear variety (§3.10 Theorem 1), and the extension from subspaces to closed convex sets with its variational inequality characterization (§3.12 Theorem 1).

Significance

The dual approximation theorem converts an infinite-dimensional constrained minimum norm problem into an $n \times n$ linear system — the book's model example of finite reduction, applied there to minimum-energy control of a motor (§3.11) and, in Chapter 4, to every linear estimation problem: least squares, Gauss–Markov, and recursive (Kalman) estimation are all instances of these results in a Hilbert space of random variables.

All results here are classical and proved in the source; the mission's product is a faithful machine-checked development with reusable statements. Mathlib already contains close relatives of several milestones (orthogonal projection onto complete subspaces, Submodule.orthogonal), so part of the work is connecting the book's formulations to that library; the Gram determinant distance formula and the dual approximation theorem itself have no direct Mathlib counterpart.

Difficulty

The individual milestones are standard Hilbert space theory. The care is in the statements, not tricks: the pre-Hilbert version of the projection theorem asserts uniqueness and the orthogonality characterization without existence, while existence requires completeness and closedness — conflating the two versions produces unprovable or vacuous statements. The Gram determinant formula requires the $(n+1) \times (n+1)$ Gram matrix of the extended family $(y_1,\dots,y_n,x)$ , where index bookkeeping (Fin.snoc) is easy to get wrong. In §3.12 the variational inequality $\langle x - k_0, k - k_0\rangle \le 0$ replaces the equality characterization valid for subspaces; the inequality direction is a known trap.

Formalization scope

The development commits to: real scalars (the book allows complex; this series does not), an abstract space H : Type with [NormedAddCommGroup H] [InnerProductSpace ℝ H] and [CompleteSpace H] exactly where the source assumes a Hilbert space; subspaces as Submodule ℝ H with explicit IsClosed hypotheses; finite families as Fin n → H; Gram matrices as Matrix (Fin n) (Fin n) ℝ via Matrix.of; minimum distances as infima (⨅) over coerced submodules. Best approximation statements are phrased as explicit inequalities ‖x - m₀‖ ≤ ‖x - m‖ rather than through any projection operator, so they are usable without choosing Mathlib's orthogonalProjection API. Statements deliberately carry no more hypotheses than the source: §3.3 Theorem 1 and the normal equations hold in any real inner product space; completeness appears only where existence is claimed.

Proofs are expected to lean on Mathlib's inner product space library; contributions of reusable bridging lemmas (e.g. between ⨅-formulations and orthogonalProjection) are welcome as child lemmas via proof sketches.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 3, pp. 46–77. ISBN 0-471-55359-X.

10 thms1 active userReviewed

Completed

Combinatorics Graph Theory·Captain: Community (Bot)

Erdős Problem 146: Failure of the 2-Degenerate Extremal BoundResearch Paper

A graph $H$ is $r$ -degenerate if every nonempty subgraph of $H$ has a vertex of degree at most $r$ . Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite $r$ -degenerate graph $H$ satisfies

\mathrm{ex}(n, H) = O\!\left(n^{2-1/r}\right).

The conjecture was known in several cases: when one bipartition class has maximum degree at most $r$ , for $r$ -degenerate blow-ups of trees, and, for $r = 2$ , for grids and certain critical 2-degenerate graphs. The best general bound was the weaker $\mathrm{ex}(n,H) = O(n^{2-1/(4r)})$ of Alon, Krivelevich and Sudakov.

This mission carries a complete Lean 4 formalisation refuting it at $r = 2$ .

Theorem. There exist a fixed connected bipartite 2-degenerate graph $H$ and constants $c, \varepsilon > 0$ such that

\mathrm{ex}(n, H) \ \ge\ c\,n^{3/2 + \varepsilon}

for all sufficiently large $n$ . Since the conjectured bound at $r = 2$ is $O(n^{3/2})$ , the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if $\mathrm{ex}(n,H) = O(n^{3/2})$ ; Janzer had already disproved the reverse implication, and this result refutes the forward one.

The construction. The counterexample $H$ is built in layers: starting from a layer $V_0$ of size $L_0$ , each subsequent layer is $V_i = \binom{V_{i-1}}{2}$ , and every vertex $\{a,b\} \in V_i$ is joined to its two parents $a, b \in V_{i-1}$ . The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.

The lower bound comes from a sampled Hamming-ball graph. With $U = \{0,1\}^m$ , two disjoint copies $U_L, U_R$ are joined whenever their Hamming distance is at most $k = \lfloor \tau m\rfloor$ , and each vertex is retained independently with probability $p = 2^{-\beta m}$ . The two parameters are governed by the thresholds

A(\tau) = \kappa + \tau\log_2 3, \qquad C(\tau) = 2h(\tau) - 1,

and the construction needs a sampling exponent with $A(\tau) < \beta < C(\tau)$ . The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than $n^{3/2}$ edges.

Exclusion runs on a conditional-entropy functional $E(u,z) = \frac{1}{m}\sum_j H(Z_j \mid X_j, Y_j)$ over parent and child arrays. An array of conditional entropy $E$ has at most $2^{mME + O(m\log_2 M)}$ realisations, while requiring its $M = \binom{L}{2}$ children to survive sampling costs $2^{-\beta mM}$ — which dominates the $2^{mL}$ possible parent arrays whenever $E < \beta$ . An embedding of $H$ would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has $\Omega(n^{3/2+\varepsilon})$ edges, and padding extends the construction to every sufficiently large order.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from [propext, Classical.choice, Quot.sound] alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.

This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.

3 thms1 active userReviewed

Completed

Combinatorics Graph Theory·Captain: Community (Bot)

Erdős Problem 180: the Erdős–Simonovits Compactness ConjectureResearch Paper

Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family $\mathcal{F}$ whose members all contain a cycle, there should be some $F \in \mathcal{F}$ and $C>0$ with $\mathrm{ex}(n,F) \le C\,\mathrm{ex}(n,\mathcal{F})$ for all large $n$ . The cycle hypothesis is essential — the folklore family $\{K_{1,2}, 2K_2\}$ already defeats the original formulation — and the corrected conjecture is Erdős problem #180.

This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family $\mathcal{F}$ of connected bipartite graphs, each containing a cycle, with

\mathrm{ex}(n,\mathcal{F}) = O\!\left(n^{4/3-1/48}\right) \qquad\text{while}\qquad \mathrm{ex}(n,F) = \Omega\!\left(n^{4/3}\right) \ \ (F \in \mathcal{F}).

The two bounds are separated by a polynomial factor $n^{1/48}$ , so no member can dominate the family up to any constant. The family is $\mathcal{F} = \{C_4, C_6\} \cup \mathcal{J} \cup \mathcal{K}$ , where $\mathcal{J}$ and $\mathcal{K}$ are the admissible quotients of two properly $2$ -coloured templates built from the subdivisions of $K_{3,2}$ and $K_{3,3}$ . The upper bound comes from counting short paths in an $\mathcal{F}$ -free graph: excluding $\mathcal{J}$ bounds the number of vertices that fail to be centres of a subdivided $K_{3,3}$ , and excluding $\mathcal{K}$ forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles $W(q)$ , with the characteristic of the underlying field chosen to suit the forbidden member — even $q$ for $\mathcal{J}$ , odd $q$ for $\mathcal{K}$ — which is exactly the freedom a family bound does not have.

5 thms1 active userReviewed