Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Nesterov's accelerated gradient method minimizes a smooth convex function at the rate in the number of iterations , against for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation
with , a heavy-ball system whose friction coefficient vanishes as (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.
Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general . This mission formalizes their result for strongly convex , where the rate of convergence of (1) depends on and improves without bound as grows.
Timeline.
Let be a real Hilbert space with inner product and norm , and let be continuously differentiable with gradient . Fix and . A solution of (1) is a twice differentiable trajectory with velocity satisfying (1) at every .
is strongly convex with constant if
Such a has exactly one minimizer , and .
For , the anchored energy is
a sum of nonnegative terms. The proof of the main theorem fixes
For strongly convex and , every solution of (1) converges strongly to the unique minimizer , and
as . The goal states the asymptotic form; the explicit constants are milestones.
The theorem shows that the rate of (1) on strongly convex functions is not capped at or : the exponent grows linearly in , and it already exceeds for every . It extends [44, Theorem 4.2], which needs and gives . The same parametrized energy is the template for the discrete analyses of Nesterov-type algorithms with parameter , so its derivative identity (10) is reusable beyond this mission.
The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.
The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at , real powers , and the chain rule for in an infinite-dimensional space. The obvious argument, that is nonincreasing, fails: even with the best choice of and the bound on its derivative keeps a term of no fixed sign, and only for is the quadratic term in nonpositive. Passing from the differential inequality to (26) therefore needs integration on for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.
InnerProductSpace ℝ H, CompleteSpace H), not . is ContDiff ℝ 1 and is Mathlib's gradient.Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. with , and solves (1)).Useful infrastructure: the derivative of via gradient, integration of differential inequalities on , and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, are welcome.
In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is -cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.
The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale with given marginals , . Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.
M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for -cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs with strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.
All measures live on or with their Borel -algebras. Two probability measures on with finite first moment are in convex order, , if for every convex .
A transport plan is a measure on with first marginal and second marginal . It is a martingale transport plan, , if under the conditional mean of given equals ; equivalently,
A cost is a Borel function satisfying the sufficient integrability condition with , ; then the cost of a plan, , is well defined in . A plan is optimal if for every , and it leads to finite costs if .
A measure on is a competitor of (Definition 1.10) if it has the same two marginals as and the same conditional barycentres: for almost every , where , are disintegrations with respect to the first marginal. A competitor redistributes the mass of in a way that a martingale plan could absorb: replacing a piece of a martingale plan by keeps both marginals and the martingale property.
Let be probability measures, a Borel cost satisfying the sufficient integrability condition, and optimal with . Then there is a Borel set with such that
The set is chosen once, before ; the quantifier order is the content.
The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:
The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs with strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound of Theorem 7.1 and the two-graph structure of the optimizers for . Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in . Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.
The classical proof of -cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every , and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor of a piece , is the technical core.
The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral (, with ); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written with a finite set and weights ; this covers every such measure, and masses are taken finite. is Fin n → ℝ × ℝ.
Committed conventions and disclosed additions:
A formalization in which is empty or -null, or in which is allowed to depend on , is trivial and is ruled out by the statement: and . The competitor ranges over all measures, not only finitely supported ones.
Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.
Proximal gradient methods are used to minimize an objective with one smooth part and one convex part whose proximal map can be evaluated. A small proximal gradient step is a practical stopping signal, but it indicates proximity to an optimizer only when the objective has an appropriate error bound. Section 4 of Drusvyatskiy and Lewis gives conditions for that bound in the structured problem : the conditions concern the dual problem and the growth of the two component functions, rather than requiring strong convexity of their sum. This matters for problems with a nontrivial solution set and for penalties that are not strongly convex. The paper places this result after its §3 comparison of quadratic growth and proximal gradient error bounds (pp. 9–11).
Let and , with their Euclidean inner products and norms. Let be linear, be continuously differentiable and convex, and be proper, lower semicontinuous, and convex. The primal objective and its minimizer set are
The mission assumes is nonempty and bounded. Its minimum is finite. For an extended-real function , its Fenchel conjugate is . The dual objective is , and denotes a dual minimizer. The effective domain is ; denotes relative interior. The paper assumes dual nondegeneracy, , and dual strict complementarity, (p. 10).
A closed convex function is firmly convex relative to when its tilt grows at least quadratically away from its minimizers on each compact set. The positive coefficient may depend on the compact set. Theorem 4.2 assumes this property for at and for at (Definition 4.1, p. 11).
For , a proximal gradient step is , and its residual is . The error bound asks whether the distance from to is controlled by whenever lies below a prescribed objective threshold (Definition 3.1, p. 5).
The milestone path records the Kuhn–Tucker description of , the relative-interior identity (4.3), the compact-set distance estimate (4.4), the two component inequalities (4.5), and the resulting quadratic growth of on every sublevel set. In particular, for each there is such that
These are the claims stated in §4 and in the proof of Theorem 4.2, pp. 10–11. The milestone for (4.5) retains the paper's printed in its quotation, while the Lean statement uses positive constants, as Definition 4.1 requires for nontrivial quadratic growth.
The goal is Theorem 4.2: under the conditions above, for every there exist such that
The formal statement makes explicit that has a Lipschitz constant. This is part of the §3 setting used by the paper's Corollary 3.6 to reach the displayed error bound. A companion statement, Theorem 4.5, pp. 12–13, says that the Moreau envelope of a firmly convex function retains firm convexity relative to the same vector.
The conclusion converts dual geometric information and component growth into an error bound expressed through a proximal gradient step. The residual is available when running the method, whereas the distance to is generally not. Combined with the paper's §3 results, the error bound yields local convergence guarantees for the proximal gradient method in structured convex problems (Corollary 3.6 and Theorem 4.2). The statement covers settings in which component functions have local quadratic growth after a tilt while the composite objective need not be strongly convex.
The research result is proved in the paper. The work of this mission is to formalize its exact assumptions and claims, including the convex dual and the relative-interior statements, then supply machine-checked proofs. The resulting Euclidean conjugate, firm-convexity, and structured-objective definitions can also support other convex optimization formalizations. The statements in this proposal are proof obligations; compiling the statements alone does not establish the theorems.
Component growth concerns distance to separate subdifferential inverse images. The desired error bound concerns distance to their intersection, which is the primal solution set. Two small component distances do not automatically control distance to an intersection: the sets can meet at a poor angle. The dual interior hypotheses supply the regularity needed in (4.4). The argument also changes the quantity being controlled from objective growth to a proximal gradient residual. Those two changes are the substantive steps a proof must justify; treating either as an unrestricted distance identity would change the theorem.
The Lean spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); dimensions zero are permitted. The linear map is continuous, and is its adjoint. Extended-real values use EReal; properness excludes values, and lower semicontinuity encodes closedness. Conjugates take suprema in EReal, and the dual objective follows (4.2). Relative interior is intrinsicInterior ℝ. The published convex subdifferential, proper-convex predicate, and proximal-point predicate are imported as reference items because their meanings match the paper's objects. The paper's Euclidean conjugate is defined locally because the available published conjugate has a strong-dual codomain.
The minimum value is real and is pinned to the nonempty primal minimizer set. The dual point is pinned as a minimizer of . Proximal steps are expressed as argmin predicates, so no default result is chosen for a failed minimization. The firm-convexity predicate requires a nonempty minimizer set of the tilted function: otherwise Lean's real distance to the empty set would be zero while the source uses an infinite distance. The growth constant of Definition 4.1 and the constants of (4.5) are strictly positive: the page leaves the sign implicit or prints , but with a zero constant every convex function would be firmly convex, contradicting the page's own example , and the growth statements would be empty. The error bound is restricted to the stated sublevel set, and all of its constants are positive. The goal includes a nonnegative Lipschitz constant for , disclosed because the source's §3 bridge to the error bound assumes one; the component-growth milestones do not assume it.
Contributions should establish the Euclidean convex-duality identities, the compact-set regularity estimate, the component and composite growth claims, and the proximal gradient conclusion. The Moreau-envelope preservation theorem is a separate companion target. None of the dual interior conditions or the firm-convexity assumptions may be replaced by a vacuous condition: the goal concerns their effect on the actual solution set of .
In many retail and spare-parts settings, demand that cannot be met from stock is lost rather than backlogged, and replenishment orders arrive only after a positive lead time. The resulting lost-sales inventory model is a basic model of inventory theory. Its optimal policy depends on the whole pipeline of outstanding orders, so dynamic programming over that state becomes intractable as the lead time grows. This is why the model is often replaced by its backlogged counterpart, even when that approximation is poor (Bijvank and Vis, 2011).
Simple heuristics are therefore of practical interest. The simplest is the constant-order policy, which orders the same amount in every period regardless of the state. Reiman (2004, unpublished manuscript) showed that the best constant-order policy sometimes outperforms the base-stock policy, and Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante (arXiv:1211.4063, Math. Oper. Res. 2016) proved that it is asymptotically optimal as the lead time grows, with a gap that decays polynomially in the lead time. Xin and Goldberg (arXiv:1409.1499v2, Oper. Res. 2016) proved that for the infinite-horizon average-cost problem the gap actually decays exponentially, with an explicit rate and explicit constants. This mission formalizes that result.
Timeline:
Demands are i.i.d. copies of a nonnegative random variable with law , finite mean and strictly positive variance. The lead time is an integer, is the unit holding cost and the unit lost-sales penalty. At the start of period there is on-hand inventory and a pipeline of orders placed but not yet delivered. In each period, arrives, a new order is placed (it enters the end of the pipeline), demand is realized, and the period cost
is incurred; then . The system starts empty. A policy chooses orders from the information available, and its long-run average cost is . The optimal cost is .
The constant-order policy orders in every period. Its cost is governed by the random walk through
the steady-state and -th waiting times of a single-server queue with interarrival law and constant service time . The best constant order is the least minimizer of over . The rate and constants are
with the largest minimizer in the definition of ( if the infimum is not attained, and ).
The quantities depend on but not on .
The theorem shows that a lead time of order suffices for the constant-order policy to be within a factor of optimal, whereas the earlier bounds of Goldberg et al. needed a lead time polynomial in . The constants are explicit and computable from the demand law: for exponential demand with and the bound is already about , and it approaches quickly as grows (Table 1 of the paper). Lemma 1 adds that the rate worsens as grows, the regime opposite to the one in which base-stock policies are known to be nearly optimal.
The result is proved on paper; no machine-checked proof is known to exist. A formalization would produce a checked infinite-horizon lost-sales model and a checked statement of Kingman's random-walk identities for this queue. It would also produce checked comparisons of an arbitrary history-dependent policy with constant-order policies through convexity. The statement here is taken over a policy class at least as large as the paper's, so a proof also extends the result to randomized history-dependent policies.
The cost of the constant-order policy is the expected supremum of a random walk, while the optimal policy has no closed form and may not even induce a stationary distribution. The paper avoids the steady state of the optimal policy by constructing a random vector with the needed stationarity properties (Theorem 2). That construction is not part of this mission. Here, the lower bound on in Lemma 2 instead goes through the published, proved lower certificate for the full policy class. The second obstacle is quantitative: the exponential rate comes from comparing the minimizers and of two different convex functions (Lemma 4) and from a first-order optimality condition involving a non-differentiable expectation (Lemma 5). Neither follows from the observation that one function dominates the other.
The model is the published CappedBaseStock model: zero-based time, an empty initial state, demand laws on with finite positive mean, and costs and long-run averages in . is the infimum over all measurable, history-dependent, possibly randomized policies. That class contains the paper's Markov deterministic class , so every statement involving is at least as strong as printed. "Strictly positive variance" is encoded as "the demand law is not a point mass". It is a hypothesis wherever the paper's argument needs it; the Chernoff step, eq. (3) and Corollary 1 do not need it.
is the model's long-run cost of the constant policy, not formula (3), and is a lower integral in , so that eq. (3) and Lemma 3 are not true by definition. and are infima of the argmin sets, whose nonemptiness is a milestone. is encoded with the paper's convention . Lemma 3's tail bound is stated additively in , and the series in Lemmas 3 and 5 are extended-real series indexed from . The goal's ratio is taken in , where for . None of , or is assumed: all three are milestones. A formalization that defines over constant-order policies only, fixes instead of , treats as free parameters, or takes the ratio in after truncating infinite costs would make the goal trivial and is ruled out. The objects are defined from the full parameter record, which includes . That they do not depend on follows from eq. (3) and the existence milestone.
No statement corrects a printed slip. Theorem 2 (existence of the stationary vector) and eq. (2) (bounded stationary optimal policies) are not stated; Observation 1 instead takes Theorem 2's properties (i)–(iii) as hypotheses on an arbitrary law. The source is arXiv:1409.1499v2, whose printed page numbers equal the PDF's. Useful infrastructure: Lindley-type random-walk suprema, Spitzer–Kingman identities, Chernoff bounds for i.i.d. sums (Mathlib's measure_le_le_exp_mul_mgf), and Cesàro limits of expected costs. All of it is reusable for other queueing and inventory missions. Proofs of any milestone are welcome, and the Chernoff step is the natural entry point.
Fractional programs minimize a ratio over a constraint set. They arise whenever a quantity has to be normalized: the scale-invariant sparse recovery model minimizes (Rahimi, Wang, Dong, Lou 2019), robust Sharpe-ratio portfolio selection maximizes a mean-to-worst-case-risk ratio, and generalized eigenvalue problems minimize Rayleigh quotients. Classical methods such as Dinkelbach's algorithm assume convex and concave ; many modern instances have neither.
Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) study the nonconvex nonsmooth case in which the numerator is a smooth convex part plus a lower semicontinuous part and the denominator is weakly convex on the constraint set. Their basic method, the extrapolated proximal subgradient (e-PSG) algorithm, converges subsequentially to lifted stationary points. When the denominator is a maximum of finitely many smooth functions, a lifted stationary point may be spurious: it only requires one element of the subdifferential of to balance the numerator. Section 6 of the paper proposes an enhanced algorithm, in the spirit of the enhanced DC algorithm of Pang, Razaviyayn, Alvarado 2017, whose cluster points satisfy the stronger condition for all such elements. This mission formalizes that result.
is a finite-dimensional real Hilbert space, is nonempty, closed and convex, and the problem is
Algorithm 2 starts from . At step it sets , picks a step size and extrapolation weights , , and forms and . For every it computes a proximal candidate
(up to constants), and keeps as the candidate minimizing the merit value .
Assume the sublevel set is bounded and . Then every cluster point of satisfies , ,
and, if is weakly convex on , is a strong lifted stationary point of (P).
For max-type denominators the result separates the enhanced algorithm from the basic one. A lifted stationary point only needs . The paper's Example 3.3 () has the lifted stationary point , which is not a local minimizer; the strong lifted stationary points of that example are exactly its minimizers. Lemma 3.4 of the paper identifies strong lifted stationarity with d-stationarity of on when and are weakly convex. This is the sharpest first-order notion used for DC-type programs.
The theorem is proved in the paper (pp. 22–24). No machine-checked version of it, of the e-PSG analysis, or of lifted stationarity exists on the platform. Formalizing it checks the step-size bookkeeping that the printed algorithm gets wrong (see below). It also produces reusable statements about weakly convex functions and the limiting subdifferential of .
The descent part follows the template of the basic e-PSG analysis, but the merit criterion couples the candidate selection with the extrapolation: the coefficient has to stay positive, and the cross term has to be split with the specific weight for the constants of (27) to close.
The limit step is the main obstacle. The algorithm works with , but the conclusion concerns at a limit point. One must show that every index active at was a candidate along the subsequence. One must also show that although is only lower semicontinuous. The naive approach, passing to the limit in the optimality condition of a single subproblem, gives one element of only, which is lifted stationarity again. The final step needs the limiting subdifferential of a finite max of functions to be the convex hull of the active gradients. The paper uses this fact without proof, and Mathlib does not provide it for .
EuclideanSpace ℝ (Fin N). Functions into are EReal-valued. is the published NonconvexSplitting.Shared.LimitingSubdiff, and properness is IsProperFn.Fin p with , so they run . is defined as Finset.sup' of the , never as an independent function. The standing assumptions of (P) are kept: is lower semicontinuous and positive on .ConvexOn of on . For extended-real it is convexity of the epigraph of .Filter.liminf τ atTop, which is well defined because . The -range is multiplied out to avoid dividing by .toReal value of never enters.A cap in an affine or projective space over a finite field is a set of points no three of which are collinear; a cap is complete when it is maximal with respect to inclusion, so that every point outside it lies on a line through two of its points. Caps are closely connected with error-correcting codes: projective caps can serve as parity-check columns for linear codes with minimum distance at least 4. Constructing small complete caps explicitly is a long-standing question in finite geometry; Giulietti's survey collects the known families.
Counting the lines through pairs of points gives the trivial lower bound
for the size of a complete cap in a Galois space of dimension and order . A short timeline:
Let and let be the field with elements. The affine space has as points the vectors ; three points are collinear when they lie on a common affine line over .
For an additive subgroup of , is the set of points whose coordinate vectors lie in . A translation cap is a cap of the form . By Giulietti, Proposition 2.5, for a translation cap has at most points; one attaining this bound is a maximal translation cap.
On the projective side, let , so that . An -subspace of (an additive subgroup) of -dimension , the rank, defines the -linear set . It is scattered when every point meets in exactly , i.e. has weight one. A scattered linear set has rank at most (Blokhuis–Lavrauw); one of rank in the plane is called maximum.
For , even, and even, there is a complete cap in with
The exponent is an integer because is even.
Theorem 1.3 shows that the trivial bound (1) is sharp up to the factor in even dimension for every even square , extending to even dimension what the constructions of Segre and Pambianco–Storme give in odd dimension. The construction supplies caps near the elementary size lower bound in a parameter range where the paper reports no comparably small infinite family. Remark 4.8 of the paper extends the construction to complete caps of comparable size in . The proof also establishes Proposition 4.3, a dictionary between scattered -linear sets and translation caps, so that any new maximum scattered linear set yields new small complete caps.
The result is proved on paper; no machine-checked proof of it or of the cited results of [6] (Lemmas 4.5, 4.6 and the bound of Prop. 2.5, whose proofs are not in this paper) is known to exist. The mission produces a formal statement of Theorem 1.3, the cap–linear set correspondence, and formal statements of the three results the paper imports from [6].
Assembling Proposition 4.7 from the milestones is short. The difficulty lies in the inputs. The doubling construction requires showing that every point of outside lies on a secant, which uses the maximality in a counting argument; it is cited from [6], not proved in the paper. The existence of a maximum scattered linear set in is the deep input: Lemma 2.8 needs a bound on the value set of a non-permutation polynomial (Turnwald) and a point count on a plane curve over . A tempting shortcut, taking any maximal cap obtained by greedy extension, gives a complete cap of unknown and generally much larger size; the content of the theorem is the exact size.
Fin r → K for a finite field with ; collinearity is Mathlib's affine Collinear K, over itself. A complete cap is quantified against every point of .Set.ncard. The goal's size is written with natural-number division, exact because is even; maximality of a translation cap is the squared form , and the [6] bound is .Welcome contributions: a general library of caps and translation caps in ; the scattered-linear-set/translation-cap dictionary; a formalization of the doubling construction of [6]; transport of the -model of Theorem 2.10 to coordinates . The linear-set definitions mirror those of the companion mission on scattered linear sets and are reusable there.
Distributionally robust optimization (DRO) replaces the expected loss of a linear decision rule by its worst case over all data laws within transport distance of the baseline . When is an empirical distribution this covers regularized regression and classification (Blanchet, Kang, Murthy 2019; Esfahani, Kuhn 2018). The optimal value is one number; a practitioner also wants to know which distribution realizes it, the adversary's best response. It shows which data points the robust model guards against, it gives stress-test scenarios, and its structure is what the paper's comparative statics (Theorem 7) and iterative schemes build on.
J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes (arXiv:1810.02403v3; Math. Oper. Res. 47(2), 2022), answer this for a state-dependent Mahalanobis cost. Theorem 6 of that paper describes the worst-case distribution through the solution of the one-dimensional dual problem. This mission formalizes Theorem 6.
The data take values in with law , a Borel probability measure. The decision ranges over a convex set (a standing assumption of the paper). Moving mass from to costs
where is positive definite. Assumption 1 asks that be lower semicontinuous and that for -almost every , with . The optimal transport cost is the least value of over couplings of and . For the worst-case objective is
Assumption 2 asks that the loss be convex, that the growth exponent be finite, and that .
The dual side is built from
the robust loss , the dual objective and the maximizer set . By the paper's Theorem 1, (6) equals , and a minimizer , the dual optimizer, exists. The threshold is ; below it .
Let and . Let be measurable selections with the largest and smallest square, , , and let be independent of with . Then
and the law of attains the supremum in (6).
Theorem 6(a): unless is constant. Theorem 6(b): . Theorem 6(d), as the paper's example: for , , and , and no distribution attains the value . Theorem 6(e), with Lemma 8: if and , then is a singleton almost surely and the law of is the unique worst case.
The result reduces a search over all probability measures to a scalar problem per data point. Each point is pushed along the single direction , by an amount read off the maximizers of , and the budget is always spent completely. When the maximizer is not unique, randomization between two extreme maximizers is needed and suffices. Part (d) shows that the threshold condition cannot be removed, and part (e) gives a deterministic transport map (a Monge solution) under smoothness. Theorem 7 of the paper, the monotone growth of worst-case displacements in , is a statement about the random variable produced here.
None of these statements has been machine-checked before. The general strong duality with complementary slackness of Blanchet–Murthy (arXiv:1604.01446) is proved on the platform, so this mission connects that abstract theorem to an explicit worst-case law. A formal proof also has to settle one point the printed text leaves loose: which extreme maximizers enter the mixture (see Formalization scope).
The first idea is to take the pointwise maximizers of at and push forward. That works only when the maximizer is unique and the budget constraint happens to be tight. In general the maximizer set is not a singleton, and the derivative of at only lies between a left and a right derivative. Turning the first-order condition into an exact cost needs three things. The one-sided derivatives must be identified as expectations over , an envelope theorem under an integral with a non-compact parameter set. The extreme maximizers must be compact and measurably selectable. Finally the resulting coupling must be certified optimal through complementary slackness. Each step needs a hypothesis that is easy to lose: the growth control of Lemma 3, the essential supremum in , measurability of selections.
Points of are EuclideanSpace ℝ (Fin d), is the inner product, and is quadInv A β x. and are extended-real valued; uses the published extended integral ModelRiskOT.Duality.extIntegral. The worst-case objective (6) is the published primal problem primalValue: a supremum over couplings with first marginal and (primalFeasible). A distribution attains (6) when a coupling with that second marginal has value primalValue. The random worst case is encoded by the joint law of , a mixture of two graph couplings, because depends on the pair. A dual optimizer is a real minimizing on .
Standing hypotheses on every statement: a probability measure, Assumptions 1 and 2, , convex. The following departures from the printed text are disclosed in each item:
Every expectation used in the goal (, ) carries an integrability conjunct. The cost identity and optimality are asserted for the measure itself, so no junk value of a non-integrable integral can make the goal hold vacuously. A statement asserting only first-order conditions for would not be Theorem 6. The goal asserts primal attainment and the exact cost.
Needed infrastructure, reusable beyond this mission: envelope (Danskin) theorems for one-sided derivatives of suprema, differentiation of convex integral functionals, measurable selection of argmax sets, and complementary slackness through the published Blanchet–Murthy theorem. Contributions of any of these as standalone lemmas are welcome.
Deciding whether a planar graph is 3-colorable is NP-complete, so a large part of the theory of planar graph coloring looks for simple local conditions that guarantee 3-colorability. Grötzsch's theorem (1959) is the model result: every triangle-free planar graph is 3-colorable. Forbidding triangles is not the only possibility, and in 1976 Richard Steinberg asked whether forbidding cycles of two other lengths suffices.
Steinberg's Conjecture (1976). Every planar graph with no cycles of length four or five is 3-colorable.
The conjecture drove four decades of work on planar coloring. It was surveyed by Borodin as one of the central problems of the area (Borodin 2013, §7), and it was one of the six graph theory problems ranked with the highest importance in the Open Problem Garden.
Timeline:
All graphs are finite and simple. A cycle of length in a graph is a sequence of pairwise distinct vertices with an edge for each (indices mod ). has no cycles of length four or five if no cycle of has length or ; triangles and cycles of length at least six are allowed. A 3-coloring of assigns one of three colors to each vertex so that adjacent vertices get different colors, and is 3-colorable if it has one. The distance is the number of edges of a shortest – path. is planar if it can be drawn in the plane without crossing edges.
The paper builds its counterexample in three steps, from three concrete graphs given as drawings.
In the Lean development these are the definitions G1, G2 and G. The hypothesis "no cycles of length four or five" is the definition NoFourFiveCycle.
This is the paper's main theorem and exactly the negation of Steinberg's Conjecture. It leaves the witness free, so any counterexample proves it.
Milestones 3–5 together give the goal, with as the witness.
The result. Theorem 3 settles a 40-year-old problem negatively. It shows that forbidding 4- and 5-cycles is not a local condition that forces 3-colorability, which redirects the Erdős relaxation: the threshold for "no cycles of lengths " lies in , since is known and is now excluded. The paper notes that the same graph also disproves the Strong Bordeaux Conjecture and the Novosibirsk 3-Color Conjecture.
Formalizing it. The theorem is proved, and the proof is short. As far as is known it has no machine-checked version. Every claim in the proof is a finite statement about explicit graphs, so the work here is to verify the three gadgets and the gluing arguments in Lean, including planarity of an explicit 166-vertex graph, which is asserted in the paper only through its figures. Planarity, cycle structure and coloring of a concrete graph of this size are a useful benchmark for computational verification in Lean.
The obvious approach is brute force: is a fixed finite graph, so in principle each claim can be decided. In practice decide is not workable at this size. Excluding 4- and 5-cycles means quantifying over walks of a 166-vertex graph. Non-3-colorability is a search over assignments unless it is reduced, as the paper does, through the gadget lemmas. The planarity witness needs explicit coordinates for 166 points and a check of all pairs of segments, in exact arithmetic. The gluing arguments ("a cycle through two copies has length at least six") are where the paper's distance claims are used. Turning those claims into statements about Mathlib walks on unions of embedded copies is the conceptual work.
Lean representation and conventions:
SimpleGraphs. G1 lives on Fin 15, with . G2 lives on Fin 42, with , and G lives on Fin 166, with .G2 is literally (⨆ k, G1.map (copy2 k)) ⊔ the triangle , with explicit embeddings copy2 k : Fin 15 ↪ Fin 42. G is (⨆ k, G2.map (copyG k)) ⊔ the twelve extra edges, with copyG k : Fin 42 ↪ Fin 166. The contact tables are in each definition's statement. A local check confirms the edge counts 23, 72 and 300, and that G agrees edge for edge with an independent transcription of Figure 3.p : H.Walk v v with p.IsCycle, and their length is p.length.H.Coloring (Fin 3), and 3-colorability is H.Colorable 3. "No 3-coloring gives one color" is ∀ C, ¬ (C a = C b ∧ C b = C c). Colorings in which two of the three share a color are still allowed, as in the paper.SimpleGraph.dist. Its junk value for unreachable pairs is never hit, because every asserted distance is positive.OPG37357.IsPlanar: an injective placement of the vertices in in which no vertex lies inside an edge segment and edges with four distinct endpoints have disjoint segments. For finite simple graphs it is equivalent to planarity by Fáry's theorem, and it implies topological planarity.Fin n. This loses no generality for finite graphs, and the empty graph cannot serve as a trivial witness because it is 3-colorable.The following trivializing formalizations are ruled out. Closed walks, instead of cycles, would exclude every graph with an edge. Girth is not used: contains triangles. Lemmas 1 and 2 do not assert that and get different colors, which would be false for . An infinite or unspecified vertex type is not allowed for the witness.
Welcome contributions: decision procedures or certificates for short cycles and colorings of explicit finite graphs; a straight-line embedding of with rational coordinates; lemmas on cycles and distances in graphs glued from embedded copies, which are reusable for other gadget constructions; and proofs of Lemmas 1–2 by computation or by the paper's arguments.
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At step it keeps an exponential moving average of stochastic gradients and an exponential moving average of their squared coordinates, corrects both for their initialization at zero (the bias correction or debiasing step), and moves the iterate by coordinatewise. Despite its use, its convergence on nonconvex objectives was poorly understood when Barakat and Bianchi wrote their paper: Reddi, Kale and Kumar (2018) exhibited convex online problems on which constant-parameter Adam fails to converge, and earlier analyses either dropped the bias correction or replaced Adam by a modified algorithm.
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size with and , the interpolated iterates follow a non-autonomous ordinary differential equation, the continuous-time version of Adam. This mission formalizes their convergence theorem for that ODE (Theorem 3.2): trajectories started as Adam is started, with zero moment estimates, approach the critical points of the objective.
Let be continuously differentiable with locally Lipschitz gradient , and let be locally Lipschitz. In the paper is the objective and the coordinatewise second moment of the stochastic gradient; §7 only uses the two properties above. Assume is coercive ( as ) and coordinatewise for every . Fix constants with .
The state is , and is the part where . All vector operations are coordinatewise. The Adam field (3.3) is, for ,
and (ODE) is . The factors and are the continuous-time bias corrections; they blow up as . A global solution with initial condition is a continuous , continuously differentiable on , satisfying (ODE) for every , with . The critical set is .
The proof passes through the autonomous field , its semiflow on , and the notions of equilibrium point, strict Lyapunov function and asymptotic pseudotrajectory (APT) of a semiflow.
Assume in addition that has empty interior in . For every global solution with initial condition , the set is non-empty and
The theorem does not claim that converges; convergence to a single critical point needs a Łojasiewicz condition (Theorem 3.4, a separate mission).
The milestones are the numbered results of §7.1–7.3 used in the proof, in the order the proof uses them: positivity of along solutions (Lemma 7.4); decrease of along (Lemma 7.5, autonomous part); compactness of trajectories (Propositions 7.6, 7.7) and lower bounds on (Lemma 7.8); well-posedness of the autonomous system and its semiflow (Proposition 7.13); the abstract limit-set theorem for APTs (Proposition 7.14, quoted from Benaïm); the strict Lyapunov function (Proposition 7.15); and the APT property of the (ODE) solution (Proposition 7.17).
Theorem 3.2 is the deterministic core of the paper's analysis of Adam. Combined with the paper's tracking result (constant-step Adam converges in probability to the ODE solution as , Theorem 4.3) it says that for small steps Adam's iterates spend their time near critical points of ; it is also the input of the decreasing-step almost-sure convergence theorem (Theorem 5.2) and of the convergence-rate theorem (Theorem 3.4), which both rely on the same Lyapunov function and limit-set argument. The condition under which the Lyapunov function decreases is satisfied by the default parameters , .
The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission produces a formal proof of the theorem, and reusable formal statements about semiflows on metric spaces: strict Lyapunov functions, and the limit set of a relatively compact asymptotic pseudotrajectory.
The obvious route is to show that decreases and apply LaSalle's invariance principle. This fails on two counts. First, (ODE) is non-autonomous, and LaSalle's principle is a statement about autonomous systems: the derivative of along the flow vanishes only on a set that depends on . Second, the field is singular: blows up at and is not Lipschitz near , because of , so neither existence and uniqueness nor continuous dependence on initial data come from standard theorems. The energy of the autonomous limit is a Lyapunov function but not a strict one: it is constant along some non-equilibrium orbits, so non-increase of an energy alone does not identify the limit points.
Each block lives in EuclideanSpace ℝ (Fin d) and is their product; Mathlib's norm on the product is the maximum of the three Euclidean norms, which is equivalent to the Euclidean norm of and changes no statement. and are abstract, with the hypotheses of the paper's §7 (Assumptions 7.1, 7.2, 2.3, 2.4); this generality implies the printed theorem for the , of (2.2). Solutions are maps constrained only on (or ), and the equation is required at only. The field is extended off by , as on p. 12 of the paper. A semiflow is Mathlib's Flow ℝ≥0 M, on the subtype or on a compact subset of it. The semiflow in the milestones is always assumed to be the flow of , never an arbitrary flow. The APT and limit-set definitions are the published StochApproxDyn.LimitSet ones.
The goal is stated for every global solution of the specific field (3.3), and keeps " is non-empty" in the conclusion. A statement about some solution of an unspecified field, or with " has empty interior" strengthened to " is finite", is a different theorem and does not count.
A complete development needs: Grönwall-type comparison and chain-rule arguments along trajectories; well-posedness of the autonomous system on and continuity of its flow; and the limit-set theory of asymptotic pseudotrajectories (Benaïm 1999), adapted to strict Lyapunov functions in the paper's sense. The last part is independent of Adam and reusable in stochastic approximation. Contributions to any milestone are welcome; Propositions 7.13 and 7.14 are the largest pieces of infrastructure.
A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).
The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor (Theorem 4, p. 11).
Let have a baseline probability law , and let a decision be a vector in a nonempty compact convex set . The loss of a possible outcome is for a convex function . A state-dependent positive-definite matrix sets the cost of moving mass from to :
Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of to lie between positive constants and for -almost every . Assumption 2 requires at most quadratic growth of and a finite fourth moment of . The ambiguity radius is positive (Assumptions 1–2, pp. 9–10).
The paper's dual objective is an expectation under the known law . Write . For a scalar and an auxiliary scalar , set
This value may be . Under the paper's duality conditions, minimizing over gives the worst-case loss at (Theorem 1 and (7), p. 10).
Assumption 3 bounds above by and excludes an almost surely zero for each . Assumption 4 makes compact. Lemma 6 supplies positive constants bounding uniformly over . With , the constants are those of (28), and
Theorem 3 first gives a bounded Hessian on and a positive lower bound on its block when , with the explicit from p. 36. The goal, Theorem 4, adds Assumption 5: is locally strongly convex and, at each , the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound
The order of the quantifiers is part of the target: works for every sufficiently small (Theorems 3–4, p. 11).
The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.
Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of does not by itself control directions that combine a change in with a change in . The inner supremum over can become infinite outside its effective domain, while at its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).
Lean uses EuclideanSpace ℝ (Fin d) for , a Borel probability measure for , and EReal for and the inner supremum. The reused extended-real integral records the and cases; the Hessian is taken only where is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use , since Lean's product norm is not the paper's Euclidean norm. The compact set is explicitly nonempty, and the positive ambiguity radius is quantified inside the goal so that and are uniform in . Theorem 3 additionally assumes for the proof's explicit formula for : nonempty compact would make that formula zero. Assumption 5 already gives in the goal.
The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes : its strict score event is empty at . Intermediate statements where the printed wording includes but the claim fails there state explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation , with independent of , rather than a pointwise or merely convex substitute.
A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.
A linear two-stage stochastic program chooses a first-stage decision before an uncertain parameter is revealed, and pays the optimal value of a second-stage linear program once the realization is known. Such programs are the basic model of planning under uncertainty in operations research, and their computational complexity determines which solution methods can be expected to work. In 2006, Dyer and Stougie argued that linear two-stage stochastic programs with fixed recourse are #P-hard even when the random data follow independent uniform distributions. Hanasusanto, Kuhn and Wiesemann showed that this proof is not correct and gave a corrected one, which also covers approximate evaluation to sufficiently high accuracy; their note also shows that, when the second-stage constraint matrix itself depends on (random recourse), even finding an approximately optimal decision is strongly NP-hard.
This mission formalizes that last result, Theorem 4 of the note. The previous missions of the series treat the hardness of evaluating the expected recourse with fixed and with random recourse.
The Integer Feasibility Problem. An instance is an integer matrix and an integer vector such that the polytope lies in the unit cube . The question is whether some binary vector satisfies . This problem is strongly NP-hard (Garey and Johnson).
The second-stage problem. For a decision and a realization , write for the all-ones vector and consider
The coefficient of in each constraint depends on , which is what makes the recourse random.
Problem (11). With uniformly distributed on ,
The second stage is not feasible for every (the problem lacks relatively complete recourse), so a decision is feasible only if the second stage is feasible for every . Let be the infimum of the objective over feasible decisions. A feasible is -optimal if
The constant . Lemma 4 fixes with and for every row .
For an instance with nonempty polytope, , as above, , and any -optimal decision of (11),
This is the mathematical content of "determining an -optimal decision is strongly NP-hard whenever ": a single comparison of any approximate decision with a threshold answers the NP-hard question.
The result. Theorem 4 implies that, unless the problems in NP admit an efficient solution scheme, there is no fully polynomial-time approximation scheme for two-stage stochastic programs with random recourse, even with a one-dimensional first stage and a uniform distribution. Together with the #P-hardness results of the same note, it delimits what algorithms such as sample average approximation can guarantee once relatively complete recourse and fixed recourse are dropped.
Formalizing it. The theorem has a short published proof, but that proof leaves several conventions implicit: the index set of the constraint block, the meaning of first-stage feasibility, and the condition on when has a zero row. A machine-checked version fixes each of them and verifies that the claimed formula for is correct under the chosen reading. To our knowledge none of these statements has been formalized before. The objects are elementary (finite-dimensional linear programs, a set integral on the unit cube), and the second-stage solution and rounding lemma are reusable for related reductions from integer feasibility.
The individual steps are short; the difficulty is bookkeeping across three layers. The second stage is an optimisation over whose feasibility depends on the sign pattern of ; the first stage requires a supremum over a polytope to be attained (compactness), and the expected recourse to be the same integral for all feasible decisions (integrability of a piecewise-defined value function over the cube). The tempting shortcut, reading off feasibility from the value of , fails: an infeasible linear program has no meaningful value, and treating it as cost would make every decision look optimal. Similarly, an almost-sure notion of feasibility looks natural for a stochastic program but invalidates the formula for whenever the polytope has measure zero, as it typically does for integer feasibility instances written with equalities.
All objects live in SPHardness.IntFeas. Vectors are functions on Fin n and Fin m; and are integer and are cast to , and integrality is kept because Lemma 4 depends on it. The uniform law on is Lebesgue measure restricted to the cube (volume ); expectations are set integrals. The recourse value, and are sInf/sSup in , and second-stage feasibility, first-stage feasibility and -optimality are separate predicates, so no statement depends on the junk value of an empty infimum.
Pinned readings and added conventions:
Strong NP-hardness, the FPTAS consequence, running times and encoding lengths are not formalized; the goal is the correctness of the reduction. A statement in which ranges over arbitrary reals satisfying a hypothesised identity, rather than over -optimal decisions of the program (11) built from , would be trivial and is ruled out: every object in the goal is defined from the instance.
Contributions welcome: proofs of the milestones, in particular measurability and integrability of the recourse function on the cube and attainment of , which are reusable for other piecewise-linear recourse functions.
The alternating direction method of multipliers (ADMM) is one of the standard splitting methods for problems of the form , in which a nonsmooth term acts on a linear image of the variable. It is used in signal and image processing, statistical learning and matrix completion, and in many of these applications or is nonconvex: sparsity penalties such as or with , rank constraints, or indicator functions of nonconvex sets. For convex problems the convergence theory of ADMM is classical; for nonconvex problems the questions of whether, and how fast, the iterates converge were open until the last decade.
R. I. Boţ and D.-K. Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020, DOI) analyse a proximal ADMM with variable metrics and its linearized variant in the nonconvex setting. Their first main result (Theorem 14, the subject of the companion mission of this series) shows that bounded iterates converge to a KKT point when a regularization of the augmented Lagrangian has the Kurdyka–Łojasiewicz property. This mission formalizes their second main result, Theorem 20: when that function has the Łojasiewicz property with exponent , the iterates converge in finitely many steps, linearly, or sublinearly, according to the value of .
Timeline. Łojasiewicz (1963) proved his gradient inequality for real-analytic functions; Attouch and Bolte (Math. Program. 2009) derived from its nonsmooth version the rates / / for the proximal point algorithm; Bolte, Sabach and Teboulle (Math. Program. 2014) gave a general KL-based convergence scheme (PALM); Li and Pong (SIAM J. Optim. 2015) proved convergence of a proximal ADMM under KL assumptions; Boţ and Nguyen (2018/2020) treated variable metrics, relaxation parameters , and the linearized variant, with explicit rates.
Let be proper and lower semicontinuous, differentiable with -Lipschitz gradient, and linear. The augmented Lagrangian with parameter is
Given positive semidefinite matrices , and , Algorithm 1 produces from any starting point by: minimizes ; minimizes ; and . Algorithm 2 replaces in the -step by .
Assumption 2 requires and to be bounded below, to be surjective with (), , , , and for all , where and are explicit functions of .
The analysis runs on the regularized augmented Lagrangian of Section 3
with explicit constants , . Along a run, . If the run converges to , put , and . has the Łojasiewicz property at with constant and exponent if
for all near , where is the limiting subdifferential.
Under Assumption 2, for a bounded run converging to at which has the Łojasiewicz property with exponent :
All constants are existential and independent of ; the goal fixes only the shape of each rate.
Theorem 20 is the quantitative half of the paper: it converts a local growth condition on one explicit function into convergence rates for the iterates of two practical nonconvex splitting methods. Since semi-algebraic functions satisfy the Łojasiewicz property with some exponent, the theorem applies to most of the sparsity- and rank-type models for which ADMM is used, and it explains when finite termination or linear convergence is to be expected. The intermediate results (Lemma 15 in particular) are the standard route from a Łojasiewicz inequality to rates and recur in the analysis of many first-order methods.
The result is proved in the paper; to our knowledge no part of it has a machine-checked proof. The mission produces a formal statement and proof of the rates, with every constant of the paper defined explicitly, and records where the paper's constants need recomputing: the constants and of Lemma 9 are reused on p. 26 for a regularization whose gradient is twice as large.
Lemma 15 is elementary but delicate: the recurrence has a lag and, for , a nonlinearity that a direct induction does not control, and the index bookkeeping determines the exponent. The rates for require a bound on an explicit subgradient of , whose limiting subdifferential involves the nonsmooth , so the calculus of limiting subgradients for a sum of a lower semicontinuous and a smooth function on a product space is needed. Transferring rates from to the iterates needs a finite-length estimate with explicit constants, uniform in the tail. A tempting shortcut, applying the Łojasiewicz inequality directly to , fails: does not decrease along the iterates; only the regularized does.
Vectors live in EuclideanSpace ℝ (Fin n); takes values in EReal and is proper and lower semicontinuous; and take values in EReal. Points of form a nested WithLp 2 product, so the norm and the inner product are the Euclidean ones of the paper. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff. The two algorithms are the constructors of an inductive type; a run is a relation (any minimizer may be taken), and every statement holds for both. and are replaced by arbitrary valid bounds. is , which the paper shows equals .
The Łojasiewicz hypothesis requires the inequality for every subgradient, so that , and only at points with , the convention ; with Lean's the hypothesis would be unsatisfiable at , and a Łojasiewicz hypothesis that no function satisfies, an Assumption 2 that no data satisfy, or a rate whose constant depends on would each make the targets trivial. Assumption 2 together with the run predicate is satisfiable (checked on a one-dimensional instance), and all constants are quantified before .
Labelled corrections: uses as displayed on p. 25 (not ); and are recomputed for the Section 3 ; Lemma 17 asks for ; Lemma 19 assumes , since for the paper's is .
Needed infrastructure: calculus of the limiting subdifferential for the sum of a lower semicontinuous function and a function on a product space, the descent lemma, and real-power estimates for sequences. Lemma 15 is independent of ADMM and reusable. Proofs of individual milestones are welcome in any order.
The alternating direction method of multipliers (ADMM) solves a constrained optimization problem by minimizing an augmented Lagrangian over one block of variables at a time and then updating a multiplier. Its two-block version had established convergence results. Applying the same cycle to three or more blocks was natural in models whose objective separates into several terms, but its convergence was unresolved when Chen, He, Ye and Yuan wrote this paper. Their analysis gives both a sufficient condition for convergence and, elsewhere in the paper, a counterexample to unrestricted convergence. This mission concerns the sufficient condition: the first and third constraint matrices are orthogonal in the sense . Chen, He, Ye and Yuan (2014)
The condition matters because the third block is separated from the first in the quadratic part of the augmented Lagrangian, while the middle block still participates in both updates. The result therefore covers a genuine three-block algorithm. It identifies what the direct cyclic extension can guarantee under this structure. The companion result gives an ergodic rate for averages of auxiliary iterates, from any starting point.
The three-block problem has variables , matrices , and a vector :
Each is closed and convex, each is convex, and the primal solution set is nonempty. For , write . The augmented Lagrangian is . The minus sign in front of fixes the sign of the multiplier step of (2.4c).
The paper analyzes a reordered cycle, numbered (2.4): minimize in , minimize in , update , then minimize in . The input state is ; is an intermediate variable. Each minimization may choose any minimizer. The reordered cycle is the cyclic direct extension with shifted by one index. A run is any sequence satisfying all four update conditions. Chen et al., pp. 4–5
Let , , and . The affine map has blocks . The variational inequality solution set consists of for which for every . Such points are the KKT points used in this mission. The paper employs and without defining them; these definitions fix their intended meaning.
Let , and let be the corresponding projection of . With the positive semidefinite block matrix in equation (2.11), the main target is Theorem 2.4:
If and have full column rank and , the entire sequence converges to a point of . The milestone list follows the paper's affine monotonicity statement, Lemmas 2.1–2.3, the displayed contraction, the summability and vanishing correction terms, and the cluster-point variational inequality. Chen et al., pp. 5–9
Theorem 2.5 bounds a gap at the average , where is the auxiliary point of (2.13). For every , the target is
This companion is stated, as on the page, for an arbitrary starting point. Chen et al., p. 9
The contraction gives a quantitative decrease relative to any variational inequality solution, even though is only semidefinite. Combined with the rank assumptions, it yields convergence of all primal blocks and the multiplier to a KKT point. The auxiliary average gives a finite-iteration gap bound with an explicit coefficient. These statements locate a useful structural regime inside a method that the same paper shows can diverge without additional conditions.
The formal development records the whole update cycle, the variational inequality, and the two block operators and . It leaves the named theorems as proof targets; compiling their statements does not claim a machine-checked proof. The definitions and intermediate inequalities can be reused when formalizing other cyclic splitting schemes or comparing this one with two-block ADMM.
The familiar two-block ADMM convergence argument cannot simply be applied to a three-block cycle: the middle iterate is updated between the first and third blocks, and the multiplier update sits before the next first-block minimization. The resulting one-step inequality contains a correction involving the previous and next essential states. Even after that correction is controlled, is semidefinite, so contraction in its quadratic form alone does not imply convergence of every coordinate. The full column rank conditions provide the additional control demanded by the paper's conclusion.
Vectors are functions on Fin n; matrices are Mathlib matrices. Every occurrence of a squared Euclidean norm in the paper is represented by a dot product or the expanded quadratic form. Mathlib's default norm on a function vector is a sup norm, so it is not used for those squares. The topology in the final convergence statement is the product topology on the four vector blocks. The block labels in the paper correspond to separate fields in Lean. The initial is unused by the run predicate. A zero-dimensional block is allowed when the stated conditions still make sense.
There are disclosed repairs to the printed text. Lemma 2.3 and the contraction are restricted to : their derivation uses the preceding optimality condition, which an arbitrary initial point need not satisfy. The convergence part additionally assumes , since the paper assumes a primal optimizer but supplies no constraint qualification guaranteeing a KKT point. Lemma 2.2's displayed uses , while its inequality and the run use ; Lean uses the latter. Theorem 2.5's verbal assertion that is represented as the indexed average .
The convex objectives are real valued on all of , as on p. 1. Such a convex function is continuous, so the paper's word “closed” adds no extra condition here. Runs quantify over actual minimizers and are not constructed by a default-valued argmin; this prevents an empty subproblem from creating a fictitious iterate. A complete proof can contribute the convex first-order conditions, matrix identities, summability argument and finite-dimensional convergence steps. The reusable interfaces are the three-block problem, run, variational inequality and block quadratic forms.
The ℓ1-regularized least squares problem (the Lasso, or basis pursuit denoising) is the model problem of compressed sensing and sparse inverse problems: given a matrix , data and a weight , one seeks a vector that fits while having few nonzero entries. The standard first-order method for it is the iterative shrinkage thresholding algorithm (ISTA), a forward-backward splitting scheme whose backward step is componentwise soft thresholding. Each iteration costs two matrix–vector products, which is why ISTA and its variants are used on problems far too large for interior-point methods.
The classical complexity guarantee for ISTA is , the rate of the proximal gradient method on any convex composite problem (Beck–Teboulle 2009). ISTA itself goes back to Daubechies–Defrise–De Mol 2004, and its link with forward-backward splitting to Combettes–Wajs 2005. An asymptotic linear rate was known, with an explanation through partial smoothness (Liang–Fadili–Peyré), but there was no global, explicit, non-asymptotic bound. Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 2017) derive such a bound from two ingredients: an error bound for the Lasso objective on balls, with a constant written through a Hoffman constant, and their general theory turning a Kurdyka–Łojasiewicz (KL) inequality into complexity bounds for descent methods.
Write with the Euclidean norm , and . For a matrix , is its spectral norm, the operator norm from to with Euclidean norms. The objective is
with and . Put and . Then is convex with gradient , Lipschitz with constant .
Given stepsizes with and any , ISTA is
where is the minimizer of . More generally, in a real Hilbert space with proper, lower semicontinuous and convex and convex with -Lipschitz gradient, the forward-backward method takes to be a minimizer of .
A sequence is a subgradient descent sequence for a convex with constants if and, for every ,
With , has the KL property on a set with desingularizing function if for every such and every .
A number is a Hoffman constant for a pair of matrices if, for every right-hand side with and intersecting, for all .
Put and , and . Let be such that whenever . Then ISTA converges to some and
The result. The theorem replaces the sublinear guarantee of ISTA by a global linear rate with explicit constants depending only on , , , the stepsizes, and a Hoffman constant. It also bounds the distance of the iterates to the limit, not only the objective gap, and needs no uniqueness of the minimizer. Through , it shows that conditioning of the objective near its minimizers, rather than strong convexity, governs the complexity of the method. The general machinery behind it (Theorem 16 of the paper, a separate mission of this series) applies to any method producing subgradient descent sequences.
Formalizing it. The result is proved on paper, and no machine-checked proof of it or of its ingredients is known. A formalization would give a verified linear-rate certificate for a widely deployed algorithm. It would also yield reusable lemmas: the descent and relative-error properties of the forward-backward method in a Hilbert space, and quadratic growth for the Lasso on balls. Lemma 10 rests on an external result (Beck–Shtern, Lemma 2.5) that a complete development must also formalize.
The Lasso objective is not strongly convex when has a nontrivial kernel, and its minimizer need not be unique. The textbook argument for linear convergence of proximal gradient methods, which uses strong convexity, therefore does not apply. Quadratic growth is the substitute, but it holds only on bounded sets, with a constant degrading in the radius. The analysis must therefore show that the iterates stay in a fixed ball and keep track of how the growth constant enters the rate. Deriving the explicit requires recasting the problem as a quadratic program over a polyhedron with facets and invoking a Hoffman-type error bound for it.
Citations refer to the arXiv preprint arXiv:1510.08234v3 (20 July 2016), with its numbering and pages; the journal version is not used. is EuclideanSpace ℝ (Fin n) and matrices act through Matrix.toEuclideanLin. Spectral norms are operator norms of the associated continuous linear maps, never Mathlib's default entrywise matrix norm. The data vector, called in §3.2.1 of the paper and in §5.3, is throughout; is the constant of (H2).
Functions with values in are EReal-valued. The convex subdifferential, Γ₀, , the prox predicate and the class of desingularizing functions are reused from published platform definitions. The stepsize condition is written , so that (where ) is covered. is the infimum of , and is a real power.
In the goal, is any positive constant satisfying the error bound on the ball of radius ; it is not fixed to the value (10) and not existentially quantified. The constants are fixed formulas, never existentials. A statement with an unspecified constant, with chosen after the sequence, or with the stepsize hypothesis written as (unsatisfiable or vacuous at ) would trivialize the goal and is ruled out.
The subgradient-descent and KL notions duplicate, in the sub-namespace ErrBoundCplx.ISTA, those of the series' first mission, because draft items cannot import each other. Proofs of any milestone are welcome, in particular Proposition 13 and the KL consequence of Lemma 10, which are self-contained. A formalization of Hoffman's error bound and of Beck–Shtern's Lemma 2.5 is the main infrastructure Lemma 10 needs.
Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of of rank is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.
Timeline.
Let be a prime power, , and let be an -dimensional vector space over ; has as points the spans of nonzero . An -subspace is a subset closed under addition and under multiplication by . It defines the -linear set
whose rank is . A linear set comes paired with , so every statement here is about . The weight of a point is , and is scattered when every point of has weight ; equivalently, for every nonzero ,
The plane construction (§2). Fix and the field with its subfields and . As an -space has dimension , so . For and an -linear the paper studies
with a monomial or a binomial . The relative norms enter the hypotheses.
For even and , in each of the cases (a) , ; (b) ; (c) , ,
Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many with odd, a regime where earlier existence results covered only a few values of . The case feeds the paper's second main result: scattered -linear sets of of rank are translation caps, from which complete caps of size in are built.
All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between -dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.
The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific . For the monomials this rests on the solvability of in , a norm condition interacting with the gcd hypotheses. For the binomial with , the existence of a suitable (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound for scattered to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking or any small subspace, is scattered but has the wrong rank; the content is in the rank .
Fin r → K; the plane of §2 on itself.Data-driven decision making estimates the cost of a decision from training data and then optimizes that estimate. The optimized estimate is biased downwards: the decision that looks best on the training data tends to disappoint on fresh data. Distributionally robust optimization counters this by optimizing the worst case of the estimate over all distributions within a radius of the empirical distribution, measured by a chosen distance function . Many distance functions are in use (φ-divergences, Wasserstein distances, moment sets), and the choice is usually justified by tractability.
Bertsimas and Van Parys, Bootstrap robust prescriptive analytics (arXiv:1711.09974v2), measure disappointment on bootstrap data: resamples drawn with replacement from the training data. Their Theorem 6 shows that with the entropic bootstrap distance the bootstrap disappointment decays exponentially in the sample size at rate at least . Proposition 1, the subject of this mission, is the converse: is the smallest distance function with this guarantee. Any distance that is strictly larger than near some distribution admits a nominal formulation whose disappointment decays strictly slower than . The result is in the spirit of Van Parys, Esfahani and Kuhn (arXiv:1704.04118), where the relative entropy is shown to be the optimal ambiguity set for i.i.d. data.
The distinct training points form a finite set , written in Lean. A distribution on it is a vector with nonnegative entries summing to one; the simplex of all such vectors is . The training data have the empirical distribution , which gives positive weight to every point of .
The bootstrap distance (Definition 6, Eq. (27)) is the relative entropy
with and if some .
A distribution distance function (Definition 4) is a map that is nonnegative, vanishes exactly on the diagonal ( iff ), and is convex in its first argument. is one.
A bootstrap sample of size is independent draws from (Eq. (14)); its law is the product , and its empirical distribution is , the frequency of each point of among the draws.
A nominal formulation here is a loss with cost estimator . Its robust counterpart (Eq. (24)) replaces the estimate by , and its disappointment set is
the bootstrap distributions on which the realized cost exceeds the robust budget.
Let be a distribution distance function, with , and a neighbourhood of , open in , on which . Then there is a loss whose disappointment set satisfies
stated in Lean in the equivalent form: for some , eventually .
Proposition 1 turns Theorem 6 from a sufficient condition into a characterization. Theorem 6 says the bootstrap distance guarantees disappointment rate ; Proposition 1 says no distance function that is larger than on an open set does, for some nominal formulation. A practitioner who wants the bootstrap guarantee with the least conservative ambiguity set therefore has no better choice than in this sense. The result is one instance of a pattern in data-driven optimization, where large-deviation rate functions appear as the optimal ambiguity sets.
The paper's proof is a short combination of three standard facts: strict separation of convex sets, Sanov's theorem, and convexity of relative entropy. None of the three is available on the platform in the form needed. Sanov's theorem for empirical distributions on a finite alphabet has no machine-checked proof in Mathlib or on the platform; the lower bound (31) is a self-contained, reusable result of independent interest. The separation step needs strict separation inside the affine hull of the simplex, which Mathlib provides only in the ambient vector space. The result is proved on paper; none of it is formalized.
The separation and convexity steps are routine once the relative topology of the simplex is handled. The central difficulty is the lower bound (31), a large-deviation lower bound for the empirical distribution of i.i.d. draws. The bootstrap probability of an event is a sum of multinomial probabilities over the empirical distributions with denominator that fall in the event, and the bound must hold for every point of the relative interior, including points on the boundary of the simplex, where some coordinates vanish and the distance is not differentiable. An argument that only treats distributions of full support, or only open sets of , does not cover these points.
A second difficulty is bookkeeping between the three topologies in play: the ambient space , the simplex , and the affine hull in which separation takes place.
stdSimplex ℝ ι. Covariates, responses, neighbourhood weights and the decision are abstracted away: the nominal formulation is the estimator (the estimator (18) with and unit weights), so the robust prescription plays no role.EReal-valued; convexity of is written out in EReal. The supremum defining is an EReal supremum. It is never empty, because lies in the -ball, so cannot collapse to all of .Measure.pi of , with fixed while .A complete development needs the method of types on a finite alphabet, strict separation in an affine subspace, and the convexity of relative entropy. The method-of-types lower bound is reusable well beyond this mission (hypothesis testing, large deviations of empirical measures). Proofs of any milestone, and alternative proofs of (31), are welcome.
A decision maker who must choose before observing an uncertain outcome usually does not know the distribution of ; only past observations are available. Data-driven optimization replaces the unknown expected cost by an estimate computed from the data. The simplest estimate, the sample average, is optimistically biased: the cost realized out of sample is, with probability close to one half, higher than predicted. Many corrections have been proposed: robust optimization over moment, -divergence or Wasserstein ambiguity sets (Delage & Ye 2010; Ben-Tal et al. 2013; Bertsimas, Gupta & Kallus 2018), and empirical-likelihood methods (Lam 2019; Duchi, Glynn & Namkoong 2021). Each is justified by a guarantee it satisfies. Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118; Management Science 67(6), 2021) ask a different question: among all estimates that satisfy a given guarantee, which one is the least conservative? Their answer singles out one distributionally robust predictor, built on the relative entropy, as the best possible one in a precise sense. This mission formalizes that answer for the prediction problem with finitely many outcomes.
The outcome takes values in . Decisions range over a compact set , and the cost is continuous in for each . These are the standing assumptions of §2 (p. 5).
A model is a point of the probability simplex , with the topology inherited from . Under a model the expected cost is .
The data are independent draws from an unknown model. They enter only through the empirical distribution . Write for probabilities when the samples are drawn from .
A data-driven predictor is a continuous function ; the number estimates . The set of all of them is . Its out-of-sample disappointment is the probability that the true cost exceeds the prediction.
The relative entropy of with respect to is
with and for .
For a threshold , the distributionally robust predictor is
It is the worst expected cost over all models under which the observed frequencies are not exponentially unlikely at rate more than . The observed frequencies are the first argument of .
The paper's meta-optimization problem (5) is
where means pointwise on . A feasible is strongly optimal if for every feasible . The goal is:
This statement contains feasibility (continuity and the decay rate) and pointwise domination of every feasible competitor.
Two further statements are included without milestones: Proposition 1(i), the information inequality, and Theorem 5, the finite-sample bound on the disappointment of .
The theorem turns a choice among robust estimators into a uniqueness statement. If a decision maker asks only for a disappointment probability that decays exponentially at rate under every possible model, then is the unique least conservative continuous predictor. Any predictor that is smaller anywhere fails the guarantee for some model. The reverse predictor (12) and the restricted predictor (13), which fix the other argument of or hedge only against models absolutely continuous with respect to the observed frequencies and are common in the literature, differ from (Remark 3, pp. 15–16), so the theorem does not single them out. The companion missions of this series extend the result to predictor–prescriptor pairs (mission 2) and to compact continuous outcome spaces (mission 3).
The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal development would also give Mathlib-level statements of the method of types: Sanov's theorem for finite alphabets in both its finite-sample and asymptotic forms, together with the convexity and semicontinuity of the relative entropy with the convention. These are reusable far beyond this paper.
Feasibility (Theorem 3) is a direct consequence of the LDP upper bound, once the disappointment set is seen to lie outside the relative entropy ball. The difficulty is the optimality half. Showing that a competitor with at a single point must be infeasible requires a lower bound on a disappointment probability. The obvious approach evaluates the LDP lower bound at a maximizer of (10). That fails: the lower bound (7b) needs a strictly positive model, the maximizer usually lies on the boundary of the simplex and on the boundary of the ball , and the bound is only in terms of the interior of the disappointment set. The argument has to move to a nearby model, and this uses the continuity of , the convexity of , and the convention of in its second argument. The asymptotic statements also require care with the logarithm of a vanishing probability.
Fin d. is the subtype of stdSimplex ℝ (Fin d), so interiors and continuity are relative to , as footnote 1 (p. 12) requires.EuclideanSpace ℝ (Fin n), and is continuous in for each outcome.EReal-valued and is whenever . A real-valued sum would give a finite value there under Lean's log 0 = 0, and so change .Real.log would give a never-disappointed predictor rate , which makes Theorem 3 false.MeasurableSet D in the simplex subtype.Welcome contributions: the method of types on Fin d (type classes, their cardinality bounds and probabilities); joint convexity and lower semicontinuity of the finite relative entropy with the convention; and Berge's maximum theorem in the form used for Proposition 3. These are reusable beyond this mission. The definitions duplicate those of mission 2 of this series and are meant to be merged once published.
The source is the arXiv preprint arXiv:1704.04118v3 (22 Dec 2019); all theorem, display and page numbers refer to it.
A retailer that sells products in categories must decide which products to offer in each category. When customers choose among the offered products according to the nested logit model, the expected revenue depends on the offered assortment in a nonlinear way, and the retailer's shelf space adds a knapsack constraint in every category. Gallego and Topaloglu (Management Science, 2014) show that the resulting space-constrained assortment problem is NP-hard even with a single nest (via Lemma 2.1 of Rusmevichientong, Shen and Shmoys, cited in the paper as 2009), give a factor-2 approximation through a linear program, and then, in Online Supplement C of the paper, refine the approach into an approximation scheme: for every desired guarantee , a polynomially sized family of candidate assortments per nest suffices.
The scheme follows the partial-enumeration idea of Frieze and Clarke (1984) for multi-dimensional knapsack problems, but has to work for a whole one-parameter family of knapsack problems, one for every value of a scalar , with a single collection of candidates fixed in advance.
There are nests and products . Product of nest has a preference weight , a revenue (no sign or order is assumed), and a space requirement ; nest has capacity with . An assortment of nest is a set ; it is feasible, , when . Write
For , problem (7) is , which equals the knapsack problem (10) . The quantity is the utility of product ; denotes the optimal value of (10). An assortment is -approximate at when for all .
For a set , problem (17) is the linear program
the LP relaxation of (10) with the products of fixed in the knapsack and every product whose utility exceeds the smallest utility in removed. Its optimal value is . Rounding a solution down gives the assortment . is the family of subsets of with at most elements.
For every , with , there is a collection such that
The paper writes ; the explicit bound above is of that order.
Together with Theorem 4 of the paper (an -approximate candidate per nest for every yields an -approximate assortment for the whole problem) and Theorem 2 (the best combination of candidates solves a linear program with variables), Theorem 9 gives, for every , an -approximation of the space-constrained nested logit assortment problem by a single linear program with constraints; for this is . It shows that the factor 2 of Section 5 is not a barrier of the method.
The result is proved in the paper. As far as the platform's records show, none of it is formalized; this mission produces a machine-checked proof of Lemma 8 and Theorem 9, including the explicit counting of parameter intervals that the paper only sketches.
A related but different construction, with large and small products and a continuous knapsack whose weights are preference weights, appears in the unconstrained variants of Davis, Gallego and Topaloglu (items NestedLogitVariants.PowersDelta.*); it is not reused here.
Two points resist the obvious argument. First, rounding down the plain LP relaxation of (10) drops one fractional product whose utility can be as large as the whole optimum, which is why Section 5 only reaches a factor 2; no choice of rounding of that relaxation alone does better. The guarantee has to come from the partially fixed problems (17), and their indicator constraint is delicate: it excludes only products of strictly larger utility than the least utility in , and a version that also excludes ties can cut off the optimal assortment of (10), and the comparison with is then lost.
Second, the collection must be fixed before . The optimal solution of (17) depends on through the ordering of the utilities, the ordering of the utility-to-space ratios and the signs of the utilities, which change only at the intersection points of lines. Because the feasible set of (17) itself depends on through the indicator constraint, the solution on an open interval between two such points need not remain optimal at its endpoints; the count must treat the breakpoints as pieces of their own.
ι; products are Fin n (0-based); assortments are Finset (Fin n), with for .NestedLogitVariants.LP.Model is referenced; its within-nest no-purchase weight is set to zero (I.vnp i = 0), which makes V and R the paper's and . The paper's extension is not formalized.Nat.ceil; is strict.Accelerated first-order methods for convex minimization, starting with Nesterov's 1983 scheme, reach the rate , which is optimal for the class of convex functions with Lipschitz gradient. Su, Boyd and Candès (NIPS 2014; JMLR 2016) showed that Nesterov's method is a discretization of the second-order ODE , and since then continuous-time inertial dynamics have been the main tool for designing and analysing accelerated algorithms: a Lyapunov argument for the ODE is found first, and then transcribed to the discrete scheme.
Nesterov-type methods oscillate. Adding to the dynamic a damping term driven by the Hessian, , attenuates these oscillations, and because is the time derivative of , time discretizations of such dynamics remain first-order methods. Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) develop this programme. This mission formalizes its first result: a convergence-rate theorem for the continuous dynamic with general damping and time-scale functions.
Timeline.
Let be a real Hilbert space with inner product and norm . Let be a convex function of class that attains its minimum at some point . Fix a starting time , a constant , and two non-negative continuous functions . These are the paper's standing assumptions (H).
A solution trajectory of
is a twice differentiable curve satisfying this equation at every . The coefficient is an asymptotically vanishing viscous damping, weights the Hessian-driven damping, and is a time-scale factor in front of the gradient.
When is differentiable, set
The rate in Theorem 1 is expressed through .
Assume is differentiable and the growth conditions
hold for all . Then and
The goal leaves and general. Specific choices are the companions below.
The paper's own proof steps, in order:
The result. Theorem 1 contains the rate of the continuous Nesterov dynamic as the case , , . It recovers the Attouch–Peypouquet–Redont theorem and the vanishing-coefficient system of Case 2 as special cases. The time scale gives faster rates when grows. For it also gives the integral estimate on , which is the continuous counterpart of the fast decay of gradients proved for the algorithms (IPAHD) and (IGAHD) later in the paper.
Formalizing it. The result is proved in the paper, and nothing about it has been machine-checked. The mission produces:
The energy estimate is an exact computation that has to match term by term. The cross terms cancel only because is chosen to match . That computation needs the chain rule in a Hilbert space.
The naive conclusion ", so integrate (4)" hides two analytic steps:
The (i) rate needs the positivity of from to divide by .
Lean conventions:
gradient f, and is fderiv ℝ (gradient f) x u.HasDerivWithinAt on . Values before are irrelevant, and derivatives at are one-sided.=O[atTop], with constants depending on all data.IntegrableOn on , never a bound on a Bochner integral that could be the junk value .These choices rule out trivial readings: Lean's zero value for the derivative of a non-differentiable function, an ODE with an unlinked velocity, and an integral that is zero because the integrand is not integrable. The goal assumes nothing about , or (4)–(6), which appear only in milestones.
Companion items:
Contributions are welcome: the chain rule for gradient along a curve, a monotonicity lemma for one-sided derivatives on Ici, and the integrability lemma for non-negative functions bounded by a non-increasing energy.
Many problems in signal processing, statistics and machine learning are of the form : a smooth data-fitting term , plus a possibly nonsmooth and nonconvex regularizer applied to a linear image of the variable. Examples are total-variation-type penalties with nonconvex potentials, -type sparsity terms, and constraints with nonconvex. The alternating direction method of multipliers (ADMM) treats and separately, which makes it the method of choice for this class. For convex problems its convergence theory is classical. For nonconvex problems it was long used as a heuristic, and the Kurdyka–Łojasiewicz (KŁ) framework of Attouch, Bolte, Redont, Soubeyran and Svaiter, and of Bolte, Sabach and Teboulle, is now the standard tool for proving that such methods converge.
Timeline. Li and Pong (SIAM J. Optim. 2015) proved global convergence of a proximal ADMM with for twice differentiable under a KŁ hypothesis. Hong, Luo and Razaviyayn (SIAM J. Optim. 2016) studied related nonconvex ADMM schemes under other assumptions. Boţ and Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020) extended this in three directions. Their scheme uses variable metrics , . It allows a relaxation parameter in the dual step. It covers both a proximal and a proximal-linearized -update. Under these conditions they proved that bounded iterates have finite length and converge to a KKT point whenever a regularized augmented Lagrangian has the KŁ property. This mission formalizes that theorem.
Let be proper and lower semicontinuous, let be differentiable with -Lipschitz gradient, and let be linear. The augmented Lagrangian with parameter is
Let and be symmetric positive semidefinite matrices, and write . Fix . From an arbitrary starting point , Algorithm 1 generates
Algorithm 2 is the same, except that in the -update is replaced by its linearization . Assumption 1 asks for four things:
With the constants and of §2.2 of the paper, the regularized augmented Lagrangian is
A KKT point of the problem is a triple with , and , where is the limiting subdifferential. A proper lower semicontinuous is a KŁ function if, near every point of , a concave desingularizing function satisfies .
Under Assumption 1, let be a bounded sequence generated by Algorithm 1 or Algorithm 2. If is a KŁ function, then
and for some KKT point .
The milestones follow the order in which the paper's proof uses them:
Theorem 6, the boundedness of the iterates under coercivity, is included as a supporting item that discharges the boundedness hypothesis.
The theorem gives global convergence of the whole sequence, not just subsequences, for a broad family of nonconvex splitting methods. The family includes full-splitting variants, in which makes the -update explicit. The KŁ hypothesis on holds, for example, whenever and are semi-algebraic. The finite length conclusion is also the starting point for the rates of Section 3 of the paper, which are the subject of the companion mission.
The paper result is proved; this mission formalizes the known proof. As far as the platform records go, no machine-checked proof of convergence of a nonconvex ADMM exists. The Li–Pong ADMM theorems on the platform are open statements about a different algorithm. A completed development would supply the following reusable pieces:
The obvious Lyapunov candidate, itself, does not decrease along the iterates: the dual step increases it by . That increase has to be paid for by primal progress, and this is possible only because surjectivity of lets the dual increment be controlled by -increments over two consecutive steps. This is where the specific constants , , and the coupling condition (15) come from. The KŁ argument must therefore be run on the lifted function in five variables, whose subgradient bound (Corollary 10) involves three past increments and two telescoping terms. The textbook one-step KŁ argument therefore does not apply directly, and the recursion has to be closed with the three-step summability Lemma 3. For the dual update is relaxed, and the estimates must handle in both regimes and .
Spaces are EuclideanSpace ℝ (Fin n), and products such as and the 5-fold domain of are nested WithLp 2 products. Their norm is the Euclidean product norm the paper uses, not the sup norm. The function and the functions , take values in EReal. The data are bundled in a structure Data, and the algorithm is a parameter Variant (prox for Algorithm 1, linearized for Algorithm 2), so every statement covers both algorithms. A run is a relation: any minimizer may be selected at each step, and existence of minimizers is not claimed. and are replaced by parameters with the inequalities the proofs use ( with , and ). The paper's statements are the instance , . The subdifferential is the published limiting subdifferential, and "KŁ function" is the published IsKLFunction. In that definition, is read as a bound for every subgradient, so . Corrections read past: the paper indexes although exists only for , and it writes "defined in Assumption 1" for and , which are defined on p. 10.
There are three ways to formalize the statement trivially, and all are excluded:
Contributions are welcome at every milestone. Lemma 3 and the subdifferential calculus behind Lemmas 8–9 are independent of the algorithm, and are good entry points.
A promise constraint satisfaction problem asks to distinguish instances that are satisfiable in a structure from instances that are not even satisfiable in a weaker structure . Approximate graph colouring (tell 3-colourable graphs from graphs that are not 5-colourable) and are standard examples. The algebraic approach to CSPs explains the complexity of such problems through polymorphisms, the multi-argument maps that preserve every relation.
Two polynomial-time relaxations dominate the algorithmic side: the Basic LP relaxation, solved over , and the affine relaxation, the same linear system solved over . Barto, Bulín, Krokhin and Opršal (BBKO19) characterized each one separately: BLP solves exactly when has symmetric polymorphisms of all arities, and the affine relaxation exactly when it has alternating polymorphisms of all odd arities. Brakensiek and Guruswami (BG19) used ad hoc combinations of the two. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383) combine them into a single algorithm, BLP+Affine, and characterize its power exactly. This mission formalizes that characterization, Theorem 4 of the paper.
A signature assigns to each symbol an arity . A relational structure on a finite domain fixes relations . A homomorphism is a map sending every tuple of into , and is a promise template if one exists. An instance has variables and constraints ; it is satisfiable in (written ) if some assignment sends each into .
A map is a polymorphism if applying column-wise to any matrix whose rows are in gives a tuple of . It is block-symmetric for a partition if it is invariant under permutations of its arguments that preserve every block, and its width is the largest minimum block size over such partitions.
The Basic LP has a probability distribution on for each variable and on for each constraint, with the marginal of at each position of equal to the distribution of the variable in that position. The affine relaxation is the same system over with unknowns , and no sign constraints. BLP+Affine (Figure 1) takes a relative interior point of the LP, keeps only the integer solutions that vanish wherever does, and accepts iff one remains. It correctly solves if it accepts every and rejects every .
The minor of along is . The minion has as -ary objects the pairs with , , both summing to , and ; the minor along sums both over fibres of . A minion homomorphism sends -ary objects to -ary polymorphisms and commutes with minors. The free structure has the -ary objects as its domain, and a tuple is in iff it is the family of coordinate minors of one -ary object.
For a promise template on finite domains, the following are equivalent:
The paper proves Theorem 4 through Lemmas 7, 8 and 9. The milestones follow that proof:
A companion item, Example 10, records that the disjoint union of a directed 2-cycle and a directed 3-cycle has no block-symmetric polymorphism of width at least .
Theorem 4 is an exact criterion: the power of an algorithm is read off from the polymorphisms of the template. Its sufficiency direction (Theorem 3, the subject of the companion mission) says that one fixed algorithm decides every PCSP with block-symmetric polymorphisms of unbounded width, which covers nearly all tractable Boolean PCSPs known at the time, including those with threshold and alternating-threshold polymorphisms. The necessity direction, new in Theorem 4, gives a method for proving that BLP+Affine fails on a template: exhibit, for some , the absence of a -ary polymorphism with blocks of sizes and . Example 10 is an instance: a tractable template that the algorithm does not solve. The minion and its free structure are the template for later characterizations of relaxation hierarchies.
The result is proved in the paper. As far as is known it has not been machine-checked. A formalization adds a checked development of minions, minion homomorphisms and free structures for PCSPs, a compactness theorem for relational structures, and a checked version of the one-block argument whose many-block extension the paper only asserts.
The equivalence passes through three different kinds of object: an algorithm, an infinite algebraic object (a homomorphism defined on all of ), and finite families of polymorphisms. From polymorphisms one obtains homomorphisms only on finite pieces , each from a different polymorphism, and these do not agree with one another; a single homomorphism on the whole minion needs a compactness argument over the finitely many restrictions, which uses the finiteness of and . The passage from "every instance satisfiable in the free structure is satisfiable in " to a homomorphism from the infinite free structure is a second compactness step. The relative interior point of Figure 1 must be kept: accepting whenever both relaxations are merely feasible is a different, weaker algorithm.
All objects are in the definitions file PCSPBLPAff.Characterization.Setting, built on Mathlib only.
(τ : Type) (ar : τ → ℕ), with no finiteness of ; the paper's requirement that arities be positive is dropped, and no statement needs it. Domains are finite types; instance variables are Fin n and arities Fin L.Two trivializing formalizations are ruled out: the acceptance condition keeps the maximal-support requirement, and the free structure's relation requires the witnessing pair to be an object of supported in .
A complete development needs finite sums over fibres, transport of objects along Fintype.equivFin, Tychonoff or König's lemma (Mathlib.Order.KonigLemma, Mathlib.Combinatorics.Compactness), and the existence of a maximal-support point of a rational polytope. The compactness theorem for relational structures and the free-structure lemma are reusable beyond this mission. Proofs of any milestone, and of the general Lemma 17 for an abstract minion, are welcome.
Best subset selection asks for the linear model that fits a response with as few predictors as possible. It is a basic problem of statistics and a standard test case for mixed-integer optimization. The penalized form
is NP-hard in general. Exact mixed-integer methods (Bertsimas, King, Mazumder 2016) certify global optimality but scale to moderate only. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed a hierarchy of local minima for the -penalized problem, together with algorithms that reach each class. These are coordinate descent for coordinate-wise minima, and coordinate descent combined with small combinatorial swap searches for the finer swap inescapable minima. The software built on these algorithms, L0Learn, runs on problems with in the millions.
The companion mission (part I) proves that the coordinate descent stage converges. This mission proves the guarantee of the second stage: the local combinatorial search stops after finitely many rounds, and it stops at a partial swap inescapable minimum.
Data and objective. Let have columns of unit Euclidean norm, let , and let , . Problem (2) is
where is the number of nonzero entries. The paper names three cases: (L0), with ; (L0L1), with ; and (L0L2), with . , and keeps the entries of in and zeroes the others.
Classes of minima. A stationary solution has nonnegative lower directional derivative in every direction . A CW minimum is a point where each coordinate minimizes with the other coordinates held fixed. For a positive integer , a PSI() minimum is a stationary with support such that, for all and with ,
In words, dropping at most active coordinates, adding at most new ones and optimizing only over the added ones never lowers the objective.
Algorithm 1 (CDSS) is cyclic coordinate descent. Each step sets one coordinate to the minimizer given by the thresholding operator of (12). Every time a support has been visited times, the algorithm also performs a spacer step: one pass of coordinate descent on restricted to that support.
Algorithm 2 (CD-PSI()) alternates two steps. It runs Algorithm 1 from to obtain . It then searches the swap problem (14),
with , for a feasible with . If it finds one, it sets and continues; otherwise it terminates.
Assume the (L0), (L0L1) or (L0L2) setting. For (L0) and (L0L1), assume also that every columns of are linearly independent (Assumption 1) and, when , that the start satisfies the objective bound of Assumption 2. Then every run of CD-PSI() satisfies
No bound on is part of the goal, and the paper states none.
The result. Theorem 4 makes CD-PSI() an algorithm with a guarantee. It always stops, and its output satisfies an optimality condition that is strictly stronger than coordinate-wise optimality: the hierarchy (4) of the paper places PSI() minima inside CW minima, and for large they coincide with global minimizers. The same termination argument underlies the full-optimization variant (FSI minima) and the swap heuristics of L0Learn, which the paper treats "by the same argument".
Formalizing it. The theorem is proved on paper, in a short argument in Appendix A.8 that rests on the convergence of Algorithm 1 (Theorem 2, the companion mission). No part of it has been machine-checked. This mission produces checked definitions of PSI minima, of the swap problem and of the two-level algorithm; a formal proof of the finite termination; and the bridge lemmas between CW minima, stationarity and the restricted least-squares problem, which any formal treatment of -penalized regression needs.
The obvious argument is that each round lowers the objective, there are finitely many supports, so the algorithm stops. A strict decrease of alone gives no finiteness: a real-valued sequence can decrease forever. What makes the argument work is that the value of at an output of Algorithm 1 depends only on its support. That needs every output to be a CW minimum, which is Theorem 2, a nontrivial convergence theorem for a discontinuous objective. It also needs every CW minimum to minimize the convex function over its support, which uses the characterization (8) and convexity.
A second difficulty is bookkeeping. Algorithm 1 never stops ("while not converged"), so its output is a limit. Each call of Algorithm 1 inside Algorithm 2 must satisfy the hypotheses of Theorem 2, in particular Assumption 2 for the new starting point, and that holds only because the objective has decreased since .
Vectors are Fin p → ℝ, so indices are -based. All norms are explicit sums, never Lean's sup norm. is Real.sign, with . The lower directional derivative is EReal-valued. The theorems are stated for the three named problems, via the hypothesis . Assumptions 1–2 are required only when .
Algorithm 1 is a deterministic state machine with a cyclic pointer, a table and a pending-spacer flag, following the box on p. 11. A run of Algorithm 2 is a pair of sequences: is the limit of the CDSS iterates from , and is any improving feasible point of (14), required only while the run has not terminated. The predicate is not vacuous: on the instance , , , , , , a run exists and terminates at . "" in Definition 3 is read as " every value".
A statement that assumes the outputs of Algorithm 1 are CW minima, or that the run terminates, or that only finitely many supports are visited, would trivialize the goal. All three are conclusions of the mission, not hypotheses.
The development needs the CDSS model shared with the companion mission, convexity of the restricted least-squares objective and a finiteness argument over Finset (Fin p). The definitions of Problem (2), Algorithm 1 and the stationarity notions are reusable for any later mission on -penalized regression. Proofs of the milestones independently of the goal are welcome; Theorem 2 can also be imported once the companion mission proves it. Theorem and page numbers are those of arXiv:1803.01454v3.
Regularized loss minimization covers support vector machines, logistic and ridge regression, and the absolute-deviation regression of robust statistics. Stochastic dual coordinate ascent (SDCA) solves these problems by maximizing the Fenchel dual one randomly chosen coordinate at a time. Shalev-Shwartz and Zhang (arXiv:1209.1873, JMLR 2013) gave the first analysis of SDCA in terms of the duality gap. For smooth losses their rate is linear; for Lipschitz but non-smooth losses such as the hinge loss it is of order , which is no better than stochastic gradient descent, although SDCA is observed to converge much faster than SGD on SVM problems asymptotically.
Section 5 of the paper explains that observation. Many non-smooth losses are smooth at most points: the hinge loss fails to be smooth only at . If, at the optimum, most margins stay away from the kink, the dual is strongly concave in most coordinates, and SDCA converges linearly in the dual objective. Earlier linear-rate results for dual coordinate ascent on SVMs (Luo and Tseng, 1992) depend on the smallest nonzero eigenvalue of the data Gram matrix, which can be arbitrarily small when two data points are close; the condition of Section 5 avoids the Gram matrix.
Data (Euclidean norm), scalar convex losses and define the primal problem
The convex conjugate of is . The dual problem is with
A dual variable is feasible when every is finite. A function is -Lipschitz if . The standing assumptions are , and .
Procedure SDCA starts from . At iteration it picks uniformly at random, independently of the past, chooses maximizing , and sets . Let be a dual optimum and .
The refined dual strong convexity condition (Definition 2, (4)) asks for functions with
For the hinge loss one may take . With constants , the dual strong convexity inequality (5) is
and counts the coordinates with small modulus.
Assume convex -Lipschitz losses, the standing assumptions, and (5) with constants . For every and with ,
The constants and are the paper's.
Theorem 5 gives a linear rate for the dual sub-optimality of SDCA on non-smooth losses whenever few constants are small. If for some (for the SVM, for all ), the iteration count is , compared with order from the Lipschitz analysis of Theorem 1 of the same paper. The paper uses Theorem 5 to explain the observed asymptotic advantage of SDCA over SGD, and its Theorem 6 converts it into a duality-gap bound.
The result is proved in the paper. It has not been formalized: no SDCA convergence result is on Prove2Me, and Mathlib has no conjugate-duality theory for this problem class. The mission produces a formal account of the dual objective in extended reals, of the exact coordinate maximization step, and of the averaging over uniformly random coordinate sequences, together with a checked proof of the rate. The companion missions of this series cover Theorem 1 (Lipschitz losses) and Theorem 2 (smooth losses).
Condition (5) gives a modulus per coordinate, and some may be zero, so the dual is not strongly concave and the standard linear-rate argument for strongly concave coordinate ascent does not apply. The per-step progress has a variance term with the sign of , which is positive exactly on the coordinates with small modulus; that term must be controlled by bounding the dual variables themselves, which requires the Lipschitz structure through the conjugate. The extended-real-valued conjugate is a second source of work: every quantity must be shown finite along the run before it can be manipulated as a real number.
Lean works in EuclideanSpace ℝ (Fin d), with data points indexed by Fin n, . The conjugate is an EReal supremum and is EReal-valued, exactly at infeasible points. Real-valued expectations of dual values appear only together with a conjunct stating their finiteness. The SDCA step is a map with the hypothesis that is an exact maximizer of the coordinate objective. The run is a fold over the sequence of chosen coordinates, and the expectation is the uniform average over all sequences of length (SAGA.Convex.expectIdx, a published definition). The optimum is a hypothesis for all ; in (5), is . Inequality (5) quantifies over feasible only. Lemmas 5 and 6 are stated for an arbitrary feasible current state, which is stronger than the history-averaged form printed. The paper's range becomes , because at the iteration bound is undefined. A formalization that admits would evaluate it to and claim the bound at , which is false.
The development needs elementary facts about conjugates of scalar functions in EReal (convexity, the Fenchel–Young inequality, the Lipschitz domain bound), the weak duality inequality , and finite averages over coordinate sequences. The conjugate facts and the expectation calculus are reusable by the other two missions of the series. Proofs of individual milestones are welcome independently.
A cubic graph has chromatic index 3 or 4 (Vizing). Cubic graphs of chromatic index 4 — the uncolourable ones — are where most of the open problems on cubic graphs live: a minimal counterexample to the cycle double cover conjecture or to Tutte's 5-flow conjecture would be among them. Uncolourable graphs with small edge cuts or short cycles reduce to smaller ones, so attention concentrates on snarks, the uncolourable cubic graphs that are cyclically 4-edge connected and have girth at least 5.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, J. Combin. Theory Ser. B 103, 2013) generated all snarks on up to 36 vertices and tested a series of published conjectures against them. One of these concerns the 2-factors of a snark, its spanning subgraphs in which every vertex has degree 2. A 3-edge-colouring of a cubic graph gives 2-factors made of even cycles, so a snark is a graph in which some 2-factors are forced to contain odd cycles. At the far end are the snarks in which every 2-factor consists of odd cycles only. Abreu, Labbate and Sheehan (European J. Combin. 33, 2012), studying pseudo and strongly pseudo 2-factor isomorphic graphs, conjectured that this happens only for the Petersen graph, the Blanuša-2 snark and the Flower snarks (paper, p. 11, Conjecture 4.11).
Timeline:
All graphs are finite and simple. A graph is cubic if every vertex has degree 3. It is colourable if its edges can be coloured with three colours so that edges sharing an endpoint get different colours, and uncolourable otherwise. The girth is the number of vertices of a shortest cycle. is cyclically -edge connected if deleting fewer than edges never leaves two components that both contain a cycle. A snark is an uncolourable, cyclically 4-edge connected cubic graph with (paper, p. 4).
A 2-factor of is a spanning 2-regular subgraph : it uses every vertex, and every vertex has degree exactly 2 in . Each component of is a cycle. Say that all 2-factors of are odd if every component of every 2-factor of has an odd number of vertices.
The witness is the graph of Appendix 8.1, given in the paper as a list of higher-numbered neighbours of the vertices :
It has 26 vertices and 39 edges. In Lean it is G81 : SimpleGraph (Fin 26) with paper vertex as .
Because has 26 vertices, it is not the Petersen graph (10 vertices), not the Blanuša-2 snark (18) and not a Flower snark ( vertices). The goal therefore refutes Conjecture 4.11 without formalizing the conjecture's list of exceptions.
The goal splits into five properties of the one graph :
A supporting statement, not from the paper, asserts that has a 2-factor, so that milestone 4 is not vacuous.
The result. Conjecture 4.11 would have characterised a natural extremal class of snarks by a short explicit list. The counterexample shows that the class is not that list: there are snarks outside the Petersen, Blanuša-2 and Flower families in which no 2-factor contains an even cycle. Such graphs are relevant to questions about 2-factor structure, oddness and cycle double covers, where the parity of 2-factor cycles is exactly what the arguments track.
Formalizing it. The result is proved in the paper by exhibiting the graph and checking it by computer; it has not been machine-checked in a proof assistant. A formal proof certifies every property of the printed graph — including that the printed adjacency list decodes to a graph with these properties — and leaves a reusable library of definitions (snarks, cyclic edge connectivity, 2-factors) that other snark statements can import.
Each property is a finite check, but some are large. Cubicity and girth are local. Cyclic 4-edge connectivity quantifies over all sets of at most three of the 39 edges (about ten thousand) and needs, for each, a component analysis of the remaining graph. The odd-2-factor property quantifies over all 2-factors; in a cubic graph these are the complements of the perfect matchings, and has 56 perfect matchings. The obvious route — decide over all subgraphs — is out of reach: there are edge subsets, and the statement is phrased through Mathlib's ConnectedComponent and IsRegularOfDegree, which do not evaluate by kernel computation at this size. Uncolourability has the same problem: the naive search space has colourings.
Conventions committed to:
Fin 26, paper vertex = Lean vertex ; adjacency is the symmetric closure of an explicit edge list G81Edges, so it is decidable.G.lineGraph.Colorable 3 (a proper 3-edge-colouring), never G.Colorable 3.egirth : ℕ∞, so "girth at least 5" is 5 ≤ G.egirth.F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2 — spanning by construction. Oddness is per component: Odd (Nat.card c.supp) for every component c. It is not the parity of the whole vertex set (26 is even).S with S.card < k, any two components of G.deleteEdges S that both contain a cycle are equal.The odd-2-factor property is vacuous for a graph without 2-factors. The goal is not trivialised this way: has 2-factors, and a supporting theorem states it.
Out of scope, because they rest on exhaustive computer enumeration: that is the smallest counterexample, that there is exactly one further counterexample on 34 vertices, Observation 4.10 (all snarks on at most 36 vertices have oddness 2), and Tables 4 and 5. The Petersen graph, the Blanuša-2 snark and the Flower snarks are not defined here; the refutation uses only their orders.
Contributions welcome: proofs of any milestone; general lemmas linking 2-factors of cubic graphs to perfect matchings, and 3-edge-colourings to even 2-factors; decision procedures for cyclic edge connectivity of explicit graphs. The definitions are shared in shape with the other missions of this series and are meant to be reused.
Many problems in statistics and signal processing ask for an orthonormal frame that is both a good fit to the data and sparse or otherwise structured. Sparse principal component analysis, compressed modes in physics, unsupervised feature selection and sparse blind deconvolution all take the form
with smooth and convex but nonsmooth, typically an penalty. Before the work of Chen, Ma, So and Zhang, algorithms for this class fell into three groups: subgradient-oriented methods, which solve a quadratic program over sampled subgradients in every step; proximal point algorithms, whose subproblems are as hard as the original problem; and operator-splitting methods such as SOC and MADMM. The manifold proximal gradient method (ManPG) carries the Euclidean proximal gradient method over to the Stiefel manifold. The paper shows that ManPG keeps the global convergence and the iteration complexity that Riemannian gradient descent has for smooth objectives (Boumal, Absil and Cartis, 2019).
The feasible set is the Stiefel manifold
The ambient space carries the Frobenius inner product and norm . The tangent space at is . The orthogonal projection onto it is .
The standing assumptions on are imposed on all of :
A point is stationary (Definition 3.3) if
where is the convex subdifferential.
A retraction maps tangent vectors at back to , with . On the compact manifold every retraction satisfies, for some and all , (Fact 3.6),
ManPG (Algorithm 1) takes , and . In iteration it solves the convex subproblem
It then backtracks until , and sets .
A point is -stationary (Definition 5.4) if the solution of (4.3) at with has . The proof of Lemma 5.2 uses a bound on over and the constants
For every run of ManPG:
has and is -stationary.
Here is the optimal value of (1.1). The constant is the paper's, kept exactly.
Theorem 5.5 is the paper's main result. It certifies ManPG as a first-order method for nonsmooth problems on the Stiefel manifold with the same complexity as Riemannian gradient descent in the smooth case. When the bound reduces to the Boumal–Absil–Cartis rate (Remark 5.6). Later proximal methods on matrix manifolds build on this analysis. Lemmas 5.1–5.3 are the reusable steps: descent of the subproblem, sufficient decrease after retraction, and the stopping test as a stationarity certificate.
The result is proved in the paper; it is not formalized anywhere. No proof assistant library contains the convergence theory of a proximal method on a matrix manifold. The mission produces a machine-checked version of the full chain from the subproblem to the iteration bound. Along the way it builds infrastructure that Mathlib lacks: the Frobenius geometry of as a trace formula, the tangent space and projection of the Stiefel manifold, and optimality conditions for convex problems restricted to a subspace.
The bookkeeping inequalities (Lemma 5.1, (5.5), the decrease estimate, the telescoping) are short computations once the right facts are available. The difficulty lies elsewhere.
A natural first idea is to restate everything for the Riemannian gradient and reuse smooth Riemannian results. That route does not work: is nonsmooth, and the argument runs in the ambient space through the Euclidean subdifferential.
Matrix (Fin n) (Fin r) ℝ.trace (Aᵀ * B) and the norm is its square root. No Mathlib matrix norm instance is used.ProjLikeRetr.Stiefel.stiefel.gradf, tied to it by derivatives along every line.Nat.ceil.Two encodings would trivialize the theorem, and the mission excludes both.
Lemma 5.2 as printed fixes and asserts the decrease for the accepted iterate. What its proof establishes is three separate facts: decrease at every trial stepsize , termination of the line search, and along a run. The mission states these three facts.
Contributions are welcome at every level: proofs of the milestones, and general lemmas such as the descent lemma for functions on , the optimality condition of a strongly convex problem on a subspace, and properties of the Stiefel tangent projection. Theorem numbers and pages refer to arXiv:1811.00980v2, the version read for this mission.