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?
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 its solutions are not characterized by the classical KKT theory.
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) introduced a hierarchy of necessary optimality conditions for (P) and matched each condition with an algorithm whose limit points satisfy it. Iterative hard thresholding (Blumensath and Davies 2008) reaches -stationarity for ; the greedy sparse-simplex method reaches coordinate-wise minimality, but each of its iterations calls up to one-dimensional minimizations. This mission formalizes the paper's compromise between the two: the partial sparse-simplex method, which examines only two candidate moves per saturated iteration, and whose limit points are -stationary.
Vectors live in with the Euclidean norm; is the -th unit vector. For :
The objective is continuously differentiable and bounded below (Assumption 1, standing throughout the paper). Assumption 2 asks that be Lipschitz with some constant . A constant satisfies the local Lipschitz condition (2.15) if for every pair , every and every supported in ,
The paper's local Lipschitz constant satisfies it, and .
The projection is the set of points of nearest to . For , a point is an -stationary point (Definition 2.3) if
The partial sparse-simplex method (p. 25) starts at . If , it moves to the best point over all and if that strictly decreases , and stops otherwise. If , it compares two candidates and takes the better one, preferring the second on ties:
Under Assumption 2, with satisfying (2.15), every accumulation point of a sequence generated by the partial sparse-simplex method satisfies
that is, is an -stationary point.
The theorem shows that a cheap index-selection rule does not cost optimality strength relative to iterative hard thresholding: every limit point satisfies , and since , this is a stronger necessary condition than the guaranteed by IHT with stepsize . In the paper's numerical comparison (Example 3.3 contd., Table 3) the method performs much better than IHT and only slightly worse than the greedy method, at a fraction of the greedy method's cost per iteration. The decrease estimates of Lemma 4.1 are the quantitative content: they turn each iteration into a lower bound on the objective decrease in terms of the violation of -stationarity.
The results are proved in the paper; to our knowledge none is machine-checked. This mission produces a formal model of the method (with its selection rules as inequality predicates, so every run is covered), the local descent lemma for two-sparse directions, and a checked proof of Theorem 3.4. The printed proof of the case contains two gaps (see Difficulty); a formal proof settles the argument.
The decrease estimates follow from the local descent lemma applied at well-chosen trial points, but passing to the limit is delicate. When , the supports of the subsequence eventually coincide with and becomes continuous there; when , the iterates along the subsequence may still have nonzeros, and does not by itself force , because kills the second term of . The swap move optimizes along a single off-support coordinate , chosen by the derivative at and not at the shifted point where the optimization happens. The printed display (4.19) claims the bound for the maximum over all of at the shifted point, which the argument does not give, and the final display takes a minimum of two bounds that each hold on only one class of indices. Theorem 3.4 itself is not affected, but a complete proof cannot follow those two displays as printed.
Lean works in EuclideanSpace ℝ (Fin n) (indices ), with of class and = gradient f. Conventions fixed by the formalization:
LipschitzWith Lf (gradient f)) are hypotheses.MapClusterPt xstar atTop x.The run predicate is satisfiable and does not force a STOP: on , , , the constant sequence at is a run. The conclusion is the projection condition itself, not the coordinate form (2.5), so it cannot be met by an empty or degenerate reading of stationarity.
Reusable parts: the local descent lemma for two-sparse directions, Lemma 2.2 (the coordinate characterization of , shared with the IHT mission of this series), and the order statistic . Contributions of proofs for any milestone are welcome, as is the companion result Lemma 3.3 (limit points are BF vectors without Assumption 2).
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.
Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a nonlinear search space: a sphere, a Stiefel or Grassmann manifold, a space of curves modulo reparametrization. Projecting iterates of a Euclidean method back onto the constraint set loses the geometry, so one designs methods that move along the manifold itself. Riemannian line-search methods do this by replacing the update with for a retraction , and by carrying old search directions to the new tangent space with a transport.
Nonlinear conjugate gradient (NCG) methods are a natural candidate on manifolds: they need only first derivatives and store one previous direction. In the Euclidean case, Al-Baali showed in 1985 that the Fletcher–Reeves method with strong Wolfe step lengths and satisfies (doi:10.1093/imanum/5.1.121); Nocedal and Wright give the standard textbook proof (Lemma 5.6 and Theorem 5.7 in Numerical Optimization). Ring and Wirth (doi:10.1137/11082885X, SIAM J. Optim. 2012) transfer this analysis to Riemannian manifolds, possibly infinite-dimensional, which is the setting of their application to shape spaces. The mission formalizes that transfer.
is a smooth manifold modelled on a real Hilbert space , with a Riemannian metric on each tangent space and norm . For , is its differential, a continuous linear functional on with dual norm , and the gradient is its Riesz representative, .
A retraction is a family of smooth maps with and . Its transport is .
A run of Algorithm 1 consists of points , directions and steps with . With , the Wolfe conditions at are
and the strong Wolfe conditions replace (1b) by
The angle between and is given by .
The Fletcher–Reeves direction is
For a non-terminating Fletcher–Reeves run with strong Wolfe steps and , if the transport is non-expansive on the search directions, , is bounded below, and the pull-backs are Lipschitz continuously differentiable on with a uniform constant, then
Proposition 15 guarantees that Riemannian Fletcher–Reeves, with any retraction whose transport does not enlarge the search direction, cannot stall at a positive gradient level: some subsequence of the gradient norms tends to zero. Together with strict convexity in the sense of the paper's Proposition 4 this gives convergence of the iterates to the minimizer, and it justifies the use of the method on the shape spaces of the paper's §4. The hypothesis on the transport is the only new ingredient compared with the Euclidean theorem, and the paper's Remark 7 notes that convergence can no longer be guaranteed without it.
The result is proved in the paper. As far as is known, neither Zoutendijk's theorem on a manifold nor the Fletcher–Reeves convergence theorem has a machine-checked proof; Euclidean versions of both appear elsewhere on the platform, but the Riemannian statements, with retraction, transport and tangent-space-dependent norms, are new. The mission produces the line-search interface on a Riemannian manifold (retraction, transport, Wolfe conditions) in a form reusable by other Riemannian methods.
Each search direction is built from a vector in a different tangent space. The transported direction lives in , and only the step equation identifies it with a vector of ; norms, inner products and differentials all depend on the base point, so every Euclidean manipulation has to be carried through that identification. Zoutendijk's theorem has to connect two different descriptions of the same step: the curvature condition (1b) is stated with the differential of at the new point applied to the transported direction, while the Lipschitz hypothesis concerns the one-variable pull-back . They agree only because the transport is the derivative of the retraction, and the agreement is a chain rule for manifold derivatives, which has to be established in Mathlib's mfderiv framework for maps out of a tangent space. The growth bound cannot use ; it needs the non-expansiveness hypothesis exactly where the Euclidean argument uses the identity.
The manifold is a Mathlib manifold modelled on a real Hilbert space E, with Mathlib's RiemannianBundle on its tangent spaces; tangent-space norms and inner products are the Riemannian ones and is mfderiv. Geodesic completeness, separability, the distance and the Levi-Civita connection, standing assumptions of the paper, are not used by any statement and are dropped. The gradient is given as a field with its Riesz property. One retraction family is used for every step (the paper allows a different retraction at each step), the steps are positive, and indices start at .
The following readings are explicit:
Summable.The transport in the conclusion and in the Fletcher–Reeves update is the derivative of the retraction, not an arbitrary linear map; with an arbitrary map, condition (1b) would no longer be a statement about the pull-back , and Zoutendijk's theorem would fail. A run predicate that no sequence satisfies would make the goal vacuous; the one-dimensional run , , , , , satisfies every hypothesis.
The paper's other main result, R-linear convergence of Riemannian BFGS (Proposition 10), is a separate mission, and its superlinear-rate results (Propositions 5, 7, 8, 12, Corollary 13), which require parallel transport and the exponential map, are out of scope. Contributions welcome: proofs of the chain rule identities for retractions (reusable for any Riemannian line search), of Zoutendijk's theorem, and of the milestones in order.
A directed polymer in a random environment is a random up-right lattice path whose law is reweighted by random site weights. Its free energy, the logarithm of the partition function, is believed to belong to the Kardar–Parisi–Zhang (KPZ) universality class: for a path of length of order , the free energy fluctuates on the scale and the path wanders on the scale . For zero-temperature analogues (last-passage percolation with exponential or geometric weights) these exponents were established through exact formulas from random matrix theory (Johansson 2000) and later through a probabilistic coupling argument based on the Burke property of queues (Balázs–Cator–Seppäläinen 2006).
For directed polymers at positive temperature no model with the KPZ exponents was known until Seppäläinen (arXiv:0911.2446, Ann. Probab. 2012) introduced the log-gamma polymer, whose weights are reciprocals of gamma variables, and proved that its free energy has variance of order in the characteristic direction. The model has since become a basic exactly solvable polymer:
The present mission formalizes the 2009 variance theorem, which needs neither of the later exact formulas.
Sites are and . A weight configuration assigns a positive number to each site. On the axes, and for are the boundary weights, and , , are the bulk weights.
An up-right path from to is a sequence whose steps are or . The partition function is
the weight of the origin excluded, . The quenched polymer measure gives the path probability , and the annealed measure is its average over the environment. The exit points and are the numbers of initial steps the path takes along the -axis and along the -axis.
Assumption (2.4). Fix . The weights are independent with
Let and be the digamma and trigamma functions. The characteristic direction is . For a real scaling parameter and a constant , the endpoint satisfies
There are constants and , depending on , such that under (2.4) and (2.6)
The upper bound runs through the Burke property and the variance identity:
The lower bound runs through partition-function comparisons:
The result. Theorem 2.1 was the first proof of the KPZ fluctuation exponent for a directed polymer at positive temperature. Its upper bound also yields a strong law of large numbers for (2.7) and, with Theorem 3.3, a central limit theorem off the characteristic direction (Corollary 2.2). The exit-point estimates of Sections 4 and 5 give the path fluctuation exponent (Theorem 2.3) and are reused for the polymer without boundaries and the point-to-line polymer (Theorems 2.4–2.6).
Formalizing it. The theorem has been proved since 2009; no formal proof of it in a proof assistant is known. A formalization checks a proof with many interacting estimates and two corrected slips (below). The definitions made here (the lattice-path partition function, the inverse-gamma environment, the recursion (3.2), exit points, quenched and annealed measures) are the base for later missions on Theorems 2.3–2.7 of the same paper. Lemma 3.2 contains a gamma-distribution characterization (Lukacs' theorem) of independent interest.
The obvious route to a variance bound, a martingale decomposition of over the independent weights, gives only , i.e. order ; it cannot see the cancellation that produces . The order is specific to the characteristic direction: off it, satisfies a central limit theorem with variance of larger order (Corollary 2.2), so any argument must use the exact relation between the boundary parameters and the endpoint . The upper bound requires controlling the annealed exit point at the scale , with tail estimates whose constants are uniform in the parameters. The lower bound is a separate statement: the path must not exit an axis at distance from the origin with non-vanishing probability, which no upper-bound estimate implies.
Source: arXiv:0911.2446v4 (26 Aug 2015, revised version); its printed page numbers equal the PDF's. All declarations are in the namespace LogGammaPolymer.Variance.
ℕ × ℕ; a path is a step sequence with a fixed number of east steps; is a finite sum over these paths with the starting weight excluded. The environment Env θ μ P bundles one weight family Y : ℕ × ℕ → Ω → ℝ, measurability, mutual independence of every weight off the origin, and the three laws as images under equal to Mathlib's gammaMeasure (shape, rate ). Positivity of the weights is not assumed pointwise in the probabilistic statements; it holds almost surely. The deterministic lemmas (3.1, 5.1, 5.4) are stated for every weight function positive off the origin.variance, and every upper bound or identity also asserts (or integrability of the averaged quantity), so that the junk value of variance and of the Bochner integral cannot satisfy it.Type), the environment, and . Upper limits in are stated as "for every there is with the bound for ". The compact-set uniformity of Lemmas 4.1, 4.3 and (4.32) is formalized. The remark after Theorem 2.1 on uniform constants is not.A formalization in which includes the origin's weight, the laws are not exactly the inverse gammas with shapes and rate , independence is dropped, is allowed, or the constants depend on the environment or on does not state Theorem 2.1.
Needed infrastructure: gamma–beta algebra and a Lukacs-type characterization, independence of finite families built by the recursion (3.2), differentiation of expectations in the shape parameter, and moment bounds for sums of i.i.d. variables. All of these are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas such as (3.3)–(3.4), are welcome.
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.
Potential-reduction methods solve a linear or conic program by driving down a single merit function that combines the objective gap with a barrier for the constraint cone. For linear programming the primal version goes back to Karmarkar (1984) and, without Karmarkar's special problem form, to Gonzaga (1990, Math. Programming 49, 7–21), whose method reduces the potential by a constant at every step while updating a lower bound on the optimal value. Nesterov and Nemirovskii (1994) extended such methods to general convex cones with self-concordant barriers, but their analysis only allows short steps: steps confined to a ball of the local norm, which in practice is a small fraction of the way to the boundary.
Nesterov and Todd (1997) singled out the self-scaled cones (the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products) and showed that for them long steps are admissible. This mission formalizes their extension of Gonzaga's method (§7.2 of the paper): a primal potential-reduction step, with a lower-bound update, that decreases the potential by a constant and, when the potential parameter is large enough, by an amount that scales with how far the step can go.
Let with its inner product, identified with its dual . Let be a closed convex pointed cone with nonempty interior, and a -self-scaled barrier for : a -self-concordant logarithmically homogeneous barrier () such that for all the Hessian satisfies and , where is the dual cone and the conjugate barrier. Here .
The problem is
with linear and surjective, and dual : s.t. , . Both have strictly feasible points: and are nonempty, and the objective is not constant on the feasible region of . Let be the optimal value.
At the local norm is , its dual is , and measures how far one can move from along : the point stays in for . The uniform norm is .
For and a lower bound , the primal potential is
At an iterate with lower bound , let and be the projections of and of into with respect to : , . For put . Whenever , the number is the value of a feasible dual solution, hence a lower bound on . The updated lower bound is the larger of and the best such bound. Finally and the search direction is , which is times the projected gradient of . Write .
If , there is with and
If , there is with and
A total potential decrease from the starting pair forces , where is the minimum of on a bounded truncation of the homogenized feasible region.
Theorem 7.4 together with Theorem 7.3 gives an -iteration method for conic programming over self-scaled cones that needs only a primal strictly feasible point and a lower bound, and that, for , matches the complexity of the short-step theory. Part (b) is the substantive claim: the step may go a large fraction of the way to the boundary of (half way when ) and the guaranteed decrease is typically much larger than . This is the property that distinguishes self-scaled barriers from general self-concordant ones, for which only steps inside the local unit ball are controlled.
The results are proved in the paper. None of them, nor the long-step theory of self-scaled barriers on which they rest, is formalized in any proof assistant as far as is known.
The obvious approach bounds by the self-concordance inequality, which controls only for ; that is the short-step regime and yields at best part (a). Part (b) requires a bound on along valid all the way to , which holds for self-scaled barriers but not for self-concordant ones. The second difficulty is the interplay with the lower-bound update: the decrease of the barrier term must be paid for by the decrease of , and this needs the scaling factor of the direction to be at most , which in turn depends on how was chosen. With an arbitrary admissible lower bound the claim fails.
, are EuclideanSpace ℝ (Fin n) identified through the inner product, and the problem data are surjective, , . The cone, the barrier, the local norms (lnorm), (dnorm), (sigma) and (absn) are the published definitions of the SelfScaledIPM.ShortStep setting; the paper's starred dual norms map to dnorm at a primal point. Nondegeneracy of is part of that barrier definition, and the conjugate barrier is an sSup over .
Standing assumptions are hypotheses of every statement: surjectivity of (6.1), strict dual feasibility (6.3) (strict primal feasibility follows from the given iterate), the objective not constant on the feasible region, and . The optimal value is the infimum of the objective over the feasible set, finite under these assumptions. The projections (7.12) are given as data satisfying their defining equations. The updated lower bound is defined as , with the set of dual bounds over with , and when is empty. Because the gap is nondecreasing in , this equals the paper's value at the minimal admissible . "A suitable value of " is an existential over , and the conclusion also asserts so that the logarithm in is genuine. and of Theorem 7.3 are defined explicitly, with the infimum of over .
A statement in which is an arbitrary lower bound above , or an arbitrary vector in , or arbitrary instead of existentially chosen, would be false; the formalization fixes by (7.17) and by (7.14).
A complete development needs the theory of self-scaled barriers along a line (Theorem 4.2 and Proposition 4.1 of the paper, posed in the sibling mission I of this series), the projection identities (Propositions 6.2–6.3, posed in mission IV), weak conic duality, and the inequalities and . These are reusable across self-scaled interior-point methods; proofs of any of them are welcome.
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.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution enters the dynamics as a control. Contact mechanics with friction, electrical circuits with diodes, dynamic traffic equilibria, hybrid engineering systems and the continuous-time limits of Nash games all have this form. Pang and Stewart's survey (Math. Program. 113, 2008; author's version hal-01366027) set up a common framework for these models and studied the most direct numerical method: the Euler-type time-stepping scheme, which replaces the time derivative by a difference quotient and solves one static variational inequality per time step.
For the scheme to converge, its iterates must exist and be bounded uniformly as the step goes to zero. Section 7 of the paper proves convergence once such bounds are available (Theorem 7.1). Section 8 supplies them for a class of DVIs in which the algebraic part is not affine: the constraint set is a cone and the VI map is a strongly monotone composite. This mission formalizes that section.
Fix , and dimensions . The data are , , , a map and a set . For ,
The initial-value DVI (6.2) is , , .
With and , the time-stepping scheme (7.2) starts at and computes, for ,
The standing assumptions are:
Choosing orthonormal bases of and of , the map is strongly monotone with some modulus (8.7).
Let be a closed convex cone, (A), (B), (D), (C′), and (E) hold. There is such that for every with and every the scheme has a unique run, and for all small
These are the hypotheses (7.5)–(7.6) of the convergence theorem of §7.
A companion item states Proposition 8.1, the derivative form of (D).
Theorem 8.1 is one of the two routes in the paper to convergence of the time-stepping scheme. The other (Theorem 7.4) needs a linear-growth property of the VI solutions that holds for affine or coercive problems; Theorem 8.1 replaces it by structural assumptions on that cover nonlinear complementarity systems on cones, including the case that yields the initial-value differential complementarity problem (Corollary 8.1). Combined with Theorem 7.1(a), it shows that the Euler trajectories have uniformly convergent subsequences whose limits are weak solutions of the DVI, and so gives existence of weak solutions constructively.
The paper's results are proved on paper but, as far as a search of Mathlib and the platform shows, no part of DVI theory is formalized. The formalization also settles a printed error: the bound (8.10) of Proposition 8.3 carries a factor that its proof does not justify, and the printed statement is false (a one-dimensional counterexample is recorded on the milestone). The milestone states the bound the proof does give; (8.14) and Theorem 8.1 are unaffected.
The obvious argument fails at the multiplier bound. The VI map is strongly monotone, but only with modulus of order , so the solution of each step is bounded only by times the data. This loss is harmless for existence and uniqueness but would destroy the uniform bounds (7.5). Recovering an bound requires separating the components of in , where is blind and only the order- monotonicity of helps, from the components in , where itself is strongly monotone; condition (E) and the cone structure of are what allow the two parts to be tested separately. A second difficulty is that (7.6) needs a Lipschitz bound on with a constant that does not blow up as .
EuclideanSpace ℝ (Fin k); matrices are continuous linear maps; is the adjoint; is the published definition SolodovSvaiterVI.Alg21.viSol Φ K.The development needs: existence for strongly monotone (coercive) VIs on closed convex sets; the implicit-function argument for the -equation of a step; orthogonal decompositions along ; and discrete Gronwall estimates. The VI existence result and the decomposition lemmas are reusable beyond this mission. Proofs of any milestone, and of the existence theorem for strongly monotone VIs as a separate theorem, are welcome.
Networks of coupled oscillators model generators in an electric power grid, pacemaker cells, Josephson junction arrays and many other systems in which units with their own rhythm interact through their phase differences. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012, doi:10.1137/110851584) show that, after a singular-perturbation reduction, the transient-stability question for a lossy power network with non-uniform generators becomes a synchronization question for a non-uniform Kuramoto model: oscillators with different damping coefficients, different natural frequencies, an arbitrary coupling graph and phase shifts induced by line losses.
This mission concerns the cleanest regime of that model: lossless coupling and natural frequencies proportional to the damping. There the oscillators do more than agree on a frequency; they agree on a phase. For the classic Kuramoto model (Kuramoto, 1975) with identical frequencies, phase synchronization from inside an open half-circle was obtained by consensus methods for nonlinear coupled systems (Lin, Francis and Maggiore, 2007) and by Jadbabaie, Motee and Barahona (2004). Theorem V.10 of Dörfler–Bullo extends this to non-uniform damping, directed coupling with a globally reachable node, and gives an explicit worst-case rate for symmetric coupling. The proof rests on the contraction theory of time-varying consensus protocols (Moreau, 2004).
There are oscillators. Oscillator has a phase on the circle, a damping coefficient and a natural frequency . Oscillators interact through coupling weights (, with ) and phase shifts . The non-uniform Kuramoto model (8) is
The weights define a directed graph with an edge from to whenever ; a globally reachable node is a node to which every node has a directed path. For the closed arc set is the set of configurations whose angles all lie in a closed arc of length .
This mission assumes zero phase shifts, , and proportional frequencies, for all . The phases synchronize exponentially to a trajectory when there are and with for all and .
For the rate, is the Laplacian of a weight array, is its second-smallest eigenvalue (the algebraic connectivity) when , , , , and .
For every solution with , :
Theorem V.10 gives phase synchronization of non-uniform oscillators from every initial configuration inside an open half-circle, for directed coupling graphs that need only a globally reachable node, and identifies the limit phase: anywhere in the initial range in general, the damping-weighted mean under symmetric coupling. The rate separates three effects: graph connectivity (), initial phase cohesiveness () and non-uniformity of the damping (, ). For the classic Kuramoto model the statements reduce to known results ([19] and [33] of the paper).
The result is proved in the paper; no machine-checked proof is known. A formal proof needs a Dini-derivative argument for the maximum of finitely many smooth functions along an ODE, a contraction theorem for linear time-varying consensus with positive, bounded weights on a graph with a globally reachable node, and a Courant–Fischer bound on the weighted disagreement. Each is a reusable piece of infrastructure for networked control and synchronization.
The obvious argument linearizes: , so the model looks like linear consensus. That only holds near the diagonal; from an arc of length close to the effective weights come close to zero and depend on the state, so neither a fixed Laplacian nor a local linearization covers the claimed region. One needs first that the arc never grows, which is a statement about a non-smooth function (the arc length) along trajectories, and then exponential convergence of a consensus protocol whose weights are time-varying and, for directed graphs, non-symmetric, so there is no quadratic Lyapunov function in general. For the explicit rate the disagreement vector is orthogonal to , not to , and the angle between the two hyperplanes has to be controlled.
Angles are represented by real lifts ; the vector field is -periodic in each coordinate, so solutions on the torus are projections of solutions on . is encoded as for all on the initial lift, and every conclusion (invariance, , , the weighted mean, the convergence bounds) refers to that lift and the same continuous lifted trajectory, which is at least as strong as the statement on the torus. A solution is a curve on whose derivative within equals the vector field at every ; statements quantify over every such curve. The model is stated with the paper's general field and hypotheses , ( arbitrary, not set to zero).
Conventions and corrections, each disclosed in the item's Formalization Note:
AlonMilman.PropertyT.lambda1 applied to the symmetric Laplacian.Exponential convergence requires a rate ; a statement with or with a solution predicate that no curve satisfies would be trivial. The synchronous trajectory satisfies the solution predicate, so the hypotheses are satisfiable.
Infrastructure welcome beyond this mission: upper Dini derivatives and comparison lemmas for maxima of differentiable functions, exponential stability of linear time-varying consensus (Moreau's theorem), and Laplacian ordering for entrywise-dominated weights.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution acts as an algebraic input to the dynamics. The class contains linear complementarity systems, mechanical systems with unilateral contact and friction, dynamic Nash games and many hybrid engineering models. Pang and Stewart's paper (Math. Program. 113 (2008); author's version hal-01366027v1) set up a unified theory of such systems: existence of solutions, uniqueness, and convergence of numerical time-stepping schemes.
The numerical question is the practical one. A DVI is solved by discretizing time and solving one finite-dimensional variational inequality per step. Whether the discrete trajectories approximate a true solution as the step size shrinks is not automatic: the algebraic variable can switch discontinuously, so the discrete 's need not converge pointwise. Section 7 of the paper answers this for a semi-implicit Euler scheme applied to the initial-value problem, and the answer is also an existence proof for the DVI.
Fix and write . Let be a nonempty closed convex set, let , , and . For , is the set of with for all . The initial-value DVI (6.2) is
The standing assumptions are (A): , and are Lipschitz continuous on (for the metric ), and (B): .
A weak solution is a pair with , integrable on with for almost every , the integral equation for , and the integral form of the VI,
The time-stepping scheme (7.2) uses a step , grid points , a parameter , and :
for . The iterates are turned into functions of time: is the continuous piecewise linear interpolant of the , and is the piecewise constant interpolant equal to on .
Suppose the iterates satisfy the uniform bounds (7.5),
for all small . Then along some ,
If moreover (a) with Lipschitz and (7.6), or (b) with positive semidefinite, then every such limit pair is a weak solution of (6.2).
The proof decomposes into the paper's own steps: Lemma 7.1 (the implicit Euler step is uniquely solvable, with the bounds (7.4)); the uniform step bound , which makes equicontinuous; the fact that a weak limit of -valued functions is -valued almost everywhere; the integral VI (7.7) under (a); the integral equation (7.8); and the weak lower semicontinuity (7.9) of for positive semidefinite , which handles (b).
Lemma 7.2 (a discrete Gronwall bound giving (7.5) from one-step growth conditions), Lemma 7.3 ((7.5) from linear growth of the VI solutions) and Proposition 7.1 (existence of the iterates for small ) are included as further targets: together with Theorem 7.1 they reduce the hypotheses on the iterates to conditions on .
Theorem 7.1 is simultaneously a convergence theorem for a practical numerical method and an existence theorem: any scheme with bounded iterates produces, in the limit, a weak solution of the DVI. Combined with Proposition 7.1 and Lemma 7.3 it yields existence for DVIs whose VI part has linearly growing solution sets, including linear complementarity systems with positive semidefinite , without the upper-semicontinuity machinery of differential inclusions. Case (b) covers monotone linear complementarity systems, the class arising in passive electrical networks and frictionless contact.
The results are proved in the paper. None of them is machine-checked. A formalization would produce a reusable Lean account of Euler polygons, equicontinuity estimates for discrete schemes, and weak limits of constrained sequences, all of which recur in the numerical analysis of nonsmooth dynamical systems.
The obvious argument would pass to the limit in each step of the scheme pointwise. This fails because has no pointwise or strong limit in general: only weak compactness is available. The nonlinear term does not commute with weak limits, so the variational inequality cannot be passed to the limit directly. Each of the two cases supplies the missing compactness or convexity: in (a) the bound (7.6) makes converge uniformly, and in (b) positive semidefiniteness makes the quadratic term weakly lower semicontinuous. Membership also does not follow from pointwise reasoning and needs convexity of .
Vectors are EuclideanSpace ℝ (Fin k), inner products are ⟪u, v⟫_ℝ, and matrices are continuous linear maps with the operator norm. is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric.
Step sizes are with an integer , so that the grid ends exactly at . "For all " becomes "for all ", and "" becomes a strictly increasing sequence of 's. The iterates are a family indexed by and are hypotheses of the goal; their existence is the separate Proposition 7.1. Weak convergence in is tested against every function, and the uniform convergence of is on all of . Condition (7.6) is imposed for , because the paper's convention makes vacuous.
A weak solution carries integrability of both integrands as explicit conditions. Without them a non-integrable pair would satisfy the integral conditions vacuously, since a Lean integral of a non-integrable function is zero. The following readings are also excluded: convergence of the scheme only at grid points; a scheme in which solves the VI at instead of ; and a conclusion about one particular subsequence instead of every subsequence along which both limits exist.
A complete development needs: compactness in (Arzelà–Ascoli), weak sequential compactness of bounded sets in , Mazur's lemma on convex combinations, and estimates for piecewise linear and piecewise constant interpolants. The last two items are reusable for other time-stepping schemes. Proofs of any milestone, and of auxiliary interpolation lemmas, are welcome.
Out of scope: the weaker Carathéodory assumption (A′), the implicit scheme (7.3), the cited fixed-point theorems 7.2–7.3, and Theorem 7.4 (which combines Theorem 7.1 with the existence results of §6).
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 spectral sparsifier of a weighted graph is a graph on the same vertices, with few edges, whose Laplacian quadratic form is within a factor of that of on every vector. Spielman and Teng introduced the notion in their work on nearly-linear-time solvers for symmetric diagonally dominant linear systems (Spielman–Teng 2004; arXiv:0808.4134): a sparsifier can replace a dense graph as a preconditioner, and it preserves every cut value up to the same factor, strengthening the cut sparsifiers of Benczúr and Karger (BK96).
Their construction first handles graphs whose edge weights lie in a bounded range. Arbitrary weights need an extra idea, which §10.2 of Spectral Sparsification of Graphs formalizes as Lemma 10.2 (Pullback): when a graph's vertex classes are held together by edges far heavier than those between them, one may contract each class to a single vertex, sparsify the much smaller contracted graph, and pull the result back to the original vertices. The approximation factor degrades only by , where measures the gap between heavy and light weights. The same contraction idea goes back to Benczúr and Karger's treatment of weighted cut sparsifiers.
A weighted graph on a finite set , , is a symmetric function with ; its edges are the pairs with . Its Laplacian quadratic form is
A graph is a -approximation of if for all . We write when for all , for the graph whose weights are the sums, and for the single edge of weight .
Let be a partition of with map . Write for the edges between different parts, , and , . The contraction of under is the graph on with weight for and no self-loops. Given a graph on , a graph on is a pullback of under if every edge of joins different parts, is the contraction of , and for every edge of exactly one edge of has , . A pullback thus has as many edges as .
Let , , let be a -approximation of the contraction of under , and let be a pullback of . Assume (1) each is connected by edges in , (2) every edge in has weight at least , (3) every edge in has weight . Then
Choose representatives ; let , be the copies of , on , and , .
The constants are the paper's; the goal is the lemma as printed.
Lemma 10.2 is the reduction from arbitrary weights to bounded weights in Spielman and Teng's sparsification algorithm (Sparsify, §10.2): the edges of each weight scale are sparsified on a graph in which all much heavier edges have been contracted, so the number of vertices handled at each scale stays small, and the total size of the sparsifier is only a logarithmic factor larger than in the bounded-weight case. The statement itself is purely about quadratic forms and holds for any approximation of the contraction, however it was obtained; it applies equally to later sparsification methods such as sampling by effective resistances.
The lemma is proved in the paper. As far as is known, none of these statements has a machine-checked proof: Mathlib has the Laplacian of a simple graph (SimpleGraph.lapMatrix) but no weighted Laplacian order, no contraction of weighted graphs and no notion of spectral approximation. The mission produces those objects and a complete formal proof of the lemma and its intermediate claims.
The individual steps are elementary, but the proof combines three kinds of bookkeeping. Lemma 10.3 is a Cauchy–Schwarz inequality along a path, which must be applied to a path assembled from two walks inside parts and one edge between representatives; obtaining a simple path of length at most from the connectivity hypothesis requires shortening walks. The summed bounds require recognising that the copies of the unit edges between representatives add up exactly to , which uses hypothesis 3 and the fact that contraction counts each edge between two parts once. Claim (c) needs, in addition, that the total weight of is at most times that of and that each pullback edge has the weight of its image edge. The constants are tight in one place: requires both and .
A natural shortcut, comparing with directly, fails: and have different edges, and their Laplacians are only comparable through the heavy intra-part edges.
A weighted graph is a function w : V → V → ℝ on a Fintype V with IsWGraph w (symmetric, nonnegative, zero diagonal); sums and scalar multiples are pointwise. lapForm w x is , IsApprox σ w̃ w keeps both inequalities of the definition, and GraphLE is . The partition is a surjective map π : V → Fin k (nonempty parts). , are crossPart w π, intraPart w π; hypothesis 1 is reachability, between any two vertices of the same part, in the simple graph of -edges. Representatives are any r : Fin k → V with π (r i) = i, and liftAlong r z places a graph on Fin k on them; the goal does not mention representatives. is Fintype.card V.
Two hypotheses implicit in the paper are explicit: (with the lemma is false), and that every edge of a pullback joins two different parts (contraction cannot see an edge inside a part, so without this a pullback could carry an arbitrary heavy edge and the lemma would be false). In Lemma 10.3 the edge weights are positive and the path has at least one edge.
A trivializing formalization is ruled out: dropping hypothesis 2 or 3, allowing or intra-part pullback edges, or letting the pullback forget the uniqueness of the edge over each makes the statement false or weaker, and stating only one of the two inequalities of -approximation is a different theorem. Every statement here keeps both.
The algorithm Sparsify and its analysis (Lemma 10.4, Theorem 10.5, Proposition 10.6, Theorem 10.7, Lemmas 10.8–10.9) and all running-time claims are out of scope. The weighted Laplacian form, its additivity and nonnegativity, and the transport of a quadratic form along an injective vertex map are reusable beyond this mission; contributions of such general lemmas, and a proof of Lemma 10.3 by Cauchy–Schwarz, are welcome.
Periodic-review inventory models with a fixed ordering cost are the setting in which the policy is optimal: when the stock falls below a reorder point , order up to a level , otherwise order nothing. Scarf (1960) proved this for independent demands over a finite horizon by introducing -convexity, and Iglehart (1963) extended it to the discounted infinite horizon. In practice the demand distribution changes with an exogenous environment: the economy, the season, the stage of a product's life cycle. Song and Zipkin (Oper. Res. 41(2), 1993) modelled this environment as a Markov chain of demand states in continuous time with Poisson demand.
Sethi and Cheng (Oper. Res. 45(6), 1997) treat the discrete-time version with general demand densities, nonstationary costs and convex surplus costs of linear growth. The companion mission (I) covers their finite-horizon result, Theorem 4.1. This mission covers the nonstationary discounted infinite-horizon result, Theorem 6.2, together with the existence theory (Theorem 6.1, proved in the paper's Appendix) on which it rests.
Demand states form the finite set and follow a Markov chain with transition matrix . In period the demand has the conditional density given , with mean at most . Orders are placed at the start of a period and delivered at once, and unmet demand is backlogged, so the surplus evolves by (2.4). Ordering costs with (2.1), where for and otherwise. The surplus cost is convex and nonnegative, vanishes at , and satisfies (2.2).
An admissible policy chooses each order as a measurable function of the past demand states and demands. With a discount factor , the objective from period , state and surplus is
and the value function is . With (3.1), the dynamic programming equations are
The truncations keep the first periods of (6.1) (6.3), their values are (6.4), and is the cost of never ordering (6.6). The function classes are (nonnegative pointwise limits of continuous functions), (those of linear growth) and (those also uniformly continuous in ). A function is -convex if for all , (4.3). Assumption (4.1) asks , and (4.2) asks as .
Under (2.1), (2.2), (4.1), (4.2) and , there are in such that
attains the infimum in (6.2) at every , and its feedback policy, started at any period and surplus , has cost : it is optimal among all history-dependent policies.
The structural lemma behind the step from -convexity to the form, Proposition 4.2 of the paper (an extension of Bertsekas' lemma to lower semicontinuous functions coercive only at , with possibly infinite , ), is posed in the companion finite-horizon mission and is not repeated here.
Theorem 6.2 says that the classical structure survives two generalizations at once: demand driven by a Markov environment, and nonstationary data over an infinite horizon. The two levels may depend on the period and on the current demand state, so only numbers per period describe an optimal policy, and with cyclic demand only pairs are needed (Corollary 7.1 of the paper). Theorem 6.1 is a self-contained existence result for a positive-cost, unbounded-state dynamic program: value iteration from zero converges to the value function, which solves the optimality equation, and any measurable minimizer is optimal among history-dependent policies.
The results are proved in the paper, with the finite-horizon existence theory delegated to Beyer, Sethi and Taksar (1998). No machine-checked proof of any of them is known. The platform has -convexity (BertsekasKConvex) and the structure lemma of Bertsekas for continuous functions coercive at both ends; it has no discounted infinite-horizon theorem with Markov-modulated demand. The related posed items SongZipkinFluct.FixedCost.theorem5e_theorem6 and theorem5ab concern the Song–Zipkin model (continuous time, Poisson demand, integer levels, stationary data), a different model.
The obvious argument is "the finite-horizon value functions are -convex, so their limit is, and a minimizer of a -convex optimality equation is ". Three steps of it fail as stated.
First, the limit of value iteration need not be the value function, nor solve (6.2), in a positive-cost problem with unbounded actions: exchanging with requires the minimizers of the truncated problems to stay in a compact set uniformly in , and that bound is where the coercivity assumption (4.2) enters. Second, optimality against history-dependent policies, not only Markov ones, requires a verification argument along histories of states and demands. Third, the functions may be unbounded below, in which case the reorder level is and the order-up-to level does not exist; the goal allows this case.
The Lean development (namespace SethiChengSS.Infinite) commits to the following.
Fin L; periods are natural numbers with the paper's base .Pins. The paper prints ; the mission assumes , since is infinite at and the Appendix divides by . Theorem 6.2 is printed without (4.1), which its proof uses through the induction of Section 4; (4.1) is assumed for every period. Theorem 6.1 is printed under (2.1)–(2.2) only, but attainment in (6.2) can fail without coercivity and the Appendix bound (A.3) divides by ; (4.2) is added to (6.9), (6.10) and to the attainment clause of (6.5). "In class " for the sequence is read with one growth constant for all periods. The boundary condition "" of (6.5) is read as , as the next sentence of the paper states.
The goal cannot be met by a degenerate encoding: the value function is the infimum over all admissible history-dependent policies (not the solution of (6.2) by definition), the demand data must be genuine probability densities with bounded mean, and the levels may not be .
A complete development needs: monotone convergence for the path-measure costs, measurable selection of minimizers, the -convexity closure properties (Proposition 4.1 of the paper; several are proved on the platform as BertsekasDP.kconvex_*), and Proposition 4.2. The model file and the infinite-horizon verification argument are reusable for other Markov-modulated inventory models. Contributions toward any milestone, or toward general lemmas on positive-cost dynamic programs, are welcome.
Stochastic differential equations (SDEs) are simulated almost always by time-stepping schemes, and the cheapest and most widely used is the explicit Euler (Euler–Maruyama) scheme. Its strong convergence with order is classical when the coefficients are globally Lipschitz. Many models in applications are not: Langevin dynamics with confining potentials, stochastic Ginzburg–Landau equations, and population or volatility models have drifts such as that grow superlinearly.
For such drifts the explicit Euler scheme fails. Hutzenthaler, Jentzen and Kloeden showed in 2011 (Proc. R. Soc. A 467) that its absolute moments diverge to infinity whenever the drift or the diffusion grows superlinearly, so it does not converge in . Implicit schemes do converge (Higham, Mao and Stuart, SIAM J. Numer. Anal. 40, 2002), but each step requires solving a nonlinear equation.
The paper of this mission (Hutzenthaler, Jentzen and Kloeden, Ann. Appl. Probab. 22(4), 2012) introduces a tamed Euler scheme: an explicit method that costs the same as the Euler scheme, modified by a second-order term in the drift. It proves strong convergence with order under a one-sided Lipschitz drift whose derivative grows at most polynomially. The scheme started a line of work on tamed and truncated methods, among them Sabanis's schemes that tame drift and diffusion together for superlinearly growing diffusion coefficients (Ann. Appl. Probab. 26(4), 2016), formalized on this platform in the series "Euler Approximations with Varying Coefficients".
Fix and . Let be a probability space with a filtration , and let be an -dimensional standard -Brownian motion. On , is the Euclidean norm and the inner product. For a matrix , is the operator norm.
The initial value is -measurable with for every . The drift is continuously differentiable and the diffusion is . There is one constant with
for all . The exact solution is an adapted process with continuous paths and
For , let . The tamed Euler scheme is and
On its interpolation is
In Lean, states live in EthierKurtz.SDEState d, takes values in Matrix (Fin d) (Fin m) ℝ, the standing hypotheses are the structures Coefficients and Setting, and the scheme is Y, Ybar, all in the namespace TamedEuler.Convergence.
There is a family , , such that for every solution
The constants are left unspecified; only the order is asserted.
These are the ten lemmas the proof rests on, in the paper's order:
The theorem gives an explicit scheme whose cost per step is the Euler cost and whose strong error is in every , uniformly in time, for the superlinear drifts on which the explicit Euler scheme diverges. Strong error bounds of this kind are what multilevel Monte Carlo (Giles 2008) needs, as the paper notes on p. 3: its complexity analysis requires strong convergence of the coarse and fine levels, and the explicit Euler scheme supplies none for these equations. The moment bound of Lemma 3.9 answers, for the tamed scheme, the open problem Higham, Mao and Stuart formulated in 2002 on when moment bounds hold for explicit methods (quoted on p. 8).
The result is proved in the paper; it has not been formalized. The mission formalizes the statement, its ten lemmas and the scheme. The dominator construction (13)–(14) is a pathwise argument that can be checked independently of the probability. The two Burkholder–Davis–Gundy inequalities with the explicit constant are reusable tools for any numerical analysis of SDEs.
Once the moments of are bounded uniformly in , the convergence proof follows the globally Lipschitz pattern: an Itô or Gronwall argument on . The difficulty is the moment bound itself. The obvious approach is a Gronwall recursion for in terms of . For superlinear it does not close: the term grows faster than , and for the untamed scheme the moments do in fact diverge. A newcomer's first idea, using the one-sided Lipschitz bound in expectation, fails for the same reason. The paper instead dominates the scheme pathwise on events and controls the rare complement separately (Lemmas 3.1, 3.5, 3.6).
The Lean development commits to the following conventions.
ℱ.IsRightContinuous) together with adaptedness to its -completion, which is how the published SabanisEuler.Shared.IsSolution treats completeness.SabanisEuler.Shared.IsWienerMartingale, defined on rather than ; this is the usual extension. Time is ℝ≥0.IsSolution relation, whose stochastic integral is the Ethier–Kurtz Brownian Itô-integral relation. Existence and uniqueness are cited by the paper, not claimed. enters IsSolution entrywise through toDiffusion. Every norm of in a hypothesis or conclusion is the operator norm opNorm.lintegral or eLpNorm, never as a Bochner integral that could default to .A trivializing formalization is ruled out: the scheme is (8) exactly, with only the drift tamed and the step size . The error is taken against the same Brownian path that drives . The setting is satisfiable for the paper's example , with (checked in a sorry-free verification file, given any Brownian motion). Replacing the Itô integral by a postulated operator or a pathwise integral is not admitted.
A complete development needs:
The BDG inequalities and the Gaussian moment identity are reusable beyond this mission. Contributions to any lemma, or to the stochastic-calculus infrastructure underneath, 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.
Large service systems (call centers, hospital wards, cloud server pools) run with many servers, and for many of them no exact formula describes how the number of busy servers moves over time. Heavy-traffic limits replace such a system by a diffusion process that is easier to analyze. The many-server regime, in which the number of servers and the arrival rate grow together, goes back to Halfin and Whitt (1981) and is the basis of square-root staffing rules in call-center practice.
The simplest many-server model is the queue. Its stationary number in system is Poisson with mean , so the centered and -scaled stationary count is asymptotically normal when . The question here is about the whole process: does the scaled number in system converge, as a random path, to a diffusion? The classical answer, the Ornstein–Uhlenbeck limit, was first established by Iglehart (1965) with Stone's theorem for birth-and-death processes, and was revisited by strong approximation (Mandelbaum, Massey and Reiman 1998) and, for general service times, by Krichagina and Puhalskii (1997).
Pang, Talreja and Whitt (2007) is a tutorial survey that proves this limit, and its finite-waiting-room extension, with martingale methods. The authors present the argument as a template for non-Markovian and network models (Reed 2009; Dai and Tezcan; Gurvich and Whitt). This mission formalizes the result and the steps of the paper's proof.
Fix a service rate . For each , the -th system has arrival rate . Let and be independent Poisson processes of rate , and let be a random initial number of customers, independent of and . The number in system is the -valued process with right-continuous paths having left limits that satisfies, almost surely,
The departure term is a random time change: each of the customers in service completes service at rate . The diffusion-scaled process is , the paper's (3). The space consists of paths on that are right-continuous with left limits, and denotes convergence in distribution.
The limit is the Ornstein–Uhlenbeck (OU) process , driven by a standard Brownian motion , with independent of :
The proof also uses the scaled martingales and , the fluid processes and , and stochastic boundedness. A sequence of real random variables is stochastically bounded if it is tight, and a sequence of processes is stochastically bounded in if is, for every .
If in , with an arbitrary limit law , then
where is the OU process (5) with . The goal fixes no initial distribution and assumes no moment condition on .
Theorem 1.1 describes the transient behavior of a large infinite-server system, not only its stationary law: fluctuations of order around the offered load form a Gaussian Markov process that relaxes at rate . It is the reference case for the Halfin–Whitt regime, whose finite-server version, Theorem 1.2 of the same paper (the queue), is the subject of the companion mission. The milestones are general tools reused well beyond queueing: Gronwall's inequality, the Lipschitz integral map, the Poisson FCLT, stochastic boundedness via Lenglart's inequality, and the fluid limit from stochastic boundedness.
The theorem is proved and classical; no machine-checked proof of it, or of the milestones below, is known. No formal library currently has the Poisson functional central limit theorem in , compensators of counting processes, or random time changes of martingales. Formalizing the paper's proof would produce these, plus a template for the martingale method of heavy-traffic analysis. Alternative proofs, such as the paper's §4.3 route without martingales, are equally welcome as solutions.
Equation (12) is a fixed-point equation: appears inside the argument of . The integral map of Theorem 4.1 is continuous, so the obvious argument is to apply the continuous-mapping theorem to the martingale representation. That reduces the goal to the joint convergence of . But is a Poisson martingale evaluated at the random time , and its limit is identified only after the fluid limit is known. The fluid limit is itself a statement about the whole sequence , and it needs a separate argument, either Gronwall at fluid scale or stochastic boundedness. Lemma 3.2 requires optional stopping at the continuum of stopping times , and the moment conditions (22) must be checked through the crude bound. Removing needs a truncation of the initial conditions (§6.3).
CouplingConverges): a Skorokhod representation with almost-sure uniform convergence on compact intervals. Convergence to a deterministic path is uniform convergence on compacts in probability (UocInProb). is stated with bounded continuous test functions.Type.A formalization that fixes , assumes converges almost surely, adds to the goal, or replaces convergence in by convergence of finite-dimensional distributions proves a weaker theorem and does not close the goal.
Contributions are welcome at every level. The Poisson FCLT, Lenglart's inequality and the composition map are reusable library results, independent of queueing.
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.