Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 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?
Federated learning combines information from several clients without pooling their raw training records. A client may later request removal of its contribution. Retraining on the retained records supplies a natural comparison model, but repeating the training process can be costly. Jin, Chen, Zhang, and Li introduce a linearized learning pipeline and a server-side removal procedure in Forgettable Federated Linear Learning with Certified Data Unlearning, arXiv:2306.02216v3. Their linearization makes the training objective quadratic, so the distinction between an exact Newton correction and an approximate correction can be studied explicitly.
This mission formalizes a corrected finite-run error bound motivated by that analysis. It is not a transcription or validation of the printed Theorem 2. The source audit found that the supplementary argument drops a finite-training term when passing to a limit, uses an invalid general inverse-perturbation inequality, and does not justify its three-term squared-norm constant. The draft preserves the removal problem while stating its error factors explicitly. The source anchors are Section III-C, Theorem 2, PDF pp. 5–6, and supplementary Section C5, PDF p. 16. The preprint first appeared in 2023; this mission fixes the revised May 2026 version so later source changes cannot silently alter its meaning.
A parameter is a vector . Record has a fixed linear feature map , an offset , and a target . Its prediction is . This represents the fixed linearization in the paper's equation (3); arbitrary real targets are permitted, and one-hot classification targets are a special case. Neither approximation accuracy for a nonlinear neural network nor an infinite-width limit is asserted.
Let be the full finite dataset and a nonempty subset of retained indices. Client removal is represented by retaining precisely the indices whose owner differs from the removed client. More general record removals are also allowed. For a fixed regularization parameter , define
Write , , and . Define and let use the full dataset. These reference parameters are computed from the data. The accepted child proofs establish the Hessian positivity and invertibility needed for the error bound; the broader unique-minimizer theorem is a separate supporting statement. The construction comes from Section III-A, PDF pp. 3–4, equations (3)–(5).
A separate nonempty server dataset has Gram operator and regularized Hessian . All operator norms below are Euclidean operator norms. The datasets and feature maps are fixed throughout the probability calculation.
Let be the trained parameter, the parameter returned by retraining on , and an approximate removal correction. The removed parameter is . Their joint probability model has finite outcome space , with masses summing to one. They may be dependent. This covers the outputs of finite randomized runs on finite data with fixed initialization; no independence assumption is used.
For each trained parameter , define the server removal objective and its exact minimizer by
This is the quadratic surrogate in Section III-B, PDF p. 5, equation (6). Define
The corrected goal is
The two completed milestones used by the accepted proof are the surrogate gap bound and the corrected signed removal-error identity:
The broader ridge-structure, exact-Newton-removal and inverse-perturbation statements remain available as separate open theorems. Their milestone entries were removed because the accepted proof does not depend on their full statements.
Formalization note: the completed root is a corrected, paper-derived error bound. Its formal bridge uses the two source-backed child theorems above, anchored to Section III-B (Section 3), PDF p. 5, equation (6), and Section III-C (Section 3), PDF p. 5 and PDF p. 6, Theorem 2; supplementary C5, PDF p. 16, unnumbered displays. The coefficients in the boxed goal are conservative; no optimality claim is made.
The result connects the removal solver's objective gap, the difference between the server and retained Hessians, and the actual optimization errors to an observable parameter discrepancy. Exact Hessian matching sets . Exact removal optimization sets , but finite retraining error still remains. This distinguishes exact optimization of the retained objective from reproducing an unfinished retraining run.
The original paper motivates the comparison; the displayed corrected bound is a new formulation derived from its quadratic setting. The root Lean theorem and its two dependency milestones are now Proved. Their accepted proofs match the original formal statements exactly; the three separate supporting statements remain open. The requested OpenProblem classification describes the formalization task and does not assert that the elementary corrected inequality is an unresolved research conjecture.
An approximate server Hessian cannot be substituted for the retained Hessian without a sensitivity term. A bound on the difference of the Gram operators alone does not bound its action on every parameter vector. Likewise, a small training error relative to the full-data optimum does not imply that the full and retained optima coincide. The displacement therefore remains visible. Formalization must respect the normalization of each empirical objective, the sign of the correction, and the operator norm used in the perturbation estimate.
The model uses finite-dimensional real Euclidean spaces, continuous linear maps and adjoints, finite index sets, a total ring inverse, and finite weighted expectations. Positive regularization must justify every use of the inverse; it is not an invertibility assumption hidden inside the dataset. Nonempty retained and server data exclude division by an empty sample count. Zero-dimensional feature or parameter spaces are permitted and harmless. A finite law on an empty outcome type has no inhabitant because its masses cannot sum to one.
The root theorem quantifies over arbitrary output maps . It is an error-propagation theorem in terms of their actual errors and surrogate gap, not a convergence theorem for a particular implementation. Obtaining algorithm-specific bounds on those quantities is separate future work. In particular, the draft does not import the source's unsupported all-smaller-learning-rates FedAvg contraction claim. It also makes no differential-privacy, distributional indistinguishability, nonlinear-network, or empirical accuracy assertion.
The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is -penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).
Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).
A sample is a point with a response and a feature vector , so the samples live in . The sample space is a compact set, and carries the norm . A training set is .
A learning algorithm maps each training set to a hypothesis ; with a loss , it is -robust (Definition 2, p. 396) if can be partitioned into disjoint sets , fixed independently of the data, such that for every , every training point , every and every ,
For a metric on and , a set is an -cover of if every point of is within distance of a point of ; the covering number is the least cardinality of such a cover (Definition 1, p. 394).
For a coefficient vector let . Given , the Lasso is
a Lasso algorithm returns a minimizer of (5) for each , and the loss is the absolute prediction error . Finally .
For every compact , every , every Lasso algorithm and every ,
The statement holds for every selection of a minimizer, since (5) need not have a unique solution.
Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form with a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.
The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the / pairing on , and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.
The constant in the robustness level depends on the training set through , while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by and the cells must depend only on and . A cover by balls is not a partition, and the radius of the cover () and the closeness threshold in Theorem 6 () differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between and is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.
ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly . is written out as , since the default norm on Fin m → ℝ is the sup norm; is dotProduct w x.Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies , which the paper leaves implicit. The factor is a real division; for it is in Lean, the objective reduces to , and all statements remain true.Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.
Classical generalization bounds control the gap between the expected loss of a learned hypothesis and its average loss on the training sample. The average is sensitive to outliers: when a non-negligible fraction of the sample is corrupted, the mean loss stops describing the quality of a solution, and quantile-type summaries such as the median become the natural measurement. Quantile losses have long been used for this reason in statistics and econometrics (Koenker and Bassett 1978; Huber 1981). The standard tools for proving generalization bounds — symmetrization, Rademacher and VC arguments — are built around the expected loss and do not extend to quantiles in any direct way.
Xu and Mannor (Mach Learn 86 (2012) 391–423) introduced algorithmic robustness: an algorithm is robust if the sample space can be partitioned into finitely many cells such that a test point falling in the same cell as a training point incurs a similar loss. Because the argument works cell by cell and needs no symmetrization, it transfers to loss functionals other than the mean. Sect. 4.1 of the paper uses this to bound the quantile value and the truncated mean of the testing error, and Sect. 5 relaxes robustness to pseudo robustness, which only asks the cell condition for a subset of the training samples. This mission formalizes the resulting Theorem 5 (p. 402), whose proof is Appendix C (pp. 415–418).
Let be a measurable sample space, a set of hypotheses and a loss, with each measurable. A training set consists of i.i.d. draws from a probability measure on ; its empirical distribution is . A learning algorithm is a map , and is the hypothesis learned from .
For a real random variable and a level , the -quantile value is
and, writing , the -truncated mean is
where the second term vanishes when . It is the contribution to of the leftmost fraction of the distribution. For a hypothesis and a measure on put and with .
The algorithm is pseudo robust, with and , if can be partitioned into disjoint sets , fixed in advance, such that every training set has a subset of samples with: whenever and lie in a common cell, . With this is -robustness.
Let and . If is pseudo robust, and , then with probability at least : whenever and ,
The constants are the paper's, and , , , , , and the algorithm are arbitrary.
The result. Theorem 5 shows that any pseudo-robust algorithm has a testing-error quantile and truncated mean that are bracketed by the empirical ones at levels shifted by , up to the robustness tolerance . The quantile of the testing error can therefore be estimated from training data for every algorithm to which the robustness framework applies — among them majority voting, SVMs, Lasso and principal component analysis (Sect. 6 of the paper) — without a separate complexity analysis of the loss class. The pseudo-robust form covers algorithms that are robust only away from a small set of training samples, which is the typical situation in the presence of outliers. The robust case is the paper's Theorem 2 (p. 400).
Formalizing it. The paper states Theorem 5 and proves it in Appendix C; no machine-checked proof exists. The appendix contains misprints (see Formalization scope) and the argument uses minimizers of the loss over each cell, which need not exist; a formal proof settles which steps are sound as written. The definitions of quantile value and truncated mean of a law on developed here are reusable beyond this mission.
The concentration step is the same as for the expected loss: on the event the empirical cell frequencies are close to the cell probabilities. The difficulty is converting this into a statement about quantiles. Quantile values are not linear in the distribution and are discontinuous in the level, so the triangle-inequality argument that bounds the mean-loss gap does not apply. Mass that moves between cells shifts every level of the quantile function, and the up to samples outside carry no guarantee at all, so an arbitrary fraction of the empirical law is uncontrolled. For the truncated mean this must be done for the whole lower tail up to level , not just at one point, and the atoms of the loss distribution (the second branch of the definition) have to be accounted for exactly.
XuMannorRobust.Quantile. is a type with a measurable space structure, an arbitrary type, a training set a function Fin n → Z, and the i.i.d. law the product measure Measure.pi (fun _ => μ).Most generalization guarantees in statistical learning theory bound the gap between training error and expected error through a complexity measure of the hypothesis class: VC dimension, Rademacher complexity, covering numbers. Such bounds are sufficient conditions, and they say little about why a particular algorithm, run on a particular data stream, does or does not generalize. Xu and Mannor (Mach Learn 86 (2012) 391–423) proposed algorithmic robustness as an alternative: an algorithm is robust if a test sample "close to" a training sample incurs a loss close to that training sample's loss. Their first results show that robustness implies generalization (Theorem 1 of the paper, the subject of the first mission in this series).
Section 8 of the paper asks the converse question: is some form of robustness also necessary? The answer is Theorem 8. For a learning method trained on a fixed, growing sequence of samples, generalization is equivalent to a weaker property, weak robustness. The authors present this as evidence that robustness is "an essential property of successful learning", and contrast it with the characterization of learnability by stability (Remark 5 of the paper, citing Shalev-Shwartz et al. 2009; journal version JMLR 11 (2010)): learnability is uniform over all distributions, whereas the generalization studied here is for one distribution and one training sequence.
Let be a measurable space of samples, drawn from an unknown probability measure . Let be a set of hypotheses and a loss with for all (the paper's standing assumption, Sect. 1.1).
expectedLoss).avgLoss).firstN).The method generalizes w.r.t. (Definition 8) if
It is weakly robust w.r.t. (Definition 9) if there are sets with and
A set can be read as a family of perturbed copies of the training set that carries almost all of the probability of the test sample.
for every probability measure , every loss measurable in with values in , every learning method and every training sequence .
Milestones 1–2 give the sufficiency direction; milestones 3–4 give necessity.
Theorem 8 is a characterization, not a bound. The sufficiency half says a quantitative robustness property yields generalization. The necessity half says every method that generalizes along a sequence is weakly robust along it, so no generalization argument can avoid something of this shape. The paper remarks that -robustness for every implies weak robustness, which places Theorem 1's condition inside this characterization. Corollary 6, the almost-sure version (generalization with probability 1 iff almost-sure weak robustness), follows from Theorem 8 applied sequence by sequence.
The result is proved in the paper; no machine-checked proof of it is known. This mission contributes a formal statement of Definitions 8 and 9 in Lean, the two directions of the proof as reusable finite- and asymptotic lemmas, and a place to formalize the bounded-loss law of large numbers for a hypothesis that changes with (Eq. (9)), which Mathlib states for a fixed random variable.
The sufficiency direction is a direct estimate once the expectation of the average test loss is identified with the expected loss; the formal work is in handling the product measure and a set that need not be measurable.
The necessity direction is where care is needed. Eq. (9) is not the weak law of large numbers for a fixed function: the hypothesis changes with , so the concentration must be uniform in the hypothesis, which holds only because the loss is uniformly bounded. Lemma 2 negates a statement with an existential over sequences of sets and a limit; the naive reading "for each some works eventually" does not by itself produce a single sequence satisfying (6) with one limit.
MeasurableSpace, a Measure with IsProbabilityMeasure, an arbitrary type. The learning method is A : (n : ℕ) → (Fin n → Z) → H, the training sequence sStar : ℕ → Z, and Measure.pi (fun _ : Fin n => μ). Indices start at .ℝ≥0∞). The sets need not be measurable; their probability is the outer measure. "For infinitely many " is ∃ᶠ n in atTop.Measure.pi of coordinate functions, a Chebyshev or Hoeffding bound for averages of bounded i.i.d. variables uniform over a family of functions, and a diagonal-sequence construction. The uniform concentration lemma is reusable beyond this mission. Proofs of the milestones, and alternative routes to Eq. (9), are welcome.A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.
Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.
Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.
Throughout, is a measurable space of samples and is an arbitrary set of hypotheses. A loss satisfies for a constant . A training set is , and a learning algorithm is a map , written .
For a probability measure on , the expected error and the training error of the learned hypothesis are
Definition 2 (p. 396). For and , the algorithm is -robust if can be partitioned into disjoint sets such that for every ,
The partition is chosen once, before the training set. Only the tolerance may depend on .
For a partition , the cell count is the number of training points in . The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.
Let be -robust and let consist of i.i.d. draws from . Then for every , with probability at least ,
The constants are the paper's and are kept as printed. , , , , , and the algorithm are all universally quantified.
Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:
Its complexity term depends only on the number of cells , not on any capacity measure of . This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.
Theorem 1 is a published result with a short proof. What a formalization adds:
A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.
The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of -measure zero, where the conditional expectation in the paper's chain is undefined.
The main obstacle is the probabilistic step. The quantity is an deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the coordinates gives a bound whose deviation level grows linearly in . That is not , and it does not give the constant of Theorem 1. The difficulty is to obtain the exact exponential rate for the deviation as a whole, with no loss in the constant.
Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and enters as a real number.
"With probability at least " is encoded as an upper bound on the outer measure, under , of the set of training sets where the inequality fails. This needs no measurability of .
The paper ignores measurability. The formalization restores it: every is measurable and every cell is a measurable set. Together with this makes the expected error a genuine expectation.
The theorems assume . The Bretagnolle–Huber–Carol step assumes , because the printed inequality is false for . No upper bound on is imposed: for the radicand is negative, the square root evaluates to , and the statements remain true.
Two trivializing readings of Definition 2 are ruled out:
IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a -valued loss would be -robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).
A two-stage stochastic linear program with fixed recourse chooses a first-stage decision before a random vector is observed, and then pays for a cheapest corrective action once is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.
Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.
The data are a random element with , , and an matrix, distributed according to a probability measure . The recourse matrix (), the first-stage matrix () and are fixed. The recourse function is
equal to if the second-stage program is infeasible and if it is unbounded.
The weak covariance condition (Definition 2.2) requires , and to be integrable for all indices; it does not require , or themselves to be integrable. The paper also assumes throughout that has full row rank (p. 312).
Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and . The expected recourse is and the objective is
The induced constraints are , where and is the support of the distribution of . The fixed constraints are , and . The deterministic equivalent program (8.2) is to minimize over .
A convex program of the form with finite value is stable (Definition 8.1(iv)) if there is with for all , . Equivalently, the dual obtained by perturbing is solvable and has no duality gap.
If the weak covariance condition holds, has full row rank, is a polyhedron and the program is finite, , then
Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function at , and hence a bounded rate of change of the optimal value under perturbations of . The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.
The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.
The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of . It fails unless that constant is integrable, and the weak covariance condition, not integrability of , is what has to deliver this, uniformly over the finitely many second-stage bases.
For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of has curved boundary, the perturbation function can have infinite slope at ; the polyhedral hypothesis on is what excludes this.
Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper (, , ) enter through dotProduct. The law is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.lintegral of the positive part minus lintegral of the negative part, with whenever the positive part is . This is the paper's ; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be for non-integrable integrands and make every expected-cost statement trivial, and it is not used. is a Bochner integral, legitimate because Definition 2.2 makes each integrable.Integrable.ConvexOn of toReal on the finite branch.PointedCone.FG/DualFG in Mathlib), LP duality with values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.A two-stage stochastic program with recourse is a linear program in which a decision is taken before a random vector is observed, and a corrective (recourse) decision is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in alone, and the first question is which are admissible at all: the random second-stage constraints induce constraints on that are not written down anywhere in the data.
Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.
Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random . The 1974 survey collects these results in the form formalized here.
The data are a fixed real matrix and a random vector with , , and an matrix. The law of is a probability measure on the product space, and its support is the smallest closed set of measure one. The recourse function is
equal to when the program is infeasible and when it is unbounded below. The expected recourse uses the paper's integral: the sum of the positive part and the negative part , with .
The weak covariance condition (Definition 2.2) asks that , and be integrable for all . Write . The candidate feasibility sets for the induced constraints are
A convex polyhedron is a set given by finitely many linear inequalities; and are polyhedra.
If is fixed and satisfies the weak covariance condition, then
so is a closed convex polyhedron. The number of inequalities is not fixed in advance, and may be empty.
Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of . This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.
The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).
Two steps resist the obvious approach. First, needs an integrable upper bound for the positive part of on the whole support. is only piecewise linear in , can equal , and , , are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra , and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of is the content of the goal, and the resulting system may be inconsistent, in which case .
Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is with its Borel structure, and is a probability measure on the whole space (the paper's sample space only carries ). Readings fixed by the formalization:
Integrable with respect to .EReal subtraction () and the Bochner integral of toReal (zero for non-integrable functions) would both make wrong and are not used.Measure.support; is the support of the pushforward under the (continuous, hence measurable) projection onto .A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral would make . Neither is used.
A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.
The periodic-review inventory problem with a fixed ordering cost is one of the basic models of operations research. A firm reviews its stock once per period, may order at a cost per order plus a unit cost, and then faces a random demand; unmet demand is backlogged. Scarf (1960) and Iglehart (1963) showed that for this model an policy is optimal: order up to whenever the stock falls below , and otherwise do nothing. That result tells a manager what shape a good policy has, but not which pair to use.
Veinott and Wagner, Computing Optimal (s, S) Inventory Policies (Management Science 11 (1965) 525–552), gave the first practical algorithm for computing an optimal pair when demand is discrete. The algorithm rests on a closed form, their Eq. (11), for the discounted cost of an arbitrary stationary policy, obtained by a renewal argument in their Section 3. The same closed form, in the undiscounted limit, is the classical expression of the long-run average cost of an policy used throughout inventory theory textbooks.
Timeline:
Demands are independent random variables on with common distribution , . Write for the -fold convolution of ( is the point mass at ) and for its distribution function, so .
In period the stock before ordering is and the stock after ordering is ; then . With the unit purchase cost eliminated as in the paper's Eq. (2), the cost of period is , where is the set-up cost, , for , and is the one-period cost. Period is discounted by with .
A stationary policy, for integers , sets if and otherwise. Its total expected discounted cost from is
and its equivalent cost per period is .
The renewal quantities are
the latter being the discount renewal function,
If is the first period in which cumulative demand exceeds , then is the expected discounted one-period cost over periods from stock without ordering, and .
With ,
Eq. (11) turns the cost of an policy, an infinite series over the trajectories of a controlled Markov chain, into a finite expression in , and the renewal sequence , which the paper computes by a one-line recursion. Everything in the paper's Section 4 builds on it: the search for an optimal pair minimizes over a finite box, and the undiscounted limit gives the long-run average cost .
The result is classical and proved in the paper. What this mission adds is a machine-checked derivation from the definition of the policy's expected cost, including the renewal step, which the paper states in one sentence ("a renewal of the process takes place"). It also produces a reusable Lean layer: discrete convolution powers, the discount renewal function, and the law of an -controlled inventory chain. To the best of our knowledge none of these is formalized in Mathlib or on the platform.
The paper's argument conditions on the random time at which the process renews and uses the strong Markov property at that time. In the formalization, is defined as a sum over periods of expectations under the law of . Relating that sum to one that splits at the random time requires either a stopping-time decomposition of the chain or an explicit accounting of the law of before and after the first order. Neither is a direct computation. A second difficulty is the interchange of the infinite sum over periods with the sum over states , which has infinitely many states reachable (demand is unbounded below). The renewal equation (milestone 4) alone does not determine without the fact that for , which comes from (9).
VeinottWagnerSS.RenewalCost. Stock levels are integers, demands natural numbers; and enter , , through Int.toNat, which is exact because the statements assume or .tsums. is defined by the series (7) and by the first line of (9), i.e. through the law ; the paper's derivations of these series from are not formalized. For all series converge for every , because after period the stock after ordering lies in the finite set .Contributions welcome: proofs of the milestones, general lemmas on discrete renewal sequences and convolution powers, and a first-passage decomposition for integer-valued Markov chains, which is reusable beyond this mission.
Markov chain Monte Carlo (MCMC) estimates an expectation by the average of along a Markov chain whose invariant distribution is . Many chains share the same : every Metropolis–Hastings acceptance rule that satisfies detailed balance, every mixture of such kernels, every choice of proposal. Practitioners need a criterion for preferring one of them. The standard yardstick is the asymptotic variance of the ergodic average, the constant in the Markov chain central limit theorem. A smaller asymptotic variance means fewer iterations for the same Monte Carlo error.
Peskun (1973) compared chains on a finite state space through a partial order on transition matrices: if one reversible matrix moves off the diagonal at least as much as another, entry by entry, its asymptotic variances are no larger, for every function. That result justifies the Metropolis–Hastings acceptance probability as the best possible among reversible acceptance rules. It covers only finite state spaces, while MCMC is used almost exclusively on continuous or mixed ones.
Tierney (1998) extended Peskun's theorem to general state spaces, using the spectral approach of Kipnis and Varadhan (1986) for reversible chains. The theorem is the one usually cited when an MCMC paper argues that one sampler dominates another; Mira (2001) surveys orderings built on it.
Let be a measurable space in which singletons are measurable, and let be a probability measure on . A Markov kernel assigns to each a probability measure , measurably in . It acts on functions by . The measure is invariant for if for every . The kernel is reversible with respect to (satisfies detailed balance) if
that is, for all . Reversibility implies invariance.
Write , for the square-integrable functions and .
Off-diagonal domination. For kernels , (OffDiagDominates π P₁ P₂) if for -almost every ,
So from almost every state moves to every region at least as readily as , and the kernels differ only in the probability of staying put.
The chain and its asymptotic variance. For a Markov kernel , let be the Markov chain with initial distribution and transition kernel (chainMeasure π H, a measure on paths ). For put (pathSum f n) and
The lag inner products are (lagInner π H f k), and for the regularized variance is (vLam π H f lam).
Let be Markov kernels reversible with respect to , , and . Then both asymptotic variances exist in and
No rate, constant or regularity of the kernels is fixed. The statement is the ordering itself, valid for every reversible pair and every .
The result. Theorem 4 turns a pointwise, one-step comparison of kernels, which is easy to check, into a comparison of the quantity that governs Monte Carlo error. Its main consequence, drawn in §3 of the paper, is that the Metropolis–Hastings acceptance probability gives the maximal kernel in the off-diagonal order among reversible Metropolis–Hastings kernels with a given proposal. It is therefore optimal in asymptotic variance, on arbitrary state spaces. Proposition 5 of the same paper (a separate mission in this series) combines with it to show that a single Metropolis–Hastings kernel built on a mixture proposal beats the mixture of the component kernels. Later orderings of samplers (Mira 2001; Andrieu and Livingstone 2021) take this theorem as their base case.
Formalizing it. The theorem has been proved since 1998. No machine-checked version exists for general state spaces, and none of its milestones is on the platform. The formalization produces reusable infrastructure: the asymptotic variance of a stationary chain as an extended-real limit on Mathlib's Ionescu–Tulcea path measure, the facts for reversible kernels (self-adjointness, contraction, the covariance formula for path sums), and the positivity of under off-diagonal domination. Each of these is used again in any formal treatment of MCMC efficiency or the Markov chain central limit theorem.
The direct approach compares the two finite- variances. This fails, and not just technically: the paper exhibits two doubly stochastic, symmetric matrices with for which the variance of is 15.4 under and 14.8 under (p. 7). Off-diagonal domination orders the lag-one covariances, but higher-order correlations "need not be ordered" (p. 5). The ordering appears only in the limit, and only for reversible kernels. The comparison must pass through an object that sees all lags at once and is monotone along the segment , and that object involves resolvents of operators on . The limit may be infinite, so every comparison must be made in . Mathlib has neither the spectral measure of a self-adjoint operator nor the Kipnis–Varadhan theory.
The state space is {E : Type*} [MeasurableSpace E] with [MeasurableSingletonClass E] wherever off-diagonal domination appears. This is an assumption the paper leaves implicit: must be an event. is a probability measure and all kernels are Markov kernels. Reversibility is Mathlib's Kernel.IsReversible, invariance is Kernel.Invariant. The function is measurable with MemLp f 2 π and, for , ∫ f ∂π = 0; measurability picks a representative of the class and costs nothing. The chain is Kernel.trajMeasure started from . The sum runs over , not . Variances are Mathlib's evariance in , and is a Tendsto limit in ℝ≥0∞, so an infinite asymptotic variance is represented. The goal asserts the existence of both limits rather than assuming it, so it cannot hold vacuously. Neither it nor any milestone specializes to finite , to Metropolis–Hastings kernels, or to a chain started from a point. Lemma 3 assumes invariance only, and the theorem requires reversibility, as printed.
Two statements depart in form from the page. The finite- variance identity and are written through the moments (a Neumann series) instead of through the spectral measure and the resolvent . The two forms agree for a self-adjoint contraction, and this is noted in each item. The paper's appeal to the spectral theorem and to Kipnis and Varadhan (1986) is not restated as an item: a complete development needs it, or an equivalent argument, as part of the proof. Proofs of any milestone, and reusable lemmas on the path measure (stationarity and the marginal laws of ), are welcome.
The Metropolis–Hastings algorithm (Metropolis et al. 1953; Hastings 1970) is the basic construction of Markov chain Monte Carlo. It turns a target probability distribution , known only up to a constant, into a Markov chain that has as its invariant distribution. Bayesian computation depends on it, and a sampler is usually designed by proving one property: reversibility, or detailed balance, with respect to .
For discrete state spaces, or when every measure involved has a density with respect to a common reference measure, the condition on the acceptance probability is the familiar . Samplers used in practice often do not fit this setting: deterministic involutive proposals, mixtures of proposals with different supports, and Green's dimension-changing moves for model selection (Green 1995) have no common density. Each of these was treated separately in the literature. Tierney (1998) gives one necessary and sufficient condition that covers all of them, on an arbitrary measurable state space. This mission formalizes that condition.
Let be a measurable space, with no topological or countability assumption. Let be a probability measure on , the target. Let be a Markov transition kernel on , the proposal, and let be a measurable function, the acceptance probability. From the current state , a candidate is drawn from and accepted with probability ; otherwise the chain stays at . The resulting Metropolis–Hastings kernel (mhKernel Q α) is
A kernel satisfies detailed balance with respect to if the two measures and on are equal (Eq. (2)). Equivalently, for all measurable , which is Mathlib's Kernel.IsReversible P π.
Put (π ⊗ₘ Q), and let be its image under the swap . A symmetric split (IsSymmetricSplit) is a measurable set with , such that and are mutually absolutely continuous on and mutually singular on its complement . Informally, consists of the pairs between which the proposal can move in both directions. A ratio version (IsRatioVersion) is a measurable that is a density of (the restriction of to ) with respect to , and satisfies at every point.
For every , , as above and every symmetric split and ratio version for :
The paper phrases the left side as condition (4), , which its text identifies with (2) for the kernel (1). The goal states it for the kernel itself.
that is, the rejection mass on the diagonal does not affect reversibility.
§2, special case 1 (pp. 3–4). If and for a -finite , then is a symmetric split, is a density of with respect to , and detailed balance is equivalent to the two conditions holding -almost everywhere.
Theorem 2 lets reversibility be checked in the same way for every Metropolis–Hastings variant: compute and for the proposal, then verify (i) and (ii). The paper derives from it the reversibility of the standard acceptance probability on (and off ), and the three special cases of §2 are instances. Together with Mathlib's Kernel.IsReversible.invariant, it yields that is invariant for the sampler. This is the correctness statement of every MCMC method built on the Metropolis–Hastings kernel. Missions II and III of this series (Peskun ordering; mixture proposals) take reversible Metropolis–Hastings kernels as their objects.
The result is proved in the paper. The mission adds a machine-checked proof at the paper's full generality: no densities, no dominating measure, no countability of . The platform currently has only finite-state statements (MarkovMixing.metropolis_stationary, a sufficiency direction on a Fintype state space with a matrix proposal), so neither the general kernel nor the converse direction is formalized there.
The obvious argument works with densities: write both sides of (3) as densities with respect to one reference measure and compare them pointwise. On a general space no such reference is given for and together, and even yields densities only up to null sets. Pointwise comparison of densities is therefore not available, and the statement mixes three kinds of almost-everywhere claim (-a.e., -a.e., and a.e. for the restrictions to and ). The Lean statement also has to hold for every version of and , not one convenient choice. Milestone 2 has its own content: the diagonal part of is a measure concentrated on the diagonal, which need not be a measurable set, and its symmetry has to be shown without that measurability.
{E : Type*} [MeasurableSpace E] with nothing else: no measurable singletons, no topology, no countable generation. π : Measure E with [IsProbabilityMeasure π] and Q : Kernel E E with [IsMarkovKernel Q].α : E × E → ℝ≥0∞ with the hypotheses Measurable α and ∀ p, α p ≤ 1, which is the paper's measurable . The kernel is Q.withDensity (fun x y => α (x, y)) + Kernel.withDensity Kernel.id (fun x _ => ∫⁻ u, (1 - α (x, u)) ∂(Q x)). The measurability hypothesis rules out the junk zero kernel that Kernel.withDensity returns for a non-measurable density.Kernel.IsReversible. It agrees with the measure identity (2) because rectangles determine a finite measure on .IsSymmetricSplit and IsRatioVersion (a symmetric Lebesgue-type decomposition of a measure against its transpose) are reusable for any reversibility argument on product spaces. Lemmas on Measure.map Prod.swap of compProd and withDensity, and on the symmetry of measures carried by the diagonal, are also welcome contributions.A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. The format covers the first-order optimality conditions of constrained optimization, nonlinear complementarity problems, traffic and economic equilibria (Wardrop, Walrasian, Nash–Cournot), and systems of nonlinear equations; see Harker and Pang's survey (Math. Programming 48, 1990) and Facchinei and Pang's monograph (Springer, 2003).
When the map has no special structure (not strongly monotone, not Lipschitz with known constant, not affine) and the feasible set is a general closed convex set, the practical algorithms are projection methods. The oldest is Korpelevich's extragradient method (1976). Without a known Lipschitz constant, extragradient-type methods need a linesearch in which every trial point costs one projection onto the feasible set, and projection onto a general convex set is itself an optimization problem.
Solodov and Svaiter (SIAM J. Control Optim. 37 (1999) 765–776) proposed a method that spends exactly two projections per iteration, whatever the linesearch does, and proved global convergence under only continuity of the map and a generalized monotonicity condition weaker than pseudomonotonicity. The method, often called the hyperplane projection method, is a standard reference point for later projection and extragradient-type algorithms.
Timeline:
Work in with the Euclidean inner product and norm . Let be closed and convex and continuous. The problem is to find with
Its solution set is . The projection onto a nonempty closed convex set is . The projected residual is ; its zeros are exactly the points of .
Condition (1.2) requires, for every ,
It holds when is monotone or pseudomonotone, and in cases where is neither.
Algorithm 2.1. Fix and . Given : if , stop. Otherwise let be the smallest nonnegative integer with
set , , , and
The hyperplane separates from .
If is closed and convex, is continuous, and (1.2) holds, then every sequence generated by Algorithm 2.1 converges to a single point of :
The theorem fixes no rate and no constant; it asserts convergence of the whole sequence, not only of a subsequence.
Theorem 2.1 gives global convergence of a projection method for variational inequalities with no Lipschitz constant, no monotonicity and no knowledge of the problem beyond continuity and (1.2), at a fixed cost of two projections per iteration. Condition (1.2) covers pseudomonotone maps, which arise as gradients of pseudoconvex functions and in equilibrium models where monotonicity fails. The separating-hyperplane-and-project template of the proof is reused throughout the later literature on projection, proximal and hybrid methods for monotone inclusions.
The result has been proved since 1999. To the best of available knowledge no machine-checked proof of it, or of any convergence theorem for a projection method for variational inequalities, exists in Lean or Mathlib. This mission produces the statement and the supporting layer: a Euclidean projection onto closed convex sets with its standard inequalities, variational inequality solution sets, the projected residual, and a formal model of an Armijo-type linesearch algorithm with termination.
The Fejér-type inequality (2.6) quickly gives bounded iterates and . The obvious next step, concluding , fails: nothing prevents the stepsizes from tending to zero, and in that regime the product going to zero says nothing about the residual. This regime is where the minimality of and the continuity of enter, and it is the step a naive formalization (for instance one that drops minimality, or fixes the stepsize) cannot reach. A second subtlety is that (1.2) is needed at an accumulation point that is only known to lie in at the end of the argument, which is why the condition must hold for every . Finally, subsequential convergence must be upgraded to convergence of the whole sequence to one solution; convergence of a subsequence, or of the distance to , is strictly weaker.
EuclideanSpace ℝ (Fin n) (not Fin n → ℝ, whose norm is the sup norm). The accumulation-point step needs finite dimension; no Hilbert-space generalization is intended.projOnto K x is a nearest point of to when one exists, chosen by Classical.choose, and the junk value otherwise. On nonempty closed convex sets it is exactly ; the paper only projects onto such sets (, , ), so the junk value is never reached under the hypotheses.x : ℕ → ℝⁿ with Armijo indices k : ℕ → ℕ (predicate IsAlg21Run). If the method has stopped and the run stalls, ; otherwise is the least index satisfying (2.1) and . A stalled point is a solution, so finitely terminating runs are included in the goal.exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero), firm nonexpansiveness, the explicit projection onto a halfspace, and a bounded-sequence subsequence argument in . The projection lemmas are reusable for any projection-type method; contributions proving them as standalone lemmas are welcome.Shor's 1997 paper (SIAM J. Comput. 26(5), arXiv:quant-ph/9508027) gives a polynomial-time quantum algorithm for factoring integers. The quantum computer does not factor directly: it finds the multiplicative order of an element modulo . The step from order finding to factoring is classical and randomized, and goes back to Miller's 1976 work on primality testing (G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13 (1976)). Every account of Shor's algorithm, and every resource estimate for breaking RSA with a quantum computer, depends on this reduction succeeding with a constant probability per trial. This mission formalizes that probability bound as Shor states it on p. 1498 of the published paper.
Let be an odd integer with prime factorization
so is the number of distinct prime factors of , all odd. The unit group consists of the residues coprime to ; it has elements, where is Euler's totient function.
For a unit the order is the least positive integer with . For each the local order is the order of , taken modulo the full prime power, not modulo . For a positive integer , denotes the exponent of the largest power of dividing .
The reduction is: choose uniformly at random from , obtain its order (from the quantum subroutine), and compute
The procedure yields a nontrivial factor at when is even and . In Lean this event is ShorAlgorithms.Reduction.successEvent n u for u : (ZMod n)ˣ, and is localOrder n u p for p ∈ n.primeFactors.
It is stated for every odd . For a prime power () the bound is , so the statement says nothing there; it is informative exactly when is not a prime power, as the paper remarks. The constant is sharp: for exactly of the units succeed, so in place of would be false.
The result. The bound turns an order-finding oracle into a factoring algorithm: when is odd and not a prime power, each trial succeeds with probability at least , so independent trials all fail with probability at most . Even numbers and prime powers are split classically, as the paper notes, so the bound completes the reduction from factoring to order finding. The same criterion — a square root of other than splits — underlies the Miller–Rabin test and several classical factoring methods.
Formalizing it. The mathematics is classical and proved; the paper gives a sketch of one paragraph. This mission writes out the sketch as machine-checked statements over Mathlib's ZMod, including the probabilistic step, which in the paper is an informal appeal to the Chinese remainder theorem and "50% probability of agreeing with the previous ones". Mathlib already has the needed ingredients (cyclicity of for odd , ZMod.chineseRemainder, ZMod.card_units_eq_totient), but not the reduction or its probability bound.
The success criterion (milestone 1) is elementary. The substance is the counting. The obvious route — treating the as independent and each "equal to the previous one with probability " — needs both a precise product decomposition of the unit group modulo into the unit groups modulo , compatible with the local orders, and the count in a cyclic group of even order of the elements whose order has a given 2-adic valuation. The informal phrase "at most a 50% probability of agreeing with the previous ones" hides a conditioning argument over coordinates that has to be done by an explicit cardinality bound. A second pitfall is milestone 3: its converse direction and its forward direction use oddness of in different places, and modulo a power of the argument breaks because .
(ZMod n)ˣ; probabilities are stated in cleared-denominator form, in , with the count as Nat.card of a subtype. Non-units have no multiplicative order and are not sampled..val, which is at least for a unit when , so the natural-number subtraction in val - 1 never truncates. is natural-number division, used only under Even r.n.primeFactors.card, at least for , so k - 1 does not truncate. Since is odd this equals the page's "number of distinct odd prime factors".ZMod (p ^ n.factorization p) under the reduction homomorphism.ZMod n instead of the units would put non-units (with junk order ) into the denominator; the goal counts over (ZMod n)ˣ and divides by . The goal's constant is the paper's , which is attained, so it cannot be weakened into a triviality without changing the theorem.ZMod.chineseRemainder to unit groups and to local orders; and proofs of the milestones in any order.Shor's factoring and discrete logarithm algorithms (Shor 1997) reduce both problems to sampling from the output of a quantum Fourier transform: a register holding a superposition with a hidden period is transformed, then measured, and the measured value carries information about the period. The whole speed-up rests on one engineering fact: for the Fourier matrix, which has entries, can be applied by a quantum circuit of only elementary gates, each acting on one or two bits.
That circuit was found independently by Coppersmith (IBM RC 19642, 1994) and Deutsch, and Shor's §4 presents it following Ekert and Jozsa (Rev. Mod. Phys. 68, 1996). It is the quantum analogue of the radix-2 fast Fourier transform, and it reappears in phase estimation, in the hidden subgroup algorithms for abelian groups, and in every textbook account of quantum computation. This mission formalizes Shor's statement that the circuit computes the Fourier matrix, up to a reversal of the output bits, together with the two displayed steps of its verification.
A register of bits has one basis state for every bit string, with the least significant bit; the string encodes the integer
A state is a vector of complex amplitudes, one per basis state. A gate is a matrix whose rows are indexed by input basis vectors and whose columns are indexed by output basis vectors (§2, p. 1489). A gate on some of the bits acts on those bits through its matrix and leaves the others alone (§2, p. 1490): the output amplitude at a string is the sum, over the possible input values of the acted-on bits, of the input amplitude at with those bits replaced by , times the matrix entry from to the corresponding bits of .
The Fourier matrix (eq. (4.1)) is the matrix with entry ; it takes to .
The circuit uses two gates (eqs. (4.2), (4.3)):
The circuit is the gate sequence (4.4), applied from left to right:
that is, for it applies and then . On three bits it is .
The bit reversal of a string is the string with .
For every and every basis state , with ,
The sum runs over all -bit strings . Reading the output register in reverse order therefore yields .
The amplitude of in is
For bit strings , with the bit reversal of and their values,
The result. The goal says that , a dense unitary on amplitudes, is realized by one-bit gates and two-bit gates, followed by a relabelling of the output. This is what makes the Fourier sampling step of the factoring algorithm (§5) and of the discrete logarithm algorithm (§6) polynomial in the number of bits. Without it, the analyses of those sections describe measurements of states that no efficient circuit is known to prepare. The bit reversal is a real part of the statement: the circuit does not compute itself for , and an implementation must either permute the output bits or read them in reverse order.
Formalizing it. The identity is classical and its proof is short on paper; its content lies in bookkeeping that is easy to get wrong: which bit a gate touches, which of the input or output value a bit holds when a phase gate acts, and the order in which the gates are applied. A machine-checked version fixes all of these conventions explicitly and yields a reusable model of gate-level circuits on bit strings. To the drafter's knowledge there is no Lean formalization of this circuit on Prove2Me; the platform's FastFourierTransform rows state the classical Cooley–Tukey recursion for the unnormalized transform with the opposite sign, which is a different object.
Multiplying out the gate matrices is not an argument beyond tiny : the difficulty is to control the whole product of gates symbolically. The paper's argument (§4, p. 1496) is informal at exactly the points a formal proof must make precise: that only one sequence of intermediate basis states from to carries nonzero amplitude, and that at the moment acts, bit already holds its output value while bit still holds its input value . Both facts depend on the order (4.4); applying the same gates in the reverse order gives a different unitary, whose phase pairs with . The phase identity then holds only modulo , not as an equality of real numbers, so it cannot be closed by rearranging sums alone.
Fin l → Fin 2, with bit j equal to and value (least significant bit first). A state is a function from bit strings to ℂ. The case (, empty circuit) is included.R j and S j k — run by a left fold, so the leftmost gate acts first. It is not defined as the matrix or by its entries; a definition of that kind would make the goal true by unfolding and is ruled out.Welcome contributions: proofs of the two milestones and the goal; general lemmas about one- and two-bit gate actions on Fin l → Fin 2 states (commutation of gates on disjoint bits, linearity, action on basis states), which are reusable for any gate-level circuit; and a proof that the circuit is unitary.
Conjugate gradient methods minimize a smooth function using only gradients and a handful of stored vectors. This makes them the standard choice when is too large for Newton or quasi-Newton methods, which store an matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.
D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as , where is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor . Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.
Vectors are columns in . A prime denotes transpose: is the inner product and the outer product. An iterative method produces points , steps along search directions , gradients , and gradient changes . A line search is exact when .
The BFGS update of a matrix with the pair is
A restart cycle begins at iteration . At a later iteration , Shanno's self-scaled restart matrix is
The matrix is its BFGS update with , and the self-scaled two-update direction is . The unscaled variant uses the BFGS update of in place of the first matrix.
Beale's direction is
The quadratic case has gradient with symmetric positive definite.
Let be symmetric positive definite, and . Assume that for we have , and , that for , and that . Then
This is the paper's claim that "for quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly .
The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with . The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale changes only the length of the step, not its direction.
Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:
The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, . It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of with all later steps. The second is , which again comes from conjugacy. Beale's formula also has to be matched in its -form: the coefficient equals only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with must be shown to remain positive definite, and this has to be done twice.
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product is u ⬝ᵥ v, the outer product is vecMulVec u v, and is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case . Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: and in the quadratic statements, and or in the generic ones.
The conjugacy for is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range of Beale's formula is not assumed.
Several formalizations would make the claim easier than the paper's, and none of them is used:
The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.
Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).
The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.
Two manufacturers sell substitutable products through one retailer. The demand for product is
where is the retail price, measures competition, and is a random shock with mean and variance . The retailer observes a demand signal that is unbiased, , and has linear expectation: for a weight (in the paper , with the signal accuracy). The retailing cost is zero, and manufacturer produces units at cost with : a production diseconomy.
The game has four stages.
The pricing stage is a Bayesian game. Its equilibrium ex ante profits are , , for the manufacturers and for the retailer, where is the number of informed manufacturers. They define a payoff table for the contracting stage.
Two contracting protocols are compared.
For every , and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),
with both inequalities strict when . Here is the retailer's profit after side payments and the manufacturers' total profit net of them. The paper's word "higher" is read as because for small neither protocol sells information and all profits coincide.
The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in (Figure 1 of the paper).
Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is . No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.
Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities and . The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold has no closed form; it is the root of a convex rational function of .
The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:
A complete development needs:
The model layer is shared with the companion mission on production economy.
A b-matching with upper bounds in a graph assigns a nonnegative integer to every edge so that the edges at each node carry at most in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching (, ) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point , find a violated blossom inequality or certify that none exists.
M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds . The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.
Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated -matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.
Let be a finite simple undirected graph, and . The system is
with the node–edge incidence matrix. For write for the edges with both ends in and for the cut-set of , the edges with exactly one end in . For with odd, the blossom inequality is
Let be a real point feasible for (3.1) and its node slacks. Let be the edges with . The labelled weighted graph has nodes , a special node , and one new node for each . For each such edge , where is the end the construction scans first, it has an edge of weight and an edge of weight . Each is joined to with weight . There are no other edges. A node is odd iff is odd; is odd iff is odd; a node is odd iff plus the of the subdivided edges scanned from is odd. A node set is odd when it contains an odd number of odd nodes, and denotes the total weight of the edges leaving (its cut capacity).
For every feasible and every scan order,
The paper's closing sentence, that and can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.
Theorem 3.1 is what makes the blossom inequalities of capacitated -matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated -matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.
The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph and of the reduction, and a checked proof of it. The definitions of the capacitated -matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.
The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets with complemented edge sets and odd node sets of . In one direction the right must pick, for every cut edge, the side of that makes the edge contribute or as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses to exclude every other position of a new node , and it uses the evenness of the total label to pass from an odd set containing to its complement. A point whose blossom violation uses an edge with has no new node for . Such a has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.
The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of is not assumed. All halves and differences are computed in ℝ. When the cut-set is empty, so the paper's convention " is empty" holds automatically.
is fixed by definitions from and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node . Weights are a symmetric function on nodes with meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by , and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.
Two trivializing formalizations are ruled out: is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is and would make the right side true when no odd cut exists.
Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.
Edmonds showed that the convex hull of the matchings of a graph is described by the degree constraints together with the blossom inequalities, one for every odd set of nodes (Edmonds 1965). There are exponentially many of them, so any cutting-plane method for matching and b-matching problems must answer a separation question: given a fractional point, find a violated blossom inequality or certify that none exists. Padberg and Rao (1982) reduced this question to a purely graph-theoretic one, the odd minimum cut-set problem, and solved that problem in polynomial time with a single Gomory–Hu computation. The same subroutine underlies separation for many other odd-set constraints (for example the 2-matching and comb-type constraints of the travelling salesman polytope), and later work refined its running time (Letchford, Reinelt and Theis 2008).
This mission covers Section 1 of the paper: the combinatorial theorem about odd cuts, independent of matchings. A companion mission covers the reduction from capacitated b-matching separation (Section 3).
Let be a finite undirected graph without loops and multiple edges, with edge weights . Write for the weight of the edge , with , and if there is no such edge. For the cut-set is the set of edges with exactly one end in , and its capacity is
A nonempty set of nodes is labelled odd, the rest even. For the label is odd if is odd, and even otherwise; is even. The paper assumes throughout that is even, i.e. is even. A cut-set is odd if is odd, and an odd minimum cut-set is a solution of
A cut-set is a minimum cut-set with respect to all pairs of odd nodes if it separates two odd nodes and no cut-set separating two odd nodes has smaller capacity.
A cut-tree for the odd nodes is the output of the Gomory–Hu algorithm applied to all pairs of odd nodes (Gomory and Hu 1961). Each tree node contains exactly one odd node and possibly some even ones, so is identified with , and each node of belongs to one tree node . Removing a tree edge splits into two subtrees; the nodes of in the tree nodes of the -side subtree form a set , and the weight of is . The defining property (Hu, Theorem 9.2) is that for every tree edge the cut-set is a minimum cut-set of separating and . The cardinality of a subtree is its number of tree nodes.
For every cut-tree of for the odd nodes:
Because is even, the two subtrees have the same parity, so the condition is checked on one side.
Theorem 1.1 turns problem (1.1), a minimization over exponentially many odd sets, into maximum-flow computations followed by a scan of the tree edges. Combined with Section 3 of the paper, this gives a polynomial separation algorithm for the blossom inequalities of b-matching polytopes, and hence, by the equivalence of separation and optimization, a polynomial-time route to weighted b-matching through linear programming. The odd-cut routine is also used for separating the odd-set constraints of other polytopes.
The theorem has been proved since 1982 and is textbook material. What this mission adds is a machine-checked proof on a precise encoding of cut-trees. As far as the platform's corpus shows, neither the Gomory–Hu cut-tree property nor any odd-cut theorem has been formalized in Lean; Mathlib has trees and reachability in simple graphs but no cut-tree theory.
The obvious argument fails at the minimum. Every tree-edge shore separates two odd nodes, so a minimum-weight odd-splitting edge certainly yields an odd cut, but showing that no odd set , however it cuts across the tree nodes, has smaller capacity requires relating an arbitrary odd to a tree edge whose shore is also odd and whose endpoints separates. The cut-tree only certifies minimality for cuts separating the two ends of a tree edge; an odd set may split many tree nodes and cross many shores at once, and nothing in the cut-tree property speaks about parity. Parity bookkeeping between odd labels in and odd cardinality of subtrees is the other place where care is needed: the two notions agree only because each tree node holds exactly one odd node.
The graph is a weight function c : V → V → ℝ on a Fintype V, with hypotheses that it is symmetric and nonnegative; a missing edge has weight 0 and the diagonal never enters a cut. Node sets are Finset V and is the complement Wᶜ. The odd nodes form a Finset odd with odd.Nonempty and Even odd.card on every statement. The cut-tree is a SimpleGraph on the subtype {v // v ∈ odd} together with a map π : V → {v // v ∈ odd}; IsOddCutTree requires that the graph is a tree, that π fixes every odd node, and the Gomory–Hu minimality for every tree edge. The tree-edge weight is computed from the shore, not supplied as data. Minimality is always stated as ≤ against every competitor; no real infimum is taken.
The existence of a cut-tree (the Gomory–Hu theorem) is a hypothesis-side object and is not part of this mission; the theorems hold for every tree satisfying the cut-tree property. A statement in which the cut-tree assumption already says that the chosen edge's shore is an odd minimum cut, or in which "odd minimum cut" is minimized only over tree-edge shores, would make Theorem 1.1 definitional; both are ruled out, since IsOddMinCut ranges over every node set with odd label.
A complete development needs: submodularity-type identities for cut capacities (reusable for any cut problem), the structure of fundamental cuts of a tree (the two sides of a removed edge are complementary and the parities of along tree edges combine), and Lemma 1.1. Proofs of the milestones, alternative arguments for the goal that avoid the recursion, and a formal Gomory–Hu existence theorem are all welcome contributions.
Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor .
Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor of optimal.
There are agents and tasks. Agent needs time for task ; the vector is the type vector, and agent alone knows its row . In the bounded scheduling problem (Definition 33) there are fixed numbers with for all , and every declaration lies in the same range. An allocation assigns each task to one agent; is the set of tasks of agent .
A strategy of agent has two parts: a declaration , and an execution, which for each decision of the mechanism specifies the actual time in which agent performs each task . The mechanism chooses from the declarations alone and afterwards observes the actual times . The objective is the make-span with actual times,
Agent receives a payment and has utility .
The corrected time vector of agent keeps agent 's actual times on its own tasks and the other agents' declarations elsewhere: for and for , . For a step , rounds up to a multiple of , and .
The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations , and pays
The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.
A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.
For every , every and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),
The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.
The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.
The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.
Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every , which covers the intended choice ; the paper leaves as "a function of and ".Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.
Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: the algorithm must compute a good solution and, through payments, make it in each agent's interest to report its input honestly. Nisan and Ronen introduced the field with the problem of scheduling tasks on unrelated machines, where each machine is an agent that privately knows how long it needs for every task (Nisan–Ronen 2001).
The classical tool for truthfulness, the Vickrey–Groves–Clarke (VGC) family of mechanisms, requires the allocation to be exactly optimal. Exact optimization is often computationally out of reach: minimizing the make-span on unrelated machines is NP-hard, and even approximating it within a factor below 3/2 is NP-hard (Lenstra–Shmoys–Tardos 1990). A mechanism designer would therefore like to plug an approximation algorithm into a truthful mechanism and keep truthfulness. This mission formalizes a result showing that the simplest way of doing so fails in the model with verification, where the mechanism may pay after the tasks are performed and observes the actual execution times.
Timeline.
There are agents and tasks. The type of agent is a vector of positive reals, being the minimum time agent needs for task ; a type vector is . An allocation gives each task to one agent. The make-span is
and is optimal for if for every allocation .
In the model with verification, an agent's strategy has two parts: a declaration (any positive vector) and an execution plan that, for every allocation the mechanism may choose, fixes the actual time in which the agent performs each task it receives. An allocation algorithm maps the declarations to an allocation ; the tasks are then executed, producing actual times .
The Compensation-and-Bonus mechanism based on pays agent
a compensation for the time actually spent plus a bonus equal to minus the make-span computed from agent 's actual times on its own tasks and the other agents' declared times on theirs (the corrected time vector ). The agent's utility is its payment minus the time it spends. A strategy is dominant if it is at least as good as every alternative whatever the other agents declare and execute; the mechanism is truthful if every agent of every type has a dominant strategy that declares its true type.
Let be an allocation algorithm such that, for some real ,
and such that for some positive and some allocation . Then the Compensation-and-Bonus mechanism based on is not truthful.
The ratio is arbitrary and existentially quantified: the theorem holds for every finite approximation ratio, so it is stated without a constant.
The result. Theorem 5.1 of the same paper shows that with an optimal algorithm the Compensation-and-Bonus mechanism is a strongly truthful implementation of make-span minimization. Theorem 5.6 shows that this guarantee is tied to exact optimization: it does not survive replacing the optimizer by any non-optimal approximation algorithm, whatever its ratio. It explains why the paper then turns to a restricted problem (bounded scheduling) and a mechanism designed around a specific rounding algorithm, and it is an early instance of the general tension between approximation and incentive compatibility.
Formalizing it. The result is proved in the paper; to the best of the platform's catalog it has not been formalized. The mission produces a machine-checked model of mechanisms with verification (declarations together with execution plans that may depend on the decision), the Compensation-and-Bonus payment rule for an arbitrary allocation algorithm, and Definition 19 truthfulness, together with a checked proof of the impossibility.
The argument is short on paper; the difficulty lies in the model. The paper's "" is not a number, and a faithful statement must replace it by a finite value that is large enough to conflict with the approximation ratio yet keeps every type positive and entrywise above the true types; both requirements refer to data fixed earlier in the argument. The incentive step compares utilities in a mechanism where an agent's strategy is a declaration and an execution plan that may depend on the decision, and where the bonus mixes the agent's actual times with the other agents' declarations, so a naive reading in which only declarations matter (the direct-revelation model of §2) does not capture the claim. Finally, Corollary 5.8 concerns a type vector modified at every agent, while Claim 5.7 modifies one agent at a time, so the claim must be applicable at type vectors that are no longer the original one.
Fin n with [NeZero n], tasks Fin k, allocations are functions Fin k → Fin n, types and declarations are positive real vectors. Make-spans are Finset.sup' over the nonempty set of agents. With no agents no allocation algorithm meets the hypotheses, so requiring loses nothing.Welcome contributions: proofs of the milestones and the goal, and reusable lemmas about the corrected time vector and the monotonicity of the make-span in the time vector.
Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: an algorithm must not only compute a good solution but also pay the agents so that reporting their data truthfully is in their own interest. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001) with task scheduling on unrelated machines as the model problem. Each machine is owned by an agent who alone knows how long it takes for each task; the designer wants a schedule of small make-span.
The paper gives a truthful mechanism, MinWork, whose make-span is within a factor of optimal, and a lower bound of for every truthful mechanism. It conjectures that no truthful mechanism beats (Conjecture 4.9) and proves the conjecture for two natural classes. This mission is about one of them, additive mechanisms (Theorem 4.10, p. 180).
Timeline of the gap between and :
There are agents and tasks . The type of agent is a vector of positive reals, being the time agent needs for task ; a type vector collects all types, and denotes the types of the agents other than . An allocation is a partition of the tasks, being the set given to agent . For a set of tasks write . The make-span is
A direct mechanism maps every declared type vector to an allocation and to payments handed to the agents. An agent with true type gets utility . The mechanism is truthful if, whatever the others declare, no agent gains by declaring a type other than its true one. It is a -approximation if for every positive type vector and every allocation .
The price offered for a set to agent (Definition 12) is the payment at any declaration for which the mechanism gives agent exactly , and if there is no such declaration. For truthful mechanisms this is well defined (Proposition 4.4, Independence). The mechanism is additive (Definition 13) if
for every agent , type vector and set of tasks. MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is additive.
For agents and tasks, for every truthful additive mechanism and every real ,
The goal leaves the mechanism, its tie-breaking and completely general. It says that the ratio of MinWork is optimal among additive mechanisms.
Theorem 4.10 shows that the gap between MinWork's ratio and the general lower bound cannot be closed by any mechanism that prices tasks separately, and so any better mechanism would have to couple the prices of different tasks. It was the first class-restricted confirmation of Conjecture 4.9, which was eventually proved for all truthful mechanisms (Christodoulou–Koutsoupias–Kovács 2023). The additive case is the cleanest entry point: its proof needs only the two basic properties of truthful mechanisms, Independence and Maximization, which every later lower bound also uses.
All results here are proved on paper, and none has a machine-checked proof on Prove2Me as of this mission's drafting. The mission produces a formal model of scheduling mechanisms and prices that other lower bounds can reuse, formal statements of Independence and Maximization, and a formal proof of Theorem 4.10. Along the way the formalization corrects two points of the printed argument (see Formalization scope).
The work is to extract prices from an arbitrary truthful mechanism. Prices are defined through the attainable sets of Definition 12. A natural first idea replaces the mechanism by per-task prices that the agent maximizes against. That gives a different class, because Definition 13 constrains the price of every set of tasks, including sets the mechanism never allocates, whose price is .
Claim 4.11 is the critical step, and its printed argument does not go through for an arbitrary truthful additive mechanism. It needs the empty set to be attainable with price . For a mechanism with a bounded ratio this holds, because a very slow agent must receive nothing, but this has to be derived from the approximation hypothesis. From that, one has to show that every task of carries a single-task price of at least . The final step also needs care. The paper's "w.l.o.g. " is a further reduction, and the paper's bound has to be replaced by .
Fin n, tasks Fin k, type vectors Fin n → Fin k → ℝ, and an allocation is a map Fin k → Fin n sending each task to its agent. taskSet x i is , and the make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]). A mechanism is a pair alloc, pay of arbitrary functions; nothing about its tie-breaking is fixed.price follows Definition 12 literally: the payment at a Classical.choose witness declaration when the set is attainable, and otherwise. Additivity (IsAdditive) is required for every set of tasks, attainable or not, as Definition 13 states. It is a condition on prices, not on the payment function.The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.
The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.
Let be the complete undirected graph on . Vertex is the depot and are the customers. Vehicles have capacity and each customer has an integer demand with . An LP point is a vector ; and are the same variable, and LP solutions satisfy .
For a vertex set , is the set of edges with exactly one end-vertex in (edges to the depot included), and is its cut value. For a customer set :
The capacity inequalities and the rounded capacity inequalities (RCIs) are
The violation of such an inequality at is (resp. ); it is violated when this is positive.
Shrinking a customer set contracts it to one supervertex. The supervertices of the shrunk graph are then and the single customers outside , so a union of supervertices is a customer set with or . Shrinking is safe if for every customer set with whose inequality is violated, there is such a union with and at least the same violation.
For every and every customer set with
shrinking is safe for the capacity inequalities .
Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.
The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.
When the violated set contains or misses it, itself is a union of supervertices and there is nothing to show. The difficulty is a set that crosses : no union of supervertices is obviously as violated as , because enlarging can raise its cut value — can be smaller or larger than depending on the edges leaving — and the hypotheses on say nothing about directly. Both hypotheses on and the sign condition matter here; for signed the statement fails. A violated strictly inside is not a crossing set in the paper's sense and has to be handled as well.
On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.
Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity is real (the paper does not say it is an integer) and demands are natural numbers with for customers. The bin-packing number is the least number of bins over assignments of the customers of to bins of total demand at most ; under this minimum exists. Of the LP point only is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis " for all " ranges over nonempty proper subsets.
A formalization that lets in that hypothesis is vacuous, because ; one that drops the condition " or " from safe shrinking is trivial (take ); and one that defines as , as an arbitrary monotone function, or with a junk value , or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.
Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.
Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).
Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.
Let the rows of a set-partitioning master problem be . A column is a subset of the rows, with incidence vector ( iff ). Let be a finite collection of nonempty columns with costs . The master problem is
with integer in the integer program. Its dual has one free multiplier per row and one constraint per column.
A column is redundant, eq. (30), p. 1015, if
with and ranging over the columns of that are proper subsets of ; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair has the subcolumn property if for all with . Given dual multipliers , the ratio pricing problem (31) is
the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.
Let satisfy the subcolumn property, , and let be arbitrary. If is strictly redundant, then
that is, is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.
If only holds for in , the shifted costs satisfy the subcolumn property, and on every with ,
This is the paper's remark that the shift "adds to a constant term equal to the number of rows and does not change the problem".
Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.
The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on , no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.
The mathematical difficulty is modest; the difficulty is in the reading. With multipliers of arbitrary sign in (30), the proposition is false: on rows take , , , with costs , , , and ; then , , the subcolumn property holds, and has the unique smallest ratio. The empty column is a second trap: its denominator is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over only.
Conventions committed to in Lean:
Fin m (indexed from ); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on matter.1 ⬝ᵥ incidence a, which equals .A trivializing formalization — a redundancy witness not tied to the proper subcolumns of in , signed multipliers, or an empty column with ratio — is ruled out by the definitions above.
Needed infrastructure is only finite sums of vectors in and the identity . Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.
Many problems in statistics, signal processing and machine learning have the form
where is smooth (a least-squares loss, for instance), is a nonsmooth regularizer or constraint, and is a linear map such as a finite-difference operator. When is nonconvex — the cardinality function , the quasi-norm, the indicator of a nonconvex set — the problem is NP-hard in general, and the realistic goal is a stationary point. The alternating direction method of multipliers (ADMM) is widely used on such problems because each iteration splits into a proximal step on and a smooth step on , but for nonconvex it was long used without a convergence theory.
Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave one of the first general analyses. Their Theorem 1 shows that, under explicit conditions on the penalty parameter and a proximal term, every cluster point of a proximal ADMM sequence is stationary, and that a suitable start is strictly improved on. Earlier, Ames and Hong (arXiv:1401.5492) proved convergence of the plain ADMM for one specific nonconvex quadratic problem with an and norm-ball term; Li–Pong's argument follows their idea of bounding the dual changes by the primal changes, together with a descent analysis of the augmented Lagrangian from Wen, Peng, Liu, Bai and Sun (Optimization Online 2013/01/3730).
Let be twice continuously differentiable with bounded Hessian , let be proper (finite somewhere, never ) and closed (lower semicontinuous), and let be linear with adjoint .
A vector is a regular subgradient of at (with finite) if . The limiting subdifferential collects all limits of regular subgradients at points with . A point is stationary if
For the augmented Lagrangian is , and for a convex function the Bregman distance is . The proximal ADMM generates, from arbitrary ,
Assumption 1 requires for some (so is surjective), Loewner bounds , with , , a strong-convexity margin , and some with . Here .
Under the standing assumptions and Assumption 1, for every proximal ADMM sequence:
and is stationary; 2. (Strict improvement) if is not stationary, and , then every cluster point satisfies
The theorem does not assert that a cluster point exists; that is the subject of Theorem 2 of the same paper.
In attack order: the robustness (3) of ; the optimality relations (11) of each iterate; the passage from (9) and (10) to (12) and stationarity; the dual-step bound (14); the one-step estimate (20) and its summed form (21) for ; the vanishing of the primal steps (16); the convergence (10) of ; and, for part (ii), , the first-step estimate (27) and the strict decrease after (28).
Theorem 1 turns the proximal ADMM into a method with a guarantee for a nonconvex : any limit it produces is a stationary point, and with the initialization of part (ii) — for example, a stationary point of a convex relaxation — it cannot return to a stationary point worse than its start. The conditions are checkable: Remark 1 of the paper shows that the choice turns the -update into a convex quadratic program, and that the last condition of Assumption 1 can be enforced by taking large when , , do not depend on . The estimate (20) is reused by the paper's boundedness result (Theorem 2), and its whole-sequence convergence result for semi-algebraic data (Theorem 3) starts from Theorem 1.
The result is proved in the paper; Mathlib contains neither the limiting subdifferential nor any convergence theorem for ADMM, so none of it is formalized yet. A formalization would give a verified library of the limiting subdifferential of extended-real-valued functions, its robustness and its Fermat rule with a smooth sum, and the first formally verified convergence theorem for ADMM with a nonconvex term.
The obvious argument — "the augmented Lagrangian decreases, so it converges" — fails: need not decrease, because the multiplier step increases it by . The proof has to bound this increase by primal steps, which uses surjectivity of and the squared Hessian bounds, and it produces a two-step recursion (involving ) rather than a monotone sequence. Nor is known to be bounded below; the proof uses the cluster point and lower semicontinuity to get a lower bound along a subsequence. Passing to the limit in the inclusion for requires , which lower semicontinuity alone does not give. For part (ii), the start is not an iterate at all, so the first step needs its own estimate.
Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); is a continuous linear map and is ContinuousLinearMap.adjoint. and take values in EReal; inequalities involving are written additively ( with real ), never through EReal.toReal. The Hessian is the derivative of the gradient. is Mathlib's Loewner order on self-maps, which includes symmetry of the difference; adds positive definiteness. for every , possibly indefinite. The witnesses of Assumption 1 are explicit parameters, universally quantified. A proximal ADMM sequence is any triple of sequences satisfying the three updates (global minimizers, not necessarily unique); are free and is unconstrained. A cluster point is the limit along a strictly increasing subsequence. Stationarity is the inclusion (4) itself.
The limiting subdifferential keeps all three requirements of its definition — , and — and the domain condition ; dropping -attentive convergence or replacing by the convex subdifferential would make stationarity a different, and for nonconvex wrong, notion. Part (ii) is a strict inequality for every cluster point, and its hypotheses are exactly non-stationarity of , finiteness of the objective at and . The paper's assumption that proximal maps of exist is not a hypothesis, since no statement asserts that the iteration can be run.
Needed infrastructure: Fermat's rule and the smooth sum rule for regular subgradients, a diagonal argument for (3), Taylor bounds for functions with Loewner-bounded Hessians (the paper's (5) and (6)), strong convexity from a Hessian lower bound, and the monotonicity of the positive square root in the Loewner order. These are reusable well beyond this mission; contributions of any of them as separate lemmas are welcome.
Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.
For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from to . For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual , the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most .
Let be a real Hilbert space with inner product . A set-valued operator assigns a subset to every point . It is monotone if whenever and , and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of . The class of maximally monotone operators is , and is the set of zeros.
For a step size , the resolvent maps to the unique with . It is single-valued for monotone and defined on all of for maximally monotone .
The general proximal point method with step coefficients starts at and iterates
Kim's proposed accelerated proximal point method starts at and iterates
The coefficients (25) are for and .
The PEP of Section 3 bounds the worst case of over all and all starts with . A semidefinite relaxation leads to the dual problem (D): minimize over nonnegative such that . The matrices are explicit symmetric matrices built from and the canonical basis . Its optimal value is .
For every , every , every run of the proposed method, and every with for a constant ,
The constant is the paper's, and nothing is left unfixed.
Theorem 4.1 gives the first rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).
The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.
The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an matrix whose entries are double sums over , uniformly in . The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in . The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at .
is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.
The resolvent step is relational: is encoded as . For monotone and this determines uniquely, and for maximally monotone such an exists for every (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's is y (0 - 1) = y 0 under natural-number subtraction. The general method has no , so its initial-distance condition is on , as in (17). The step size is written lam.
PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i . is the infimum of the feasible values of computed in EReal, so an infeasible gets the value as in the paper; Eq. (28) compares it with the real bounds cast to EReal.
A formalization in which the iterate predicate cannot be satisfied, the residual is , the correction term is dropped or has the wrong sign, the initial point is decoupled (), or is only monotone on finitely many points, would state a different theorem, and none is used here.
Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.
A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).
Timeline:
Fix a context-switch cost . A lock wait is described by its release time . An algorithm handling the wait chooses a blocking time : it spins until time and then blocks (: never block). The cost of the wait is
so a lock released exactly at the blocking time costs . The optimal off-line algorithm, which knows , pays .
An input is a finite sequence of lock waits. A deterministic on-line algorithm chooses the blocking time of wait as a function of , the release times it has already observed. Its cost is the sum of the wait costs, and the off-line cost is .
A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space and a deterministic algorithm for each , with measurable for every . Its expected cost is . Following §1 of the paper, is -competitive against an oblivious adversary if there is a constant with
The adversary is oblivious: it fixes before the algorithm's random choices are made.
The paper's algorithm blocks at a random time with cumulative distribution
where is the probability of blocking before time .
For every :
Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.
The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.
The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant : a single hard lock wait proves nothing, because absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.
All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:
Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step .