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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
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.
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 problems in data analysis and signal processing are posed as minimizing a sum of three terms over two blocks of variables: a nonsmooth function of the first block, a nonsmooth function of the second block, and a smooth coupling term. Nonnegative and sparse matrix factorization, blind deconvolution and dictionary learning all have this form, with constraints or sparsity penalties as the nonsmooth parts. The functions involved are usually nonconvex, so convexity-based convergence theory does not apply, and the classical alternating minimization (Gauss–Seidel) scheme requires solving an exact nonconvex subproblem in each block.
Bolte, Sabach and Teboulle (Math. Program. 146 (2014)) introduced Proximal Alternating Linearized Minimization (PALM), which replaces each exact block minimization by one proximal-gradient step, and proved that every bounded sequence it generates converges to a critical point whenever the objective has the Kurdyka–Łojasiewicz property. The result became a standard template for the convergence analysis of first-order methods on nonconvex, nonsmooth problems.
Timeline.
Let and , let , and set
The product carries the Euclidean norm . Assumption A: and are proper (never , finite somewhere) and lower semicontinuous, and is . Assumption B:
The proximal map of with parameter is the set
Fix . A sequence is generated by PALM if, from an arbitrary , with and ,
The limiting subdifferential consists of the limits of Fréchet subgradients at points with ; is critical if . Let be the class of continuous concave functions with , on and there. A proper lsc has the KL property at if there are , a neighbourhood of and with
and is a KL function if it has this property at every point where is nonempty.
If is a KL function, Assumptions A and B hold and is a bounded sequence generated by PALM, then
The result. Theorem 3.1 gives convergence of the whole sequence, not only subsequential convergence, for a method whose steps are explicit: a gradient step on followed by a proximal step on or . The KL hypothesis holds for semi-algebraic, subanalytic and o-minimal data, which covers penalties, rank constraints and polynomial couplings. The paper applies the theorem to sparse nonnegative matrix factorization (Theorem 4.1), and the same scheme (sufficient decrease, relative error, KL) underlies many later convergence proofs for nonconvex splitting and alternating methods.
Formalizing it. The result is proved on paper; no machine-checked proof is known to exist. A formalization produces reusable components: the nonconvex proximal-gradient decrease lemma, the structure of limit point sets of sequences with vanishing steps, and the uniformized KL lemma, which is independent of PALM and is used in essentially every KL-based convergence proof.
Lemmas 3.2–3.5 are estimates and compactness arguments; the core difficulty is in passing from them to convergence. Square-summability of the steps (Lemma 3.3) does not give summability of the steps themselves, and a bounded sequence with vanishing steps may wander along a continuum of limit points. The KL inequality supplies the missing control, but only near each critical point separately, with point-dependent and ; the iterates are known only to approach the compact set , not a single point. Combining Lemma 3.6 with the decrease and relative-error estimates requires handling the concave function along the sequence and an extended-valued whose subdifferential is a limiting construction. Lemma 3.5(i) also needs along subsequences, which lower semicontinuity alone does not give.
, are EuclideanSpace ℝ (Fin n), EuclideanSpace ℝ (Fin m), and the product is the product WithLp 2 (… × …) of the published setting ProxAltMin.Conv.Setting, not Lean's default product with the sup norm. Values in are EReal. The prox map is a set with weight , exactly as in (2.2). Iterates are selections from it, and the starting point is arbitrary, so is allowed; inequalities between values of are stated with the difference moved across. are given modulus functions and fixed constants. The limiting subdifferential and the KL notions are the published definitions NonconvexSplitting.Shared.LimitingSubdiff and NonconvexSplitting.ADMMKL.KLProperty, with real and the KL inequality read for every (equivalent to the form). Assumption A together with B(iv) is AssumptionH; B(i)–(iii) and the PALM run are defined in PALM.Conv.Setting. The satisfiability of all hypotheses of the goal has been checked on a concrete instance.
The goal is not weakened: it asserts summability of and convergence of the full sequence to one critical point, not that every cluster point is critical (that is Lemma 3.5(i)). The constants and are explicit as in the paper, with chosen once for all .
Theorem numbers and pages are those of the author version (source PDF), whose page numbers coincide with its printed pages; they may differ from the Springer typesetting.
Welcome contributions: proofs of any milestone; a general-space version of Lemma 3.2; a proof of the published Proposition 2.1 (ProxAltMin.Conv.proposition_3, still open), which Lemma 3.4 relies on.
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.
The Weil positivity criterion relates the zeros of the Riemann zeta function to an arithmetic quadratic form. The existing Connes mission now has a proved positivity-implies-RH goal. Stronger actual-zero quartet separation also controls the complete complementary coefficient energy. Neither result by itself identifies those scalar coefficients with the adjoint of a physical Dirichlet Green operator.
This mission addresses that identification. The underlying mathematics is the classical Hilbert-space realization of a positive Dirichlet operator, as treated in Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, applied to the original source functions and analytic multiplicities in the Connes–Weil development. It formalizes a known functional-analytic construction; it does not claim a proof of Weil positivity or unconditional RH. The exact goal is the assembly specified below, rather than a theorem quoted verbatim from Brezis or Connes.
Fix a positive radius and put , with restricted Lebesgue measure. A supported test is a smooth compactly supported complex function on the real line whose closed support lies strictly inside . The differential operator and its energy map are
The ambient space is the Hilbert direct sum of two copies of , using the sum of squared norms, not the Banach product maximum norm. Define the physical carrier to be the closure of the complex linear span of for all supported tests. Thus its metric is fixed by
This carrier is defined independently of the zeta-zero set. It is the energy-image completion of the Dirichlet test space; the source-side interpretation is through Riesz representation, not by identifying the positive Sobolev norm of with the source norm of .
For an source , the source lift is the orthogonal projection of onto . The factor two fixes the pairing convention: its inner product against represents . The induced map on functions uses their classes. Its total definition sends non- functions to zero; all actual sources and tests used in the target must explicitly satisfy the required conditions, so this fallback cannot discharge the target.
Let be exactly the set of zeros of the actual Riemann zeta function with . Let be their natural analytic multiplicity. No surrogate zero configuration or simple-zero convention is used. Write
The original Green column is the existing function
Its energy is the existing Dirichlet integral . The reflected ordinate is retained because the Hilbert inner product is conjugate-linear in its first argument. The ported native definitions have been checked for definitional equality against the repository definitions.
The goal, for every , is the following conjunction. First, the source lift from has dense range in . This asserts density, not surjectivity. Second, every actual Green column has the required regularity and belongs to the prescribed energy completion, and
Third, for every supported test , the source is square integrable, the Green product is integrable, and
Finally, the full actual-zero weighted energy is summable. For , construct the bounded synthesis with these exact columns. Every synthesis series must be summable, and
Require uniqueness among bounded maps on this same coefficient carrier with these same basis columns. None of these norm, projection, density, pairing, or summability conclusions appears as a hypothesis of the goal.
The published reciprocal-square theorem supplies the actual-zero majorant underlying the native energy bound. The published bounded-synthesis theorem supplies the generic operator construction and adjoint identities. They are included as references with their existing identities, not re-created.
The aggregate goal and all seven original mission milestones are now Proved on P2M, with zero open leaves. The independent native development also proves original-constructor physical selected-quartet separation, preserving the exact columns, packet coefficients, complete positive zero family, analytic multiplicities and half-sum/half-difference actor normalization. The realization hypotheses have been discharged for the specified carrier at each positive support window. Neither this construction nor conditional positivity-implies-RH establishes Weil positivity or unconditional RH.
An explicit smooth column vanishing at the endpoints is not, solely by those facts, an element of the closure of tests supported strictly inside the interval. The certified proofs establish that boundary-density statement in the chosen energy topology and identify the Riesz projection with the explicit Green column. Source-lift density uses the value component to distinguish vectors in the closed derivative graph. No physical column-norm or pairing assertion is assumed.
All definitions, target statements and accepted proofs are checked against Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The additive repository model also compiles with the existing Lean 4.34.0 development. The approved mission retains its shared definition bundle, aggregate goal and seven original proved milestones. Subsequent accepted supporting library lemmas are linked separately, with their exact published hypotheses and conclusions.
Each support radius has its specified carrier . Subsequent native results construct the original test-preserving isometries for nested positive support windows and transfer their actual source columns and syntheses. These are constructed inclusions, rather than identifications with a single fixed physical carrier. Downstream packet transfer retains the same-radius basis-column custody. The goal makes no claim that every prescribed window contains a negative Weil witness. The globally constructed separating test may choose its support radius after amplification. The original finite-packet inner regularization norm limits and outer right-hand support norm limits are proved natively, in that order. Subsequent certified reductions classify actual-quartet good windows and express the original fixed-window half-bound as all-accuracy finite certificates. These results do not prove the arithmetic lower inequality. Identification with the prescribed arithmetic/provenance packet endpoint and the arithmetic endpoint lower bound with original neutral-shell custody and persistence remain open for ZP-WEIL-MARKER-TRANSFER / RH-ZERO-PROV-2. The selected-coefficient certificate theorem retains the complete actual-positive tail; it establishes an equivalence, not certificate nonnegativity.
The Textbook category applies to this mission's original known functional-analytic construction. Its realization-and-synthesis goal is complete. The existing downstream milestone list and dependency graph are retained as an archive of certified extensions; milestone completion does not mean that every linked result is a premise of the original goal or that RH has been established. Future supporting definitions and lemmas remain shared library nodes unless they warrant a substantial, source-grounded checkpoint.
The unresolved arithmetic lower bound is being organized in a separate OpenProblem draft, Connes–Weil arithmetic lower bound: cofinal actual-quartet certificates. Its target requires arbitrarily large actual-quartet windows with all-accuracy nonnegative selected certificates and the complete omitted positive tail controlled at the same accuracy. The existing cofinal quartet criterion and finite selected-certificate criterion are proved reductions. The new draft goal itself is unproved and is equivalent to RH in the existing development.
monocap-tech/weil, existing native definitions in DirichletResolvent.lean and DirichletEnergy.lean. Canonical model and goal specification are supplied explicitly in this proposal. The complete independently checked Green-frontier source snapshot has SHA256 ce194a69770846a9027a274e581de56b507be219c393d080a06259e175cbe798; this is a source custody record, not a claim that the archive was attached to P2M.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.
All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an -vertex weighted directed graph. Floyd–Warshall solves it in time, and for decades no algorithm beat for any constant on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) gave a deterministic algorithm, the campaign's first entry. Later entries tightened the accounting to , and .
This entry records the deterministic exponent , a saving of about below , roughly 11% more than the entry.
The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo , indirect load and store, a sign branch, and accept or reject, on words of width . Inputs have integer weights of absolute value at most for a fixed , and there are no negative cycles. The machine has no source of randomness; the algorithm behind this entry is deterministic.
The goal is the campaign template with the value :
which says there is a deterministic word-RAM program that solves APSP in steps.
The algebraic core is the tensor construction of Alman and Vassilevska Williams, which evaluates independent by integer products in one run and answers requested output entries. Two local refinements sharpen its exponents: pruned encodings (branches with more than copies of the symbol are never materialized) and an exact binomial tail for the box preprocessing, giving
On top of the deterministic filtering reduction of the entry (moduli chosen one small prime factor at a time, with exact modular witness counts certifying positive answers and eliminating blocks of unresolved queries), this entry adds two changes to the counting oracle:
With middle blocks of size the encoding cost becomes with , and all-edges Exact Triangle runs in with
subject to the batch conditions and , where . Deterministic bit scaling transfers the bound to min-plus product and APSP with polylogarithmic overhead.
The exact rational parameters , and give (rational interval certificate for with error below ). Hence APSP runs in , and the gap absorbs the subpolynomial factor.
This is the strongest deterministic entry so far. Compared with , the saving below cubic time grows from about to about , coming entirely from cheaper input encodings in the counting oracle.
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.
Genetic algorithms with local search ("memetic" or hybrid genetic algorithms) are among the most effective heuristics for vehicle routing. Their recurring weakness is premature convergence: selection and local improvement both favour good individuals, so the population fills with near-copies of a few solutions and the search stalls. Vidal, Crainic, Gendreau, Lahrichi and Rei addressed this in their hybrid genetic search with adaptive diversity control (HGSADC) for multi-depot and periodic vehicle routing (CIRRELT-2010-34, 2010; journal version Operations Research 60(3), 2012). Instead of judging an individual by its cost alone, HGSADC ranks it by a Biased Fitness that mixes its cost rank with its rank in contribution to population diversity, and it uses that score to decide which individuals survive.
Trading cost for diversity raises an obvious worry: a very good but unoriginal solution could be discarded. The paper answers it with its only stated result, an elitism property (Section 4.6, an unnumbered Proposition with a three-sentence proof): the best individuals by cost are never discarded, as long as they are not clones. The HGSADC framework has since become the basis of state-of-the-art codes for many routing variants, and this guarantee is the one formal statement on which its population management rests.
HGSADC keeps two subpopulations (feasible and infeasible) and manages each separately. Everything below concerns one subpopulation; no routing object is involved.
A population is a finite set of individuals, with . Each individual has a penalized cost , its fitness (lower is better); a distance to every other individual; and a diversity contribution , which in the paper is the mean distance from to its nearest neighbours in (higher is better).
The normalized ranks of relative to the current population are
so that the best individual has rank and the worst rank . For an integer parameter , the Biased Fitness is (equation (7))
An individual is a clone in if some other has or . With the current best solution, is the set of individuals of , other than , that have a clone.
Survivor selection. When a subpopulation reaches individuals, of them are discarded one at a time: if , an individual of maximum in is removed; otherwise an individual of maximum in the whole population. After each removal the distances, , the ranks and are recomputed on the remaining population. An individual is among the best of in terms of fitness when fewer than members of have strictly smaller cost.
For every run of the survivor-selection procedure that removes individuals from and ends at , with :
The result. The Proposition explains what the parameter means: it is the number of top individuals whose survival is guaranteed from one generation to the next, whatever their diversity contribution. It lets the algorithm designer push for diversity through without risking the loss of the best solutions, and it is what makes the "removal zone" of the paper's Figure 4 a meaningful picture. The same Biased Fitness and survivor rule are reused in later HGS variants, so the guarantee transfers to them.
Formalizing it. The proof in the paper is three sentences long, but it leaves several things implicit: what happens with ties in cost or diversity, why "the" worst individual has rank exactly , why the coefficient of is nonnegative, and why the one-step argument survives successive removals with everything recomputed. A machine-checked version settles each of these. To our knowledge no formalization of this or any other population-management guarantee for genetic algorithms exists.
The arithmetic of each step is elementary. The difficulty is in reading the statement correctly. "The individual with the worst fitness has rank 1" fails when costs tie; it holds only in the branch , where equal costs are excluded because two individuals with equal cost are both clones and at most one of them is the best solution. The inequality needs , which the Proposition does not state: it follows from the population sizes ( reduced to , with , , Table 1). Without it the Proposition is false: if and , some elite individual must be removed. Finally, the one-step argument must be iterated: the population, its ranks and change after each removal, and one must check that the hypotheses on persist.
Individuals are elements of an arbitrary type with decidable equality; populations are Finset α. Costs, distances and diversity contributions are real-valued, and is an arbitrary function of (population, individual), which includes the paper's equation (5); the goal is therefore stated for every diversity measure. Explicit readings of loose phrases:
A formalization that freezes the initial Biased Fitness, that takes the ranks as arbitrary functions into , that states the existence of one good run, or whose size hypothesis cannot be met, would not be this Proposition. The supporting definition file contains the ranks, the Biased Fitness, clones, , a removal step and a run of steps; no further library is needed beyond Finset cardinalities. Proofs of the three milestones and of the goal are welcome, as is a formalization of the paper's Hamming distance (6) and diversity contribution (5) as an instance of .
Online learning and stochastic learning ask different questions. An online learner faces an arbitrary sequence of loss functions and is judged by its regret: the excess of its cumulative loss over that of the best fixed hypothesis in hindsight. A stochastic learner receives independent samples from an unknown distribution and is judged by the risk of a single hypothesis it outputs. Regret bounds hold without any probabilistic assumption, so they are strong guarantees; risk bounds are what statistical learning and stochastic optimization actually need.
The online-to-batch conversion connects the two: run any online learner on losses built from i.i.d. samples and output either the average of its predictions or one prediction chosen at random. The expected excess risk of the output is then at most the expected regret divided by the number of rounds. A general form of the conversion is due to Cesa-Bianchi, Conconi and Gentile (IEEE Trans. Inf. Theory 2004). Shalev-Shwartz's survey (Found. Trends Mach. Learn. 2011) states it in expectation, in Vapnik's general setting of learning, as Theorem 5.1 and Corollary 5.2 (§5, pp. 186–189). Every stochastic-gradient analysis that goes "regret bound, then online-to-batch" rests on this statement.
Fix a dimension and a hypothesis class . Examples range over a measurable space and are drawn from a probability distribution on , which the learner does not know. A cost measures how badly hypothesis does on example , and the risk of is
This is Vapnik's general setting of learning (Definition 5.1); supervised classification, regression and stochastic convex optimization are special cases.
The conversion draws independently from and runs an online learner on the losses . Its prediction in round , , may depend only on . The output is either the average or the randomized choice , with uniform on the rounds and independent of the sample.
For every comparator , under the conditions of Theorem 5.1,
for the randomized output, and for the averaged output when and are convex. The right side is the expected regret divided by . The statement contains no constant: it is an exact reduction, valid for every online learner.
Corollary 5.2 makes every regret bound a risk bound. Combined with the regret of online gradient descent or online mirror descent, it gives the excess-risk rate of stochastic gradient methods for convex Lipschitz problems; combined with logarithmic regret for strongly convex losses, it gives rates. The survey's own "Stochastic Online Mirror Descent" box (p. 189) is exactly this composition.
The result is proved in the paper. What this mission adds is a machine-checked version in a measure-theoretic model with honest non-anticipation and a genuine model of the randomized output. The platform has a related statement, Mohri, Rostamizadeh and Talwalkar's Theorem 8.15 (FoundationsML.OnlineLearning.online_to_batch_conversion), which is a high-probability bound for bounded convex losses in supervised learning; it is a different statement and neither implies the other. The expectation form here is the one stochastic-optimization arguments use.
The result is short on paper; the formal content is the conditional-expectation step. The prediction is a random variable built from , while is a fresh draw, so must be computed by integrating out first, which means a Fubini–Tonelli argument on a product of copies of split into the past, the present and the future of round . The first idea, that has the same law as for a fixed , is wrong: is random. The identity also fails as soon as may look at (take a minimizer of ), so the argument must use the information structure, not only the marginal laws. The averaging part additionally needs Jensen's inequality for and the measurability of as a function of the hypothesis.
EuclideanSpace ℝ (Fin d) with a set, because averaging needs a vector space. Rounds are numbered , and .ψ : Fin T → Ψ under Measure.pi (fun _ => Q), with Q a probability measure: independent draws from .A t : (Fin t → Ψ) → ℝ^d of measurable maps with values in , so non-anticipation holds by typing: . The learner may read the examples, not only the losses; this class contains the paper's learners, so the statements are at least as strong.Fin T. The expectation over is not replaced by the average over rounds (that replacement is the first line of the proof).Infrastructure needed: Tonelli/Fubini on finite products split at a coordinate (Mathlib's Measure.pi), measurability of parametric integrals, and Jensen's inequality for a convex function of a finite average. The round- identity is reusable for any non-anticipating stochastic process; contributions of proofs of any milestone are welcome.
A monotone disjunction over Boolean variables is a rule of the form . Learning such a rule online — predicting the label of each example before it is revealed and paying one unit per wrong prediction — is the basic test case for learning when only a few of many features matter. Littlestone's Winnow algorithm (Littlestone 1988) learns a -literal disjunction with mistakes, while additive algorithms such as the Perceptron need a number of mistakes that grows linearly in on the same problem. Kivinen and Warmuth (1997) placed this gap inside a general theory of multiplicative versus additive updates. Shalev-Shwartz's survey (2011) derives Winnow as a special case of Online Mirror Descent with an unnormalized entropy regularizer, and obtains its mistake bound from a general local-norm regret bound. This mission formalizes that derivation.
Throughout, labels are and instances are . For with , the hypothesis is the disjunction of the variables with . A weight vector errs on when .
Winnow with parameter starts from . On round it receives , predicts , and receives . If it sets for every ; otherwise . The set collects the rounds on which it errs. On those rounds the surrogate loss is the hinge loss , and on all other rounds.
Unnormalized Exponentiated Gradient with parameters , run on linear losses , keeps , where . Winnow is this algorithm with and on , otherwise.
Online Mirror Descent (OMD) with link function predicts . Its analysis uses the Fenchel conjugate of a regularizer on a set , and the Bregman divergence .
For , and every with ,
and if for all , the run with satisfies
with equality at a minimizer of . 2. Theorem 2.23: if for all , then for all
together with its specialization to . 3. (3.3): for Winnow. 4. (3.4): for every round.
The theorem gives a mistake bound for learning sparse disjunctions that is logarithmic in the number of irrelevant features, against the of the Perceptron run on the same surrogate (p. 173). The first inequality also covers non-separable data: the bound degrades by , the total hinge violation of the best disjunction. The milestones are general and carry weight beyond Winnow. Lemma 2.20 is the standard duality form of the OMD regret bound. Theorem 2.23 is a local-norm bound that also allows negative losses down to .
All four results are proved on paper. To our knowledge none has a machine-checked proof, in Lean or elsewhere. This mission produces such proofs for the survey's own route: OMD duality, then unnormalized EG, then Winnow.
The obvious route bounds Winnow directly with a potential function, but the survey's statement sits at the end of a chain. The chain needs Fenchel–Young with an attained supremum, a telescoping identity for the conjugate, and the inequality for . It also needs a reduction in which the surrogate losses depend on the algorithm's own error set . Since is defined after the run, the subgradient inequality must be argued for exactly these losses. The bound uses that is Boolean and that ; for fractional or for it fails. Solving (3.3) and (3.4) for needs .
Vectors are Fin d → ℝ with explicit sums ; Lemma 2.20 is stated in an arbitrary real Hilbert space. Rounds are numbered in place of . Instances, labels and comparators carry the hypotheses , , , . is the natural logarithm, and through Real.log 0 = 0.
Erratum corrected. The Winnow box on p. 173 prints the update , and the proof on p. 174 uses . With that sign the algorithm demotes on a false negative, and Theorem 3.10 is false. Take , , , , and , on every round. The margin condition holds, and errs on round 1. The printed update only shrinks , so every round is an error, and exceeds . On an error round the hinge surrogate has gradient at . The mission therefore formalizes the update (Littlestone's Winnow) and on . With this update the run above errs once. The milestone texts are quoted verbatim, with the printed sign.
Implicit hypotheses made explicit.
Conventions.
The bounds carry no and no constant is instantiated. A trivializing formalization is ruled out: is the run's own surrogate, not a free function, and the conjunct quantifies over the weights.
Infrastructure needed: conjugates and the Fenchel–Young inequality on a subtype, telescoping sums, elementary exponential inequalities, and the case analysis on -valued data. Lemma 2.20 and Theorem 2.23 are reusable for other OMD and EG analyses. Lemma 2.20 is also stated in the companion mission on normalized EG. Proofs of any milestone, and alternative routes to the goal, are welcome. Excluded: the Perceptron comparison (p. 173), and Theorem 3.9 (Perceptron), which is already proved on the platform.
Single-leg capacity allocation under customer choice is the basic dynamic problem of revenue management: a firm holds a fixed stock of a perishable resource (seats on a flight leg, rooms on a night), and in every period of a finite selling horizon it decides which products (fare classes) to offer to the arriving customer. Talluri and van Ryzin (Management Science, 2004) showed that under a multinomial logit (MNL) choice model with known parameters, the optimal assortment in every period is revenue-ordered and shrinks as capacity becomes scarcer ("nesting by fare order"), which is what justifies the protection levels and bid prices used in practice.
The MNL parameters are estimated from data and are never known exactly. Rusmevichientong and Topaloglu (Operations Research, 2012) study the robust version, in which an adversary picks the parameters of each period from an uncertainty set after seeing the offered assortment, following the robust Markov decision process framework of Iyengar (Mathematics of Operations Research, 2005). Their Section 4 shows that the structure of the known-parameter problem survives: the value function is concave in capacity, the optimal assortment is a revenue threshold set, and it grows with remaining capacity and, when uncertainty does not shrink, over time. This mission formalizes those results.
There are products with revenues . An MNL parameter vector is ; offered the assortment , a customer buys product with probability
and nothing with probability . The expected revenue is .
Static problem (Section 3). For a compact nonempty uncertainty set ,
and is an optimal assortment of smallest cardinality.
Dynamic problem (Section 4). Periods each bring one customer, whose parameter vector lies in a compact nonempty . A purchase consumes one unit of capacity. The value function , the maximum worst-case revenue from period on with units of capacity, satisfies
for , with and . The marginal value of capacity is , and is a maximizer of the right-hand side of smallest cardinality.
For every and , and, in the second part, every with :
The result. Theorems 4.1–4.3 say that robustness costs nothing structurally: the robust policy is still a nested threshold policy, so it can be implemented with the protection levels or bid-price controls already in use, and it can be computed by examining at most revenue-ordered assortments per state instead of . Theorem 4.3 gives the operational content: with less inventory, offer fewer, higher-revenue products; nearer the end of the season (when the uncertainty sets are nested), offer more.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a checked robust finite-horizon dynamic program over finite action sets with compact adversary sets, the reduction of each Bellman step to a static max–min problem with shifted revenues, and checked concavity and time-monotonicity arguments that are reusable for other single-resource problems. The known-parameter analogues for general regular choice models and for the Markov chain choice model are separate drafts on the platform (RevenueOrdered.Nesting.*, MarkovChainChoice.SingleResource.*); they have no uncertainty set and are not used here.
The obvious route to concavity, an induction on in which is a maximum of concave functions, fails: a maximum of concave functions is not concave, and here each candidate assortment is evaluated by a minimum over , and the worst-case parameter vector changes with the capacity level, so the known-parameter argument cannot be reused term by term. Any induction on also has to handle the boundary , where the Bellman equation does not apply and only is given. Every step involving a minimum must use that the minimum over a compact set is attained, and translating a minimum by a constant must be justified rather than assumed.
Fin n (Lean index is product ). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 . is the published ChoiceCDLP.MNL.mnlObjective. Minima over uncertainty sets are real infima (sInf), equal to the attained minima under the standing hypotheses; maxima are Finset.sup' over all assortments.V t, , is compact, nonempty and contained in (IsUncertaintySeq); the static results assume the same of V. The paper writes "" in Theorem 3.2 and Corollary 3.5; this is read as , compact.RobustMNL.Dynamic, the companion mission on Section 3 of the same paper, identically up to namespace.Assortment optimization is the problem a retailer faces in deciding which subset of its products to put in front of customers. Under the multinomial logit (MNL) choice model each product carries a preference weight, and a customer facing an offered set buys each product with probability proportional to its weight, or buys nothing. The optimal assortment under known weights is classical: it is one of the revenue-ordered sets (Talluri and van Ryzin, 2004). In practice the weights are estimated from data and are uncertain.
Rusmevichientong and Topaloglu (2012) study a robust version: the seller knows only that the weights lie in an uncertainty set, and maximizes the worst-case expected revenue over that set. They also treat the case where the offered set is limited in size, as when a display window or a web page holds only a fixed number of items. Under known weights the size-constrained MNL problem is solvable in polynomial time (Rusmevichientong, Shen and Shmoys, 2010); for a general uncertainty set the robust size-constrained problem has no comparable structure. This mission formalizes the result showing that, for a rectangular uncertainty set, the robust size-constrained problem is exactly a known-weights problem at an explicit parameter vector.
There are products with revenues . A parameter vector gives the no-purchase weight and the preference weight of each product. When the seller offers an assortment , a customer buys product with probability , and the expected revenue is
An uncertainty set is a compact set of parameter vectors. The worst-case revenue of is . For a size limit , the size-constrained robust problem is
and with no size limit its value is . A rectangular uncertainty set is a product of intervals
in which each weight, including the no-purchase weight , varies independently over its own range.
For every rectangular , every vector of revenues and every ,
The unconstrained case: for rectangular , which the paper establishes by a separate argument.
The result. Theorem 3.8 converts a max–min problem over a continuum of parameter vectors into a single deterministic size-constrained MNL problem with weights : the largest no-purchase weight and the smallest product weights. The size-constrained MNL problem with known weights has efficient algorithms, so the robust problem inherits them. The theorem also identifies the worst-case customer explicitly, which means robustness against a box costs nothing computationally beyond a known-weights solve. The parametric description of in Milestone 1 holds for every compact uncertainty set and is the starting point for other uncertainty sets.
Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a Lean formalization of the size-constrained robust MNL problem built on the published MNL objective ChoiceCDLP.MNL.mnlObjective, the parametric (Dinkelbach-type) characterization of a max–min ratio problem with attainment, and the box reduction. The definitions are shared in convention with the companion missions on the same paper (the revenue-ordered structure of the unconstrained robust problem and the dynamic robust problem).
The direct approach — for each assortment , find the worst parameter vector in the box and compare — does not work as stated: for a fixed containing a product whose revenue is below the target ratio, the minimizing no-purchase weight is , not , so the per-assortment worst case is not attained at . The identity holds only after maximizing over assortments of size at most , and the size constraint interacts with which products can be discarded. A second point is that the ratio is not linear in , so its minimum over the box is not determined coordinate by coordinate from the signs of the revenues alone, and every "max" in the statements asserts attainment, which has to be established, not assumed.
The source is the authors' manuscript of 20 Sep 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's.
Representation. Products are Fin n (Lean index is the paper's product ). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 . The revenue is the published ChoiceCDLP.MNL.mnlObjective p.2 r p.1 S. Every minimum over is a real sInf of the image; every maximum over assortments is a Finset.sup' over all subsets of size at most (a nonempty family, since it contains ). Every "" is stated as IsGreatest, which asserts attainment. The rectangular set is Set.Icc l₀ u₀ ×ˢ Set.Icc l u. is any natural number, with no lower or upper bound.
Hypotheses.
Trivializations ruled out. is defined through the worst case over the whole box and the maximum over all assortments of size at most , never through the vertex or a restricted family of sets, so the goal is not definitional. The box hypotheses make nonempty, so no sInf is evaluated on an empty set.
Contributions welcome. Proofs of the four milestones and the goal; lemmas on attainment of sInf of a continuous function over a compact set used for the inner minimum; a reusable parametric characterization of of ratios with positive denominators.
A retailer that orders stock months before the selling season carries inventory risk: its profit depends on a demand it cannot observe when it commits. For many goods that demand moves with a quantity traded on financial markets: sales of housing-related products with an interest-rate or construction index, sales of fashion or luxury goods with a stock index, sales of commodity-intensive products with a commodity price. V. Gaur and S. Seshadri, Hedging Inventory Risk Through Market Instruments (MSOM 7(2), 2005), ask what such a firm gains by trading in that market, and how the trade interacts with the ordering decision.
Their analysis has two halves. When demand is perfectly correlated with the asset price, the newsvendor payoff can be replicated by a portfolio of the asset and call options, and inventory risk can be removed completely (§2). When demand is only partially correlated, the hedge is imperfect, and the question becomes whether a decision maker with a concave utility still benefits from hedging, and whether hedging changes the order quantity (§3.2). This mission formalizes the first of these two questions in the partially correlated model: Proposition 5, which says that a small fair hedge never lowers expected utility at the margin. A companion mission of the same series treats Proposition 7, on the order quantity.
A firm orders units now at unit cost , sells at price at a future time , and salvages leftovers at . The demand is
where is the time- price of a traded asset and is a forecast error, independent of , with and (§3, p. 107). Write . The paper's standing assumptions (§2, p. 106) are , , and , where is the risk-free rate.
After scaling all cash flows by (p. 110) the firm's terminal wealth without hedging is
with and the scaled initial wealth plus . In these units reads and .
A hedge is a portfolio with time- payoff and time-0 price . The paper requires it to be a fair gamble, (12), and to be an increasing function of (p. 111). If the firm shorts units of the hedge, its wealth is
and a decision maker with utility evaluates it by .
In Lean, the law of is a probability measure ν on ℝ, the law of is a probability measure G on ℝ, the hedge is X_T = φ S_T for a function φ : ℝ → ℝ, the forward price is one real x0r, and every expectation is an integral against the product measure ν.prod G. The definitions file provides unhedgedPayoff, hedgedPayoff and expUtil.
For any concave and differentiable utility function , and any fixed order quantity ,
The Lean statement asserts that the two-sided derivative exists at and is nonnegative.
Proposition 5 is the paper's answer to "should a risk-averse newsvendor hedge at all?": with any concave utility and any order quantity, a small short position in a fair hedge that rises with the asset price weakly increases expected utility. It needs no assumption on the shape of the utility beyond concavity, no sign of , and no assumption on the law of the forecast error beyond independence. It is the starting point for the paper's later results on the optimal hedge (Proposition 4) and on how hedging raises the optimal order (Propositions 6 and 7), and it is a clean instance of a general principle in operations-finance: a fair bet that is negatively correlated with marginal utility is worth taking at the margin.
The result is proved in the paper in a few lines. What this mission adds is a machine-checked version with every regularity condition explicit: the paper differentiates under the expectation and multiplies expectations without stating when this is legitimate, and conditions on informally. To the best of a search of the Prove2Me catalog, neither the result nor the two steps of its proof (an integral version of Chebyshev's covariance inequality for monotone functions, and differentiation of a concave expected utility under the integral sign) is formalized there.
The obvious argument has two analytic gaps. First, exchanging with the expectation needs a dominating function, and the only integrability available is at finitely many values of , for both signs of . Second, " is a decreasing function of " is false as a statement about the pair : depends on too. The covariance step is Chebyshev's inequality for the function and the function , which needs independence (Fubini on the product measure) and has to cope with the conditional expectation being finite only almost everywhere. Neither nor the hedge payoff is bounded.
The Lean development commits to the following conventions.
ν (law of ) and G (law of ) on ℝ; independence is the product measure ν.prod G. The standing assumptions and are hypotheses (∫ e, e ∂G = 0, MemLp id 2 G).φ : ℝ → ℝ, monotone (nondecreasing, reading the paper's "increasing" weakly), measurable and ν-integrable; the fair-gamble condition (12) is ∫ s, φ s ∂ν = x0r. The paper's further remark that is piecewise continuous and a.e. differentiable is not needed and not imposed.u : ℝ → ℝ with ConcaveOn ℝ Set.univ u and Differentiable ℝ u, exactly "concave and differentiable"; no monotonicity of is assumed.A statement of the form 0 ≤ deriv (fun α => expUtil …) 0 would be trivially true whenever the derivative fails to exist (Lean's deriv returns 0 there); the goal instead asserts HasDerivAt with a value D and 0 ≤ D. The hypotheses are satisfiable with a non-constant hedge: a sorry-free check uses , uniform on , uniform on and .
Infrastructure that a complete proof needs, reusable beyond this mission: Chebyshev's integral (covariance) inequality for two monotone functions of a real random variable; differentiation under the integral sign for concave integrands with integrability at three points; Fubini-based conditioning on one coordinate of a product measure. Contributions of these general lemmas as separate theorems are welcome. The source PDF is a scan of the published article.
Manufacturers routinely share rolling schedules with their suppliers: each period the buyer commits to a purchase for the current period and issues non-binding estimates for future periods, then revises those estimates as the horizon rolls forward. Unconstrained revisions push forecast risk upstream and are a recognized source of the bullwhip effect. A quantity flexibility (QF) contract bounds how far each estimate may move between consecutive issues, giving the supplier a guarantee in exchange for a commitment to cover any order within the bounds. Tsay and Lovejoy (MSOM 1(2), 1999) model a chain of firms linked by QF contracts and ask how a firm in the middle of the chain, the flex node, should translate the schedules it receives into the schedules it issues. Their answer is the Minimum Commitment (MC) policy, justified by Proposition 1: MC solves the node's open-loop planning problem and never breaks either contract.
This mission formalizes Proposition 1. A companion mission (Quantity Flexibility Contracts and Supply Chain Performance 1) formalizes Proposition 2, on when MC keeps zero inventory.
Periods are . In period the node receives from its customer a release schedule : is bought now, estimates the purchase in period . The node issues to its supplier a replenishment schedule of the same form. Its ending stock is .
The contracts carry parameters and (): output parameters with the customer and input parameters with the supplier. The incremental revision (IR) constraints are, for all and ,
The cumulative parameters are and , so . A convex cost , minimized at , is charged on ending stock.
At period , with , and known, the open-loop program (F-OLFC) chooses and the planned purchases , , to minimize subject to the stock balance (17), coverage (18), the input IR constraints (19) between and , and the cumulative bounds (20).
The MC policy computes and projected inventories by one recursion on : ,
In Lean: QFParams, Acum, Ωcum, IROut, IRIn, mcStep, run, inv, sched, projInvAt (module Model) and stock, Feasible, RelaxedFeasible, objective, lbar, pStar (module FOLFC).
For an MC run from with , against any customer schedules obeying (6), and any convex minimized at zero:
and for every the schedule , with suitable planned purchases, is feasible for (F-OLFC) at period and attains its minimum.
Proposition 1 is what makes MC a well-defined operating rule for an intermediate firm: whatever the customer does within its contract, the node can serve it from stock and its own revisions stay within the supplier's contract, so the chain of contracts composes. Proposition 2 and the paper's simulation study of how flexibility propagates along a supply chain (§§5–6) both assume the node uses MC, and rely on Proposition 1 for that choice being both feasible and myopically optimal.
The paper's optimality argument is sketched: the relaxed solution is attributed to "a straightforward application of Kuhn–Tucker conditions" with details in an unpublished thesis, the equivalence of (32) with (21)–(23) is omitted, and Lemma 1's proof is replaced by intuition. A machine-checked proof supplies these steps. To our knowledge no part of this paper has been formalized before. The mission also fixes the statement: the printed range of (19) makes the optimality claim false, and the claim needs a start of the run that the paper leaves implicit.
The obvious argument treats (F-OLFC) as a lot-sizing problem with minimum lot sizes and observes that the greedy purchases (30) are optimal. That only solves the relaxation. The difficulty is that MC is not stated through (30): it is a recursion on the replenishment schedule with a positive part in the projected inventory, and one has to show that the MC schedule can carry the greedy purchases within the upper bounds of (19) and (20). Those bounds can bind, and whether they do depends on the previous period's schedule, so the optimality claim is not a one-period statement: it needs an induction over the run, through Lemma 1 and the customer's IR constraints. The admissibility half needs the same induction, with the nonnegativity of the schedules carried along.
All quantities are real numbers. Parameters are sequences ℕ → ℝ whose index is unused; schedules are infinite sequences, and the MC recursion runs over all . (6) and (7) are written with replaced by . The standing assumptions , () are hypotheses. is any convex function with for all ; no strict convexity, differentiability or monotonicity is assumed.
The run starts from an arbitrary state (run period ); the MC policy acts from period . The following departures from the printed statement are disclosed:
(F-OLFC) ranges over all real schedules and purchases; the only MC-specific object in the goal is the candidate schedule. Optimality is stated as "feasible, and no feasible point has a smaller objective", never as an infimum, so an infeasible program cannot make it vacuous. The MC step is literally (21)–(23), with the carried-over term and the positive part; a run that sets or drops the max is a different policy.
Infrastructure: the model and (F-OLFC) are self-contained over Mathlib (Finset.prod, ConvexOn). Proofs of the three milestones, and of the monotonicity of a convex function minimized at zero on , are welcome as separate contributions.
Assortment optimization asks which subset of products a firm should offer when customers choose among the offered products, or leave without buying. It underlies shelf-space planning in retail, the choice of which fare classes to keep open in airline revenue management, and the selection of items shown on a web page. The multinomial logit (MNL) model is the standard choice model in this literature: when the model parameters are known, the optimal assortment is revenue-ordered, that is, it consists of the products with the highest revenues (Talluri and van Ryzin, 2004; Gallego et al., 2004; Liu and van Ryzin, 2008), so only candidate assortments need to be compared instead of .
In practice the parameters of the choice model are estimated from limited data. Rusmevichientong and Topaloglu (Operations Research, 2012) take a robust view: the parameters are only known to lie in an uncertainty set, and the firm maximizes its worst-case expected revenue. Their main structural result is that the revenue-ordered structure survives this uncertainty, whatever the uncertainty set. This mission formalizes that result and the comparative statics the paper derives from it.
There are products, , and product earns revenue . A customer's choice is governed by a parameter vector (all components strictly positive): is the weight of the no-purchase option and the preference weight of product . When the assortment is offered, the customer buys product with probability
and buys nothing with the remaining probability. The expected revenue of is
The parameters are unknown and lie in an uncertainty set , which is compact and nonempty. The Robust Logit problem maximizes the worst-case expected revenue:
Among the optimal assortments, is one with the smallest cardinality. For a single parameter vector , write and ; this is the classical problem with known parameters. Finally, for , and are the same quantities when every revenue is replaced by .
Equivalently: an assortment is optimal with smallest cardinality if and only if it is the set of products whose revenue strictly exceeds the optimal worst-case revenue. When this set is for some .
Milestones 3–6 are consequences of the goal on the same definitions.
Theorem 3.2 reduces the robust problem, a max–min over assortments and a possibly infinite parameter set, to at most revenue-ordered candidates, each requiring one worst-case evaluation . Applied to a singleton it also reproves the classical revenue-ordered optimality under known MNL parameters, together with the exact tie-breaking description. Corollary 3.5 and Theorem 3.6 say that more uncertainty calls for a larger assortment, and that the robust assortment is the largest assortment optimal for some parameter in ; Theorem 3.7 compares assortments when all revenues shift by a constant, which the paper uses in Section 4 to show that robust dynamic assortments grow with remaining capacity and over time.
The results are proved in the paper; none of them has a machine-checked proof on Prove2Me. The platform has ChoiceCDLP.MNL.top_ranked_optimal (from Liu and van Ryzin, 2008), a statement about top-ranked offer sets for known MNL weights, which is a different statement without uncertainty or tie-breaking. A formal development here gives a checked version of the robust structure theorem stated for arbitrary real revenues, the generality in which the dynamic part of the paper uses it.
The obvious argument fails at the max–min. For known parameters, Lemma 3.1 immediately shows that a product should be added exactly when its revenue beats the current expected revenue; but under uncertainty the minimizing parameter vector changes with the assortment, so one cannot compare and at a single worst-case . The argument has to establish a strict improvement uniformly over and then pass to the minimum, which is where compactness enters: a pointwise strict inequality survives the minimum only because it is attained. The tie-breaking rule is equally essential: a product with can be added to an optimal assortment without changing its worst-case value, so without the smallest-cardinality rule the characterization is false.
Products are Fin n, so Lean index stands for the paper's product . A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 and p.2 i the weight of product ; IsPos p expresses . The expected revenue is the published definition ChoiceCDLP.MNL.mnlObjective. The worst case is a real infimum (sInf), and is a maximum over all subsets of products. is encoded as the predicate IsSmallestOptimal V r S (optimal, and of cardinality at most that of every optimal assortment), not as a choice function, so every statement about is asserted for every optimal assortment of smallest cardinality. and are the same objects for the revenue vector , which is exact since is at those revenues.
Standing assumptions and departures from the page:
The infimum is meaningful only under the standing assumptions (on an empty set it is ), which is why they appear as hypotheses of every statement. A complete development needs continuity of on positive vectors and attainment of minima on compact sets, both available in Mathlib, and finite maxima over Finset (Finset (Fin n)). The lemmas about (milestones 1–2) are reusable for any MNL model. Proofs of any milestone, and alternative proofs of the goal, are welcome.
The source is the authors' manuscript of 20 Sep 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's page numbers, and all page citations refer to it.
Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely and successfully applied to nonsmooth functions. Lewis and Overton (Math. Program. 141 (2013) 135–163) study why. A quasi-Newton step needs a step length along each search direction, and on a nonsmooth function the usual line searches have to decide what to do at points where the function is not differentiable. Classical inexact line searches for nonsmooth optimization (Lemaréchal 1981, Wolfe 1975, Mifflin 1977) ask an oracle for a subgradient at such points. Lewis and Overton propose a simpler rule: a trial point at which the objective is not differentiable simply fails the Wolfe test. This mission formalizes the analysis of that line search, §4 of the paper: when an acceptable step exists, when the bisection search finds one, what happens when it does not, and how many trials it takes on a convex function.
Let be an iterate of an optimization algorithm and a search direction. The line search objective is for . Only enters the analysis.
Assumption 4.1. The function is absolutely continuous on every bounded interval and bounded below, and
The number plays the role of the directional derivative .
Armijo and Wolfe conditions. Fix constants in . For ,
An Armijo–Wolfe step is a satisfying both.
Algorithm 4.6. Start from , , . At each trial: if fails, set ; otherwise, if fails, set ; otherwise stop. Then set if , and otherwise. So the search doubles until fails and then bisects the bracket . Write for the state before trial (lsRun), so . The search terminates if some trial passes both tests (Terminates).
Under Assumption 4.1 and :
Theorem 4.7 is the convergence guarantee for the line search used by the BFGS implementation analysed in the rest of the paper. It isolates the only failure mode: a derivative that oscillates as increases to a limit point, which condition (4.8) excludes. The paper notes that (4.8) holds for every semi-algebraic , so the search terminates on the functions met in practice. The same line search is the one whose trial sequence produces the binary-expansion behaviour of the secant method in §5. Theorem 4.5 shows that an acceptable step exists on a set of positive measure, which is why a sampling line search is not defeated by the null set of nondifferentiable points. Proposition 4.11 bounds the work per line search on convex functions.
All statements are proved in the paper. None has been formalized; there is no line search for nonsmooth functions on Prove2Me or in Mathlib. A formalization checks the measure-theoretic argument (absolute continuity and the fundamental theorem of calculus for Lebesgue integrals), the bookkeeping of the bisection, and the complexity count, where the printed upper bound turns out to be false for .
The obvious proof of termination fails: on a nonsmooth function the bisection can land on a kink at every trial, and the paper's §4.2 constructs a convex where it does. Termination therefore cannot follow from Assumption 4.1 alone, and both the existence of acceptable steps and the convergence of the brackets have to be argued through measure: Lemma 4.4 needs the fundamental theorem of calculus for absolutely continuous functions and a supremum argument over almost-everywhere inequalities. The non-termination analysis has to combine the bracket invariant with Lemma 4.4 on every late bracket and with a limit argument for (4.9). The complexity bound needs a careful count of doubling and bisection trials, including the regime where no doubling occurs.
The objective is h : ℝ → ℝ; only its values on enter. Lebesgue measure is volume with values in , and "nonzero measure" is volume S ≠ 0. Limits superior and inferior are computed in EReal. The upper bound is in WithTop ℝ, with . Stopping freezes the state of lsRun. Mathlib's deriv is at nondifferentiable points, so the Wolfe condition, condition (4.8) and (4.9) all state differentiability explicitly.
Deviations from the page, each disclosed in the item's Formalization Note:
Algorithm 4.6 is encoded as the literal state machine; a definition of the search as "some Armijo–Wolfe step" or as an arbitrary nested sequence of brackets would make the goal trivial and is ruled out. The Wolfe condition includes differentiability; without it every kink would pass, since .
A complete development needs absolute continuity (AbsolutelyContinuousOnInterval, with almost-everywhere differentiability and the fundamental theorem of calculus, both in Mathlib), the mean value theorem, and facts about one-sided derivatives of convex functions. Lemma 4.4 and the bracket invariant are reusable for other bracketing line searches. Contributions of the milestones in order, of proofs of the definitions' basic properties (all trial steps are positive, the brackets are monotone), and of the §4.2 non-termination example are welcome.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string that both parties share, without revealing anything beyond the truth of the statement. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988) and are a building block of chosen-ciphertext secure encryption, signatures and secure multi-party computation. For a long time every NIZK proof for all of NP was zero-knowledge only computationally: a simulator produced proofs that no efficient adversary could tell apart from real ones.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006) gave the first NIZK argument for all of NP whose zero-knowledge is perfect: real and simulated proofs have exactly the same distribution, so even an unbounded adversary learns nothing. The construction is the Circuit SAT proof of their Figure 3, run on a perfectly hiding key of a homomorphic proof commitment scheme. Its zero-knowledge is Lemma 8 of the paper, and it is the zero-knowledge half of their Theorem 11.
A homomorphic proof commitment scheme has a message space (a finite cyclic group with generator , here ), a randomizer space and a commitment space , all finite abelian groups, and a commitment function . A hiding key generator outputs a commitment key together with a trapdoor . The scheme is assumed to have:
A NAND circuit on wires is a list of gates and an output wire ; a witness satisfies it, , if for every gate and . The prover of Figure 3, with , commits to every wire, with , proves that each commitment contains or , and for each gate proves that contains or .
The simulator is , returning and , and , which commits to on every wire except the output wire, and makes all the 0/1 proofs from openings it knows or obtains with the trapdoor. In the zero-knowledge game an adaptive adversary reads , submits pairs to an oracle one at a time, sees each answer before choosing the next, and outputs a bit. The real oracle answers with , the simulation oracle with ; both answer failure when .
For every adaptive adversary ,
where is restricted to its first output.
Lemma 8 makes the Circuit SAT argument of Section 7 the first perfect NIZK argument for every language in NP. Combined with the computational indistinguishability of binding and hiding keys it also gives the computational zero-knowledge of the proof of Figure 3 (Theorem 6), and it is the template for the perfect zero-knowledge of the universally composable NIZK of the paper's Section 8. The same simulation pattern, commit to everywhere and use the trapdoor where an opening is needed, recurs in later pairing-based proof systems such as Groth–Sahai proofs.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal proof fixes the simulator completely, including the cases the paper leaves to the reader, and makes the adaptive multi-query argument explicit: the paper's proof treats one proof at a time and does not spell out why answering many adaptively chosen queries preserves equality of distributions.
The real and simulated proofs never use the same randomizers, so the proof cannot compare outputs value by value; it must compare laws. Two gaps in the printed argument need to be closed. First, witness indistinguishability is assumed only for one opening to against one opening to , while comparing a simulated gate proof with a real one compares two openings that may carry the same message; the trapdoor supplies the missing intermediate opening. Second, the printed gate recipe gives the gate commitment the message only when no input of the gate is the output wire; when the output wire is an input, the message is or , and has no 0/1 opening, so the simulator must open the gate commitment itself with the trapdoor. The adaptive adversary adds a third point: equality of laws must survive an arbitrary interaction in which later queries depend on earlier answers.
ZMod N with (the paper describes Figure 3 for order at least 4, p. 14); and are finite nonempty types, a commutative group. Key generators and the 0/1 prover's randomness are probability mass functions; the coins are uniform.A prophet inequality compares two players facing the same random sequence of rewards . The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and Garling showed that when the are independent, non-negative and , the gambler has a stopping rule with
and that the factor cannot be improved. This inequality, labelled (1) in Kleinberg and Weinberg's Matroid Prophet Inequalities (arXiv:1201.4764, STOC 2012), is the starting point of optimal stopping theory's prophet inequalities and, more recently, of a large literature in online algorithms and algorithmic mechanism design, where it is the reason that a single posted price can extract a constant fraction of the optimal welfare or revenue.
Timeline.
This mission formalizes that §3.1 result.
Let be a probability space and . Let be real random variables on that are independent (as a family), non-negative, and such that the prophet's value has finite expectation. Define
The single-threshold rule observes in order and stops at the first time with , collecting . If no reaches , the rule accepts nothing and collects . Write for the amount collected; it equals on the event , which has probability , and off it.
In Lean the variables are X : Fin n → Ω → ℝ with [NeZero n]; is maxX X, is thr P X, is stopProb P X, and is reward P X, all in the namespace MatroidProphetKW.RankOne.
This is inequality (1) for an explicit rule, which is stronger than (1)'s existence statement. The constant is sharp, so the goal is stated with it.
The result. A threshold that depends on the distributions only through one number, , already matches the optimal worst-case guarantee of the best stopping rule. Because it is a single price, the rule translates directly into a posted-price mechanism: a seller who posts the price to arriving buyers obtains half of the expected maximum value. The same accounting, in which accepted value is charged against the threshold and rejected value against the probability of having accepted nothing, is what Kleinberg and Weinberg generalize to matroids (missions 1 and 2 of this series).
Formalizing it. The result is proved and classical; the work here is to formalize its known proof. No machine-checked proof of the factor-2 prophet inequality is in Mathlib, and none was found among the platform's published theorems in October 2026. A completed development provides the inequality itself, the tail comparisons, and the layer-cake bookkeeping for a stopped reward, all of which are reusable for other single-threshold prophet inequalities (Samuel-Cahn's median rule, -choice and posted-price variants).
The expected reward of the rule is not a function of the marginals of the individual alone in an obvious way: the event that the rule is still running when arrives depends on , and the reward is at a random index. The natural first attempt, comparing and pointwise, fails, since on a given outcome the rule may stop early at a value just above while the maximum comes later. The comparison has to be made between distributions, at each level , and it has to use independence to decouple "nothing accepted before time " from "". The rest is measure-theoretic bookkeeping that is routine on paper and not routine in Lean: expressing expectations of non-negative variables as integrals of tail probabilities, splitting them at , and keeping track of integrability.
Ω with a MeasurableSpace, P : Measure Ω with [IsProbabilityMeasure P].X : Fin n → Ω → ℝ, [NeZero n]; each X i measurable; iIndepFun X P (mutual independence); 0 ≤ X i ω for all i, ω; Integrable (maxX X) P, which is the paper's .Finset.sup' over the nonempty index set; no junk supremum.∫ ω, … ∂P) and Measure.real probabilities. Tail integrals are Lebesgue integrals of over and .The threshold is a definition, , not a free parameter constrained by hypotheses; a formalization in which is arbitrary and the upper-tail bound is assumed would make the goal a rearrangement of its hypotheses, and is ruled out.
Infrastructure that a complete development needs, and that is welcome as separate contributions: the layer-cake formula for non-negative integrable split at a level (Mathlib has the unsplit form, MeasureTheory.integral_eq_integral_meas_lt); measurability and integrability of the stopped reward (it is dominated by ); and the probability of the event "the first values are below and " as a product under iIndepFun.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string that both parties share, without revealing why the statement is true. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988). They are a basic component of chosen-ciphertext secure encryption, signature schemes and secure multi-party computation.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at EUROCRYPT 2006 and CRYPTO 2006) built NIZK proofs for all of NP from bilinear groups. The construction rests on one abstraction, the homomorphic proof commitment, and one protocol, the NIZK proof for Circuit SAT of their Figure 3. Theorem 6 says that the Figure 3 protocol works for every homomorphic proof commitment. This mission formalizes the part of Theorem 6 that holds exactly, with no computational assumption.
A homomorphic proof commitment scheme (Section 3) has a message space , a finite cyclic group with generator . It also has a randomizer space and a commitment space , both finite abelian groups. It comes with algorithms :
The exact properties used here are the following. The homomorphic property is on keys of either mode. Perfect binding says that on binding keys no commitment has openings to two different messages. Perfect completeness of the 0/1 proof says that honest proofs for are always accepted, on keys of either mode. Perfect soundness of the 0/1 proof says that on binding keys an accepted proof implies for some . Perfect extractability says that on binding keys for .
A NAND circuit on wires is a list of gates , with inputs and output , and an output wire . An assignment satisfies it, , when for every gate and .
The protocol of Figure 3 takes with . The prover commits to every wire, , with . It proves with that each contains or . For each gate it proves that contains or , using message and randomizer . The verifier checks and every 0/1 proof.
If and the scheme has the homomorphic property, perfect binding, and perfectly complete and perfectly sound 0/1 proofs, then
The theorem holds for every scheme with these properties, with no assumption on how the scheme is built.
Theorem 6 is the step from a commitment primitive to NIZK proofs for an NP-complete language. With the subgroup-decision commitment of Section 4 or the decisional-linear commitment of Section 5 it gives Corollaries 9 and 10: perfectly sound NIZK proofs for Circuit SAT with proofs of size . When the common reference string is instead a hiding key, the same protocol becomes the perfect NIZK argument of Theorem 11. Its completeness clause is the hiding-key half of the completeness formalized here.
The result is proved in the paper. Lemma 5 and the soundness of the circuit protocol are left to the reader there or proved in three sentences. No machine-checked proof of this theorem, or of any commitment-based NIZK, was found in Mathlib or in the public Lean libraries searched. This mission states its exact content against an abstract scheme interface. The same interface can then be instantiated by machine-checked versions of the concrete commitments, which are the third and fourth missions of this series.
The argument is short, so the difficulty lies in the bookkeeping. On a binding key the verifier only learns that each commitment opens to some bit. Perfect binding is what identifies the message a gate proof certifies with , which in turn identifies it with the wire bits. Lemma 5 must then be checked in rather than in the integers, where , and must be shown to differ from and . This is exactly where enters: for the all-zero assignment passes every gate check, since . The output wire is handled by the literal check together with binding. Completeness needs the prover's convention to be used consistently in the gate proofs.
ZMod N. A finite cyclic group with a chosen generator is this group, and every theorem that needs it assumes 4 ≤ N, the paper's restriction on p. 14.AddCommGroup and a finite CommGroup. Key generators are PMFs. takes its randomness as an argument.Prop, quantified over the support of the relevant generator. The paper's "for all adversaries, " (or ) is equivalent for unbounded adversaries.Fin n with an output wire. No acyclicity is required, so the statements cover every system of NAND constraints.Dropped, because they are computational:
Perfect zero-knowledge on hiding keys (Lemma 8) is the second mission of this series. The definitions of this mission (the scheme interface, NAND circuits, the protocol) are reusable by any formalization of commitment-based proof systems. Proofs of the milestones are welcome in any order.
Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.
A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.
The problem is (2.1):
with , , , , , all continuously differentiable. Write and .
The PHR augmented Lagrangian (2.2) with respect to is, for , , ,
Algorithm 3.1 has parameters , , , boxes and , and tolerances with . At outer iteration it finds and lower-level multipliers , satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing over to tolerance ; it chooses new safeguarded multipliers , in the boxes; and it keeps when
and sets otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.
A point is a KKT point of a problem with objective , equalities and inequalities if it is feasible and for some and some vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near . CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.
Let be a run and a limit point of it. If is bounded, then . Otherwise at least one of the following holds:
Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.
The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by removes the objective and the multiplier estimates, but the lower-level multipliers divided by need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at whose gradients are independent at points arbitrarily close to . Taking limits of the original multipliers without this reduction does not work.
is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as on all of . The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors , use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by : x 0 is the initial point , the outer iterations are , the three subproblem tolerances are kept separate, and is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of . KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.
No hypothesis is added to Theorem 4.1 beyond the reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and only at ; the gradients are taken of functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.
Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.