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.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture: a minimal counterexample to any of them, if one exists, is a snark. Lists of all small snarks are therefore used to test such conjectures by computer.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, 2013) generated all snarks on up to 36 vertices. Testing 3-edge-colourability is NP-complete, and only a vanishing fraction of cubic graphs are snarks (0.00044% of the cubic graphs of girth at least 5 on 28 vertices, p. 4), so the generation algorithm needs cheap criteria that recognise, before a graph is built, that it will be colourable and can be skipped. Section 3.1 of the paper supplies such a criterion for the last construction step, and this mission formalizes it.
All graphs are finite and simple. A graph is cubic if every vertex has degree 3. A 3-colouring of a graph is a map that gives different colours to any two distinct edges sharing an end-vertex; is colourable if it has one, i.e. its chromatic index satisfies (p. 2, Isaacs' terminology).
A 2-factor of is a spanning 2-regular subgraph (p. 4); each connected component of is a cycle. is an even 2-factor if all its cycles have even length (p. 5). For a 3-colouring and colours , write for the spanning subgraph whose edges are those coloured or .
The edge insertion operation (Figure 1(d), p. 5) takes two distinct edges and of , which may share an end-vertex, subdivides by a new vertex and by a new vertex , and adds the edge . The resulting graph has vertex set and edge set
If is cubic, so is . In the generation algorithm every graph of girth at least 4 is produced from a graph with two fewer vertices by this operation.
Let be a cubic graph with a 3-colouring , let be colours, and let , be distinct edges of lying on the same cycle of . Then
Theorem 3.4 (p. 6, stated as folklore without proof). If is a colourable cubic graph and the inserted edge lies on a 4-cycle of , then is colourable.
The result. Theorem 3.3 is the look-ahead of the snark generator: one 3-colouring of a graph on vertices excludes, at once, every pair of edges lying on a common cycle of one of its three bicoloured 2-factors. For 28 vertices the first colouring alone discards on average 85% of the candidate edge pairs (p. 6), and the overall ratio of weak snarks among generated graphs on the last level improves by a factor of 85 (p. 4). The enumeration of all snarks up to 36 vertices, on which the paper's counterexamples and statistics rest, depends on this pruning being sound: a wrong pruning rule would silently delete snarks from the lists. Theorem 3.4 is a second pruning rule of the same kind.
Formalizing it. The results are proved (Lemma 3.1 is classical; the paper gives the argument for Lemma 3.2 in one sentence and for Theorem 3.3 by combination). None of them, and no statement about 3-edge-colourings of cubic graphs and their 2-factors, is formalized on the platform. The mission produces a machine-checked soundness proof of the pruning criterion and, along the way, a reusable development of the equivalence between 3-edge-colourings and even 2-factors in Lean's SimpleGraph library. Theorem 3.4 has no proof in the paper.
The combinatorial content is short; the difficulty lies in graph-theoretic infrastructure that Mathlib does not have. Lemma 3.1 relates a global object (a proper colouring of all edges) to the cycle structure of a spanning 2-regular subgraph, and either direction needs the description of a finite 2-regular graph as a disjoint union of cycles together with parity information along each cycle. Mathlib has walks, cycles and connected components, but no decomposition of a 2-regular graph into cycles and no notion of the length of a component as a cycle.
Lemma 3.2 and Theorem 3.3 change the vertex type: lives on , so 2-factors, connected components and cycle lengths must be transported from to , and the case where and share an end-vertex (allowed by Figure 1(d)) has to be handled alongside the generic one. A first idea, to extend a given 3-colouring of directly to , does not work in general: the colours forced on the edges at and by the old colours of and can conflict, and the hypothesis "same cycle" is what has to be used to avoid the conflict.
Vertices form a type V with [Fintype V] [DecidableEq V]; graphs are SimpleGraph V with decidable adjacency, and "cubic" is Mathlib's G.IsRegularOfDegree 3. Colourability is G.lineGraph.Colorable 3 (an edge colouring, not a vertex colouring), and a 3-colouring is G.lineGraph.Coloring (Fin 3). A 2-factor is a graph F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2; it is even if every connected component has an even number of vertices (Nat.card). The edge insertion operation produces a graph on V ⊕ Fin 2, with Sum.inr 0 subdividing and Sum.inr 1 subdividing ; edges are unordered pairs Sym2 V. "On the same cycle" is encoded as membership of both edges in the 2-factor plus reachability of their end-vertices inside the 2-factor. Oddness is not defined as a number; Lemma 3.1 is stated in its second form.
Dropping "on the same cycle" would make Theorem 3.3 and Lemma 3.2 false (inserting edges between different cycles of a bicoloured 2-factor is exactly how snarks are produced), and both statements require the two edges to be distinct; a formalization without either hypothesis is ruled out. Every statement assumes cubicity, without which Lemma 3.1 fails.
Out of scope: the algorithmic content of §3 (isomorphism rejection, the look-ahead implementation, recolouring along non-hamiltonian cycles, the 85% / 11% / 3.4% statistics), the generation counts, and every exhaustive-search claim of the paper. The remaining results of the paper are covered by three sibling missions of this series.
Reusable beyond this mission: the 2-factor and even-2-factor definitions, the two-colour 2-factor of an edge colouring, and Lemma 3.1 itself. Contributions welcome: the cycle decomposition of finite 2-regular graphs, alternating colourings of even cycles, and a proof of Theorem 3.4.
Quasi-Newton methods replace the Hessian of an objective by a matrix that is updated from observed pairs of steps and gradient changes. The secant equation asks the new matrix to map the observed steps to the observed changes . The best-known update is BFGS, which for simultaneous pairs reads
Schnabel (Quasi-Newton methods using multiple secant equations, technical report, University of Colorado at Boulder, 1983, reference [25] of the paper) studied such multiple-secant updates; one of his results is that a positive definite with exists exactly when .
Dahl and Andersen (Math. Program. 194:341–370, 2022) use multiple-secant BFGS updates to build primal-dual scaling matrices for an interior-point algorithm on the nonsymmetric exponential cone, following Tunçel (Found. Comput. Math. 1:229–254, 2001) and Myklebust and Tunçel (arXiv:1411.2129). In their setting , and they need the update in factored, low-rank form. Their Theorem 2 supplies it: the term , and its counterpart for the inverse update, are computed by rank-one steps. These steps resemble single-secant quasi-Newton updates, and no inverse is formed. This mission formalizes Theorem 2 and the steps of its proof.
Let and . Write for the -th unit vector of and for the inner product of , so that . The hypothesis of the theorem is
meaning that the matrix is symmetric and positive definite.
For the recursions (25)–(26) are
Both updates of step use the previous pair . Collect the vectors into and .
The proof uses two more objects. The first is the matrix
The second is , the principal submatrix formed by the last rows and columns of . In Lean these are ExpConeIPM.Secant.Ys, Ss, d, V, U, L and Ψ, all in one definition item.
The first identity of the goal follows from milestones 4 and 5. The paper says the second "follows similarly". The analogous identity is not displayed in the paper, so it is not a milestone.
The result. Theorem 2 expresses the multiple-secant part of the BFGS update (23), and of its inverse, as a sum of rank-one terms and . Each term comes from a recursion that touches one column at a time. On pp. 359–360 Dahl and Andersen apply it twice with . This gives the BFGS scaling of their exponential-cone algorithm as an explicit rank-3 update of , which is how the algorithm implemented in MOSEK computes its scaling matrices (§6, p. 361 of the paper). The argument is a Cholesky factorization of carried out implicitly on the factors and .
Formalizing it. The theorem is proved in the paper, in under a page. Its proof leaves two steps implicit. The first is that the symmetry of every , which (27) and the step to use, propagates from . The second is the second identity, which the paper does not prove. A machine-checked proof records both. To our knowledge no proof assistant has a formal treatment of multiple-secant updates. The recursion also gives a reusable statement: a column-by-column Schur-complement process on a product produces its Cholesky factor.
The obvious route expands directly and compares it with . This leads nowhere, because depends on all earlier steps through and . The step that carries the proof is an invariant over the recursion. The trailing blocks of must stay symmetric positive definite, and the leading columns of and must stay zero. Both must be maintained together through a pair of coupled updates, in which is updated with the old . A second difficulty is bookkeeping: the paper's 1-based columns, the step count , and the trailing block of size shift relative to each other.
The hypothesis needs care. If is only assumed to satisfy for , without symmetry, the identities are false in general. A instance whose symmetric part is positive definite, with a small antisymmetric part, violates the first identity by in the largest entry.
Everything is real matrix algebra over Matrix (Fin n) (Fin p) ℝ, with arbitrary (including , where both sides are zero). The formalization commits to the following conventions.
Matrix.PosDef, which includes symmetry. The inverse is Matrix.inv. It is a genuine inverse under this hypothesis.j : Fin p is the paper's . Ys Y₀ S₀ k and Ss Y₀ S₀ k are and after steps, and they are left unchanged after step . d Y₀ S₀ j is .Real.sqrt. The division by it is multiplication by an inverse. Both return junk values on non-positive arguments, which never occur under the hypothesis; milestone 2 states this.No repair of the printed statements was needed. On p. 359 two misprints are not copied: for , and for . The definition of uses .
A complete development needs rank-one updates of products, Schur complements of a positive definite matrix in its leading entry, and inverses of for an invertible . Schnabel's existence theorem (Theorem 1 of the paper) and the applications on pp. 359–360 are outside the mission. A general lemma on Schur-complement recursions producing Cholesky factors would be reusable on its own. Contributions on the U-side identity are welcome.
The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.
Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.
Timeline:
All matrices are complex matrices with . For a self-adjoint (Hermitian) matrix , and are its algebraically largest and smallest eigenvalues. The semidefinite order means that is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if then ; this gives the matrix exponential and, on positive-definite matrices, the matrix logarithm .
A random matrix is a measurable map on a probability space , and its expectation is taken entrywise. The matrix moment generating function of is .
The objects of the mission are independent random Hermitian matrices that are almost surely psd contractions: and . Their average expectation has extreme eigenvalues
and the binary information divergence is
In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.
Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with , the extreme eigenvalues of ,
Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor , which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound .
The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.
The scalar Chernoff argument uses for independent . For matrices unless and commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. , are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "" hold almost surely. The sequence has terms wherever an average appears. An infimum over is stated as a bound for every admissible ; integrability of is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean , so at the boundary values the divergence is finite where the paper's is ; this only weakens the stated bound.
A formalization in which (empty spectrum, ) or (the average ) were allowed, or in which the range of were dropped, would state a different, partly false theorem; these cases are excluded.
A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in . Contributions of any of these as stand-alone lemmas are welcome.
A matrix Gaussian series , a sum of fixed self-adjoint matrices each multiplied by an independent standard normal variable, is the simplest sum of independent random matrices. It already appears in the analysis of random designs, in compressed sensing, in randomized numerical linear algebra and in quantum information, wherever one needs to know how large the spectrum of a random linear combination of matrices can be. Its Rademacher analogue , with random signs, plays the same role in symmetrization arguments.
For real coefficients the answer is classical: is normal with variance , so its upper tail is at most . Tropp's paper (arXiv:1004.4389v7) shows that the same bound holds for the largest eigenvalue of a matrix series, with an explicit dimensional factor and with the variance parameter .
Timeline. Noncommutative Khintchine inequalities (Lust-Piquard 1986; Lust-Piquard and Pisier 1991) control the moments of matrix Rademacher and Gaussian series and imply tail bounds of this type. Ahlswede and Winter (2002, arXiv:quant-ph/0012127) introduced the matrix Laplace transform method, whose bounds depend on the sum of the norms . Oliveira (2010, arXiv:1004.3821) obtained bounds of the same form as Theorem 4.1. Tropp (2012) derived the result from a master inequality built on Lieb's concavity theorem (1973), which produces the norm of the sum, , as variance parameter. The paper itself notes that Theorem 4.1 and Corollary 4.2 are not new results; the contribution is the route through the master bound.
Fix a dimension . Matrices are complex arrays; a matrix is self-adjoint if it equals its conjugate transpose. For a self-adjoint , is its largest eigenvalue, and is the spectral norm, the operator norm on with the Euclidean norm. Functions of a self-adjoint matrix are defined through its eigen-decomposition: , (for positive-definite ), . The semidefinite order means that is positive semidefinite.
A random matrix is a measurable map from a probability space into the complex matrices; its expectation is taken entry by entry. A Rademacher variable takes the values with probability each; a standard normal variable has law .
The data of the mission are fixed self-adjoint matrices and independent scalar variables , all standard normal or all Rademacher. The variance parameter is
For all ,
For fixed matrices and ,
The result. Theorem 4.1 is the template for every inequality in the paper: a scalar tail bound carried over to matrices at the cost of a factor , with a variance parameter that is the norm of a sum rather than a sum of norms. The difference matters: can exceed by a factor of , and §4 of the paper shows that both the variance parameter and the dimensional factor in (4.3) are needed in general. Corollary 4.2 transfers the bound to the largest singular value of a rectangular series, which covers Gaussian matrices with nonuniform variances (§4.3).
Formalizing it. The theorem is proved in the paper; the work here is to formalize that proof. The milestones are reusable beyond this mission: Theorem 3.6 and Corollary 3.7 are the common entry point of the Chernoff, Bernstein and Azuma missions of this series, and the Rademacher half of Lemma 4.3 is used again in the matrix Azuma mission. No machine-checked proof of these matrix inequalities was found in Mathlib or on the platform when this mission was drafted.
The scalar argument bounds by the product of the individual mgfs, using . For matrices this identity fails when the summands do not commute, and the trace inequality that replaces it for two matrices (Golden–Thompson) has no analogue for three or more. Controlling the trace mgf of a sum of many noncommuting independent matrices therefore requires a genuinely matrix-analytic input with no scalar counterpart; the naive product bound is not available. A second difficulty is infrastructural: matrix functions, the semidefinite order and expectations of random matrices must be combined in a single setting.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; self-adjointness is IsHermitian; , , are Mathlib's continuous functional calculus cfc; is Mathlib's Loewner order under MatrixOrder; is the supremum of the real spectrum; is the operator norm on . Expectation is entrywise, and the paper's standing regularity assumption is made explicit as entrywise integrability of every matrix whose expectation is taken. The infimum over is stated pointwise: the bound is asserted for every at which the mgfs exist, which is equivalent to the infimum form. Independence is iIndepFun of the scalar variables, and "Gaussian or Rademacher" is the disjunction of two hypotheses, never a mixture of laws.
The variance parameter is the norm of the sum ; a formalization with , with a constant different from , or with the dimensional factor omitted is a different theorem. At , Lean's division by zero makes the bound the trivial ; this is the only degenerate case and it is valid.
The development needs: the spectral calculus for Hermitian matrices, monotonicity of the trace exponential, operator monotonicity of the matrix logarithm, Lieb's theorem, and moments of the Gaussian. These are reusable well beyond this paper; proofs of the milestones, of supporting matrix-analysis lemmas, and alternative routes (for instance through noncommutative Khintchine inequalities) are all welcome.
A data curator holds a database of individual records and wants to publish something from which many statistics can be computed, while guaranteeing differential privacy: no single record should noticeably change what is published (Dwork, McSherry, Nissim, Smith 2006). Interactive mechanisms answer queries one at a time and add noise to each answer, so their accuracy degrades as more queries are asked; Dinur and Nissim showed that answering too many arbitrary queries accurately reveals the database (Dinur, Nissim 2003).
Blum, Ligett and Roth asked a different question: can a curator release, once and non-interactively, a synthetic database that is accurate simultaneously for every query of a large, structured class, while remaining differentially private? Their answer (arXiv:1109.2229; JACM 60(2), 2013; conference version STOC 2008) is yes for every class of counting queries over a discretized universe, with accuracy governed by the class's VC-dimension rather than its cardinality. The mechanism it introduces, the Net mechanism, became the starting point of the literature on private query release (SmallDB, private multiplicative weights, and the lower bounds that followed).
Fix a finite data universe (for instance ). The curator's input is an -tuple , read as a multiset of records. Two inputs are neighbouring if they differ in exactly one entry.
A database of arbitrary size is a finite nonempty multiset of elements of . For a predicate the counting query is
the fraction of records satisfying . A class of predicates is identified with its class of counting queries, and its VC-dimension is the size of the largest set of points that shatters.
A randomized mechanism , whose output on input is a random database , is -differentially private if for all neighbouring and all sets of outputs. It is -useful for if for every input , with probability at least , for every .
The global sensitivity of is over neighbouring pairs. An -net for is a finite set such that every has some with for all ; denotes a net of minimum size.
The exponential mechanism with quality score over a finite range outputs with probability proportional to . The Net mechanism is the exponential mechanism over with score .
There is an absolute constant such that, for every finite , , , , , , whenever
a minimum -net exists and the Net mechanism run on any minimum -net is -useful for . The constant is left unspecified, as in the paper; the goal asserts the shape of the bound, not a value of .
The result. Theorem 3.10 shows that a database of size roughly suffices to release, privately, a synthetic database answering every query of to within . This is only a polynomial factor above what sampling needs without privacy, and it covers classes with exponentially many queries in , which interactive noise addition cannot. Together with Property 3.3 it is the first general feasibility result for non-interactive private release, and it identified VC-dimension as the governing parameter.
Formalizing it. The result is proved in the paper, modulo the cited uniform-convergence lemma (Lemma 3.8). No part of it is machine-checked on the platform. A complete development would give a formal exponential mechanism with a general score and its privacy proof, a formal utility analysis of a mechanism with a finite range, and a formal ε-approximation theorem for VC classes, which is the deepest dependency and reusable across learning theory.
The privacy and utility of the exponential mechanism (Theorem 3.2, Property 3.4) are short ratio arguments. The difficulty is concentrated in bounding the size of the net. For finite classes a random-sampling and union-bound argument suffices (Lemma 3.7). For infinite classes the union bound over is unavailable, and Lemma 3.8 needs uniform convergence over a class of finite VC-dimension, uniformly over every finite multiset : a symmetrization or chaining argument together with the Sauer–Shelah lemma, none of which is in Mathlib in this form. The obvious route of applying the finite-class bound to the restriction of to the support of gives a size depending on and fails.
Fin n → X with X : Type finite; neighbouring means "replace one entry", the platform's PrivLearn.Generic.Neighbors. The paper's "" read literally for equal-size multisets forces and would make every mechanism private.Database X), with every set measurable. Queries are real functions on multisets, so the same query reads inputs and outputs. Predicates are X → Bool; VC-dimension is the platform's HighDimProb.Chaining.vcDim (valued in ℕ∞; the theorems take it finite, equal to ).Welcome contributions: a general ε-approximation theorem for VC classes (Lemma 3.8), reusable well beyond this mission; a reusable exponential-mechanism privacy proof; the finite-range utility analysis of Property 3.4.
Nonnegative matrix factorization (NMF) approximates a data matrix by a product of two nonnegative factors. Adding a cap on the number of nonzero entries of each factor gives sparse NMF, used in signal separation, text mining and image analysis because sparse nonnegative factors are easier to interpret. Bolte, Sabach and Teboulle (Math. Program. 146 (2014)) introduced the algorithm PALM (proximal alternating linearized minimization) for problems of the form with nonconvex, nonsmooth and , and proved that its bounded runs converge to critical points when the objective has the Kurdyka–Łojasiewicz property. Sparse NMF is the paper's main application (§4).
PALM is only implementable when the proximal map of each nonsmooth term can be computed. For sparse NMF the nonsmooth term is the indicator of the nonconvex set of nonnegative matrices with at most nonzero entries. Proposition 4.1 of the paper computes that proximal map in closed form. This mission formalizes Proposition 4.1 and the steps of its proof. The convergence theory of PALM is a separate mission of the same series.
Matrices are real arrays . The squared Frobenius norm is . The sparsity count is the number of nonzero entries of , and means for every .
For a set , the indicator is on and off . For a natural number , set
the function that is on nonnegative matrices with at most nonzero entries and elsewhere.
For and , the proximal map (2.2) of the paper is the set
Throughout, is the set of all points of where attains its smallest value on .
The hard-thresholding operator of Definition 4.1 is
which is multi-valued when the largest entries of in absolute value are not uniquely determined. The projection onto the nonnegative orthant is , componentwise.
In the proof, is fixed and , , with partial squared norms .
For every and every ,
Both equalities are equalities of sets, and both are part of the goal.
The result. Proposition 4.1 says that the proximal step for the nonnegative sparsity constraint is computed by clipping the negative entries of to zero and then hard-thresholding: keeping entries of largest magnitude and zeroing the rest. The paper remarks that this costs operations. It is what turns PALM into the explicit algorithm PALM-Sparse NMF, and the same formula applies to any method that needs a projection onto nonnegative sparse matrices (projected gradient methods, iterative hard thresholding with sign constraints).
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The platform has a projection-onto-sparse-vectors statement without nonnegativity and stated as a single inclusion, which is a different theorem. The mission produces a set-level statement that handles ties, the degenerate cases and , and the interaction of the sign and the sparsity constraints, all of which the informal proof passes over quickly.
The obvious argument is: "project onto the nonnegative orthant, then onto the sparse matrices". Composing two projections onto nonconvex sets is not in general the projection onto their intersection, so this argument is not valid as it stands; the equality holds here because of the specific coordinate structure, and the proof must show it. The second obstacle is that everything is set-valued: when several entries of tie for the -th largest magnitude, has several elements, and the equality must account for every one of them, in both directions. The step "(4.1) = (4.2)" and the removal of are dismissed in the paper as "a simple contradiction argument" and "arguing in a similar way"; each needs an explicit modification of a feasible point that preserves sparsity and does not increase the objective.
Matrices are Matrix (Fin m) (Fin n) ℝ, with 0-based indices (harmless relabelling of ). is the Frobenius inner product of the published definition CaiCandesShen.ProximalLimit.Basic. The indicators and take values in EReal, with ; membership in is the inequality in EReal for every . The proximal map carries the weight of (2.2), not . is defined by the componentwise formula. No restriction is placed on .
Every operator in the statement is a set of minimizers. A formalization that selects one element (for instance "keep the largest entries with a fixed tie-break") proves only one inclusion of a weaker statement and does not count.
The development needs only finite sums and the argmin-set definition shared by all items; no further library is required. Lemmas about hard thresholding on matrices (the description of by largest entries, nonnegativity of of a nonnegative matrix) are reusable well beyond this mission, and contributions of such lemmas are welcome.
Theorem numbers and page numbers refer to the author version of the paper (36 pages, printed page = PDF page), not to the Springer typesetting.
In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.
Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation of a set-partitioning formulation , rather than on the LP relaxation of that formulation. Their Theorem 2 is the justification for that design choice: the best bound can deliver is never weaker than , and can be strictly stronger. This mission formalizes that comparison.
An instance has a depot , satellites and customers , a symmetric travel cost (in which the fixed vehicle costs have already been folded into the depot–satellite and satellite–customer entries), positive integer demands , capacities for first- and second-level vehicles, a bound on first-level vehicles, second-level vehicles at satellite , a global bound on second-level vehicles, a capacity and a unit handling cost for each satellite.
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the cost of that closed walk. A second-level route leaves satellite , visits a set of customers and returns; its load is , counts its visits to customer , and its cost is its closed-walk cost plus .
Formulation uses binaries (route of satellite is used), binaries , and nonnegative integers (quantity route delivers to satellite ). It minimizes subject to: each customer is covered exactly once (2); at most routes at satellite (3) and overall (4); the load delivered from satellite is at most (5); at most first-level routes (6); what first-level routes bring to satellite equals what its second-level routes carry (7); and (8).
The LP relaxation replaces the integrality of by , . Its value is , equal to when is infeasible.
The relaxation relaxes (2)–(4) with penalties , and , and replaces the second-level routes by marginal routing costs that must satisfy, for every route ,
Its variables are binaries (customer is supplied from satellite ), and ; it minimizes
subject to single assignment of each customer, flow balance , satellite capacity , and (6), (8). A choice with and (12) is admissible.
Formally: (1) for every instance and route families whose is feasible, some admissible satisfies ; (2) some instance, route families and admissible choice give .
Theorem 2 places the relaxation in the hierarchy of bounds for the 2E-CVRP. The remark on explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so degrades as first-level routing costs grow. keeps binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through . The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation of the paper worth computing.
The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on needs positive first-level route costs, and the "max" in Theorem 2 is attained only when is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than .
is not the Lagrangean dual of in the textbook sense: it changes the variables (customer-to-satellite assignments instead of routes ), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of , an admissible that is compatible with the flow-balance and capacity constraints of . For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, , route loads at most , ), and must be feasible, so that the gap is a genuine gap between finite bounds.
Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families , are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, variables real. Optimal values are infima over the feasible set in EReal, for an infeasible problem; there is no junk value .
Part 1 of the goal assumes feasible: when is infeasible the printed relation would read "", which is not attained by any single choice of penalties. Part 2 requires , which rules out the trivial witness of an instance with infeasible; admissibility includes , without which the supremum is for trivial reasons.
The definitions (instance, route systems, , , (12), ) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect to the platform's general-form LP and its strong duality theorem are welcome.
Differential privacy (Dwork, McSherry, Nissim, Smith 2006) asks that a randomized algorithm run on a database behave almost identically whether or not any single record is changed. A central question for data curators is non-interactive release: publish, once, a sanitized object (ideally a synthetic database) from which analysts can answer many statistical queries accurately. Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that over a discrete data universe this is possible for every class of counting queries of bounded VC-dimension, with accuracy governed by the VC-dimension and the logarithm of the universe size.
That dependence on the universe size raises an obvious question: can the discretization be removed? For real-valued data the class of interval queries ("what fraction of the records lies in ?") has VC-dimension 2, so a learning-theoretic intuition suggests that releasing a database accurate for all intervals should be easy. Section 5 of the paper shows that it is impossible under differential privacy. This mission formalizes that impossibility.
The phenomenon was later quantified: Bun, Nissim, Stemmer and Vadhan (FOCS 2015) showed that for approximate differential privacy, releasing threshold queries over a finite ordered domain of size requires sample size growing with , so that the infinite case is impossible for approximate privacy as well. The present result is the pure-privacy statement for the real line.
A real-valued database of size is a tuple . Two databases are neighbours if they differ in exactly one coordinate. A mechanism maps each database to a probability distribution on a measurable output space . It is -differentially private if for all neighbours and all measurable ,
For real the interval query is . A mechanism with a readout (the answer that output gives to ; for synthetic data , ) is -useful for interval queries if for every database ,
A real number is a -percentile point of (the paper's " percentile" with ) if at least entries satisfy and at least entries satisfy . A mechanism with real outputs answers median queries usefully with positive probability if on every database its output is a -percentile point with positive probability.
In Lean, databases are Fin n → ℝ; neighbours and differential privacy are the published PrivLearn.Generic.Neighbors and PrivLearn.Generic.IsDP; the new objects are intervalQuery, IsPercentile, AnswersMedianUsefully and UsefulIntervals in PrivateRelease.Continuous.
For every , and , no -differentially private mechanism with a measurable readout is -useful for interval queries on :
No constant is hard-coded; the thresholds are the paper's.
For every , and real , no -differentially private mechanism answers median queries usefully with positive probability on every database:
The result. Corollary 5.2 is the reason the paper's general release mechanism needs a discretized data universe and why its halfspace mechanism (§6) relaxes usefulness to large-margin queries. More broadly it separates private release from non-private learning: the class of intervals is learnable from samples without privacy, yet no pure-private mechanism can release it at all over . It anticipates the line of work on private learning of thresholds and the role of the domain size in private query release.
Formalizing it. Both statements are proved in the paper; neither is, to our knowledge, machine-checked. A formal proof needs the countability of the atoms of a finite measure on , the stability of differential privacy under measurable post-processing, and a measurable selection of a percentile point from approximate interval answers. These pieces (especially post-processing for general measurable outputs) are reusable across formalized differential privacy.
The obvious argument for Theorem 5.1, a direct comparison of two neighbouring databases, gives nothing: changing one record moves the percentile set only slightly, and differential privacy allows each probability to change by a factor , so no single pair of neighbours yields a contradiction. A naive appeal to "the median reveals a record" also fails, since the statement must exclude even mechanisms that are correct with tiny positive probability.
For Corollary 5.2 the difficulty is measure-theoretic: the usefulness event intersects uncountably many conditions, the release must be converted into a single real output measurably, and the converted output must be a percentile point on the useful event for every real database, not only those in .
Conventions committed to in Lean:
Fin n → ℝ with ; the paper's neighbour relation "" is read as replace-one-entry.IsProbabilityMeasure (A z) is a hypothesis). Theorem 5.1's outputs live in with its Borel σ-algebra.Contributions welcome: a proof of Theorem 5.1; a general post-processing lemma for IsDP; the reduction from interval usefulness to median answers.
Many estimation problems in signal processing and statistics look for a vector with few nonzero entries that fits data well. Compressed sensing (Donoho 2006) recovers a sparse from linear measurements by minimizing over sparse vectors. Sub-wavelength optical imaging and phase retrieval (Shechtman, Eldar, Szameit, Segev 2011) lead to the same task with a quartic, nonconvex objective, because the measurements are quadratic in the unknown image. Beck and Eldar (SIAM J. Optim. 2013) treat the common abstraction: minimize a general smooth function under a cardinality constraint.
For linear least squares, greedy methods such as matching pursuit (Mallat, Zhang 1993) and orthogonal matching pursuit (Tropp 2004) add one coordinate at a time, and iterative hard thresholding (Blumensath, Davies 2008) is a projected gradient method. For a general nonconvex objective the question is which optimality condition an algorithm can actually guarantee at its limit points. Beck and Eldar introduce the greedy sparse-simplex method, a coordinate-descent scheme that never leaves the feasible set, and prove that its limit points satisfy coordinate-wise optimality, the strongest of the necessary conditions studied in their paper. This mission formalizes that convergence theorem.
Let and be integers with , and let be continuously differentiable and bounded below: there is with for all (Assumption 1, a standing assumption of the paper). The problem is
where the norm counts the nonzero components of . Write for the support of , for its complement, for the feasible set, and for the -th unit vector.
A feasible is a coordinate-wise (CW) minimum of (P) (Definition 2.4) if
Below the sparsity level no single coordinate can be changed profitably; at the sparsity level no support coordinate can be profitably swapped for any coordinate carrying any value.
The greedy sparse-simplex method starts from . If , it minimizes over all points (all , all ); if , it minimizes over all points with , any and any . If the best candidate strictly improves on it becomes ; otherwise the method stops. A run is any sequence produced this way, for any choice of minimizers.
For every run of the greedy sparse-simplex method and every accumulation point of ,
No Lipschitz assumption on is made.
Milestones 2–4 together with closedness of give the goal.
The theorem certifies what a cheap, feasible-point method achieves on a nonconvex, discontinuously constrained problem: its limit points cannot be improved by changing a single coordinate or by swapping a single support coordinate. Combined with Theorem 2.4 of the same paper (every CW-minimum is an -stationary point), it gives Corollary 3.2: when is Lipschitz, the limit points are -stationary, where is a local Lipschitz constant that can be much smaller than the global one used by iterative hard thresholding, and the method needs no knowledge of either constant. For quartic objectives arising in phase retrieval each inner step reduces to minimizing a scalar quartic, so the guarantee applies to a practical algorithm.
The result is proved in the paper (§4.2.1). As far as a search of the Prove2Me library shows, neither coordinate-wise optimality for sparsity constrained problems nor any convergence theorem for sparse-simplex methods has a machine-checked proof. The mission produces a formal model of the method that is faithful to its selection rules and stopping rule, and a formal proof of the convergence theorem. The companion missions of the series formalize Theorem 2.4 and the partial sparse-simplex method.
The obvious argument passes to the limit in the inequality "the next iterate is at least as good as every candidate move from the current iterate" along a subsequence converging to . This works directly when the candidate moves from converge to the candidate moves from . It fails in the case while the iterates near sit at the sparsity level : there the method cannot simply add a coordinate , only swap one out, and the candidate set from is not the candidate set from . The discontinuity of means that the regime of the iterates (below or at the sparsity level) need not be that of the limit.
Vectors live in EuclideanSpace ℝ (Fin n); indices are in Lean and on the page, and is EuclideanSpace.single i t. The function is ContDiff ℝ 1, Assumption 1 is the hypothesis ∃ γ, ∀ x, γ ≤ f x, and 0 < s, s < n are hypotheses, as in (P). No Lipschitz hypothesis appears anywhere.
A run is a predicate IsGreedyRun f s x on a sequence x : ℕ → EuclideanSpace ℝ (Fin n): , and each step is either a move to a point that strictly decreases and attains the minimum of over all candidate points, or a STOP, in which is at most every candidate value and the sequence stays put, (the convention behind Lemma 3.2). The argmin selections are therefore arbitrary, and every theorem holds for every run. An accumulation point is MapClusterPt xstar atTop x. Membership is part of the definition of a CW-minimum and has to be proved.
The predicate is not vacuous: a sorry-free check shows that on , , , the sequence , for is a run with one move followed by a STOP. A formalization in which the STOP branch is missing, or in which accumulation points are replaced by limits, would prove a weaker or empty statement and is ruled out by this encoding.
The needed infrastructure is small: closedness of , the behaviour of supports along convergent sequences (supports eventually contain the support of the limit), and continuity arguments for limits of inequalities. A lemma that the support of nearby points contains the support of the limit is reusable for any -constrained problem. Proofs of the milestones as stated, and alternative proofs of the goal, are welcome.
Theorem and page numbers refer to the arXiv version (arXiv:1203.4580v1), whose printed and PDF pages coincide; the published version is SIAM J. Optim. 23(3), 2013.
Differential privacy (Dwork, McSherry, Nissim and Smith 2006) is the standard guarantee for releasing statistics about a sensitive database: replacing one record changes the probability of any outcome by at most a factor . In their paper on non-interactive database privacy, Blum, Ligett and Roth propose an alternative motivated by learning theory, distributional privacy. When a database is a sample from a population, a release should reveal no more about the sample than is inherent in the population itself. Their example is a group of hospitals, each treating a random sample of the patients with a disease in a region: a hospital can publish information that describes the regional population without revealing which hospital's patients produced it.
The two notions look incomparable at first. Differential privacy protects only databases that differ in one record, but protects every such pair; distributional privacy can protect databases that differ in all their records, but only for typical pairs, and it tolerates a small failure probability . §7 of the paper (p. 19) shows that distributional privacy is the stronger notion once is small compared with . This mission formalizes that implication, Theorem 7.3.
Fix a data universe and a measurable space of outputs. In §7 a database of size is a set with ; databases are drawn without replacement, so they have no repeated elements. A mechanism assigns to each database of size the probability law of its random output, a measure on , and denotes .
The Lean development uses the same names: SetNeighbors, IsDPSet, GoodPair, badPairCount and IsDistPrivate in the namespace PrivateRelease.Distributional.
For a family of mechanisms , one per database size, and failure probabilities :
The goal keeps the paper's asymptotic hypothesis and leaves the rate of unfixed beyond .
For a single size , the threshold the paper's argument actually uses:
The goal follows from it, since forces eventually.
The result. Theorem 7.3 places distributional privacy above differential privacy: a mechanism designed for the distributional guarantee automatically inherits every consequence of differential privacy, including its composition properties and its robustness to auxiliary information about individuals. The paper complements it with a separation (Theorem 7.5), so the inclusion is strict. A footnote extends the conclusion to -privacy for databases that differ in elements.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The value of the formalization lies in fixing the definitions. Definition 7.2 is informal about the sampling model ("drawn at random without replacement"), about whether the guarantee holds for all events at once or event by event, and about what means for a mechanism defined on one database size. The proof's count "with probability " is also loose: the exact probability of a given unordered pair is . The mission records one precise reading of each and the theorem under it, and the definitions are reusable for further work on distributional privacy and on the paper's separation result.
The mathematics is short; the difficulty is in the encoding. The step that fails under a careless reading is the passage from "with probability " to "with certainty": it requires the population to be finite and small (the proof takes ), so that a single pair has probability bounded below. If the guarantee is read event by event (for each , most pairs satisfy the inequality for that ), the counting argument still applies to each event separately, but the definition is weaker than the paper's. If databases are allowed to repeat elements, the theorem is false, because distributional privacy never examines a database with repetitions while differential privacy does.
Finset X of cardinality ; a mechanism is A : Finset X → Measure R, and only its values on -element sets matter. [DecidableEq X] is assumed for set difference.(D \ D').card = 1). The paper's literal "" holds for equal-size sets only when ; the replace-one reading is the intended one.Tendsto (fun n => n^2 * β n) atTop (𝓝 0) and the conclusion is ∀ᶠ n in atTop; the claim for every would be false at small .Contributions welcome: proofs of the milestone and the goal, and the footnote's extension for databases differing in elements, stated as a new theorem.
A data curator holds a database of records and wants to publish answers to a large family of statistical questions about it without revealing any individual record. Differential privacy (Dwork, McSherry, Nissim, Smith 2006) makes the requirement precise, and the most basic questions are counting queries: what fraction of the records satisfy a given predicate? Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that a single private release can answer every query of a class to error once the database has size roughly , so that the sample size depends on the class only through its VC-dimension, a quantity from learning theory.
This mission formalizes the converse in §3.1 of that paper: the dependence on the VC-dimension cannot be removed. On databases of fewer than records, every differentially private mechanism has constant error on some query of . The argument is an early instance of the reconstruction attack idea of Dinur and Nissim (2003): accurate answers to many counting queries determine the database, and a mechanism that determines its input cannot be private.
Let be a set (the data universe). An input database of size is a tuple . A predicate is a map , and its counting query is
A class of predicates is identified with its class of counting queries. A finite set is shattered by if every function is the restriction of some ; the VC-dimension is the supremum of the sizes of shattered sets.
A mechanism maps each input to a probability distribution on an output space ; an output is read through an answer map . Two inputs are neighbours if they differ in exactly one entry. The mechanism is -differentially private if for all neighbours and all measurable events . It is -useful for if for every input , with probability at least over , every query is answered to within :
In the paper the output is a synthetic database and .
There is an absolute constant such that for every universe , class , size with , and : every -differentially private mechanism that is -useful for on databases of size satisfies
Theorem 3.11 shows that the VC-dimension term in the paper's upper bound is necessary: for a class of VC-dimension , no private mechanism is accurate on databases of size below , whatever its running time. It thereby locates the sample complexity of private query release between and up to accuracy and privacy factors, a gap that later work on private learning and on fingerprinting codes studied in detail (Bun, Ullman, Vadhan 2014).
The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a checked reconstruction-attack lower bound for differential privacy, together with the corrected statement disclosed below: the printed proof drops the failure probability of the two reconstructions, and keeping it shows that the conclusion requires below , not merely "bounded away from 1". Milestone 3 records the inequality the argument actually yields.
The combinatorial core (Lemmas 3.12 and 3.13) is elementary. The difficulty lies in the last step, which compares the output distributions on two different inputs. The paper argues about a uniformly random , a random element and a random , and the swapped set . Privacy applies to one fixed pair of neighbouring inputs and one fixed event, while the reconstruction guarantee only controls , not whether a particular element is recovered. The "probabilities" of the printed proof mix the mechanism's randomness with the random choice of , , , and they are not the probability of any single event under any single , so the privacy inequality cannot be applied to them as written. The reconstruction event must also be measurable, which depends on the readout, and the failure probability must be carried through both reconstructions. A proof that sets , as the printed one does, does not prove the stated theorem.
Fin n → X with ; the empty database is excluded because every mechanism is private on it and there. In the proof, a set is given to the mechanism as any injective listing of its elements.PrivLearn.Generic.Neighbors); read literally, it would make every mechanism private and the theorem false. Under this reading and are neighbours, so the paper's factor becomes .ans. Synthetic-data mechanisms are the special case databases, so the lower bound covers a larger class of mechanisms. The hypotheses require IsProbabilityMeasure (M z) and the measurability of o ↦ ans o φ for . Without the first, the zero measure is private; without the second, a mechanism into a trivial -algebra would be private and "useful".PrivLearn.Generic.Privacy (neighbours, IsDP) and Vershynin's HighDimProb.Chaining.Shatters and vcDim. Contributions needed: subsets of shattered sets are shattered, and yields a shattered set of size exactly ; measurability of the argmin reconstruction; the averaging/bijection argument. The first two are reusable beyond this mission.Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.
Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.
Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.
Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.
Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.
Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.
Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.
Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.
Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.
The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.
Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.
Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.
The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.
Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.
Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, -regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.
Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.
The space is split into blocks, with and every . A point is the family of its blocks , and is the point whose -th block is and whose other blocks are zero. Each block carries a Euclidean norm with (3.4).
The objective is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing for the -th block of the gradient, there are constants with
The weighted norm is (3.5). The function is strongly convex in with constant if for all (3.1).
The problem is (4.1), with and each nonempty, closed and convex. Its optimal value is , attained at an optimal solution . The constrained coordinate update (4.2) is
The uniform coordinate descent method UCDM (4.5) draws uniformly from and sets . Its expected objective is , the expectation over . The level-set radius is the largest -distance between a feasible with and an optimal solution.
For every ,
and, if is strongly convex in with constant ,
The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each , the cost of the unconstrained one: block steps for accuracy , and under strong convexity. The method needs no knowledge of ; the same iteration attains whichever rate applies. The Lyapunov function of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.
The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming , which is where footnote 2 enters.
is the dependent product Blocks E , each a finite-dimensional real inner product space whose inner product is the paper's . Indices are 0-based. The dual norm is the operator norm of linear functionals, and is the Fréchet derivative of composed with the block inclusion. Random draws are explicit index sequences, so is the finite average of over all sequences of draws; no measure theory is involved.
Explicit choices where the paper is silent:
A formalization in which the update is an arbitrary point of or an unprojected gradient step, the draws are not uniform, or is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.
Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.
Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.
Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.
Timeline:
All matrices are arrays of complex numbers with . A matrix is self-adjoint (Hermitian) when ; it then has real eigenvalues, and denotes the largest one. For a function and a self-adjoint with unitary and diagonal, . This defines the matrix exponential of every self-adjoint matrix and the matrix logarithm of every positive-definite matrix, with . The trace exponential is .
A random self-adjoint matrix is a measurable map from a probability space to the self-adjoint matrices. Its expectation is the matrix of the expectations of its entries. A finite sequence is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of are
which may fail to exist for some . In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.
For independent random self-adjoint matrices and every ,
It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.
The master bound reduces every tail estimate for of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.
All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).
The scalar argument factors , which needs . For non-commuting matrices , so this step fails. The Golden–Thompson inequality handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever appears; for the largest eigenvalue would be and the bound would fail at . Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.
The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of is integrable for the in question. The infimum over is stated as the bound for every at which the moment generating functions exist; since an inequality is equivalent to for every , and the paper treats a non-existent moment generating function as , this is exact. A real-valued infimum over , or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ( of an unbounded set and the integral of a non-integrable function are ); the formalization rules both out.
Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.
In city logistics, goods often cannot be carried by large trucks all the way to the final customers. A common design routes the goods through intermediate depots, called satellites: large first-level vehicles carry freight from a central depot to the satellites, and small second-level vehicles deliver it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest such two-level distribution plan. It contains the capacitated vehicle routing problem as a special case (a single satellite), and the location-routing problem can be reduced to it.
Exact methods for problems of this kind rest on lower bounds: a branch-and-bound or enumeration scheme can discard a partial solution only when it has a certified bound above the best known cost. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built an exact algorithm for the 2E-CVRP on a chain of relaxations of a set-partitioning formulation . Its first link is a Lagrangean relaxation and a further relaxation , a multiple-choice knapsack problem solved by dynamic programming. Its optimal value, maximised over the penalties, gives the lower bound that drives the rest of the method. This mission formalizes the statements that make a valid bound.
An instance has a depot , satellites and customers , a symmetric cost matrix (with the vehicle fixed costs already added to the depot–satellite and satellite–customer entries), positive integer demands with total , first-level vehicles of capacity , second-level vehicles of capacity at satellite , a global limit on second-level vehicles, satellite capacities and handling costs per unit.
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the cost of this closed walk. A second-level route is a simple cycle from satellite through a set of customers of total demand ; its cost is the cost of the cycle plus . In formulation , binary variables and select the routes and integers give the amount that route delivers to satellite . The constraints require that every customer is served exactly once (2), that the vehicle limits , , hold (3), (4), (6), that satellite capacities hold (5), that each satellite receives what its routes deliver (7), and that first-level capacities hold (8).
Relaxation removes (2)–(4) with penalties , , , and replaces the second-level routes by marginal costs of serving customer from satellite , subject to
where counts the visits of route to customer . Its variables are an assignment of customers to satellites and the first-level variables , .
Relaxation chooses for every first-level route at most one load in the interval of integers, so that the loads add up to . A route with load costs , where is the optimum of a continuous knapsack problem that serves demand at the cheapest marginal costs . Both objectives carry the constant .
For every satisfying (12), every , every , , and every feasible solution of with cost ,
The bound is the first lower bound of the paper's exact method. The configuration enumeration of its §5 and the reduced-cost elimination of second-level routes both use it as a certificate: a configuration or a route is discarded only when this bound shows that no cheaper solution contains it. If the bound were invalid, the method could discard the optimum. Theorem 4 provides, at every step of the paper's subgradient procedure, a to which the bound applies.
The paper's proofs are in an electronic companion. As printed, Theorem 3 () is false: does not limit a satellite's load by its fleet capacity , whereas the loads of are capped by it. A small instance with one satellite and two unit-demand customers, and has finite and . The bound (23) is nevertheless true, because the solutions that come from feasible solutions of respect the fleets. A machine-checked version pins down exactly which hypotheses the chain needs, including the positivity of demands, without which (23) fails. None of these results has been formalized before.
Theorems 1, 4 and Corollary 1 are bookkeeping with sums over routes, customers and satellites. The substantive step is the corrected Theorem 3. A solution of assigns whole customers to satellites, while sees each first-level route only through its total load and a continuous knapsack. The two descriptions have to be related, and that relation must respect every side condition of : the knapsack bounds , the load window (whose lower end depends on the vehicle count ) and the fleet cap . The obvious route, comparing the optimal values and directly as the paper states, does not work: the inequality between them is false, and the fleet condition is what has to be carried from .
Satellites are Fin ns, customers Fin nc (0-based). Demands are positive integers; capacities, fleet sizes and loads are natural numbers, and costs are real. Binary variables are Bool and integer variables ℕ. The route families and are arbitrary finite families of routes (nonempty, no repeated vertex, second-level loads at most ), not necessarily all routes as in the paper; every statement holds in this generality. Route costs are computed along the closed walk, so costs . The triangle inequality is not assumed. Optimal values , and are infima in EReal, equal to on infeasible problems, and comparisons with an upper bound are written with instead of . Where the paper writes "optimal solution of cost below ", the statements cover every feasible solution below any real .
The formalization cannot be trivialized: every optimal value is an infimum over the feasible set of the paper's own problem, so it equals , not , when that set is empty. The hypotheses of each theorem are satisfiable, which is checked on explicit small instances. The definitions of the instance, , and are written in the shape shared by the other missions of this series. Proofs of any milestone and reusable lemmas on finite sums over route families are welcome.
Coordinate descent methods update one block of variables at a time. For problems with millions or billions of variables, where even one full gradient is too expensive to compute or store, a step that touches a single block can be orders of magnitude cheaper than a full gradient step. Nesterov's Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global complexity bounds for randomized coordinate descent on smooth convex functions: choosing the block at random makes the expected progress per step comparable to that of a full gradient step divided by the number of blocks.
Section 5 of the paper asks whether the multistep acceleration of the full gradient method (Nesterov 1983) carries over to the randomized coordinate setting, and answers it with the accelerated coordinate descent method ACDM. This mission formalizes that answer: Theorem 6, the expected rate of ACDM, together with the lemmas of its proof.
Timeline. Nesterov (1983) introduced the accelerated full-gradient method with rate . Nesterov (CORE DP 2010/2; SIAM J. Optim. 2012) proved the rate of random block coordinate descent and the rate of its accelerated variant ACDM. Later work (Lee and Sidford 2013; Fercoq and Richtárik 2015, arXiv:1312.5799; Allen-Zhu, Qu, Richtárik and Yuan 2016, arXiv:1512.09103) made the accelerated scheme efficient per iteration and sharpened its constants.
The space is , split into blocks. A point has blocks , and is the point whose -th block is and whose other blocks vanish. Each block carries a Euclidean norm with .
The objective is convex and differentiable, and has a coordinate-wise Lipschitz gradient: the partial gradient satisfies with constants . The method weighs blocks by these constants through the norm
The function is strongly convex in this norm with parameter if for all ; is plain convexity. A point minimizes , and .
The optimal coordinate step is , where maximizes . ACDM keeps two sequences with and deterministic scalars , . At step it computes from , sets and , forms , draws a block uniformly at random, and updates
, . The quantity is the expectation over the first draws.
For every , with ,
and, when ,
The result. Theorem 6 shows that randomized coordinate descent can be accelerated: the expected error falls as instead of the of the plain method, so after iterations (about full-gradient equivalents) the error is , the rate of the accelerated full-gradient method. For the same scheme converges linearly with a ratio governed by rather than . This is the starting point of the accelerated randomized coordinate methods (APPROX, NU-ACDM, accelerated proximal coordinate gradient) now used in large-scale machine learning.
Formalizing it. The theorem is proved in the paper; to our knowledge neither it nor any accelerated coordinate method has a machine-checked proof. The Lean development pins down a scheme whose correctness rests on a delicate parameter identity and on several conventions left implicit in the text (the range of , the reading of (5.3) at ).
The plain coordinate descent analysis tracks alone and fails to accelerate: one coordinate step gains only of a full gradient step, and a momentum term built naively from coordinate steps does not keep the expected progress. The accelerated proof needs a potential mixing the function gap with a squared distance , weighted by the deterministic sequences and ; the weights must make the cross terms in and cancel exactly after taking the expectation in the drawn block, which is what the coupled choice of achieves. The second difficulty is quantitative: the growth of follows from coupled recursions for and , not from a closed form.
Blocks E, the dependent product of finite-dimensional real inner-product spaces E i over Fin n (indices ); is absorbed into the inner product of E i. The dual norm is the operator norm of E i →L[ℝ] ℝ.Fin k → Fin n; and are finite averages over all sequences with weight . No measure theory is needed.Blocks, partialGrad, CoordLipschitz, coordStep, wnorm, expect) is shared verbatim with the other missions of this series. The coefficient lemmas (5.2), (5.4), (5.5) and the growth bounds are pure real analysis and welcome as standalone contributions; so is a Lean proof of the block descent inequality (2.3)–(2.4) for Euclidean blocks, which the potential inequality needs.ConvexOptAlg.NesterovSmooth.theorem_3_19). https://arxiv.org/abs/1405.4980Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem
where is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and its solutions are not characterized by the classical KKT theory.
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) introduced a hierarchy of necessary optimality conditions for (P) and matched each condition with an algorithm whose limit points satisfy it. Iterative hard thresholding (Blumensath and Davies 2008) reaches -stationarity for ; the greedy sparse-simplex method reaches coordinate-wise minimality, but each of its iterations calls up to one-dimensional minimizations. This mission formalizes the paper's compromise between the two: the partial sparse-simplex method, which examines only two candidate moves per saturated iteration, and whose limit points are -stationary.
Vectors live in with the Euclidean norm; is the -th unit vector. For :
The objective is continuously differentiable and bounded below (Assumption 1, standing throughout the paper). Assumption 2 asks that be Lipschitz with some constant . A constant satisfies the local Lipschitz condition (2.15) if for every pair , every and every supported in ,
The paper's local Lipschitz constant satisfies it, and .
The projection is the set of points of nearest to . For , a point is an -stationary point (Definition 2.3) if
The partial sparse-simplex method (p. 25) starts at . If , it moves to the best point over all and if that strictly decreases , and stops otherwise. If , it compares two candidates and takes the better one, preferring the second on ties:
Under Assumption 2, with satisfying (2.15), every accumulation point of a sequence generated by the partial sparse-simplex method satisfies
that is, is an -stationary point.
The theorem shows that a cheap index-selection rule does not cost optimality strength relative to iterative hard thresholding: every limit point satisfies , and since , this is a stronger necessary condition than the guaranteed by IHT with stepsize . In the paper's numerical comparison (Example 3.3 contd., Table 3) the method performs much better than IHT and only slightly worse than the greedy method, at a fraction of the greedy method's cost per iteration. The decrease estimates of Lemma 4.1 are the quantitative content: they turn each iteration into a lower bound on the objective decrease in terms of the violation of -stationarity.
The results are proved in the paper; to our knowledge none is machine-checked. This mission produces a formal model of the method (with its selection rules as inequality predicates, so every run is covered), the local descent lemma for two-sparse directions, and a checked proof of Theorem 3.4. The printed proof of the case contains two gaps (see Difficulty); a formal proof settles the argument.
The decrease estimates follow from the local descent lemma applied at well-chosen trial points, but passing to the limit is delicate. When , the supports of the subsequence eventually coincide with and becomes continuous there; when , the iterates along the subsequence may still have nonzeros, and does not by itself force , because kills the second term of . The swap move optimizes along a single off-support coordinate , chosen by the derivative at and not at the shifted point where the optimization happens. The printed display (4.19) claims the bound for the maximum over all of at the shifted point, which the argument does not give, and the final display takes a minimum of two bounds that each hold on only one class of indices. Theorem 3.4 itself is not affected, but a complete proof cannot follow those two displays as printed.
Lean works in EuclideanSpace ℝ (Fin n) (indices ), with of class and = gradient f. Conventions fixed by the formalization:
LipschitzWith Lf (gradient f)) are hypotheses.MapClusterPt xstar atTop x.The run predicate is satisfiable and does not force a STOP: on , , , the constant sequence at is a run. The conclusion is the projection condition itself, not the coordinate form (2.5), so it cannot be met by an empty or degenerate reading of stationarity.
Reusable parts: the local descent lemma for two-sparse directions, Lemma 2.2 (the coordinate characterization of , shared with the IHT mission of this series), and the order statistic . Contributions of proofs for any milestone are welcome, as is the companion result Lemma 3.3 (limit points are BF vectors without Assumption 2).
Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem
where is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and the classical optimality theory (KKT conditions, convex duality) gives no usable characterization of its solutions.
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) replaced that missing theory with a hierarchy of necessary optimality conditions of increasing strength, and matched each condition with an algorithm whose limit points satisfy it. This mission formalizes the comparison between the two strongest conditions of that hierarchy: coordinate-wise minimality and -stationarity.
Vectors live in with the Euclidean norm. For :
The objective is continuously differentiable and bounded below (Assumption 1). Assumption 2 asks that be Lipschitz with some constant .
The local Lipschitz condition (2.15) with constant asks that for every pair , every and every supported in ,
where . The paper's local Lipschitz constant satisfies it, and , often by a large factor.
A point is a basic feasible (BF) vector (Definition 2.1) if when , and on when .
A point is a coordinate-wise (CW) minimum (Definition 2.4) if either and for every and every (Case I), or and
(Case II): no swap of a support coordinate for any coordinate, with any value, decreases .
Every CW-minimum of (P) satisfies
that is, is an -stationary point. The constant multiplies exactly.
Optimality conditions for (P) matter because no efficient algorithm finds a global minimizer; what algorithms can guarantee is a limit point satisfying some necessary condition, and the strength of that condition is the guarantee. The paper's hierarchy runs: optimal CW-minimum -stationary -stationary for BF vector. Theorem 2.4 is the step that ties the coordinate-wise notion, which needs no Lipschitz constant to state, to the stationarity notion behind iterative hard thresholding. Combined with "every optimal solution is a CW-minimum", it shows that every optimal solution of (P) is -stationary, with the local constant instead of . It is the reason the greedy and partial sparse-simplex methods of the same paper, whose limit points are CW-minima or -stationary, are at least as strong as iterative hard thresholding.
The result is proved on paper. To our knowledge none of these notions (BF vectors, CW-minima, the local Lipschitz constant, the local descent lemma) has a machine-checked formalization. The mission produces a formal statement of the hierarchy's central step together with reusable definitions of the sparse-optimization objects, which the companion missions on the same paper (iterative hard thresholding, the greedy and partial sparse-simplex methods) state their results against.
The local descent lemma has no proof in the paper ("it is not difficult to see"). The global descent lemma integrates the gradient along the segment and applies the global Lipschitz bound; the local version must instead observe that along a direction supported on two coordinates only the two corresponding gradient components enter, and that the restricted Lipschitz bound (2.15) controls exactly those. Formally this requires the integral form of the mean value theorem for functions on a Euclidean space, together with the bookkeeping that stays in the class of perturbations allowed by (2.15).
In Theorem 2.4 the natural first attempt, perturbing a single zero coordinate and comparing with , fails when : the perturbed point has nonzeros and is infeasible, and Case II of the definition only compares with points obtained by swapping a support coordinate out. The bound on must therefore be extracted from swaps alone, and the degenerate case breaks the printed identity in the paper's chain (2.18).
All statements are in the namespace SparseNLO.CWOpt and work on EuclideanSpace ℝ (Fin n); indices run over Fin n, so instead of . The gradient is Mathlib's gradient, is EuclideanSpace.single i t, and is ContDiff ℝ 1. Assumption 1 is carried as a hypothesis on every statement, as the paper's standing assumption; Assumption 2 is carried wherever the page states it, with a free constant .
is the entry at position of the list of sorted in nonincreasing order; the hypotheses of (P) make it meaningful. The local Lipschitz constant is not computed as a maximum: is any real constant satisfying (2.15), with "at most two nonzero components" read as "supported in some , " (the reading of Example 2.1). Every statement therefore holds for every valid , in particular for . The minima in (2.11)–(2.12) are written as " every value", which is equivalent. The goal states the displayed condition (2.16); its identification with Definition 2.3's -stationarity goes through Lemma 2.2, which belongs to a companion mission.
A trivializing formalization is ruled out: the CW-minimum predicate requires feasibility in and is satisfiable (for , , , the point is a CW-minimum), is the -th largest absolute value, and is constrained by (2.15) rather than left free.
Contributions welcome: proofs of Lemma 2.6 (reusable for any coordinate-descent analysis on two coordinates), Lemma 2.5, (2.18) and the goal; general lemmas on (it is attained by some coordinate, and it vanishes exactly when ).
Theorem numbers and pages follow source.pdf, the arXiv version arXiv:1203.4580v1, not the SIAM typesetting.
How many Euclidean symmetries can a real plane algebraic curve of degree have? Rotational symmetry of a curve is classically detected from the monomials of its equation in the complex coordinate : a rotation of order about the origin can preserve the curve only if the differences of the nonzero monomials satisfy a congruence modulo (Lebmeir and Richter-Gebert, Section 4; Lebmeir, Theorem 5.4). Bounds on the number of symmetries in terms of the degree enter symmetry detection algorithms (Alcázar, Lávička and Vršek) and incidence geometry: Pach and de Zeeuw, Lemma 2.6 use a bound of on the number of isometries of a curve in a distinct-distances argument.
The note Sharp symmetry bounds for real algebraic curves (C. Perassi, 2026; PDF) determines the sharp bounds, classifies the curves attaining the rotation bound in degree , and describes their Möbius geometry. This mission is the complete Lean formalization of that note.
Let be irreducible in , of total degree , and let , identified with a subset of through . Assume that is infinite and is not a circle. Write for the group of Euclidean isometries of with , and for its orientation-preserving subgroup (the rotations and translations preserving ).
For an integer and a nonreal with , the extremal family is
a curve of degree . Its closure in the Riemann sphere is acted on by Möbius maps and by anti-Möbius maps, a Möbius map composed with complex conjugation. In the coordinates , the family has the equation , whose zero set has bidegree .
The goal asserts the bounds only; their sharpness and the equality case are milestones.
The result. The bounds and are attained in every degree, so they cannot be improved as functions of alone; for the curves attaining the rotation bound form one explicit family up to similarity, with a complete invariant. The bound sharpens the auxiliary estimate used by Pach and de Zeeuw (no improvement of their distance exponent is claimed), and the quintic of equation (2) contradicts the degree restriction stated in Lemma 9 of the arXiv version of Alcázar, Lávička and Vršek (the journal version has not been checked).
The formalization. Every statement of the note is proved in Lean 4 with Mathlib: 208 theorems and 12 definition files here, all proved, using only the axioms propext, Classical.choice and Quot.sound. It contains material that Mathlib does not have yet and that is reusable on its own: the genus of a function field over defined through its places and holomorphic differentials, and its invariance under isomorphism; the places of quadratic covers and Kummer covers , with uniformizers and local Kähler differentials; the classification of places of a Dedekind domain; the four-chart atlas of with its Zariski topology; and Möbius and anti-Möbius maps acting on the Riemann sphere. Theorem 1 is also registered with the Palomar registry as PALOMAR-2026-09-18-000007. The Lean code was written by AI agents under the author's direction; the Lean kernel checks it. The results have not been reviewed by an independent human, and neither the kernel checks nor the registration certify novelty.
The first argument is Bézout: the images of a point of under the rotations about a common center are distinct points on one circle, so there are at most of them. This gives for , not , and it says nothing about which curves are extremal. A second obstacle is that a symmetry of the zero set need only fix the polynomial up to sign, as equation (2) shows, so invariant-theoretic arguments that assume do not apply directly. For the Möbius statements the difficulty is that a Möbius map of the sphere does not act on the real equation; the curve must be compactified and its singular points identified. In the formalization, the genus comparison of Remark 5 needs a genus that does not depend on a chosen model, which Mathlib does not provide.
MvPolynomial (Fin 2) ℝ), and the curve is their real zero set as a subset of . Geometric irreducibility means irreducibility over .ℂ ≃ᵢ ℂ preserving that subset. Group orders use Nat.card, which is for an infinite set, so finiteness is part of the statements.OnePoint ℂ with the action of .Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.
Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.
Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.
All matrices are with complex entries, . A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. , is its largest eigenvalue and its spectral norm. Functions of s.a. matrices are defined spectrally: if then , and is defined the same way on positive-definite matrices. is the semidefinite order: is positive semidefinite.
Let be a probability space with a filtration , and write . The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence of random matrices is adapted when each is -measurable. A matrix martingale is an adapted sequence of s.a. matrices with and ; its difference sequence satisfies .
The hypotheses of the main theorem are: is an adapted sequence of random s.a. matrices, and is a fixed (non-random) sequence of s.a. matrices, with
The variance parameter is .
For all ,
In the order they are used:
Corollary 7.2 is the martingale form, . Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, for a matrix-valued function of independent variables whose changes in one coordinate have squares bounded by .
The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor , and a variance parameter equal to the norm of the sum rather than the sum of the norms . In the commuting case the two coincide; in general the first can be smaller by a factor of up to . The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).
Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.
The scalar proof of Azuma's inequality multiplies conditional moment generating functions, , and bounds each factor. For matrices this fails: unless and commute, and is false, so the Golden–Thompson inequality cannot be iterated over terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis bounds squares, not the matrices themselves; it does not give , so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.
Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. is the supremum of the real spectrum, which is why is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by , so is never truncated. The bound is required almost surely. The bounds are deterministic matrices. The infimum over in Proposition 3.1 is posed as the bound for each at which the expectation is finite.
The hypotheses must not be made vacuous. Integrability of each is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is and the centring hypothesis would say nothing. The are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.
Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given is replaced by the expectation over at each fixed value with ; by independence these agree. Corollary 7.2 adds the hypothesis that is almost surely constant, without which .
A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.