Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic 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 -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
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.
The sharp Hlawka inequality for Schatten -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 . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Luenberger's generalized Kuhn–Tucker theorem turns inequality-constrained optimization into an order-theoretic statement on normed vector spaces. Instead of listing scalar inequalities, it lets a convex cone P define positivity in a target space Z; one condition G x ≤ₚ 0 can therefore represent finite, infinite, or function-valued families of constraints. At a regular local minimizer, a positive continuous functional on Z simultaneously provides stationarity and complementary slackness. This mission is a separate capstone because the cone-separation argument is conceptually independent of the equality-constrained theorem and because Mathlib currently lacks this general cone-valued KKT result.
Let X and Z be real normed spaces, P : ConvexCone ℝ Z, f : X → ℝ, and G : X → Z. The cone order is coneLE P z₁ z₂, meaning z₂ - z₁ ∈ P; strict inequality uses the topological interior of the convex cone P. The cone is assumed to have nonempty interior. At x₀, both f and G possess linear Gâteaux derivatives represented by continuous linear maps f' and G'. The source's regularity condition requires feasibility together with a direction h for which G x₀ + G' h lies strictly below zero in the cone order.
The point x₀ is a local, not global, minimizer of f on {x | coneLE P (G x) 0}. The resulting multiplier z₀ : Z →L[ℝ] ℝ is positive on P. This mission reuses the previously published VectorSpaceOpt.coneLE and VectorSpaceOpt.dualPositive definitions from the global Lagrange-duality mission; it deliberately does not introduce equivalent duplicate constants.
The root theorem is VectorSpaceOpt.generalized_kuhn_tucker, corresponding to §9.4, Theorem 1. It produces z₀ such that
Three milestones expose the exact logical interfaces of the source theorem. kkt_no_strict_linearized_descent says local minimality and feasibility exclude a direction that strictly decreases f' while making the linearized constraint strictly feasible. kkt_linearized_separator packages the separation step: nonintersection of the strict descent system, cone regularity, and nonempty cone interior yield a positive continuous multiplier with both KKT conclusions. kkt_complementary_slackness isolates the algebraic extraction of stationarity and complementarity from the separating inequality valid for every direction. The items use the shared namespace VectorSpaceOpt and list dependencies in this order.
This mission generalizes the standard finite-dimensional KKT rule without choosing coordinates or reducing cone constraints to components. It provides a reusable basis for semi-infinite optimization, ordered Banach-space problems, and state constraints expressed in function spaces. The multiplier positivity predicate connects directly to the dual cone used in the earlier global duality mission, while complementarity links local differential theory to primal–dual optimality. A successful formalization would also close a conspicuous gap in general-purpose optimization infrastructure: cone-valued KKT conditions are referenced often but rarely available as a theorem with all topological hypotheses exposed.
The statement is also a useful stress test for compositional textbook formalization. It deliberately shares its order and dual-positivity vocabulary with an earlier mission, so subsequent results can consume one stable API instead of translating among locally invented conventions.
The main challenge is functional-analytic separation. The relevant convex set mixes objective descent and strict cone feasibility, and the separating functional must be normalized so that its objective component is nonzero. Regularity rules out an abnormal separator and nonempty cone interior controls the sign of the Z component. The Gâteaux assumptions are directional rather than full Fréchet differentiability, so local contradiction statements must use only the one-dimensional expansions actually supplied. Lean also requires careful sign discipline: feasibility is encoded as 0 - G x ∈ P, while positivity is evaluated on elements of P. Small convention errors would reverse the dual cone or the stationarity equation.
The source says that X is a vector space, but its definition of Gâteaux differentiation and its local perturbation argument require a norm and topology. The proposal therefore makes both X and Z normed real spaces and represents derivatives by continuous linear maps. It keeps Luenberger's cone assumptions: convexity and nonempty interior are explicit; pointedness and closedness are not added because the printed separation argument does not need them. The optimality hypothesis is faithfully local through IsLocalMinOn. Feasibility is included in IsConeRegularAt, and the no-descent milestone states it separately.
This is proposed as “Vector Space Methods XI” and depends on the earlier global Lagrange-duality mission, proposed as “Vector Space Methods IX,” for coneLE and dualPositive; the missions should be submitted in numerical order. The proposal does not cover equality constraints, second-order KKT conditions, multiplier uniqueness, constraint qualifications other than Luenberger's strict linearized feasibility condition, or sufficient conditions based on convexity. It also does not specialize to a finite list of scalar inequalities. These omissions preserve the exact role and scale of §9.4.
Equality-constrained optimization is the point where the geometric language of vector spaces becomes an operational calculus. In finite dimensions, the familiar rule says that the gradient of an objective at a regular constrained optimum is a linear combination of the constraint gradients. Luenberger's Chapter 9 replaces coordinate gradients by continuous linear maps between Banach spaces and identifies the genuinely important hypothesis: the derivative of the constraint map is onto. The resulting theorem covers constraints with infinitely many degrees of freedom and prepares the functional-analytic form of optimal control. This mission formalizes the local theorem rather than a finite-dimensional specialization. It also records the generalized inverse theorem that makes regular level sets locally rich enough to test every tangent direction.
Let X and Z be real Banach spaces, U ⊆ X an open set, f : X → ℝ an objective, and H : X → Z an equality-constraint map. The distinguished point x₀ lies in U and satisfies H x₀ = 0. Both maps are continuously Fréchet differentiable on U; their derivatives at x₀ are named f' and H'. A regular point is one at which H' : X →L[ℝ] Z is surjective. Local optimality is expressed relative to the actual feasible set {x | x ∈ U ∧ H x = 0}, and may be either a local minimum or a local maximum. Multipliers live in the continuous dual Z →L[ℝ] ℝ, never in an untopologized algebraic dual.
The mission also treats a map T : X → Y between Banach spaces. Surjectivity of its derivative at x₀ yields local metric surjectivity: sufficiently nearby target points possess preimages in U, with displacement controlled linearly by their distance from T x₀. This is the Lyusternik–Graves form of the generalized inverse theorem, not the ordinary inverse theorem requiring a bijective derivative.
The main target is VectorSpaceOpt.equality_lagrange_multiplier, the exact regular equality-multiplier theorem from §9.3. Its conclusion is the existence of a continuous linear functional z₀ satisfying
Three source-aligned milestones organize the mission. First, generalized_inverse_function formalizes §9.2, Theorem 1: an onto derivative gives constants ε > 0 and K ≥ 0 so every y with dist y (T x₀) < ε has a preimage x ∈ U obeying T x = y and ‖x - x₀‖ ≤ K ‖y - T x₀‖. Second, constrained_extremum_tangent_stationary states that f' h = 0 for every h in the kernel of H' at a regular local extremum. Third, abnormal_lagrange_multiplier records Luenberger's closed-range corollary: without surjectivity there is a nonzero pair (r₀,z₀) satisfying r₀ • f' + z₀ ∘ H' = 0.
This theorem is the Banach-space bridge between unconstrained differentiation and multiplier theory. It isolates the quotient-space geometry behind the multiplier rule and supplies an interface reusable in variational problems, PDE-constrained optimization, and smooth optimal control. The abnormal alternative matters independently: it represents the degeneracy that later appears in Fritz John conditions and endpoint-constrained control. Formalizing the quantitative generalized inverse statement also contributes infrastructure with uses beyond optimization, including nonlinear solvability, metric regularity, and perturbation estimates.
The mission is mathematically compact but technically demanding. The hard object is local surjectivity from an onto, noninjective derivative. Its natural linear model passes through the Banach quotient by the kernel and the open mapping theorem, while the nonlinear statement must preserve the open domain and a quantitative norm estimate. At the multiplier stage, a functional defined on the range of H' must be shown well-defined, bounded, and represented as a continuous functional on Z. Lean must also reconcile ContDiffOn, pointwise Fréchet derivatives, kernels and ranges of continuous linear maps, and filter-based local extrema. These are substantial analytic interfaces even though the final equation is short.
The proposal follows printed pp. 240–244. All domain, completeness, differentiability, feasibility, and locality hypotheses that are inherited implicitly in the prose are explicit in the Lean statements. The primary theorem assumes surjectivity and therefore produces a normalized multiplier with coefficient one on the objective. The abnormal milestone assumes only that Set.range H' is closed and explicitly requires the pair (r₀,z₀) to be nonzero. No finite-dimensionality, choice of coordinates, second-order condition, constraint qualification weaker than surjectivity, or sufficiency theorem is claimed.
Boundary cases are intentional. The zero constraint space is allowed and reduces the conclusion to ordinary stationarity. A local maximum is covered alongside a local minimum because the tangent argument is symmetric. The generalized inverse target explicitly returns a preimage inside U; it does not silently rely on extending T outside its domain. The mission does not identify the feasible level set with a manifold or claim uniqueness of a multiplier. Those are natural later developments but are not statements in the cited pages.
Alternating permutations are a classical meeting point of enumerative combinatorics, permutation statistics, and special functions. An up--down permutation alternates between rises and falls, and their ordinary counts are the Euler secant and tangent numbers. Refining this count by the inversion statistic produces the -secant polynomial . Its values and congruences retain information that disappears after setting : they distinguish how the alternating permutations are distributed by inversion number and reveal cancellation at roots such as . Ji-Cai Liu's article isolates the next nontrivial term in the -adic expansion of this polynomial, strengthening an earlier Andrews--Foata congruence. The mission formalizes the article's main result, Theorem 1.1, as an exact polynomial-divisibility statement.
For , let be the set of permutations of satisfying
The empty permutation is the unique member of . The inversion number is
The -secant inversion enumerator is the integer polynomial
Congruence modulo means divisibility in : two polynomials and are congruent precisely when divides . This formulation avoids evaluation at a single number and records the first three orders of behavior at .
In Lean, a permutation is represented as an equivalence of Fin (2*n). The alternating inequalities and inversion number are finite predicates and counts on this zero-based type. The polynomial variable is the canonical indeterminate in Polynomial ℤ.
For every integer , prove
Equivalently,
The boundary value is included. With the empty-permutation convention and natural-number truncated subtraction in the exponent, both sides reduce correctly, so the formal target does not hide a separate exceptional case.
The theorem identifies the exact quadratic correction to the highest-inversion monomial near . It therefore explains why the prior congruence modulo does not generally lift unchanged to the cubic modulus. Specializing at also yields the corresponding refinement modulo for the ordinary secant numbers. More broadly, the statement is a compact test case for formal reasoning that combines finite permutations, order predicates, inversion statistics, generating polynomials, binomial coefficients, and divisibility in a polynomial ring.
A machine-checked proof would contribute reusable infrastructure for permutation enumerators and polynomial congruences. The published article supplies a human proof; the Prove2me goal is the formal reconstruction of its theorem in Lean. The mission does not encode a proof certificate, an orbit count, or the desired divisibility inside a definition. A successful submission must derive the divisibility from the concrete finite definitions.
The result also gives a useful interface between two styles of formal combinatorics. On one side, alternating permutations are finite objects that can be enumerated, mapped, and partitioned. On the other, their aggregate is an algebraic object in whose divisibility can be studied without referring to individual permutations. Infrastructure connecting these levels can be reused for other -Euler numbers, descent and major-index enumerators, and congruences obtained from finite weighted actions. The mission keeps that infrastructure general-purpose by making the final target an equality in a quotient of the polynomial ring rather than a specialized computational procedure.
Direct expansion of is factorial in and gives no uniform explanation of divisibility by a third power. Divisibility by is stronger than merely checking the value at : it simultaneously constrains the value and the first two formal orders there. A formal solution must control the entire finite family of alternating permutations while preserving exact inversion exponents and polynomial coefficients. Index conventions are also delicate, because the paper numbers positions and values from , whereas Lean uses Fin indices from .
The source argument introduces combinatorial structure beyond the bare statement. Formalizers may contribute reusable lemmas about switching consecutive values, invariance of alternation under permitted switches, inversion-number changes, finite group actions, and divisibility of orbit enumerators. Those are natural milestones, but the present root goal deliberately remains the stable polynomial congruence rather than committing to one decomposition.
The mission fixes the coefficient ring to and uses exact polynomial divisibility. It does not replace congruence by coefficientwise arithmetic modulo , evaluation at , or a numerical check for bounded . UpDown is defined directly on permutations of Fin (2*n), invNumber counts ordered index pairs with the required inequality, and qSecant is the finite sum of monomials .
The formal statement quantifies over every natural number. The conventions at and are part of the same theorem and have been audited explicitly. The uploaded definition bundle is transparent and sorry-free; the only admitted declaration is the mission theorem itself. Useful contributions include general lemmas about polynomial divisibility, finite involutions and orbit sums, or bridges between one-based paper notation and Lean's finite types.
The calculus of variations replaces optimization over finitely many coordinates by optimization over paths. Its necessary conditions underlie geodesics, minimum-energy curves, classical mechanics, and many optimal-control models. Chapter 7 of David G. Luenberger's Optimization by Vector Space Methods presents this transition as an application of differentiation in normed vector spaces: a local extremum first forces every directional derivative to vanish, and the resulting integral identity forces a differential equation along the optimizing path. This mission formalizes the scalar, fixed-endpoint version in §§7.4–7.5. The target is intentionally the theorem actually isolated by the source, not a stronger modern Sobolev-space variant.
Fix real numbers . A path on the segment is represented in Lean by two functions, . Both are continuous on , and has derivative at every . Ordinary two-sided derivatives are not demanded at or ; this makes the formal endpoint convention match the one-sided role of endpoints in a closed interval.
Let be a scalar Lagrangian. Along a candidate path, write
The Lean statement records these partial derivatives with HasDerivAt and assumes that and are continuous on . A fixed-endpoint variation is another pair with . The first variation already computed from the action is
The main theorem begins from the stationarity identity for every such variation. It does not claim that the complete passage from a local extremum in Luenberger's norm to this integral formula has already been bundled into the root statement.
From the computed first-variation identity, prove that
The conclusion is expressed as HasDerivAt Lv (Lx t) t, so it asserts both differentiability of and the equality of its derivative with . This is equation (2) and the conclusion reached on printed pages 180–181.
The first milestone formalizes §7.4, Theorem 1: a local minimum or maximum of a real functional has zero derivative along every direction whenever that scalar directional derivative exists. The remaining milestones are the three fixed-endpoint fundamental lemmas from §7.5. They respectively show that a continuous coefficient annihilating all variations is zero, that a continuous coefficient annihilating all variation derivatives is constant, and that an identity involving both and forces the second coefficient to have derivative equal to the first. These are stated with the same variation class used by the goal.
The result turns an infinite family of scalar integral equalities into a pointwise differential equation. Once available, the same interface can support standard variational examples by supplying a concrete , its two partial derivatives, and a stationary path. It also provides the analytic core needed before treating natural boundary conditions, vector-valued paths, higher derivatives, or weak Euler–Lagrange equations.
The formalization adds reusable interval-sensitive infrastructure. In particular, IsC1OnSegment separates a path from its chosen continuous derivative and avoids silently imposing derivatives outside the optimization interval. The three fundamental lemmas are useful independently of the named Euler–Lagrange theorem: they are test-function principles for interval integrals and can serve later missions involving integration by parts or weak formulations. The mathematics is classical and proved in the cited text; the open work is a machine-checked Lean development of these exact statements in the pinned Mathlib environment.
The source argument uses informal phrases such as “arbitrary function vanishing at the endpoints” and treats endpoint differentiation according to standard calculus convention. In Lean, those phrases must determine a precise domain, derivative witness, continuity requirement, and interval-integral orientation. Replacing variations by merely continuous functions would change Lemmas 2 and 3, while requiring HasDerivAt at the endpoints would add a hypothesis not present in the book.
Another tempting shortcut is to assume from the outset that is differentiable and then use integration by parts. That would trivialize the central regularity conclusion of Lemma 3: the book derives differentiability of from stationarity and continuity. The root therefore assumes only continuity of the two coefficient functions and concludes a HasDerivAt assertion on the open interval. Conversely, constructing the first variation from a local extremum of the action requires a separate differentiation-under-the-integral development and a topology on bundled paths; it is not hidden inside the main goal.
The scalar field, path values, time variable, and action values are all real. The interval is nondegenerate through the explicit hypothesis . Integrals use Mathlib's oriented interval integral, but all principal statements are made in the forward orientation. Paths and variations are total functions on whose relevant regularity is restricted to . The Lagrangian is finite-valued. No measurability or integrability premise is omitted: continuity of the coefficient and variation factors on the compact interval supplies the intended finite integrals.
The goal starts from an already computed first-variation identity. Contributions connecting a genuine local extremum of the action in the norm to that identity are welcome as a strengthening, but they must not be advertised as part of the present root theorem. Other welcome contributions include reusable continuous test-function constructions and endpoint-aware interval integration lemmas. Sobolev paths, vector-valued state spaces, free endpoints, and weak derivatives are outside this mission and should be proposed separately rather than obtained by weakening the stated hypotheses until the result becomes vacuous.
Linear equations between Hilbert spaces need not have unique solutions and may not even be exactly solvable for a given right-hand side. Least squares selects a vector with the smallest residual; when several such vectors exist, minimum norm selects one canonical representative. Luenberger packages this two-stage optimization into the pseudoinverse of a continuous linear operator with closed range. The construction unifies exact equations, approximation, normal equations, and orthogonal projections, while retaining a bounded linear operator suitable for subsequent optimization methods (Luenberger, §§6.9--6.11, pp. 159--165).
This mission continues the series into Chapter 6. Its capstone formalizes the structural identities of the pseudoinverse, including involution, compatibility with adjoints, reflexive inverse laws, self-adjoint projection products, and factorizations through the normal operators. Earlier milestones establish the adjoint facts and minimum-norm characterizations on which that operator calculus depends.
Let and be real Hilbert spaces, represented in Lean by complete real inner-product spaces, and let be a continuous linear map whose range is closed. The Hilbert adjoint is written in the Lean statements and is Mathlib's adjoint continuous linear map. It is characterized by the inner-product relation and satisfies (Luenberger, §6.5, Theorem 1, p. 151). Closed range gives the range-kernel identity
the Hilbert-space specialization of the closed range theorem used in the chapter (§6.6, Theorem 2, p. 156).
For , a vector is a least-squares solution when is no larger than for every . A least-squares solution is minimum norm when its norm is no larger than that of every other least-squares solution. A continuous linear map satisfies VectorSpaceOpt.IsPseudoinverse A B when, for every , has both properties. This predicate is the mission's one lightweight definition, directly encoding the definition in §6.11 (pp. 163--164).
Formalize . Under closed range, formalize
These record §6.5, Theorem 1 and the Hilbert form of §6.6, Theorem 2.
Formalize the least-squares equivalence
as in §6.9, Theorem 1 (p. 160). For solvable and closed-range , characterize the minimum-norm solution by with , following §6.10, Theorem 1 (pp. 161--162). Finally, formalize existence and uniqueness of a continuous linear satisfying IsPseudoinverse A B.
Given such a , formalize that is the pseudoinverse of , that is the pseudoinverse of , and that
Also produce pseudoinverses of and of satisfying
Together with the continuous-linear-map type of , these clauses encode all nine items of §6.11, Proposition 1 (p. 165).
The pseudoinverse turns a possibly inconsistent or underdetermined equation into a canonical bounded linear solution operator. The normal equations connect residual minimization with the self-adjoint operator ; the minimum-norm theorem selects the component orthogonal to the kernel. The capstone identities show that the construction behaves like an inverse on the effective ranges and that is self-adjoint, while the two factorizations reduce pseudoinverse questions to the normal operators.
The underlying results are proved in Luenberger's text. Their Lean formalization supplies a reusable predicate for minimum-norm least squares and an operator-level API linking adjoints, kernels, ranges, composition, and optimization characterizations. This bridges the earlier missions on minimum norm and estimation with later chapters that use normal operators and generalized inverses. It also records explicitly which conclusions require closed range, preventing accidental use of a bounded pseudoinverse where only an unbounded generalized inverse could exist.
Pointwise existence of a best residual is not enough. The selected minimum-norm solutions must collectively form a linear bounded map, and closed range is the hypothesis that makes this global operator well behaved. Without closed range, least-squares minimizers may fail to exist and the inverse on the effective range need not be bounded. A formulation that chooses an arbitrary minimizer for each target would therefore miss the main analytic content.
Several notationally similar operations must also remain distinct. The book writes a star for the adjoint and a superscript dagger-like symbol for the pseudoinverse; Mathlib's displayed dagger denotes the Hilbert adjoint. The mission consequently names the generalized inverse through IsPseudoinverse instead of overloading dagger notation. Orthogonal complements apply to submodules, compositions must retain their source and target spaces, and each factorization involves a different normal operator. These typing constraints expose domain/codomain mistakes that paper notation suppresses.
The mission uses real Hilbert spaces only: NormedAddCommGroup, InnerProductSpace ℝ, and CompleteSpace. Operators are ContinuousLinearMap, composition is ∘L, the Hilbert adjoint is Mathlib's †, and the closed-range assumption is IsClosed (A.range : Set H). The orthogonal complement in the range theorem is the submodule A.kerᗮ.
IsPseudoinverse A B requires two pointwise inequalities for every target: B y minimizes residual norm among all inputs, then minimizes norm among all residual minimizers. The second clause cannot be dropped or weakened to exact solutions, because it is what makes the choice canonical for inconsistent as well as underdetermined systems. The minimum-norm-solution milestone states y ∈ A.range explicitly; the source treats solvability as part of speaking about a solution. The capstone accepts a continuous linear satisfying the predicate, so linearity and boundedness are represented by its type, corresponding to the first two items of Proposition 1. Contributions may add reusable lemmas about adjoints, orthogonal complements, closed range, normal equations, or uniqueness of optimizers, but must preserve the closed-range and completeness assumptions in the public operator theorems.
Best approximation asks how closely a point can be represented by a prescribed linear model. In a Hilbert space, orthogonality turns this into a geometric projection problem. A general normed space has no inner product and may have no nearest point, so the corresponding certificate must live in the continuous dual rather than in the original space. Chapter 5 of Luenberger's Optimization by Vector Space Methods develops exactly this passage from geometry to duality: the Hahn--Banach theorem supplies continuous linear functionals that detect norms, separate points from closed subspaces, and certify an infimum distance even when that distance is not attained (Luenberger, §§5.4--5.8, pp. 111--120).
This mission continues the book's vector-space formalization series at the point where minimum-norm arguments cease to be specifically Hilbertian. Its capstone identifies the distance from a point to a linear subspace with the largest value at that point among all norm-at-most-one continuous linear functionals annihilating the subspace. The statement is a prototype for dual certificates throughout approximation theory and convex optimization.
Let be a real normed space and let be a linear subspace. In Lean, is represented by Submodule ℝ X; no topological closure assumption is imposed on the capstone. A continuous linear functional is an element , with operator norm . It annihilates when for every . The set of all such functionals is the annihilator in the book's terminology.
For , the infimum distance to is
The Lean target uses Metric.infDist x (M : Set X). Since every submodule contains zero, the underlying set is nonempty and this extended geometric notion is an ordinary nonnegative real number here. A functional is aligned with a vector when . Alignment is the normed-space replacement for the familiar inner-product equality associated with a projection direction.
Two auxiliary dual notions are also formalized. A norm-preserving Hahn--Banach extension takes a functional on a subspace and extends it to all of without changing its norm. A norming functional for is a nonzero functional aligned with . Finally, for closed , the preannihilator of its annihilator is exactly : the functionals vanishing on distinguish every point outside it (Luenberger, §§5.4 and 5.7, pp. 112--118).
For a continuous functional on , formalize an extension satisfying
For nontrivial and every , formalize the existence of a nonzero with . These are Corollaries 1 and 2 of §5.4 (pp. 112--113).
For closed , formalize
This is the concrete set-valued form of Theorem 1 in §5.7 (p. 118).
For arbitrary and , produce one functional with , , and
for every other of norm at most one annihilating . Thus realizes the dual maximum. If a best approximant exists, the same certificate also satisfies
This packages both parts of the minimum-distance theorem in §5.8 (Theorem 1, pp. 119--120).
The capstone gives an exact lower-bound certificate for an infinite-dimensional approximation problem. Every feasible dual functional supplies the inequality , while the distinguished functional reaches equality. Consequently, the primal infimum is identified without assuming reflexivity, strict convexity, finite dimension, closedness of , or existence of a nearest point. When a nearest point does exist, alignment records the equality case of the norm estimate and links the dual certificate back to the geometry of the residual.
The source result is classical and proved in the book; the open work here is its machine-checked Lean formalization in the same namespace as the earlier vector-space missions. The reusable output includes norm-controlled extension infrastructure, norming functionals, a concrete double-annihilator theorem, and a certificate form of distance duality suitable for later convex-separation and constrained-optimization missions.
The obvious Hilbert-space formulation fails because a normed space has no canonical orthogonal complement and a minimizing element of need not exist. Replacing the minimum by Metric.infDist avoids an unjustified attainment assumption, but the desired dual maximizer must still be an actual continuous functional, not merely a limiting family. Norm control is essential: an algebraic separator without continuity cannot serve as a bounded dual certificate.
There are also degenerate cases that informal notation can hide. The distance may be zero even when if is not closed, and then the zero functional is the correct capstone witness. Conversely, the book's assertion that a norming functional is nonzero requires a nontrivial ambient space. The formal statements must handle these cases without silently strengthening the main theorem to closed subspaces or positive distance.
All spaces and functionals are real, matching the chapter and avoiding extra complex-scalar conjugation conventions. The ambient object uses Mathlib's NormedAddCommGroup, NormedSpace, Submodule, and ContinuousLinearMap; completeness is not assumed because the cited Hahn--Banach consequences do not require it. The distance is exactly Metric.infDist, and annihilation is written pointwise rather than by introducing a new annihilator definition. This keeps the capstone self-contained while the double-annihilator milestone states the same construction explicitly as a set.
No claim is made that a best approximant exists. The alignment clause is conditional on an element already satisfying the global minimum property. No closedness assumption may be added to the capstone, since the zero-distance/nonclosed case is part of the source theorem's generality. The norming-functional milestone alone assumes [Nontrivial X]; this prevents a vacuous encoding of “nonzero functional” on the zero space. Contributions may establish the four stated theorems and any generally useful lemmas about restrictions, quotient norms, annihilation, or Metric.infDist, provided the public statements retain these conventions.
The final sections of Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) derive the discrete-time Kalman filter (§4.7 Theorem 1, attributed to Kalman 1960) purely from Hilbert space geometry: the optimal estimate of a linearly evolving random state is an orthogonal projection onto the span of past measurements, and the projection updates recursively as measurements arrive. This derivation — no Gaussian assumptions, no density calculations — is a canonical application of the projection theorem formalized in Mission I and the estimation theory of Mission II.
Following §4.2 and §4.7 of the source, all random variables have zero mean and finite second moments, and are treated as elements of a Hilbert space of random variables: an abstract real inner product space in which the inner product of two random variables is their correlation, . Random -vectors are families ; two random variables are uncorrelated iff they are orthogonal in ; the covariance matrix of a zero-mean random vector is the Gram matrix . A white process satisfies .
The dynamic model (§4.7) consists of a state process and measurements
with known matrices , , white noises with covariances , ( positive definite), mutually uncorrelated and uncorrelated with the initial state . The estimate is the projection of each component of onto the subspace spanned by the components of .
The goal is §4.7 Theorem 1: the estimates generated by the recursion
started from and , are the linear minimum-variance estimates: each lies in the span of past measurement components, its error is orthogonal to all past measurements, and its error covariance is .
Milestones: orthogonality of the innovation to the past-data subspace, and the single-step updating formula (§4.6 Example 1) — given a prior projection with error covariance and new data , the updated projection is with error covariance .
The Kalman filter is among the most used algorithms in engineering — navigation, tracking, control, time-series analysis — and this mission gives it a machine-checked correctness statement at the natural level of generality: linear minimum-variance optimality over arbitrary zero-mean second-order processes, with no Gaussian hypothesis. Mathlib currently has no Kalman filter and no linear filtering theory. The abstract Hilbert-space formulation also makes the development directly reusable: the update milestone is a general two-stage projection lemma independent of the dynamic model.
The recursion couples two invariants that must be established simultaneously by induction: the geometric one (the error is orthogonal to the growing measurement subspace, and the estimate lies in it) and the algebraic one (the error Gram matrix equals ). Whiteness enters precisely through the index inequalities — and are orthogonal to everything generated by — and an off-by-one in these ranges silently breaks the induction. Invertibility of must be derived, not assumed: is positive semidefinite as a Gram matrix and is positive definite. The naive approach of expanding all projections over a concrete probability space adds measure-theoretic overhead the abstract formulation avoids entirely.
The Hilbert space of random variables is an abstract H : Type with [NormedAddCommGroup H] [InnerProductSpace ℝ H]; zero means are implicit in this representation (§4.7 assumes all variables zero-mean), so expectations never appear — only inner products. Matrix-vector actions on random vectors are written componentwise as ∑ j, A i j • x j. Processes are indexed by ℕ, with x̂(0 | -1) rendered as xh 0 = 0 and covariances as explicit Gram identities. Whiteness and uncorrelatedness are hypotheses on inner products with if k = l then _ else 0. The span of past data at time is Submodule.span ℝ {a | ∃ l < k, ∃ j, a = v l j}. The recursion defining xh and P is supplied as hypotheses, so the goal asserts exactly the optimality and covariance claims of the source theorem. Statements deliberately avoid Mathlib's orthogonalProjection; the projection property is asserted by membership plus orthogonality, which characterizes it uniquely.
Every sampling guarantee in this series so far is approximate: run the chain for steps and the output is within of stationarity. In 1996 Propp and Wilson showed that, astonishingly, one can often sample exactly from the stationary distribution of a chain — with no error at all and no knowledge of the mixing time — by running the chain not forward from the present but from the past. Their algorithm, coupling from the past (CFTP), drives all states simultaneously with the same sequence of random update maps drawn from times ; as soon as the composed map from some time collapses the entire state space to a single value, that value is an exact sample from . Chapter 22 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009; the chapter is by Propp and Wilson themselves) presents the algorithm, the monotone shortcut that makes it practical for huge state spaces, and the proof of exactness. This mission — the final one of the series — formalizes that correctness proof.
Throughout, is a chain on a finite state space with stationary distribution . A random mapping representation of is a probability distribution on update functions that reproduces the transition probabilities in one step:
Sampling and applying it to the current state is exactly one -step — simultaneously from every possible current state.
CFTP draws i.i.d. maps indexed by past times and composes them forward from the past up to time zero:
Note the order: extending the horizon deeper into the past prepends new randomness inside the composition, while the maps near time stay fixed — this is the crucial asymmetry between running from the past and running into the future. The composition has coalesced when is a constant map — all starting states have been funneled to one common value — and the algorithm outputs that value. In the monotone variant, carries a partial order with a bottom state and a top state and every update map is monotone; then it suffices to track the two extreme trajectories.
Correctness of coupling from the past (Propp–Wilson; §22.2–22.3), the capstone of the series: if is a random mapping representation of , is stationary for , and coalescence is almost sure, then for every state the probability that the CFTP composition has coalesced to the value within steps from the past tends, as , to exactly — the output of the algorithm is an exact sample from the stationary distribution, with no mixing-time error term.
The results. CFTP is one of the most striking algorithmic ideas probability has produced: a Las Vegas algorithm whose output distribution is exactly , side-stepping every mixing-time estimate of the previous twelve missions. The monotone shortcut is what made it explode in practice — for the Ising model of Mission IX the trajectories collapse to two, and Propp–Wilson famously drew exact Ising samples on large grids at the critical temperature. CFTP remains the foundation of exact-simulation methods across statistical physics, spatial statistics, and randomized algorithms.
Formalizing it. The correctness argument is short but famously slippery — the standard pitfall (running the coupling into the future yields a biased sample) is precisely a statement about the order of composition, which a formal proof pins down mercilessly. Nothing about exact sampling exists in any proof-assistant library. Formalized CFTP correctness is a fitting keystone: it consumes the random-map representation (Chapter 1), stationarity (Mission I), and the almost-sure-coalescence analysis, and certifies the algorithm practitioners actually run.
The whole content lies in managing the composition order and the limiting argument without measure theory. The probability space at horizon is the finite product of copies of (tuples of update maps, weighted by products); the key observation — for fixed , the law of applied to any fixed start equals the law of forward steps — is a finite re-indexing argument. Exactness then follows from a sandwich: on the event of coalescence by time , the output equals for every ; choosing the start according to shows the output law differs from by at most the non-coalescence probability, and the hypothesis drives that to zero. Formalizing this needs care at exactly the point where informal proofs wave: the event "coalesced by " is increasing in because the maps near zero are shared between horizons — the tuple encoding must make this monotonicity provable. The coalescence milestone is a geometric-trials argument (independent blocks each collapse with probability bounded below), and the monotone milestone is an induction showing monotonicity of compositions plus the squeeze between the extreme trajectories. All randomness is finite products of a finite distribution; limits are limits of explicit real sequences.
Update-map distributions are functions with the distribution predicate of Mission I; the random-map representation condition is a finite-sum identity. The composition is encoded by a tuple with the map used at time , folded so that the last entry applies first — the from-the-past order. Coalescence probabilities and output probabilities are finite sums over tuples of products of -weights; "coalescence is almost sure" is the statement that the non-coalescence probability tends to , and the goal's conclusion is a limit of real sequences (Filter.Tendsto), not a measure-theoretic almost-sure statement. The monotone milestone is stated abstractly for any finite partial order with OrderBot and OrderTop and any tuple of monotone maps — reusable beyond CFTP. No measure theory, filtrations, or i.i.d. infrastructure is required anywhere.
The first mission of this series established that an irreducible finite Markov chain has a unique stationary distribution . The present mission, covering Chapters 3–4 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009), answers the two questions that make that fact useful. First, the inverse problem of sampling: given a target distribution — uniform over proper colorings, a Gibbs measure, a posterior — how does one build a chain whose stationary distribution is ? The Metropolis and Glauber constructions of Chapter 3 are the universal answers, and they are the engine of Markov chain Monte Carlo across statistical physics, Bayesian statistics, and approximate counting. Second, the convergence question: in what sense, and how fast, does an irreducible aperiodic chain approach ? Chapter 4 introduces the total variation distance, proves the Convergence Theorem — geometric convergence to stationarity — and defines the mixing time, the parameter the entire remainder of the book estimates.
All chains live on a finite state space and are presented by row-stochastic matrices, with the definitions of Mission I. The total variation distance between distributions and is
the maximal discrepancy over events. A coupling of and is a distribution on whose marginals are and . For a chain with stationary one sets
and the mixing time is , with .
The Metropolis chain for a target and a symmetric proposal chain accepts a proposed move with probability ; a general (not necessarily symmetric) base chain is handled by the ratio . The Glauber dynamics for a distribution on configurations picks a uniform site and re-samples its value from conditioned on the rest.
This is Theorem 4.9, the Convergence Theorem. It asserts only the geometric shape of convergence, leaving all quantitative rates to later missions, which is why it is the goal.
The milestones are the chapter's working parts: stationarity and reversibility of the Metropolis chain for symmetric and general base chains (§3.2, Exercise 3.1), stationarity and reversibility of the Glauber dynamics (§3.3, Exercise 3.2); the three characterizations of total variation distance — the half- formula (Proposition 4.2 with Remark 4.3), the supremum over -bounded test functions (Proposition 4.5), and the coupling characterization with an optimal coupling attaining it (Proposition 4.7 with Remark 4.8); the comparison (Lemma 4.11) and submultiplicativity (Lemma 4.12); the standard mixing-time consequences and (§4.5); and the equality of distance to stationarity for a group walk and its inverse walk (Lemma 4.13 and Corollary 4.14).
The results. The Convergence Theorem is the qualitative foundation on which quantitative mixing theory stands: it guarantees that is finite, so every bound in Missions III–XIII is a bound on a well-defined quantity. The TV characterizations are used constantly — the coupling characterization is the engine of Mission III, the half- formula of every explicit computation. The Metropolis and Glauber stationarity results justify the chains analyzed in Missions III (colorings, hardcore), VIII (path coupling) and IX (Ising). Submultiplicativity of is what makes a meaningful single number.
Formalizing them. None of this exists in Mathlib: there is no total variation distance for finitely supported distributions, no coupling theory, no mixing time, no MCMC correctness statement. The definition layer published here (TV distance, , , , couplings, Metropolis, Glauber) is imported by every subsequent mission of the series.
The tempting proof of Theorem 4.9 via spectral decomposition fails twice: it needs reversibility, which the theorem does not assume, and spectral machinery that arrives only in Mission VII. The book's proof is the Doeblin decomposition: by Proposition 1.7 some power satisfies , so with the rank-one matrix of rows , and induction gives . The formal work is matrix algebra with careful bookkeeping of the remainder chain , plus the monotonicity of needed to interpolate between multiples of . For Proposition 4.7 the delicate half is constructing the optimal coupling: mass on the diagonal and the normalized product of the positive parts off it, with the degenerate case handled separately. The Glauber stationarity statement must be phrased with care because configurations outside the support of have junk rows; the formalization asserts stochasticity only at supported configurations, and detailed balance globally.
Total variation distance is defined as the supremum over events, over Finset V, exactly as in (4.1); the half- formula is a milestone, not the definition. The mixing time is sInf of the set in (junk value if empty — impossible under the goal theorem). Couplings are distributions on the product with prescribed marginals; no probability-space machinery is used. The mixing-time inequalities are stated with the integer-rounding slack made explicit (e.g. via Nat.ceil of a real logarithm) so that no statement is true only "up to rounding". The Metropolis definitions use total real division, so the hypotheses require pointwise; this matches the book, which divides by throughout.
Welcome contributions beyond the milestones: simp lemmas for tvDist, monotonicity of and in , and triangle-inequality infrastructure — all reused by Missions III–XIII.
Fix machines and jobs arriving one at a time in the order . Job carries a whole vector of nonnegative loads , one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and irrevocably, knowing nothing about the jobs still to come. A machine's load is the sum of over the jobs assigned to it.
The setting formalized here is one normalized phase: loads are already scaled by a guessed makespan, so machine counts as eligible for job exactly when . The phase is allowed to give up rather than assign badly — it fails if an arriving job has no eligible machine, or if an internal weight grows past .
The algorithm keeps a weight per machine, initialized to . Job goes to the eligible machine minimizing ; that machine's weight is then scaled by , so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP
and each assignment raises one dual variable to . The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.
The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load
The source states this as ; the explicit constant is what its proof yields.
Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of succeeded, assigns all, and the bound.
The doubling wrapper — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an -competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.
Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). PDF · doi:10.1561/0400000024
Chapter Five of Jim Hefferon's Linear Algebra is one long search for a canonical form for matrix similarity, and Theorem IV.2.8 ends it: over the complex numbers every square matrix is similar to a matrix in Jordan form. That is the goal theorem of this mission and the capstone of the book. Mathlib carries the generalized eigenspace decomposition but has no Jordan canonical form, so this is a genuine target rather than a wrapper around an existing lemma; the Jordan block and the block-diagonal Jordan matrix are supplied as a mission definition. The milestones are the three results the proof is assembled from: diagonalizability as the existence of an eigenbasis, Cayley-Hamilton, and the canonical form of a nilpotent map, which is Jordan form applied to on each generalized eigenspace.
When is a system of linear constraints infeasible? Sections 4.6-4.7 of Bertsimas-Tsitsiklis answer with the archetypal theorem of the alternative. The capstone is Farkas' lemma (Theorem 4.6): for an matrix and , exactly one of the following holds — (a) some satisfies , or (b) some satisfies and ; such a is a certificate of infeasibility, geometrically a hyperplane separating from the cone of the columns of . The mission also carries the cone-membership restatement (Corollary 4.3), the inequality form (Theorem 4.7: every solution of satisfies iff some has and ), and the application to asset pricing (Theorem 4.8: a market's prices admit no arbitrage iff there is a nonnegative state-price vector with ). The book proves Farkas' lemma from LP strong duality; Section 4.7 then reverses the arrow from first principles: every polyhedron is closed (Theorem 4.9), Weierstrass' theorem (Theorem 4.10, already in Mathlib), and the separating hyperplane theorem (Theorem 4.11: for nonempty closed convex and there exists with for all ), from which Farkas' lemma — and hence the duality theorem itself — follows geometrically.
Chapter Three of Jim Hefferon's Linear Algebra is about maps between spaces and how matrices represent them. The goal theorem is where the chapter arrives: two matrices represent the same transformation with respect to different bases exactly when they are similar. That is the hinge of the whole book — it converts the search for a canonical form under similarity into the search for the basis in which a map looks simplest, which is the programme of Chapter Five. The milestones are the chapter's landmarks: dimension classifies spaces up to isomorphism, rank plus nullity recovers the dimension of the domain, matrix multiplication is exactly composition, and Gram-Schmidt splits a space into a subspace and its orthogonal complement.
Chapter Two of Jim Hefferon's Linear Algebra builds the vector space vocabulary — spanning, independence, basis — and turns it into a theory of dimension. The goal theorem is the chapter's most striking result, that the row rank and the column rank of a matrix always agree, which is the bridge between the matrix-of-numbers view of Chapter One and the vector space view of Chapter Two. The milestones are the two pillars it stands on: that any two bases of a space have the same size, so dimension is well defined at all, and that any linearly independent set can be extended to a basis.
Is the shadow of a polyhedron again a polyhedron? §2.8 of Bertsimas–Tsitsiklis answers this with perhaps the oldest method for solving linear programming problems: Fourier–Motzkin elimination. Given , one sorts the constraints by the sign of the coefficient of — rewriting them as , , or — and forms the polyhedron whose constraints are all pairwise combinations together with the constraints not involving . The capstone, Theorem 2.10, states that is exactly the projection of onto its first coordinates: a value of can be interpolated if and only if every lower bound is below every upper bound. Though hopeless as an algorithm (the number of constraints can grow exponentially), elimination has powerful theoretical corollaries, all formalized here: projections of polyhedra are polyhedra (Corollary 2.4), the image of a polyhedron under any linear mapping is a polyhedron (Corollary 2.5), and the convex hull of finitely many vectors is a polyhedron (Corollary 2.6) — the first half of the finite-basis picture completed by the resolution theorem of Mission VII.
Chapter One of Jim Hefferon's Linear Algebra develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.
Where should one look for the optimum of a linear programming problem? Chapter 1 of Bertsimas–Tsitsiklis suggests that optima "tend to occur at corners" of the feasible polyhedron; §§2.5–2.6 turn this intuition into theorems. Not every polyhedron has a corner — a halfspace in () has none — and the exact dividing line is the presence of an infinite line: a nonempty polyhedron
has an extreme point if and only if it does not contain a line, if and only if of the vectors are linearly independent (Theorem 2.6). In particular every nonempty bounded polyhedron and every nonempty standard-form polyhedron has a basic feasible solution (Corollary 2.2). The capstone, Theorem 2.8, is the sharpest form of the corner principle: if has at least one extreme point, then for any cost vector either the optimal cost is , or there is an extreme point of that is optimal — existence of an optimal solution comes for free once the cost is bounded below. Its companion Theorem 2.7 places an optimal extreme point under the weaker assumption that an optimal solution exists, and Corollary 2.3 — the fundamental theorem of linear programming — concludes that every feasible LP either has optimal cost or attains an optimal solution, in stark contrast with nonlinear problems such as minimizing over . These results license the extreme-point search that the simplex method (Mission IV) performs.
Beneath Exp3, Exp4 and their relatives lies one algorithm: minimize past losses plus a convex regularizer. Chapters 26–28 of Lattimore–Szepesvári develop this unifying view. For a Legendre potential with Bregman divergence , both mirror descent and follow-the-regularised-leader satisfy the master bound ; the negentropy potential on the simplex recovers Exp3 exactly. The goal theorem is the payoff for adversarial linear bandits: FTRL on the unit ball with the self-concordant-flavoured potential achieves — improving the factor over the Exp3-style approach of Chapter 27 and matching the lower bound of Mission XI up to logarithms.
Real decisions come with context: a news site chooses an article for a particular user. Competing with the single best arm is then meaningless; the right benchmark is the best mapping from contexts to arms, or more generally the best of expert policies. Chapter 18 of Lattimore–Szepesvári formalizes this via Exp4 — exponential weighting over experts, fed by the importance-weighted estimator of Mission V. The goal theorem: with learning rate , Exp4 satisfies against the best of experts. Since enters only logarithmically, the learner can compete with exponentially large policy classes — the conceptual gateway from bandits to reinforcement learning with function approximation.
Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.
Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the even case: for squarefree even n, the representation-count identity 2|C_n| = |D_n| — where C_n and D_n count integer solutions of n = 8x² + 2y² + 64z² and n = 8x² + 2y² + 16z² — implies that n is a congruent number.
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the odd case: for squarefree odd n, the representation-count identity 2|A_n| = |B_n| — where A_n and B_n count integer solutions of n = 2x² + y² + 32z² and n = 2x² + y² + 8z² — implies that n is a congruent number.
That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.
In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.