Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Complexity bounds for first-order methods (proximal gradient, forward–backward splitting, alternating minimization) rest on a quantitative description of how a function grows away from its set of minimizers. Two such descriptions are in common use. An error bound controls the distance to the minimizers by the function value; a Kurdyka–Łojasiewicz (KL) inequality controls the function value by the size of the subgradients, after a reparameterization . KL inequalities with an explicit are what the convergence-rate analysis of descent methods needs (Attouch–Bolte 2009, Bolte–Sabach–Teboulle 2014), while error bounds with explicit constants are known for many concrete problem classes (Hölderian bounds for convex polynomials, Hoffman-type bounds, the bounds surveyed by Pang 1997).
Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 165 (2017)) show that for convex functions on a Hilbert space the two notions coincide, with essentially the same function , as soon as has a mild regularity property they call moderate behavior. This mission formalizes that equivalence (Theorem 5 of the paper) together with the subgradient-curve results its proof rests on.
Timeline:
Let be a real Hilbert space and a proper, convex, lower semicontinuous function. Its minimizers form the set , assumed nonempty, and is normalized so that . The subdifferential of at is
and is the set of points where it is nonempty. For , is the element of least norm of ; for one sets . The band is , and is the ball of radius around .
A desingularizing function is an element of
satisfies the KL inequality on with if there, and the error bound with residual function if there. has moderate behavior if on for some .
A subgradient curve issued from is a curve with and for almost every ; its length between and is .
Let , , , and . Then
and, if on ,
Both directions form the single goal theorem.
and then converges strongly to a minimizer.
Theorem 5 makes the computation of desingularizing functions a matter of proving error bounds. Since every semi-algebraic or subanalytic has moderate behavior (Lemma 4 of the paper), any known error bound with such a residual function yields a KL inequality with the same function up to the constant , and through the complexity theorem of §4 of the paper an explicit iteration bound for subgradient descent sequences. The paper uses this route to obtain the linear rate of ISTA for -regularized least squares and complexity bounds for projection methods.
The result is proved in the paper; to our knowledge none of it is machine-checked. A formalization adds three things: a Lean development of the Brézis subgradient semiflow on a general real Hilbert space (cited, not proved, in the paper), a checked proof of the length estimate of Theorem 27, and the two directions of Theorem 5 on top of them. The semiflow results are reusable well beyond this paper: they underlie the continuous-time analysis of proximal and gradient methods.
Direction (ii) is elementary convex analysis. Direction (i) is not: the error bound is a statement about , while the hypothesis only constrains subgradients on a band, and the minimizer realizing the bound must be produced. The paper produces it as the strong limit of the subgradient curve from , which requires the existence and regularity theory of the nonlinear evolution equation in an infinite-dimensional Hilbert space (Theorem 1), the energy identity along the curve, and strong (not merely weak) convergence. In finite dimensions compactness would supply limit points; in a Hilbert space Bruck's theorem only gives weak convergence, and it is the length bound of Theorem 27 that upgrades it. Neither the semiflow nor absolutely continuous Hilbert-valued curves with their a.e. derivative calculus are developed in Mathlib to the extent this needs.
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; EReal with the published GammaZero f (never , somewhere finite, convex epigraph, lower semicontinuous) and the published subdifferential subgrad. is the hypothesis " and attains "; is argminSet f, is Metric.infDist.IsDesingularizer r0 φ for ; values outside are irrelevant, and is deriv φ, used only on .A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates and with a homomorphism , distinguish instances satisfiable in from instances not even satisfiable in the weaker . Approximate graph colouring (colour a graph with more colours than its chromatic number) is the standard example. For CSPs, the resolution of the Feder–Vardi dichotomy conjecture by Bulatov and Zhuk (FOCS 2017) ties tractability to the existence of polymorphisms satisfying non-trivial identities; for PCSPs no such dichotomy is known, and the question of which polymorphism families yield algorithms is open in general.
A polymorphism of a PCSP is a function mapping tuples of rows satisfying the strict constraints to columns satisfying the weak ones. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383v3, SIAM J. Comput. 2020) give a single algorithm, BLP+Affine, that decides every PCSP with infinitely many symmetric polymorphisms, and extend it to block-symmetric polymorphisms. As a corollary the same algorithm solves all tractable Boolean CSPs of Schaefer's dichotomy (2-SAT, Horn-SAT and its dual, linear equations mod 2).
Timeline, as recorded in the paper's introduction:
A signature is a set of symbols with arities . A relational structure on a finite domain gives, for each , a relation . A homomorphism is a map sending every tuple of , componentwise, into ; is a promise template when one exists.
An instance has variables and constraints , , where is a tuple of variables. is satisfiable in if some assignment sends every into .
A polymorphism of of arity is such that for every and every matrix whose rows lie in , applying to each column gives a tuple in . It is symmetric if it is invariant under all permutations of its arguments.
The Basic LP has rational unknowns , a distribution on for each variable, and , a distribution on for each constraint, linked by the marginal conditions when is the -th variable of . The affine relaxation is the same system of equations in integer unknowns , , with no sign constraints.
The BLP+Affine algorithm (Figure 1) finds a relative interior point of , rejecting if there is none; restricts the affine system to by forcing wherever and wherever ; and accepts if and only if the restricted system has an integer solution. It correctly solves (Definition 1) if it accepts every instance satisfiable in and rejects every instance unsatisfiable in .
The hypothesis is a property of the template alone; the conclusion quantifies over all instances.
The same conclusion when contains block-symmetric polymorphisms of arbitrarily large width: is split into blocks, each of size at least , within which is invariant.
Theorem 2 gives one algorithm that decides every PCSP with an infinite family of symmetric polymorphisms, without knowing or evaluating the polymorphisms; it subsumes the BLP-then-AIP algorithm of Brakensiek and Guruswami for Boolean templates and applies over any finite domain. Theorem 3 extends this to block-symmetric families, which covers nearly all known tractable Boolean PCSPs, including 1-in-3-SAT versus NAE-SAT, whose alternating threshold polymorphisms are block-symmetric but not symmetric.
The results are proved in the paper. No machine-checked formalization of PCSPs, polymorphisms or the Basic LP is known to exist; Mathlib has no theory of constraint satisfaction. This mission produces a formal model of promise templates, instances, polymorphisms, the two relaxations and the algorithm's acceptance condition, together with a formal proof of the correctness theorem. The same model is the starting point for the characterization theorem (Theorem 4) treated in the companion mission.
Completeness is routine. Soundness is the substance: from a rational LP solution and an integer solution of the refined affine system one must produce an actual assignment in , using a polymorphism whose arity is chosen only after the instance is known. The natural first idea, clearing denominators of the LP solution and feeding the resulting multiplicities to a polymorphism, needs a polymorphism of exactly the arity the denominators dictate; with polymorphisms of only some arities it fails, and the paper's introduction notes that the LP alone does not suffice there. An integer affine solution, on the other hand, may have negative entries, which are not multiplicities. The paper stresses that the affine system must be the one refined by the support of a relative interior point: an arbitrary solution of the unrefined lattice gives no control on where the negative entries sit. In the formalization, the counting step (the columns of the matrix built from the constraint multiplicities have the variable multiplicities) and the passage from equal multiplicities to equal values of a symmetric function require explicit combinatorics on finite tuples, and the existence of a maximal-support LP solution requires an averaging argument over the finite set of coordinates.
All declarations are in the namespace PCSPBLPAff.Symmetric. Conventions:
Fintype and DecidableEq; variables are Fin n, constraints Fin m, and a constraint's scope is a function Fin (ar R_j) → Fin n, possibly repeating variables.The acceptance condition must not be replaced by "the LP is feasible and has a solution", nor by an affine solution vanishing outside the support of an arbitrary LP solution; the first is a different algorithm and the second bypasses footnote 1.
Contributions welcome: proofs of the milestones, in particular the combinatorial lemma that a symmetric function takes the same value on tuples with the same multiplicities, and the averaging argument for maximal-support solutions; the block-wise version for Theorem 3.
Many noncooperative problems in communication networks, power markets and supply chains are stochastic Nash games. Each player minimizes an expected cost that depends on its own decision and on the decisions of its rivals, and the expectation can only be sampled, not evaluated. A natural distributed way to compute an equilibrium is the best-response scheme: each player repeatedly replies optimally to the rivals' current strategies. In a stochastic game an exact best response is itself an expectation-valued optimization problem, so a practical scheme replies inexactly, running a few stochastic gradient steps per reply. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyse three such inexact proximal best-response schemes: synchronous, randomized and asynchronous. For each they prove a linear rate of convergence and a bound on the total number of projected stochastic gradient steps.
This mission concerns the randomized scheme. In large games it is unrealistic for all players to update at every round; in the paper's model each player independently decides to update with probability . This is the game-theoretic analogue of randomized block-coordinate descent (Nesterov 2012; Richtárik–Takáč 2014). A local Poisson clock per player is a special case (Remark 5 of the paper). The synchronous scheme, the paper's Theorem 1, and the asynchronous scheme are separate missions of this series.
There are players. Player chooses in a compact convex set and minimizes
where is a random vector and the oracle returns sampled gradients with (Assumption 1). A Nash equilibrium is a profile in from which no player can lower its cost by deviating alone.
For the proximal best response to a profile is
The matrix has entries and , built from the extreme curvatures and . Assumption 2 is (spectral norm).
Algorithm 2. At major iteration , each player flips an independent coin with , independent of the past information (Assumption 3). If , the player replaces by an inexact proximal best response with
otherwise . The accuracy is tied to the number of updates the player has made so far. The reply is computed by projected stochastic gradient steps
from , where and is the diameter of . The analysis uses the weighted norm and the constants , and .
Let , , , , and , where . After major iterations, is an -NE, i.e. , and for every player
In the order the proof uses them:
Theorem 2 gives an explicit, non-asymptotic sample complexity for computing a Nash equilibrium of a stochastic game when only a random subset of players acts at each round. Its exponent quantifies the price of randomization: Remark 7 of the paper shows it reduces to the synchronous exponent exactly when every . Lemma 5 is the first linear-rate statement for inexact randomized best responses in this setting. The weighted-norm argument of App. A–B is the device that makes block-randomized fixed-point iterations contract.
The results are proved on paper. None of them has a machine-checked proof, and the platform holds no stochastic Nash game, proximal best-response map or randomized best-response scheme. A formal proof checks every constant of (34), including the interplay of the random inexactness with the random number of steps . The paper does not prove (5): it adapts it from Facchinei–Pang 2009. A formal proof of (5) closes that gap.
The conditional-expectation bookkeeping is where a naive argument fails. The accuracy and the step count are random, being functions of the past coins. The coin must be independent of both the past and the samples the player uses in round . The descent step (A.4) multiplies the coin with the inexactness error, and its factorization uses exactly this joint independence. Bounding the expected work requires the moment generating identities (B.3) and (36) of a binomial count, with two different constants (through ) and (through ). Merging them gives a false bound. Lemma 6 is a stochastic approximation estimate conditional on , at a random, -measurable centre . Applying the unconditional bound for strongly convex SGD pointwise is not enough. On the deterministic side, (5) needs a mean-value argument along a segment in the product space, using the mixed Hessian blocks.
Players are Fin N and player 's space is EuclideanSpace ℝ (Fin (n i)). Costs are functions of the whole profile. The Euclidean norm of the vector of block norms and the weighted norm are written out explicitly, since Lean's norm on the product type is the sup norm. is the operator norm on Euclidean . is an infimum of Rayleigh quotients. The proximal best response is any map satisfying the argmin property on . is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. Randomness lives on a probability space with a filtration , and conditional expectations are Mathlib's condExp.
Statement repairs, all recorded in the items' Formalization Notes:
A formalization in which the coins are almost surely is the synchronous scheme, not this one. Coins and samples here are genuinely random with the stated laws and independence, and the expectation bounding the work is taken over both.
Reusable infrastructure includes the conditional bound for projected SGD on strongly convex problems (Lemma 6), the binomial moment identities (B.3)/(36), and Lemma 2 and (30). Contributions of intermediate lemmas, such as (A.4)–(A.5), (B.2) and the measurability of the iterates, are welcome as separate theorems.
Many equilibrium problems in operations research have the form of a stochastic Nash game: each of players minimizes an expected cost that depends on the strategies of the others, and the expectation can only be sampled. The paper's introduction lists applications in generation-capacity and power markets and in communication networks (Abada, de Maere d'Aertrycke and Smeers, 2017; Başar, 2007). A natural way to compute an equilibrium is a best-response scheme: each player repeatedly re-optimizes against the current strategies of its rivals. In a large network the players cannot synchronize. They update at different times and see their rivals' strategies with delays.
Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in three regimes: synchronous, randomized and asynchronous. This mission formalizes the asynchronous one (§5 and Appendix C). It adapts the partially asynchronous iterations of Bertsekas and Tsitsiklis (1989) to stochastic games with inexact, sampled best responses, and it gives an explicit bound on the number of stochastic gradient steps each player needs.
Player chooses in a nonempty compact convex set . A profile is . Player 's cost is , which is convex and twice continuously differentiable in a neighbourhood of . A sampling oracle returns , whose second moment is at most (Assumption 1). A Nash equilibrium is a profile in which each minimizes over .
For , the proximal best response of player to a profile is
The curvature constants and define the matrix with and . Assumption 5 (strict diagonal dominance) asks . It makes , the maximum absolute row sum, smaller than one.
The asynchronous scheme (Algorithm 3) runs on a deterministic schedule. At time the players in update. Player sees the outdated profile and computes with
The other players keep their strategies. Assumption 4 requires every player to update at least once in every consecutive times, and every delay to be at most . The accuracy is , where counts player 's updates so far. The inexact response is computed by projected stochastic gradient steps (43), with step size and . Write , and .
Let , , , and
where . After major iterations, , and player has taken at most
projected gradient steps.
In the order the proof uses them:
Theorem 3 makes the cost of asynchrony explicit. Bounded delays and a bounded update window enter only through the rate per window, . The overall effort stays polynomial in , and the paper's Table 1 summarizes the exponent as for a suitable choice of . The result connects classical partially asynchronous fixed-point theory with the sample-complexity analysis of stochastic approximation. Lemma 7 holds for any inexact solver that achieves the accuracy (38), not only for the stochastic gradient loop, so it applies to other subproblem solvers as well.
The paper proves these results by hand. As far as is known, no part of them has been machine-checked: there is no formal treatment of stochastic Nash games, of proximal best-response maps, or of asynchronous iterations with delays in Mathlib or on this platform. A formalization would check the induction over windows in Appendix C, whose index bookkeeping has several printed slips. It would also make precise which properties of the delays the argument needs.
The obvious argument does not carry over from the synchronous case. There, one step of the scheme contracts the whole error vector by in one norm. Here a step updates only some players, and each of them uses information up to steps old. No single step contracts anything. The proof has to show that every window of steps contracts the worst-case expected error by a factor , with the delays absorbed into the root . This requires a nested induction with case distinctions on the window position (Appendix C). The analysis also mixes three layers: a deterministic contraction of the exact best response; conditional expectations, Jensen's inequality and adaptedness for the inexact responses; and an stochastic-approximation bound for the inner loop, which in turn needs strong convexity, the first-order optimality conditions and nonexpansiveness of the projection.
Players are indexed by Fin N. Player 's space is EuclideanSpace ℝ (Fin (n i)), and costs are functions of the whole profile: is f i (Function.update y i z). The projection is any map satisfying the published predicate SpectralProjGrad.Shared.IsProjOnto. The proximal best response is a map constrained by an argmin predicate on . and are Rayleigh-quotient infima and suprema of second Fréchet derivatives, and is the maximum absolute row sum. The probability space carries a filtration to which the iterates are adapted. The inner-loop -algebras are parameters satisfying the inclusions the proof uses. Conditional expectations are Mathlib's condExp.
Statement repairs and implicit hypotheses, each recorded in the item it affects:
The special case , of Theorem 3, Corollary 3 (cyclic updates) and Theorem 4 are not stated.
The goal cannot be met trivially. The schedule is a parameter, not "every player at every step". The sampled gradients may be genuinely random, since the second-moment hypothesis is an inequality. is tied to by its argmin property, and is a Nash equilibrium. Each expectation in a conclusion is of a bounded measurable quantity, so it cannot vanish by non-integrability.
The development needs the following:
The projection and strong-convexity lemmas, and (5) itself, are reusable for the synchronous and randomized missions of this series. Proofs of individual milestones, or of general Mathlib-level facts such as the first-order optimality condition over a convex set, are welcome.
Regularized loss minimization (training a linear predictor with a convex loss and an penalty) covers support vector machines, ridge and logistic regression, and much of classical linear learning. A standard way to solve these problems at scale is dual coordinate ascent: optimize the dual problem one coordinate, i.e. one training example, at a time. Hsieh et al. (ICML 2008) reported that it can outperform stochastic gradient descent when moderately high accuracy is needed. Its theory, however, was unsatisfying (paper, §2): the known linear rates, adapted from Luo and Tseng's analysis of coordinate ascent, have a contraction factor that may be arbitrarily close to (it depends on the smallest nonzero eigenvalue of ), and they bound only the dual sub-optimality, which translates into a much weaker primal guarantee.
Shai Shalev-Shwartz and Tong Zhang (JMLR 14, 2013; arXiv:1209.1873) analysed stochastic dual coordinate ascent (SDCA), in which the coordinate is drawn uniformly at random, and bounded the expected duality gap, hence the primal sub-optimality, with explicit constants. For -smooth losses the bound is linear: iterations. This mission formalizes that result, the paper's Theorem 2.
Timeline:
Let , let be convex, and let . The primal problem is to minimize
The convex conjugate of is . The dual problem is to maximize
and the dual point determines the primal point . Weak duality gives for all , so the duality gap bounds the primal sub-optimality of .
A loss is -smooth if it is differentiable with a -Lipschitz derivative. Procedure SDCA starts from . At iteration it draws uniformly from , independently of the past, chooses to maximize
and sets , . Its outputs are the last iterate, the average with , or a random iterate from the same range. The paper's standing assumptions are , and .
For convex -smooth losses under the standing assumptions, and every ,
and, for ,
for the averaging and the random outputs. The constants are the paper's.
Theorem 2 shows that a stochastic method whose per-iteration cost is a single example converges linearly in the primal objective, through the duality gap, with a condition number that enters additively with rather than multiplicatively. This additive dependence is the benchmark against which later variance-reduced and accelerated methods (SVRG, SAGA, accelerated proximal SDCA, Katyusha) are compared. The duality gap is computable, so the bound also yields a stopping criterion.
The result is proved in the paper. As far as the platform's catalogue shows, no part of it, nor the smoothness/strong-convexity duality for scalar conjugates, has been machine-checked. The mission produces a checked statement of the rate with explicit constants and checked versions of the lemmas reused by the series' other two missions (Lipschitz losses, almost-smooth losses).
The proof is short on paper, but each step crosses between objects that Lean keeps apart. The conjugates are extended-valued: is off a bounded set for many smooth losses (logistic loss), so the dual objective, the coordinate step and the strong-convexity inequality all live in extended reals, and every passage to real arithmetic must be justified by finiteness along the run. The smoothness-to-strong-convexity step (milestone 1) is the classical duality, but Mathlib has no scalar conjugate calculus and no ready statement of it. The expectation is over the coordinate sequence, and the recursion compares expectations over histories of different lengths. The obvious attempt, a deterministic per-sequence bound, fails: the linear rate holds only in expectation.
Data are x : Fin n → EuclideanSpace ℝ (Fin d), φ : Fin n → ℝ → ℝ (convex), lam : ℝ with 0 < lam, and 0 < n. -smoothness is a derivative function φ' with HasDerivAt everywhere and . The conjugate conj and the dual dual are EReal-valued (⨆, never a real sSup). Dual values are converted to reals only under conjuncts asserting their finiteness. The SDCA step is a map Δ : (Fin n → ℝ) → Fin n → ℝ constrained by the argmax predicate IsSDCAStep, which is satisfiable. The run is a fold over an index sequence js : Fin T → Fin n from α⁽⁰⁾ = 0, and is the uniform average over all sequences (the published SAGA.Convex.expectIdx). Indices are 0-based. Lemma 1 and (10) are stated in the conditional one-step form at an arbitrary dual-feasible point, which implies the printed history-averaged form. The goal assumes no dual optimum; milestones 6–7 take a maximizer of as a hypothesis (it exists under the standing assumptions). The random output is stated over the iterates , which is what the proof bounds.
A trivializing formalization is ruled out: no statement takes the step, the conjugate or the expectation as an unconstrained variable, no real-valued toReal absorbs an infinite dual value, and the bounds are stated for the paper's exact iteration counts.
Needed infrastructure: scalar Fenchel conjugates in EReal (Fenchel–Young inequality and equality at subgradients), smooth/strongly convex duality, and averages over finite index sequences. The conjugate facts and the expectation bookkeeping are reusable beyond this mission, by the series' Lipschitz and almost-smooth missions in particular. Proofs of any milestone, and lemmas on EReal conjugates, are welcome.
Analysts of first-order optimization methods often know how quickly an error bound decreases as the number of iterations grows, but the bound may leave a substantial gap from the method's actual worst case at a fixed iteration count. This matters when comparing concrete methods or step sizes: an asymptotic rate alone does not determine which method has the smaller worst-case error after ten or twenty steps. A performance estimation problem asks for that fixed-count worst case over a specified function class, initial radius, method, and performance criterion. Taylor, Hendrickx, and Glineur show that, for a broad class of fixed-step methods, this question has an exact semidefinite formulation rather than merely a relaxation Taylor, Hendrickx & Glineur, 2016, §§1–3.
Work in Euclidean space with its usual norm and inner product. Fix . The class consists of convex functions for which is convex and any subgradients and satisfy . A subgradient here means that for every . The interpolation milestones also cover , using and Taylor, Hendrickx & Glineur, 2016, Definition 1, p. 5.
A fixed-step method uses coefficients chosen before seeing the function. Starting at , its iterates satisfy for . The coefficients are recorded in a lower triangular matrix . A minimizer and radius constrain the start by . The criterion uses coefficients and a symmetric matrix . Its function values are normalized as , and its Gram matrix comes from the columns . The value to maximize is Taylor, Hendrickx & Glineur, 2016, Definition 4 and §§3.2–3.3, pp. 12–13.
The semidefinite performance estimation program, denoted (sdp-PEP), instead chooses a positive semidefinite matrix and normalized values . For each ordered pair from , it requires , where the star value is zero. It also requires . The matrices and are the explicit coefficient matrices on page 13, computed from , , and Taylor, Hendrickx & Glineur, 2016, §3.3, pp. 13–14.
The main target is Theorem 5. Write for the supremum of the criterion over actual class members, minimizers, and fixed-step runs in , and for the (sdp-PEP) supremum. For every ,
The milestones follow the paper's path: convex interpolation (Theorem 1), curvature subtraction (Theorem 3 and Lemma 1), conjugate interpolation (Lemma 2), the exact pairwise interpolation criterion (Theorem 4), and the page 13 translation between that criterion, actual runs, and SDP feasible points. Theorem 4 states a necessary and sufficient condition for finite triples to be realized by one function in . The final two milestones require both directions of the correspondence between a function instance and a feasible SDP pair. These targets use the paper's fixed constants and its full ordered-pair index set Taylor, Hendrickx & Glineur, 2016, Theorems 1, 3–5 and §3.3, pp. 7–14.
The equality means an SDP optimum is the exact worst-case value for the stated dimension range, for every linear criterion of this form. A feasible SDP point can represent a concrete adverse function and run when its rank fits the dimension; a dual certificate can supply an upper bound. The paper also gives a rank-constrained formulation below dimension , so the dimension threshold has a precise role rather than being a technical ornament Taylor, Hendrickx & Glineur, 2016, Theorem 5 and Proposition 2, pp. 14–15.
The result is already proved in the cited paper. The formalization task is to give its definitions, interpolation claims, matrix constraints, and two-way correspondence machine-checkable statements and eventually proofs. The subgradient predicate, finite interpolation interface, and Gram-matrix representation are reusable beyond this mission. Formalized instances can then support verified worst-case calculations for particular methods and choices of and .
Sampling a smooth convex function at finitely many points gives necessary inequalities, but arbitrary triples satisfying familiar local smoothness or convexity bounds need not come from one common function. Theorem 4 supplies a simultaneous criterion over every ordered pair. The next obstacle is that the function-level problem contains whole functions and iterates, while the SDP retains only normalized values and inner products. Its matrix must encode every iterate relation and interpolation condition, and its rank determines whether those inner products can be realized in . Dropping the rank condition below changes the problem Taylor, Hendrickx & Glineur, 2016, §§2–3.
Lean uses EuclideanSpace ℝ (Fin d) and the ordinary Euclidean inner product. A general subgradient has its defining inequality; FClass records Definition 1, and Interpolable quantifies over a single class member realizing all finite data. The SDP file defines the fixed-step run, the coefficient vectors and matrices, Gram matrices, the criterion, feasibility, and both optimal values. The values lie in EReal, preserving empty or unbounded suprema. The function-level problem explicitly quantifies over a minimizer and actual runs. A gradient appears in a run only in the finite- regime, where the class is differentiable. The theorem requires , , symmetric, , and .
The original Definition 1 allows proper closed functions taking , and Definition 2 allows an arbitrary index set. This mission uses real-valued functions and finite interpolation data. For the finite- result, the paper notes that functions in its class have full domain; its interpolation constructions also yield real-valued functions. The SDP coefficients and do not have values at under the paper's two stated conventions, and Remark 4 confines the later SDP analysis to finite Taylor, Hendrickx & Glineur, 2016, pp. 5, 14. The radius domain is explicit because the SDP constraint squares : a negative radius would admit in the SDP while excluding every actual start.
The goal cannot be met by a junk gradient, a real-valued supremum with a default at an empty or unbounded set, omitting the minimizer, allowing , or discarding the rank requirement at small dimensions. Contributions that establish the interpolation equivalences, the matrix identities, Gram realization, and the two directions of instance correspondence directly advance the goal.
A cycle cover of a graph is a collection of cycles that together use every edge at least once. Covering the edges of a network by closed tours appears in routing and inspection problems (the Chinese postman problem is the closed-walk version), and the minimum total length of a cycle cover is a classical extremal parameter of bridgeless graphs. Alon and Tarsi (Covering multigraphs by simple circuits, SIAM J. Algebraic Discrete Methods 6, 1985, pp. 345–350; reference [2] of the paper) conjectured that every bridgeless graph with edges has a cycle cover of length at most (Conjecture 7.1 of the paper).
The question is closely tied to cycle double covers (CDCs): families of cycles covering every edge exactly twice. The Cycle Double Cover Conjecture of Szekeres and Seymour asserts that every bridgeless graph has one, and it suffices to prove it for cubic graphs. Brinkmann, Goedgebeur, Hägglund and Markström (Generation and properties of snarks, arXiv:1206.6690v3, 2013; J. Combin. Theory Ser. B 103, 2013) generated all snarks on up to 36 vertices and tested these conjectures on them. Section 7 of their paper derives cycle-cover bounds from double covers. For colourable cubic graphs (those with a proper 3-edge-colouring) the argument gives the bound , and the authors conjecture (Conjecture 7.4) that holds for all snarks. This mission formalizes the colourable bound and the chain of statements behind it.
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 a vertex receive different colours.
A cycle is a 2-regular connected graph. Inside a graph a cycle is recorded by its edge set , with distinct and ; its length is . A 2-regular subgraph of is an edge set such that every vertex lies on none or exactly two edges of : a union of vertex-disjoint cycles, possibly empty and not necessarily spanning. A 2-factor is a spanning 2-regular subgraph. An even subgraph is an edge set such that every vertex lies on an even number of edges of .
A cycle double cover of is a multiset of cycles such that every edge lies in exactly two of them. It is a -CDC if the cycles can be coloured with colours so that cycles sharing an edge get different colours. Each colour class is then an even subgraph, and following the paper the -CDC is written as a family of even subgraphs with every edge in exactly two of them, counted with multiplicity.
A cycle cover of is a set of cycles of such that every edge lies in at least one of them, and its length is . Throughout, denotes the number of edges of .
For every colourable cubic graph with edges there is a cycle cover with
Equivalently, the shortest cycle cover of has length at most .
The bound is far below the Alon–Tarsi bound and is attained up to lower-order terms on the snarks the paper enumerates (Corollary 7.3, which rests on a computer search and is not part of this mission). It isolates the colourable case of Conjecture 7.4, so any proof of that conjecture must at least reproduce it. Proposition 5.3 is a strong form of the Strong Cycle Double Cover Conjecture for colourable cubic graphs: every 2-regular subgraph, not only every cycle, is a colour class of a 4-CDC. Lemma 7.2 is the general device that turns a double cover containing a long 2-regular subgraph into a short cycle cover; the paper applies it again with long cycles of snarks.
On the formal side, none of these objects exists in Mathlib or on the platform: there is no cycle double cover, no cycle cover, and no decomposition of even graphs into cycles (Veblen's theorem). Mathlib has walks, cycles as walks (Walk.IsCycle), Eulerian trails and the predicate IsCycles, but the step from an even edge set to a family of edge-disjoint cycles is missing. The results of this mission are all proved in the paper or classical; none has a machine-checked proof.
The arithmetic of the goal is immediate once the pieces exist: a 3-edge-colouring of a cubic graph on vertices consists of three perfect matchings, two of which form a 2-factor with edges, and . The work lies elsewhere.
First, Veblen's theorem must be formalized: an even edge set is a union of edge-disjoint cycles. This requires extracting a cycle (a walk with no repeated vertex) from a nonempty even edge set and inducting on the number of edges; the bookkeeping between walks, their edge lists and finite edge sets is where formal proofs of this kind spend their effort. Lemma 7.2 needs it, because the colour classes of a CDC are even subgraphs, while a cycle cover consists of cycles.
Second, Proposition 5.3 needs the passage from a proper 3-edge-colouring (a colouring of the line graph) to three perfect matchings and to the three 2-factors formed by pairs of colours, and then a parity check that the symmetric differences with are even and cover every edge exactly twice. A tempting shortcut fails: the three pairwise unions of colour classes already form a 3-CDC, but a prescribed 2-regular subgraph need not be one of its classes.
Graphs are SimpleGraph V on a finite type V with decidable equality and decidable adjacency. Cubic is G.IsRegularOfDegree 3. Colourable is G.lineGraph.Colorable 3, a proper vertex colouring of the line graph, never a vertex colouring of G. Edges are Sym2 V, and every subgraph is recorded by its finite edge set. A cycle is the edge set of a closed walk satisfying Walk.IsCycle, of length its number of edges. A -CDC is a function Fin k → Finset (Sym2 V) of even edge sets with every edge of G in exactly two indices, so repeated and empty classes count correctly. A cycle cover is a Finset of cycles covering every edge, of length ∑ C ∈ F, C.card.
"The shortest cycle cover has length at most " is stated as "some cycle cover has length at most "; the two agree because a finite graph has finitely many cycle covers. Bounds are kept in without subtraction or division: the goal is , and Lemma 7.2 is . Lemma 7.2 is stated for a CDC given as a family of even subgraphs, the form in which the paper applies it (with a 2-factor that is a colour class of a 4-CDC); a CDC of single cycles is a special case. The cubic hypothesis of Lemma 7.2 is kept as printed although the argument does not use it.
The bound becomes trivial if a "cycle" is weakened to an even edge set or to the edge set of a closed walk, since then the single set is a cover of length . The cycles here are genuine cycles of G.
Out of scope: Corollary 7.3 (the cycle-cover lengths of all snarks on at most 36 vertices) and every other statement resting on the exhaustive enumeration, Conjectures 7.1 and 7.4, and the Strong Cycle Double Cover material of §5.1 and §6.
Reusable infrastructure: cycles as edge sets, even subgraphs, -CDCs, cycle covers and Veblen's theorem are general graph-theoretic objects, useful well beyond this paper (for flows, the Cycle Double Cover Conjecture, and Eulerian subgraph arguments). Proofs of Veblen's theorem and of the passage from a 3-edge-colouring to perfect matchings are particularly welcome.
A snark is a cubic graph that cannot be properly edge-coloured with three colours and that does not reduce to a smaller such graph. Snarks are the smallest possible counterexamples to several central conjectures about cubic graphs, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture, so structural statements about snarks narrow the search for counterexamples to those conjectures.
Permutation graphs are cubic graphs built from two disjoint cycles of equal length joined by a perfect matching, so that the two cycles are induced. The Petersen graph is the classical example: its outer 5-cycle and inner pentagram are joined by five spokes. In his monograph Integer Flows and Cycle Covers of Graphs (1997), C.-Q. Zhang conjectured that the Petersen graph is the only permutation snark that is also cyclically 5-edge connected.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, J. Combin. Theory Ser. B 103, 2013) built a generator for snarks and enumerated all snarks up to 36 vertices. Among them they found twelve cyclically 5-edge-connected permutation snarks on 34 vertices, which refute Zhang's conjecture (Observation 4.2), and they printed all twelve in Appendix 8.6 of the paper. This mission formalizes the refutation using the first of those graphs.
All graphs are finite and simple. A cycle is a 2-regular connected graph. A graph is cubic if every vertex has degree 3. A 2-factor of is a spanning 2-regular subgraph. The girth is the number of vertices in a shortest cycle of .
A cubic graph is colourable if it has a proper 3-edge-colouring: a map giving distinct colours to distinct edges with a common endpoint. Otherwise it is uncolourable.
A graph is cyclically -edge connected if deleting fewer than edges from never leaves two distinct components that both contain a cycle.
A snark is an uncolourable, cyclically 4-edge connected cubic graph with .
A cubic graph is a permutation graph if it has a 2-factor consisting of two induced cycles. Equivalently, its vertex set splits as with both induced subgraphs and cycles. A permutation snark is a snark that is a permutation graph.
The Petersen graph is the graph on with the outer cycle , the spokes , and the inner pentagram .
Zhang's Conjecture 4.1. Let be a cubic cyclically 5-edge-connected permutation graph. If is a snark, then must be the Petersen graph.
The witness is the first graph in Appendix 8.6 (p. 36). It is given as a list of higher-numbered neighbours of the vertices ; decoded, it has 51 edges. In the Lean development the paper's vertex is i - 1 : Fin 34.
that is, there is a finite cubic, cyclically 5-edge connected permutation snark that is not isomorphic to the Petersen graph. This is SnarkGen.Zhang.observation_4_2.
Each milestone is a property of asserted by the heading of Appendix 8.6, "The 12 cyclically 5-edge connected permutation snarks on 34 vertices":
The goal follows from milestone 7 directly. Two supporting theorems are included: cyclic -edge connectivity is monotone in , and the paper's remark (p. 9) that every permutation snark has order .
Zhang's conjecture predicted that the Petersen graph is isolated among highly connected permutation snarks. Its refutation shows that this is false, and the twelve 34-vertex graphs went on to serve as counterexamples to further conjectures in the same paper (Conjectures 5.17, 5.20 and 5.21, about cycle double covers containing a prescribed 2-factor). They are also listed in the House of Graphs database.
The refutation in the paper is a computer result: the graphs were found by an exhaustive search, and their properties were checked by programs. A formal proof would replace that check with a machine-verified one that is independent of the generator. It would also produce reusable certified tools for finite cubic graphs: a kernel-checked test for uncolourability, cyclic edge connectivity, and girth. No machine-checked proof of any of these properties of is known to exist.
The statements are short, but none of the properties of follows from a general theorem; each must be checked on the specific graph. The obvious approach, to unfold the definitions and let a decision procedure enumerate, does not scale:
The definitions are stated in terms of Mathlib's general notions (line graphs, walks, connected components), not in terms of a computable representation. Connecting them to an efficient computation is the main work.
Graphs are SimpleGraph V with [Fintype V]. The conventions are as follows.
G.lineGraph.Colorable 3, a proper 3-colouring of the line graph. It is not a vertex colouring of .S ⊆ G.edgeSet with S.card < k. Components and cycles are taken in G.deleteEdges S.5 ≤ G.egirth, the extended girth, which is for acyclic graphs.Type and reads "must be the Petersen graph" as Nonempty (H ≃g petersen).The conjecture keeps every printed hypothesis, including the redundant "cubic". Dropping "permutation graph" or "cyclically 5-edge connected" would make the refutation easier, since other cyclically 5-edge-connected snarks are known. The cyclic connectivity must be computed in the graph after deletion and must require both components to contain a cycle; otherwise it degenerates into ordinary edge connectivity, which is at most 3 for cubic graphs and would make the conjecture vacuous.
Proofs should be checked by the Lean kernel. The decision procedures for colourability and cyclic connectivity are the reusable part of this mission, and contributions that build them for arbitrary finite cubic graphs are welcome.
Out of scope.
Many stochastic differential equations used in physics, biology and Bayesian sampling are ergodic: their law converges to an invariant measure , and quantities of interest are averages . Estimating such averages by simulation requires a numerical method whose accuracy does not deteriorate as the simulated time grows. Two obstacles meet here. First, the drifts of interest (the FENE polymer model, Langevin dynamics with polynomial potentials) are not globally Lipschitz, and for such drifts the explicit Euler–Maruyama method with a uniform timestep has moments that blow up as the step tends to zero (Hutzenthaler, Jentzen, Kloeden 2011). Second, standard strong error bounds grow exponentially with the time horizon, which makes them useless for long-time averages.
W. Fang and M. B. Giles (Ann. Appl. Probab. 30 (2020) 526–560) answer both with an adaptive timestep: the step is chosen from the current state, small where the drift is large. On a finite interval they prove strong convergence of order ; for a class of contractive ergodic SDEs they prove that the moments of the numerical solution and its strong error are bounded uniformly in time. The second result is the subject of this mission. It underlies the paper's multilevel Monte Carlo estimator for invariant measures.
Earlier work on the same problem used tamed schemes, which modify the drift instead of the step: Hutzenthaler, Jentzen, Kloeden 2012 on finite intervals and Sabanis 2016 with a time-uniform rate. An adaptive Euler–Maruyama scheme of a different form, with error control, was shown to converge and to be stable by Lamba, Mattingly, Stuart 2007.
Let carry a filtration and a -dimensional standard Brownian motion with respect to it. On (Euclidean norm , inner product ) consider
with drift and diffusion ; matrices carry the Frobenius norm .
Given a timestep function , the adaptive Euler–Maruyama scheme is
For let be the last grid time not after . The piecewise-constant interpolant is and the continuous interpolant is .
The hypotheses are:
Under Assumption 9, with bounded, satisfying Assumption 8 and satisfying Assumption 3, for every there is such that, with computed with timestep ,
The constant is fixed before and ; uniformity in is the content of the theorem.
The remaining step from (52) to Theorem 6 is a time-uniform bound , obtained as in the finite-time analysis of §6.2.
Theorem 6 says that the adaptive scheme tracks the true solution with error of order forever, not merely on a fixed window. Combined with ergodicity, it bounds the bias of long-time averages of the scheme uniformly in the averaging horizon, which is what the paper's adaptive multilevel Monte Carlo method for invariant measures (§3) needs. Theorem 5 is of independent use: it shows that the adaptive scheme preserves the time-uniform moment bounds of a dissipative SDE, a property the uniform-step Euler scheme lacks for superlinear drift.
All results here are proved in the source; none is open. To our knowledge none has a machine-checked proof. A complete formalization would give the first verified strong convergence result for an adaptive-step SDE scheme, and the infinite-horizon energy estimates (45)–(47) and the error inequality (52) would be the first verified time-uniform estimates of this kind.
The timestep is random and depends on the state, so the grid times are stopping times rather than fixed numbers, and the number of steps up to time is random. Standard discrete Grönwall arguments, which iterate over a deterministic grid, do not apply directly; neither does the usual argument that the scheme is an Itô process with adapted, piecewise-constant coefficients, which must be rebuilt for random grids.
The obvious route to a time-uniform bound — a finite-time bound with constant followed by — fails because grows exponentially. Uniformity has to come from an exponential weight ( in (45)–(47), in (52)) that converts dissipation or contractivity into a bound that survives division by the weight, with every constant independent of and of the timestep function.
The state space is EuclideanSpace ℝ (Fin m); diffusion values are EuclideanSpace ℝ (Fin m × Fin d), whose norm is the Frobenius norm. Times are in ℝ≥0, grid indices start at , and is deterministic. The grid is defined by recursion; the index is the least with and equals the junk value on the event that the grid never passes (a null event under the hypotheses). Moments are lower Lebesgue integrals ∫⁻ … ‖·‖ₑ ^ p in with real exponents, never Bochner integrals. A solution on is a process that solves the SDE on every horizon , in the sense of the published definition SabanisEuler.Shared.IsSolution. Existential constants are placed before every quantifier they must not depend on: before in Lemma 3, before , , and in Theorem 5, before , , , and in Step 2, before and in Theorem 6. A constant chosen after , or a moment that is a Bochner integral of a possibly non-integrable function, would make these statements trivial; both are ruled out. Pages are the journal's printed pages (PDF page + 525).
Two deviations from the printed text are deliberate. Theorem 6 additionally assumes : its proof invokes Theorem 5, whose Assumption 7 contains this bound, which Assumption 9 does not imply, and the introduction (p. 527) assumes "a bounded and non-degenerate diffusion coefficient". Each is assumed measurable. Separately, the printed (47) has in its last term; the formalized inequality uses , as the expansion and the source's (48) require. The undefined word "nondegenerate" in Assumption 7 is not encoded.
A full development needs the Itô formula for applied to Itô processes with random-grid coefficients, the Burkholder–Davis–Gundy inequality, and moment bounds for Brownian increments over stopping-time intervals. These are reusable well beyond this mission. Contributions of any of them, or of proofs of the deterministic inequalities (45) and (47), are welcome.
A retailer that decides which products to put on a shelf, or an airline that decides which fare classes to open, faces an assortment problem: the set of products offered changes which product a customer buys, and the firm wants the offer set that maximizes expected revenue. When customers first pick a category (a brand, a store aisle, a flight time) and then a product within it, the standard choice model is the nested logit model of Williams (1977) and McFadden (1978). Real offer sets are constrained: a shelf section displays at most a fixed number of products, and that limit is set per category.
Gallego and Topaloglu (Management Science, 2014) study assortment optimization under the nested logit model when the assortment in each nest must satisfy a cardinality or a space constraint. Their method reduces the joint problem over all nests to a small linear program, provided that each nest admits a short list of candidate assortments that always contains an optimal solution of a one-parameter single-nest subproblem. This mission formalizes the cardinality case, where the paper shows such a list of candidates exists. For a single nest and the multinomial logit model, the cardinality-constrained problem was solved earlier by Rusmevichientong, Shen and Shmoys (Operations Research, 2010).
There are nests and products in every nest. Product of nest has a preference weight and a revenue . An assortment of nest is a subset (the paper writes it as a vector ; the empty assortment is ). The total preference weight and the expected revenue of nest given that the customer chooses it are
with . Under cardinality constraints the feasible assortments of nest are
where is the maximum number of products that can be offered in nest .
For a parameter , the paper's single-nest problem (7) is
By identity (8), its objective equals , so under cardinality constraints (7) is the unit-weight knapsack problem (9)
The utility lines of the products are for , together with .
For every nest there is a collection , fixed before is chosen, with
such that for every some is an optimal solution of problem (7):
The paper states . The goal pins this to , which the paper's count of the intersection points of the utility lines supports, and leaves the exact constant unfixed beyond that.
Combined with the paper's Theorem 4 (candidates containing an optimal solution of (7) for every contain an optimal combination for the full problem) and Theorem 2 (the best combination of candidates is found by a linear program), Theorem 5 shows that the nested logit assortment problem with per-nest cardinality limits is solved exactly by a linear program with variables and constraints. The same parametric argument, in which a one-dimensional parameter sweeps the line and the combinatorial optimum changes only at intersection points of finitely many lines, recurs in the paper's treatment of space constraints and of joint assortment and pricing.
The result is proved in the paper; it has no machine-checked proof. A formal proof also makes explicit two points the paper leaves to the reader: that a solution optimal on an open interval of remains optimal at its endpoints, and how ties between utilities are handled.
The parameter ranges over an uncountable set, and the number of feasible assortments, , is exponential in when grows with . Taking the candidates to be all of satisfies everything except the size bound, and choosing a different collection for each satisfies the size bound trivially. The content is the uniform bound with the collection chosen first. The step that needs care is passing from "the optimum does not change inside an interval between breakpoints" to a statement covering every , including the breakpoints themselves, where ties occur and the greedy choice is not unique.
Fin n (0-based); assortments are Finset (Fin n) and is ∅; is a natural number.NestedLogitVariants.LP.Instance, with V, R from NestedLogitVariants.LP.Model. That model carries a within-nest no-purchase weight vnp i; every statement assumes vnp i = 0, which is this paper's model, so V I i S = ∑ j ∈ S, I.v i j. The paper's extension (p. 15) is not formalized.ConstrNestedLogit.Card.Knapsack defines , the objective of (9), and optimality for (7) and (9) over .The goal cannot be satisfied by an unbounded collection ( is excluded by the bound ), by a collection chosen after (the collection is quantified first), or by a special case of the constraint: is arbitrary, and the optimal member must beat every assortment of , not only the other candidates.
Contributions welcome: proofs of the three milestones and the goal; a general lemma that finitely many affine functions of one real variable keep a fixed weak order and sign pattern between consecutive pairwise intersection points, which is reusable for the paper's §5 and §6 and for other parametric optimization results.
A retailer chooses which products to offer, knowing that what customers buy depends on what is on the shelf. In the nested logit model (Williams 1977) products are grouped into nests, and a customer first picks a nest (or leaves) and then a product inside it. Choosing the offer set to maximize expected revenue is the assortment problem. In practice each nest carries its own limit: at most products (a cardinality constraint) or a shelf of size (a space constraint). Gallego and Topaloglu (2014) show that the problem with cardinality constraints is solvable in polynomial time, and that the problem with space constraints, which is NP-hard, admits approximation guarantees.
The paper's method has two parts. The first (Theorem 2, mission 1 of this series) finds, by a small linear program, the best assortment that can be stitched together from given candidate assortments in each nest. The second, which this mission formalizes, says when such candidates are good enough: it reduces the multi-nest problem to a family of single-nest problems with a linear objective, one for each threshold . The authors call the two results the pivot of their approach; every later section of the paper (cardinality, space, joint pricing, the approximation scheme) invokes Theorem 4.
There are nests and products . Product in nest has preference weight and revenue (no sign is assumed); the no-purchase option has weight ; nest has a dissimilarity parameter . An assortment in nest is a set ; the empty assortment is written . Define
and the expected revenue per customer of the assortment ,
Each nest has a set of feasible assortments, and problem (1) is
with optimal solution . For a threshold , problem (7) of nest is
whose objective equals and so is linear in the assortment. An -approximate solution of (7) at is some with for every . A candidate collection of nest is a set .
Let . If, for every nest , the candidate collection contains an -approximate solution of (7) for every , then there is with each a candidate and
The collection is fixed before ; the conclusion holds for any constraint family, any and any .
Milestones 1–3 are steps of the proof of Lemma 3, in the order the proof uses them; Lemma 3 holds at the single, unknown thresholds , and Theorem 4 is its threshold-free form.
The result. Theorem 4 turns the combinatorial problem (1), whose objective couples all nests through a ratio and through the powers , into a family of single-nest problems with a linear objective, one per threshold. A candidate collection that is good for every threshold is then fed to the linear program of Theorem 2, with variables and constraints. The paper builds an exact collection of candidates per nest under cardinality constraints (Theorem 5), a factor- and a factor- collection under space constraints (§5), an exact collection for joint assortment and pricing (§6), and a polynomial-time approximation scheme (Theorem 9); each of these rests on Theorem 4. The paper also notes (p. 15) that the argument uses only , so it extends to a within-nest no-purchase option of the form ; that extension is not formalized here.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. A formal proof supplies the reduction that the other missions of this series (cardinality, space, pricing, the approximation scheme) need to turn their per-nest statements into guarantees for problem (1). The related criterion of Davis, Gallego and Topaloglu (2014, Theorem 1), already on the platform for the unconstrained problem, is a different route to a factor and does not imply Theorem 4.
The obvious approach compares the approximate and the optimal assortment nest by nest, but the objective is not separable: is a ratio, and each nest enters through , not . Problem (7) has no power , so a solution that is good for (7) is not obviously good for the nest's contribution . The threshold at which the comparison works depends on and , which are unknown, and it is not itself when . A further subtlety is the empty assortment: a nest offering nothing has , where the factor is not finite, so the case split on the sign of and the positivity of have to be handled before any division.
NestedLogitVariants.LP.Model (referenced, not redefined). Every statement sets its within-nest no-purchase weight to zero (I.vnp i = 0), so V is the paper's .Fin n, indexed from . Assortments are Finset (Fin n); is ∅. via , the paper's convention. Powers are Real.rpow, with for .C : ι → Set (Finset (Fin n)), covering cardinality and space constraints alike. Candidate collections are sets A i ⊆ C i; the index set is not named and no finiteness is required.revenue I Sstar for a hypothesised optimum Sstar (IsOptimal1: feasible, and at least the revenue of every feasible assortment), not a defined maximum.Real.rpow with exponent in .A retailer that sells products in several categories has to decide which products to put on display. Under the nested logit model a customer first picks a category (a nest) and then a product inside it, so offering a product changes the purchase probabilities of every other product. Choosing the assortment that maximizes expected revenue is assortment optimization, a standard problem of revenue management. Gallego and Topaloglu (Management Science, 2014) study it when every nest carries its own constraint on the assortment. With a limit on the shelf space of each nest the problem is NP-hard even for a single nest, so the paper builds an assortment that is guaranteed to earn at least half of the optimum.
A worst-case factor of two says little about one concrete instance. For its computational study (§7.1) the paper therefore needs, instance by instance, a number that is provably at least the optimal expected revenue, and it obtains one from a linear program, (13), whose constraints come from the linear programming relaxations of knapsack problems. Proposition 7 (Online Supplement A, p. 33) proves that this linear program does give an upper bound. This mission formalizes that proposition.
There are nests and products in each nest. Product of nest has a preference weight and a revenue (any real number); is the preference weight of buying nothing, and is the dissimilarity parameter of nest . For an assortment of nest put
with for the empty assortment . The expected revenue of is
Under space constraints product of nest uses units of space and nest has capacity , with for every product, so the feasible assortments are . Problem (1) is .
For a scalar , the knapsack problem (10) of nest maximizes over with . Its linear programming relaxation allows . The paper partitions into finitely many intervals , , on each of which one vector solves the relaxation. For a fractional vector it writes and .
The linear program (13) in the variables is
If is an optimal solution of (13), then
The proposition makes the optimality gaps of §7 meaningful: the expected revenue of any assortment that respects the space constraints, divided by the optimal value of (13), is a certified lower bound on its fraction of . The bound is a linear program with variables and one constraint per interval solution, so it can be solved for instances where itself, an NP-hard quantity, cannot be computed.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it checks the interplay of three ingredients that the paper treats briefly: the role of the interval solutions (only their feasibility and their optimality for every matter), the extension of and to fractional vectors, and the concavity of . A related but different program is Davis, Gallego and Topaloglu's LP (16) (NestedLogitVariants.LP.lp16_upper_bound), which bounds the unconstrained problem by another argument.
The constraints of (13) are indexed by finitely many fractional vectors, while is attained at an integral assortment that need not be among them. The obvious argument, that (13) is a relaxation of an exact linear-programming formulation of problem (1), does not apply: no constraint of (13) involves directly. The link between the two has to be made nest by nest, through the knapsack relaxations at values of that depend on the unknown optimum, and the fractional vectors are compared with integral assortments through the nonlinear map .
The formalization references the published nested logit model NestedLogitVariants.General.Model (instance, , , , ) and NestedLogitVariants.General.Relaxation (the unit box and the term of the constraints of (13)). The conventions are:
Fin n, indexed from ; assortments are finite sets of products and is the empty set;Real.rpow, and , which gives as in the paper and makes the constraint term at equal to ;The statement is not to be trivialized: setting , taking to be the whole box (not a finite set and not LP (13)), assuming , or proving the bound for one particular feasible point are all excluded.
A complete development needs the concavity (tangent-line) inequality of at a positive point and elementary facts about fractional knapsack relaxations; both are reusable. Proofs of the milestones and of the goal are welcome.
The Frank–Wolfe algorithm minimizes a smooth convex objective over a compact convex domain by choosing an atom through a linear optimization problem and moving toward it. On a domain that is the convex hull of atoms, each ordinary iteration introduces at most one new atom. That makes the method useful when a solution represented with few atoms is valuable, but it raises a basic question: how much accuracy can a solution with only a few atoms attain? Jaggi's 2013 analysis gives upper bounds on primal error and duality gap for four Frank–Wolfe variants. Its sparsity section supplies a matching obstruction on the unit simplex. This mission isolates that obstruction so the claimed dependence on sparsity can be checked independently of any particular implementation of the algorithm.
The paper calls the number of used atoms the sparsity of an iterate. It proves two lower bounds for one quadratic objective: a sparse point cannot have arbitrarily small objective value, and, with fewer active coordinates than the simplex dimension, it cannot have arbitrarily small duality gap. These are worst-case statements about feasible points themselves. Consequently, any method whose iterates retain the stated sparsity is subject to them, regardless of how it selects its next atom. The source statements and constants are Lemma 3 and Lemma 4, PDF p. 5.
Let be a positive integer and let the unit simplex be
For a vector , let be the number of nonzero coordinates. The objective is the squared Euclidean norm . Its minimum on the full simplex is , reached at the uniform point. The paper compares that optimum with the best value permitted by a bound on . The dimension and sparsity budget are separate: the goal assumes , so at least one coordinate must be zero at every eligible point.
The duality gap at a feasible is
For a convex objective, this gap bounds the difference between the current objective value and the optimum; the paper introduces that certificate in display (2), PDF p. 2. Here the maximum exists because the simplex is nonempty and compact and the expression is continuous in . It is the same certificate computed by minimizing a linear function over the domain in a Frank–Wolfe step. The paper's Table 1, PDF p. 6 identifies the simplex linear subproblem with choosing a coordinate having the largest coefficient.
For , Lemma 3 asserts an attained minimum:
The associated primal-error statement says that a point with exactly nonzero coordinates has , where is an optimizer on the full simplex. The minimum and the primal-error reading are both included as draft theorems.
For every natural number , Lemma 4 states the mission goal:
The threshold is essential to this exact value. If all coordinates may be active, the uniform optimizer has zero gap. The case is formally allowed by the paper's natural-number wording, but has no eligible simplex point. The formal statement keeps the paper's quantifier order and does not add a positive- hypothesis.
Three milestones accompany the goal. The first records that an atomic set and its convex hull have the same support function. The second records the simplex support value from Table 1. The third is Lemma 3's attained sparse minimum. They are stated as mathematical claims independent of any algorithmic running-time assertion.
The source's convergence analysis gives error guarantees that decrease with the number of iterations, while its simplex example shows that using only atoms leaves primal error at least and, for , gap at least . Together they delimit what the paper's sparsity guarantees can achieve. The duality-gap claim concerns a certificate of approximation quality, so it applies even when the optimal value is unavailable to an algorithm. The result is already proved in the 2013 paper; the open work here is its Lean formalization and the finite-dimensional facts needed to connect sparse coordinates, linear optimization, and the gap.
The formalization also produces reusable interfaces for sparse simplex optimization: a coordinate-count notion of sparsity, an attained minimum formulation, and a support-function statement that avoids making a real supremum silently return a default value on an empty or unbounded set. These can serve later work on atomic methods without tying that work to one choice of Frank–Wolfe steps.
Bounding the quadratic objective alone does not establish the duality-gap statement. The gap also involves the best linear comparison point in the simplex. The unrestricted simplex optimum, the optimum under a sparsity budget, and the best linear comparison are different objects and must retain their respective domains. An encoding that replaces the gap's domain with the sparse feasible set would change the theorem. Another easy mistake is to use the ambient norm of a function as the objective: that norm is the supremum norm, whereas the paper uses the Euclidean squared norm.
The paper's displayed curvature value is included as a companion statement. It uses the Euclidean diameter of the simplex, which is for . The one-dimensional simplex is a single point, so extending that equality to would be false. The formalized companion makes the dimension condition explicit.
Vectors are functions . The domain is Mathlib's ; the objective is an explicit sum of coordinate squares, and sparsity counts nonzero coordinates. The gradient pairing in the source is represented by the Fréchet derivative applied to a direction. For this quadratic, the two agree coordinate by coordinate. The duality gap is a real supremum of those derivative values over the simplex. Its use in the goal is guarded by , which implies and makes the simplex nonempty; compactness makes the supremum a maximum. The support-function milestone states equality through all upper bounds, so it also has a meaningful reading for empty or unbounded atomic sets.
The curvature set follows display (3), PDF p. 3, with step size because the printed quotient has no value at zero. The companion assumes , a necessary dimension pin beyond the paper's sentence. Other standing conditions of the general problem are discharged by the chosen quadratic and simplex, rather than added as free hypotheses. No theorem assumes the quadratic minimum, a gap maximizer, or a zero coordinate as a premise; those are consequences to be established from feasibility and sparsity. The source PDF contains the statements but not its cited appendix proofs, so formal proof contributions may use other valid arguments. The simplex support, sparse minimum, and curvature interfaces are reusable beyond this mission.
An assortment planner chooses which products to offer to arriving customers. When products are grouped into nests, a customer's choice of nest depends on all the assortments offered at once. A planner may nevertheless be able to generate only a short list of promising assortments for each nest. The remaining task is to choose one assortment from each list so that their combined expected revenue is as large as possible. Testing every combination requires a number of evaluations equal to the product of the list sizes. Gallego and Topaloglu show that the choice can instead be described through a linear program whose number of constraints grows with the sum of those sizes; this is Theorem 2 of their 2014 paper, in the authors' September 11, 2013 manuscript, pp. 10–12.
This mission isolates that selection result. Later parts of the paper address how to construct useful candidate lists under cardinality, space, and pricing constraints. Here the candidates are already given, and the question is which combination earns the most. The result matters whenever the candidate lists are much smaller than the space of all assortments: it makes the last step of those algorithms an exact optimization over the candidates, without enumerating their Cartesian product.
Let be a finite set of nests and a finite set of products available in each nest. An assortment is the set offered in nest . Product in nest has preference weight and revenue . The empty assortment is allowed. The main model has no within-nest no-purchase option, so its total offered weight is . The conditional revenue in nest is , with under the paper's convention.
The weight of no purchase outside the nests is . Each nest has a dissimilarity parameter . Its attraction weight is . The expected revenue of a combined assortment is
For each nest, is a finite nonempty collection of candidate assortments. The paper obtains these from a feasible set , which may impose a cardinality or space constraint; Theorem 2 compares only combinations drawn from the supplied candidates. Equation (2) defines a real scalar through the maximum, over separately, of . Problem (3) selects a maximizing candidate in each nest at that scalar. Linear program (4) has decision variables , minimizes , and imposes and for every and every .
The goal is the exact candidate-selection claim of Theorem 2. If minimizes among all feasible pairs of program (4), and every solves problem (3) at , then
The milestones record three statements from pp. 11–12: equation (2) has a unique real root; the balance equation and its inequality form characterize the expected revenue of a fixed assortment; and Lemma 1 identifies the root as the best revenue attainable from candidate combinations while showing that local maximizers attain it. They separate the paper's numerical characterization of the best candidate revenue from its LP formulation. The target does not prescribe how the candidate lists were generated or claim that the selected combination is best among assortments outside those lists.
The theorem gives an exact, compact choice rule for assembling nestwise candidates. If the lists contain useful assortments under the original constraints, their best combination can be selected through program (4). The rest of the paper establishes candidate-generation and approximation results under particular constraint families; the stitching theorem supplies the common final selection step for those results. A larger candidate list may improve the obtainable revenue, but its Cartesian product need not be searched explicitly. The authors' manuscript, p. 12, states that program (4) has variables and constraints when the candidates are indexed by .
Formalizing the theorem yields a reusable statement about the interaction of a fractional revenue objective, independent nestwise candidate families, and a shared scalar LP. The published Prove2Me definition NestedLogitVariants.LP.Model already supplies the instance, , , , and the feasibility and optimality predicates for program (4). Its previously proved lp4_opt_binding concerns an equality at an LP optimum under ordered, nonnegative revenues; it does not contain Theorem 2's maximality claim under this paper's revenue assumptions. The four statements in this mission are draft targets awaiting machine-checked proofs.
Optimizing a candidate independently in every nest at an arbitrary value of does not generally optimize the combined revenue: the revenue denominator couples all nests. Likewise, an LP-feasible value need not be its minimum, and using such a value in problem (3) does not establish the theorem. The substantive assertion is that choosing the local maximizers at the optimal LP value solves the combined selection problem. The unique-root statement also needs care at empty assortments, where a nest contributes zero attraction and the conditional revenue uses the paper's convention.
Nests are represented by any finite type, and products by Fin n, indexed rather than the paper's . A Boolean offer vector is represented by Finset (Fin n); is the empty finset. Each is a finite set of such assortments. There is no single-nest or specialization, and no substitution of all possible assortments for the supplied candidates. The LP assumption is its full minimum objective property, not merely feasibility. The imported LP4Optimal predicate uses a set of candidates, supplied by coercing each finite to a set.
The source's main model is selected from the imported general instance by setting . In the paper's later extension, ; this is different from the imported unmodified when , so the extension is outside this mission. Positive and product weights are stated explicitly to keep the probability denominator positive and to match the model's preference interpretation. Revenues remain arbitrary real numbers: neither an order nor nonnegativity is assumed. The dissimilarities satisfy the paper's range. The paper states candidate feasibility ; this mission's claim holds for arbitrary candidate collections because no step compares against . The definitions of revenue and LP feasibility are imported, so useful contributions include proofs of the balance characterization, the root result, Lemma 1, and the final LP statement.
A retailer that sells through a choice model decides two things at once: which products to put on the shelf and at what price. Under the nested logit model of discrete choice, products are grouped into nests (brands, categories, store sections); a customer first picks a nest, or leaves without buying, and then picks a product inside the nest. The price of a product changes its attractiveness, and the attractiveness of every product changes the purchase probabilities of all the others, so assortment and price interact.
Gallego and Topaloglu (Management Science, 2014) study assortment optimization under the nested logit model with constraints on what may be offered in each nest. Their §6 treats joint assortment and pricing when each product can be sold at one of finitely many price levels. Earlier work on nested logit pricing, by Li and Huh (2011) and Gallego and Wang (2011), assumes that a product priced at has preference weight . With a finite menu of price levels, no parametric link between price and preference weight is required, and the prices can be restricted to a range or a grid (for example $49.99, $59.99, …), as retail practice often demands.
There are nests . In each nest there are products , and each product can be offered at one of price levels . Offering product at level in nest earns the price and gives the product the preference weight . The relation between and is arbitrary.
Each pair (product, price level) is a virtual product. Nest has virtual products ; is the set of the virtual products of product , and the sets are disjoint. Virtual product at level has revenue and preference weight . An assortment of nest is a set , and the feasible assortments are
so each product is offered at no more than one price, or not at all.
For an assortment write and , with . For a number , problem (7) of the paper is
Its objective equals with ; under this is problem (12) of the paper.
For every nest there is a collection , fixed independently of , with
such that for every some is an optimal solution of problem (7). The page states ; the explicit bound is the count of intervals left by the intersection points of the lines , , with .
The paper's Theorem 4 shows that a collection containing an optimal solution of (7) for every yields an optimal solution of the full nested logit problem, and its Theorem 2 that the best combination of candidates solves a linear program with variables and constraints. With the goal above, the joint assortment and pricing problem is solved exactly by a linear program of polynomial size, constraints, for arbitrary price–weight relations. This is one of the paper's three headline results.
The result is proved in the paper in prose, without a numbered statement. No machine-checked proof of it is known. The mission fixes the constant hidden in , states the feasible set exactly, and isolates the two steps of the argument as separate statements.
The naive candidate set is all of , which has members; the content of the goal is the polynomial bound with the collection fixed before . The argument must handle ties between coefficients, lines that coincide or never cross, intersection points at negative , and the boundary points between intervals, where several assortments are optimal at once. The count must be made per product: a count over all pairs of virtual products gives and misses the stated bound.
ι; virtual products are Fin n and products Fin p, both 0-based. is the fiber of a map prod : Fin n → Fin p; the hypothesis that every fiber has exactly elements is IsVirtualProductMap prod b. The price level of a virtual product is left implicit.NestedLogitVariants.LP.Instance fields r i j and v i j; there is no parametric price–weight relation and no ordering of prices.Finset (Fin n); the empty assortment is allowed and has objective .0 ≤ u).A complete development needs the reduction of (7) to the linear objective (identity (8)), the per-product optimality of problem (12), and a counting argument for the intersection points of finitely many lines on . The last one is reusable beyond this mission: the paper's cardinality-constrained result uses the same kind of argument. Proofs of the milestones, and lemmas such as (8) for the published V and R, are welcome.
The scalar Bernstein and Bennett inequalities bound the upper tail of a sum of independent, zero-mean random variables that are bounded above: the tail is governed by the total variance at moderate deviations and by the uniform bound in the far tail. Many questions in randomized numerical linear algebra, matrix completion, covariance estimation, graph sparsification and statistical learning reduce to the same question for a sum of independent random matrices, where the quantity of interest is the largest eigenvalue or the spectral norm of the sum rather than a scalar.
Ahlswede and Winter (2002) introduced a matrix Laplace transform method based on the Golden–Thompson inequality. Oliveira (2010) and Gross (2011) proved matrix Bernstein-type bounds with this method. Tropp (arXiv:1004.4389, Found. Comput. Math. 12 (2012)) replaced the Golden–Thompson step with Lieb's concavity theorem, obtaining a master tail bound for independent sums (Theorem 3.6) from which matrix Bennett and Bernstein inequalities follow with the variance parameter , the natural analogue of the scalar variance. This mission formalizes §6 of that paper.
Timeline:
All matrices are complex matrices with . For a self-adjoint (Hermitian) matrix , is its largest eigenvalue and its spectral norm. The semidefinite order means that is positive semidefinite. Functions of a self-adjoint matrix are defined spectrally: if , then ; this gives the matrix exponential and, on positive-definite matrices, the matrix logarithm . The trace is .
A random matrix is a measurable map on a probability space ; its expectation is taken entrywise. A finite sequence of random self-adjoint matrices is independent if the maps are mutually independent.
The setting of the goal: are independent random self-adjoint matrices with
and the total variance is . Bennett's function is for .
For every , the following chain holds:
and the last term is at most for and at most for . The first inequality is the matrix Bennett inequality, the second the matrix Bernstein inequality, and the case split the split Bernstein inequality.
Lemma 6.8 (the matrix mgf bound under ) and Theorem 6.2 (matrix Bernstein, subexponential case: , split as and ) are included as further theorems.
Matrix Bernstein is the most used inequality of the paper: it bounds the spectral norm of a sum of independent bounded random matrices with only a logarithmic dimensional factor, and it is the standard tool behind sampling bounds for matrix completion, randomized low-rank approximation, spectral sparsification, covariance estimation and the analysis of random features. Theorem 6.1 assumes only an upper bound on the largest eigenvalue of each summand, so it applies to summands with unbounded smallest eigenvalues; applied to and separately it controls both tails.
The results are proved in the paper. As far as the local catalog shows, no machine-checked proof of the matrix Bennett or Bernstein inequality for complex Hermitian matrices exists; the platform has a matrix Bernstein statement for real symmetric matrices in a different form (Wainwright, Theorem 6.17), still open, and scalar Bennett and Bernstein inequalities. Formalizing Theorem 6.1 produces a reusable matrix concentration inequality together with its two ingredients, the matrix mgf bound of Lemma 6.7 and the scalar inequality relating Bennett's and Bernstein's exponents.
The scalar argument multiplies moment generating functions of independent summands. For matrices, unless and commute, so does not factor; the master bound of Theorem 3.6 rests on Lieb's concavity theorem for , which is not in Mathlib. The mgf bound of Lemma 6.7 needs a semidefinite comparison between functions of a random matrix, the transfer rule on the spectrum , and the operator monotonicity of the logarithm. The remaining steps (optimizing over , the inequality between and the Bernstein exponent) are real analysis.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; is the supremum of the real spectrum; is the operator norm on ; and are Mathlib's continuous functional calculus cfc; the semidefinite order is Mathlib's MatrixOrder; expectation is entrywise. A random matrix is a measurable map, each is Hermitian at every , independence is iIndepFun, and the measure is a probability measure. The bound is assumed almost surely; no lower bound on the eigenvalues is assumed. The paper's standing regularity (§2.2) is made explicit as integrability of the entries of and (and of where its expectation is taken). The infimum over in Theorem 3.6 and Corollary 3.7 is stated for every admissible .
The printed formulas divide by and , so and are hypotheses of Theorems 6.1 and 6.2; with Lean's convention , the case would turn the Bennett bound into the trivial value , so the statement is not allowed to degenerate there. The chain is a conjunction of the probability bound and the inequalities between consecutive bounds, so the weaker reading "the probability is below each bound" does not satisfy it.
A complete development needs the matrix Laplace transform method, Lieb's theorem (or a substitute), operator monotonicity of the logarithm, the transfer rule for the functional calculus, and the scalar inequality . The first four are reusable for every matrix concentration inequality of this paper and beyond. Contributions to any milestone are welcome.
Regularized loss minimization over linear predictors is the training problem behind support vector machines, logistic regression, ridge regression and their many variants. Given examples , one minimizes an average of convex losses of the predictions plus a quadratic penalty. Dual coordinate ascent (DCA) solves the Fenchel dual of this problem by optimizing one dual variable at a time; it has been the workhorse of linear SVM solvers such as LIBLINEAR (Hsieh et al., ICML 2008). Before Shalev-Shwartz and Zhang's work, the available analyses of DCA either gave linear rates with constants depending on unknown problem quantities or did not control the duality gap, which is the quantity a practitioner can actually monitor as a stopping criterion.
Shalev-Shwartz and Zhang (2013) analysed stochastic dual coordinate ascent (SDCA), where the coordinate is picked uniformly at random, and proved explicit bounds on the expected duality gap. For Lipschitz losses (hinge loss, absolute loss) the bound is iterations, which matches stochastic gradient descent when the accuracy is low and improves on it when is small compared with . This mission formalizes that result, Theorem 1 of the paper, together with the lemmas of its proof.
Timeline. Hsieh, Chang, Lin, Keerthi and Sundararajan (2008) proposed dual coordinate descent for linear SVMs and proved linear convergence with an unspecified constant. Shalev-Shwartz and Zhang (arXiv 2012, JMLR 2013) gave the first explicit duality-gap rates for SDCA, for Lipschitz and for smooth losses. Proximal and accelerated variants followed (Shalev-Shwartz and Zhang, Math. Program. 2016).
Fix examples (Euclidean norm), convex losses and a regularization parameter . The primal problem (1) is to minimize
The convex conjugate of a scalar function is . The dual problem (2) is to maximize, over ,
Weak duality gives for all , so the duality gap bounds the primal sub-optimality of .
A loss is -Lipschitz if for all . The paper's standing assumptions are , and .
Procedure SDCA starts from . At iteration it picks a coordinate uniformly at random, chooses maximizing
and sets and . The averaging option outputs and . Let maximize and write for the dual sub-optimality.
For convex -Lipschitz losses under the standing assumptions, if and
then
The constants and are the paper's.
In the order the proof uses them: the one-coordinate increase (10); the identity ; Lemma 1 (expected dual increase at least times the gap minus ); Lemma 2 (, ); Lemma 3 ( outside ); Lemma 4 (); the recursion after (13); the rate (14), ; and the averaged duality-gap bound of p. 16.
Theorem 1 makes the duality gap of SDCA a certified stopping criterion with an explicit iteration count. Because the gap upper-bounds the primal sub-optimality, it also gives a primal guarantee for the averaged output . It covers non-smooth losses, the hinge loss in particular, where linear rates are not available. The analysis pattern, a lower bound on the expected dual increase by the duality gap (Lemma 1) followed by a recursion for the dual sub-optimality, was reused in the analyses of proximal, accelerated and mini-batch dual methods.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. The mission produces a formal account of the primal–dual pair of regularized loss minimization with extended-real conjugates, a formal SDCA run with uniformly random coordinates, and the complete chain of lemmas. Lemma 1 is stated with a general strong-convexity modulus , as in the paper, so it serves the smooth-loss analysis as well.
The obvious first idea is to treat SDCA as stochastic coordinate ascent on a concave function and import a standard rate. That fails: is neither smooth nor strongly concave for Lipschitz losses, and its domain is a box, so the per-coordinate progress cannot be bounded by a gradient norm. The argument instead compares the exact coordinate maximizer with an explicit interpolation towards a sub-gradient, which needs the conjugate's value at a sub-gradient (Fenchel–Young equality) and its infinite values outside .
The rate (14) is not a plain geometric recursion. It needs a burn-in phase and then an induction with a step size that changes with , and the duality gap of the output has to be recovered from the dual progress by Jensen's inequality over the averaged iterates. Everything happens in expectation over the coordinate sequence, while the dual values have to be kept finite along every run.
Lean conventions:
EuclideanSpace ℝ (Fin d), examples and losses are indexed by Fin n, and is inner ℝ w x.EReal supremum, and is EReal-valued. Real values of are used only where the same statement asserts that they are finite.Δ : (Fin n → ℝ) → Fin n → ℝ constrained by an arg-max predicate (IsSDCAStep). Any maximizer is admissible, and one exists for convex real losses.js : Fin T → Fin n, started at , with .SAGA.Convex.expectIdx, a published definition).A real-valued conjugate, which returns where the supremum is infinite, or an unconstrained step map would make the statements false or vacuous. The EReal conjugate and the arg-max predicate rule both out.
Infrastructure needed: Fenchel–Young for scalar convex functions, the existence of sub-gradients of convex real functions and their bound by the Lipschitz constant, Jensen's inequality for the convex and the concave , and the algebra of uniform averages over . The conjugate and sub-differential definitions and the duality-gap identity can be reused beyond this mission. Proofs of any milestone are welcome, as are lemmas on EReal sums that keep the finiteness bookkeeping short.
Stochastic differential equations (SDEs) model physical, biological and financial systems whose drift often grows superlinearly: the stochastic Lorenz equation, the stochastic van der Pol and Duffing–van der Pol oscillators, Langevin dynamics. Solutions are rarely explicit, so they are simulated by time-stepping schemes. For multilevel Monte Carlo methods (Giles 2008) the cost of a simulation is governed by the strong convergence rate, the speed at which tends to as the step size shrinks.
For superlinearly growing coefficients the classical Euler–Maruyama method diverges in (Hutzenthaler, Jentzen, Kloeden 2011). Tamed schemes repair this, and rate was proved for them under a global monotonicity condition: for all (Hutzenthaler, Jentzen, Kloeden 2012; Sabanis 2016). Most of the examples above violate that condition. Before this paper no strong rate was known for any time-discrete scheme for a multidimensional SDE with non-globally monotone coefficients.
Timeline. 2011: divergence of explicit Euler for superlinear drifts. 2012: tamed Euler, rate under one-sided Lipschitz drift and globally Lipschitz diffusion. 2012–2013: strong convergence without rates for non-globally monotone SDEs (stopped and tamed schemes). 2014: this paper (arXiv:1401.0295), rate for the stopped-tamed Euler–Maruyama scheme under the conditions below; published in Ann. Probab. 48 (2020).
Fix and . On a probability space with a normal filtration , is a standard -dimensional -Brownian motion. Matrices carry the Hilbert–Schmidt norm . Given coefficients and , is an adapted continuous process with
The taming map is . The stopped-tamed Euler–Maruyama scheme with steps is and
The whole increment, drift and noise together, is tamed, and the scheme freezes once it leaves a ball whose radius grows slowly as .
The conditions use a Lyapunov-type function and a function . The generator is , where is the -th column of . For partitions with mesh , the same recursion run in continuous time on defines interpolations .
Let , , and with . Let be with polynomially growing derivatives. Let satisfy , , and , and assume for
Then there is such that for all ,
The constant is not specified. Only the rate is asserted, and that is the stable content of the result.
In the proof's order:
Theorem 1.3 gives strong rate , and with it the complexity bounds of multilevel Monte Carlo, for SDEs with non-globally monotone coefficients. The paper's applications include the stochastic Lorenz equation with bounded noise, the stochastic van der Pol and Duffing–van der Pol oscillators, a model from experimental psychology and overdamped Langevin dynamics. The perturbation estimate, Theorem 2.10, is a separate tool. It compares a solution with any Itô process, so it also gives local Lipschitz dependence on the initial value and, in the paper's §3.2, rates for Galerkin approximations of SPDEs.
All results listed here are proved in the paper, and none has been machine-checked so far. This mission produces Lean statements of the goal and of every numbered step of its proof. The development needs Itô calculus for , a localization argument, exponential-moment bounds via Lyapunov functions, and calculus for the taming map. Several of these pieces are reusable well beyond this paper.
The obvious argument is Gronwall's lemma applied to . It needs the global bound , which fails for the Lorenz and van der Pol drifts: there the one-sided Lipschitz "constant" grows with . The difficulty is to control a random, state-dependent Gronwall exponent . That requires exponential integrability of and along both the solution and the scheme. For the scheme it holds only because of the taming and the stopping, and only up to an error of the right order.
EuclideanSpace ℝ (Fin d). Diffusion values are the published Diffusion d m, whose norm is the Hilbert–Schmidt norm the paper uses throughout. Time is .SabanisEuler.Shared.IsSolution / IsItoProcess. The normal filtration is right-continuity plus completion, and is the published IsWienerMartingale, a Brownian motion on . For , the paper's cylindrical Wiener process is exactly such a Brownian motion. All processes are hypotheses; existence is never claimed.Many equilibrium problems in operations research, such as networked Cournot competition, power markets and communication networks, are stochastic Nash games: each player minimizes an expected cost that depends on the rivals' strategies and on a random vector whose law is accessible only through samples. Best-response schemes, in which every player in turn solves its own optimization problem given the others' latest strategies, are the natural distributed method for such games. In the stochastic setting no player can compute an exact best response, because evaluating requires the expectation itself. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in which each best response is approximated by a finite number of stochastic gradient steps, and they ask how many sampled gradients each player needs to reach an approximate equilibrium.
The deterministic theory of proximal best responses, including the contraction matrix used here, is due to Facchinei and Pang (Nash equilibria: the variational approach, 2009, §12.6; reference [19] of the paper). The present mission covers the paper's first scheme, the synchronous one, in which all players update simultaneously.
There are players. Player chooses from a closed, compact, convex, nonempty set ; a profile is , and is the profile with its -th block replaced by . A Nash equilibrium is a profile such that every minimizes over .
Assumption 1 asks that each be convex in and twice continuously differentiable near , that the sampled gradients be unbiased for , and that . For the proximal best response is
The matrix has entries and , where is the least eigenvalue of over and the largest spectral norm of the mixed block over . Assumption 2 is (spectral norm).
Algorithm 1 starts from a deterministic . At major iteration every player computes with , by running projected stochastic gradient steps
and setting . A random profile is an -NE if .
With , , , , , , and , the iterate after major iterations is an -NE, and player uses at most
projected stochastic gradient steps. The goal fixes the paper's explicit expression, not its summary.
Theorem 1(a) shows that the synchronous inexact scheme keeps the linear rate of the exact best-response iteration, with factor arbitrarily close to , and turns it into a sample complexity explicit in , in the number of players and in the game's constants. Choosing gives a bound of order for any (Theorem 1(b)), close to the of a single stochastic convex program; the dependence on is mild, which matters for games with many players. The same building blocks (the contraction (5), Lemma 2, Lemma 3 and (30)) are reused by the randomized and asynchronous schemes of the same paper.
The result is proved in the paper; it has not been machine-checked. A formalization adds a verified proof of the complexity bound together with fully explicit hypotheses: several conditions that the paper leaves implicit or states imprecisely (listed under Formalization scope) are made exact, and the Lean statement records which version of each is used.
The arithmetic of Theorem 1(a) from Proposition 4, Lemma 3 and (30) is routine. The weight lies elsewhere. The contraction (5) is quoted from Facchinei–Pang and not proved in the paper; it needs the variational optimality conditions of the two proximal problems and a mean-value argument along a segment of for the partial gradient, which mixes the Hessian blocks and . Lemma 3 is a conditional-expectation argument about a stochastic approximation recursion: the iterate must be shown measurable for the nested -fields generated by the samples, and the conditional unbiasedness and moment hypotheses must be combined with the tower property and the projection's nonexpansiveness. Proposition 4 then needs conditional Jensen to pass from (8) to the Euclidean norm of block errors.
Players are Fin N, player 's space is EuclideanSpace ℝ (Fin (n i)), profiles are dependent functions, and is Function.update y i z. The Euclidean norm of the vector of block distances is written out (blockDist), since Mathlib's norm on profiles is the sup norm; is the operator norm of Matrix.toEuclideanCLM Γ. and are the infimum and supremum of Rayleigh-type quotients of the second derivative over and unit vectors. The proximal BR is any map minimizing the proximal objective on (unique there), and is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. The -fields and are generated by the samples. Every expectation carries an integrability hypothesis.
Statement repairs, each recorded in the item's Formalization Note:
The goal is not trivialized by deterministic gradients: the sampled gradients are random, constrained only by conditional unbiasedness and a conditional second-moment bound, the proximal BR is tied to by its argmin property, must be a Nash equilibrium, and the norms are Euclidean. A deterministic instance (, on a ball, exact gradients) satisfies every hypothesis jointly.
Needed infrastructure: optimality conditions for constrained strongly convex minimization, the mean-value inequality for partial gradients of functions on convex sets, conditional expectation of vector-valued functions with the tower property and conditional Jensen, and the nonexpansiveness of Euclidean projection. The contraction (5) and Lemma 3 are reusable beyond this mission. Proofs of any milestone are welcome.
For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.
Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.
Let be a simple graph on , . A set of vertices is stable if no two of its members are adjacent; the stability number is the size of a largest stable set, so .
Put and write a vector of as , with indexed by vertices and indexed by pairs of vertices. The tensor has entry at the six orderings of the triple of coordinates for every non-adjacent pair , and elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.
For a real 3-tensor the cubic form is , and a real is a unit -eigenvalue of if
Finally, for . In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and is Mathlib's SimpleGraph.indepNum.
That is, is an eigenvalue of , and no with is. This is the statement on which the paper's -query reduction rests; nothing is claimed about .
both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.
The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.
Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.
The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing and maximizing over by Cauchy–Schwarz, reduces the cubic problem to a quartic one in , whose value still has to be identified with ; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.
ι → ι → ι → ℝ on a finite index type. For the index type is the disjoint union of the vertices Fin v and the pairs ; this is with coordinates labelled by name instead of by the paper's enumeration . Vertices are .SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.The rank of a matrix does not depend on the field in which its entries are read: a rational matrix has the same rank over , and , because rank is computed by Gaussian elimination, which never leaves the field of the entries. For 3-tensors, arrays with three indices, this fails. Tensor rank governs the complexity of bilinear maps (the exponent of matrix multiplication is a statement about the rank of one tensor), the uniqueness of the CANDECOMP/PARAFAC decompositions used in psychometrics and signal processing, and the identifiability of latent-variable models. In each application the field matters: algorithms are run over or , while complexity results are often proved over or finite fields.
Håstad (1990) proved that deciding is NP-complete over finite fields and NP-hard over . De Silva and Lim (2008) gave real tensors whose rank over is strictly smaller than their rank over . Hillar and Lim (2013, Theorem 1.14) showed that the same phenomenon already occurs between and , for a tensor with integer entries, so that Håstad's result over does not by itself say anything about rank over .
Let be a field. The outer product of , , is the tensor with entries . The rank of over is
If has entries in a subfield , both and are defined, and .
The paper's example uses , and
A decomposition with , is equivalent to the eight cubic equations (30) in the twelve unknowns , one for each entry of .
In Lean, outer x y z and rankOver E A implement the two definitions, tensorA is , and System30 is (30).
The theorem shows that tensor rank, unlike matrix rank, is not invariant under field extension even between and , and even for the smallest nontrivial format . Its consequence for complexity is that a hardness result for rank over cannot be transferred to by reading the same instance in a larger field; the paper accordingly re-examines Håstad's construction to obtain hardness over and (Theorem 8.2), which is outside this mission.
The result is proved in the paper, with the decisive algebraic step delegated to a computer-algebra computation (Appendix). A machine-checked proof replaces that computation by a certificate verified in Lean, and it settles a printed error: one of the two consequences of (30) in the proof of Lemma 8.1 is printed with the wrong sign (see Formalization scope). No formalization of array tensor rank over a field, or of its field dependence, is known to exist in Mathlib or on this platform.
The upper bound is an identity among explicit arrays. The lower bound is the substance: one must show that the cubic system (30), which has real solutions, has no rational one. Since (30) is solvable over , no argument by signs, inequalities or real geometry can work; the obstruction is arithmetic, coming from the irrationality of . The step that fails in a naive attempt is the elimination: eliminating ten of the twelve unknowns from eight cubic equations by hand is impractical. A second, smaller difficulty is the reduction from "" to two terms of the special form (29), which requires absorbing the scalars and padding a decomposition with fewer than two terms.
Fin l → Fin m → Fin n → E, with 0-based indices: the paper's is A (i-1) (j-1) (k-1). Vectors are Fin n → E.rankOver E A is the sInf over of the lengths of decompositions . The set is nonempty (one term per entry), so this is the paper's minimum. Zero summands are allowed; this gives the same minimum as the paper's sum of nonzero rank-1 tensors.rankOver ℝ of its entrywise cast to ; is rankOver ℚ, whose witnesses are rational. A formalization in which both ranks range over real witnesses would make the theorem false.Needed infrastructure: finite sums of arrays, Real.sqrt and irrational_sqrt_two, and an ideal-membership certificate for milestone 3. The array rank rankOver is reusable for any statement about tensor rank over a field. The platform's mme_tensor_rank (restriction-based rank of a TensorObj over a single field, from the matrix-multiplication exponent series) is a different object and is not reused. Proofs of any milestone, and alternative certificates for Lemma 8.1, are welcome.
Interior-point methods for conic optimization are best understood on symmetric cones: the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices. On these cones the barrier functions are self-scaled, and Nesterov and Todd showed that every primal-dual pair then has a unique scaling point with and . The resulting primal-dual algorithms, implemented in solvers such as SeDuMi and MOSEK, combine long steps with good worst-case complexity.
Many models in statistics, geometric programming, entropy maximization and logistic regression need the exponential cone, which is not symmetric. Dahl and Andersen (Math. Program. 194, 2022) designed the primal-dual algorithm behind MOSEK's exponential-cone support. To explain why they cannot simply transplant the Nesterov–Todd construction, they use a property that sits between "self-scaled" and "arbitrary": negative curvature of the barrier. Barriers of symmetric cones have it; a barrier is self-scaled if and only if both it and its conjugate have it (Nesterov–Tunçel, 2016); and barriers with negative curvature still admit a unique scaling point satisfying one secant equation. Dahl and Andersen observe in §5 that the exponential-cone barrier lies outside this class, by an explicit witness. This mission formalizes that observation and the derivative formulas of their Appendix A it rests on.
Timeline:
Points of are written . The exponential cone is the closure
whose interior is . Its standard barrier is
defined and smooth on . Appendix A of the paper writes with
For a smooth on an open set, is its Hessian, a symmetric linear map of , and the third directional derivative is the symmetric linear map
A barrier of a cone has negative curvature if for all and for
where is the Loewner order: for every . The direction ranges over the closed cone , including its boundary.
The goal asserts only the qualitative failure, so it does not depend on the particular witness.
The result. Negative curvature is the property that gives symmetric-cone barriers their long-step Hessian estimates and a unique scaling point with one secant equation. Its failure for the exponential-cone barrier means that none of these consequences can be invoked for the exponential cone. An algorithm for this cone has to obtain its scalings by other means; Dahl and Andersen take them from Tunçel's framework, via the quasi-Newton secant updates of §5. The witness also shows that the failure occurs already for a direction on the boundary of the cone, at an interior point with simple coordinates.
Formalizing it. The claim is proved in the paper by a computation "using the expressions in the appendix", with the details left to the reader. The appendix formulas for the gradient, Hessian and third directional derivative of the exponential-cone barrier are the ones an implementation evaluates, including the higher-order corrector term . A machine-checked version certifies these closed forms, including the zero padding of the "leading parts" in (33), and gives a reusable definition of negative curvature that applies to any cone and barrier. As far as is known, none of these statements has a machine-checked proof.
The obstacle is computational, not conceptual. The barrier is a composition of logarithms with a function that is itself a perspective of the logarithm, so its third derivative is a sum of terms with denominators , and . Stating it as a derivative of the Hessian map requires showing that the Hessian is differentiable on the open interior, which in turn requires a description of that interior, a set defined as the interior of a closure. The membership claims about are not definitional either: lies on the boundary, reached only as a limit of points of the generating set, and its non-interiority needs a neighbourhood argument. Finally, the cone condition on matters: replacing by makes the claim nearly trivial, because .
EuclideanSpace ℝ (Fin 3); the paper's are (x 0, x 1, x 2), and vectors are written !₂[·, ·, ·].Real.log; every statement evaluates them, and their derivatives, only at points of , where all logarithms are the genuine ones. The appendix formulas carry the hypothesis .SelfScaledIPM.ShortStep.hess (derivative of the gradient), and is fderiv ℝ (hess F) x u. The Loewner order is stated through the quadratic form for every . Matrices act through the standard basis (Matrix.toEuclideanCLM).The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).
The proof is a reduction from the clique number of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding is one of Karp's (1972) NP-complete problems.
A real 3-tensor is an array with trilinear form . With the Euclidean norm , its spectral norm is
A real is a unit -singular value of if there are unit vectors with
for all : the stationarity conditions of on a product of unit spheres.
Let be a simple graph on , , with edges , , and clique number . Let be the standard simplex, the adjacency matrix and the all-ones matrix. For a positive integer set and . Let , and let be the maximum over unit , of the multilinear form
The graph tensor has as entry the coefficient of in (26).
For every graph on vertices and every enumeration of its edges:
so is the largest for which is a unit singular value of . The paper's -query Turing reductions rest on exactly this.
The result. The goal shows that a single comparison with of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size encodes whether . It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.
Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.
The construction of is explicit, and the comparison with is arithmetic once is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.
Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with , clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. is a rational tensor, read over by casting.
Explicit readings of the paper:
This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of , the -query procedure, the scaling to a general fixed , and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.
Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.
Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.
Conic optimization over the exponential cone models entropy, relative entropy, logistic regression, log-sum-exp and geometric programming. Unlike the nonnegative orthant, the second-order cone and the semidefinite cone, the exponential cone is not symmetric (self-scaled), so the Nesterov–Todd primal-dual machinery that makes solvers such as SeDuMi and MOSEK fast does not apply as is. Dahl and Andersen (Math. Program. 194 (2022) 341–370) describe the nonsymmetric-cone algorithm implemented in MOSEK (version 9.2 in the paper's experiments). Its central new ingredient is a corrector for nonsymmetric cones, an analogue of Mehrotra's predictor-corrector that is responsible for much of the practical performance of symmetric-cone solvers. The paper reports that the corrector gives a substantial and consistent reduction in iteration counts across its test sets.
Timeline. Nesterov and Todd (1997, 1998) built primal-dual methods for self-scaled cones. Nesterov, Todd and Ye (1999) and Tunçel (2001) studied primal-dual scalings for general cones, Tunçel proving polynomial complexity of an infeasible method without a corrector under bounded scalings. Skajaa and Ye (2015) gave a homogeneous method for nonsymmetric cones with a Runge–Kutta corrector. Myklebust and Tunçel (2014) analysed BFGS-type scalings. Dahl and Andersen (2022) introduced the third-order corrector studied in this mission.
Let be linear with full row rank, , , and let be a proper cone (pointed, closed, convex, with nonempty interior). A -logarithmically homogeneous self-concordant barrier (LHSCB) for is a convex function on with and . The primal problem minimizes subject to , ; the dual maximizes subject to .
The homogeneous model adds : , , , , . With , the residual is
a linear map whose -block is skew-symmetric. An iterate has , , and . The shadow iterates are and , with the conjugate barrier. A scaling is a nonsingular with and (the double secant equations (8)).
The affine direction solves , (11). The corrector is (16). For a centering parameter , the combined direction solves
Every solution of (18) satisfies
and for all
The goal fixes no constants beyond those of the direction itself. It holds for every solution of (18), not a chosen one.
The result. Lemma 4 says that a step of any length along the combined direction reduces the infeasibility residuals and the complementarity gap by exactly the same factor. Starting from a point with , the iterates satisfy and , so the algorithm needs no merit function to balance feasibility against optimality, in contrast with earlier nonsymmetric methods. The lemma also shows that adding the third-order corrector does not cost this property, which is what justifies using the corrector in MOSEK's exponential-cone solver.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of Lemmas 2–4, the §2 homogeneity identities or the barrier sum rule has a machine-checked proof. The mission produces a formal homogeneous model for a general proper cone with a general LHSCB and a formal account of third-derivative calculus for logarithmically homogeneous barriers. Both are reusable in any analysis of interior-point methods for nonsymmetric cones (power cones, generalized power cones, hyperbolicity cones).
The obvious reading of Lemma 4 as bookkeeping with the linear map stalls at the corrector: the term
in (18) involves the third derivative of the barrier, and nothing in linear algebra says how it
interacts with the complementarity gap. Controlling it needs the third-derivative calculus of logarithmically
homogeneous barriers. In Lean that means relating gradient, the Hessian as fderiv of the gradient, and the
third derivative as fderiv of the Hessian, and working with the symmetry of iterated Fréchet derivatives of a
function, for which the Mathlib interface is thin. A second obstacle is the augmented barrier: the
barrier properties of must be transported to on through the
splitting , including the boundary behaviour at the corner
, .
The first identity of Lemma 4 is misprinted in the paper as . A formalization following the printed statement would be false, not merely awkward.
Vectors of the augmented space are EuclideanSpace ℝ (Fin (n + 1)); is the first coordinates and
(resp. ) the last. is a continuous linear map and its Hilbert adjoint; full row rank
is surjectivity. Proper cones, the Hessian hess, the barrier class IsLogHomBarrier and the conjugate
conj are the published SelfScaledIPM.ShortStep.Setting. That barrier class adds three standard conditions
to the paper's two (boundary blow-up, the -inequality and a positive definite Hessian), which the
paper uses implicitly when it writes and calls a barrier. is a continuous linear
equivalence and the adjoint of . is fderiv ℝ (hess F) x u w and
is ContinuousLinearMap.inverse. Every inner product includes the homogenizing term .
Repairs, generalizations and specializations, each disclosed in the item statements:
The directions are predicates (" solves (11)"), and the lemmas quantify over all solutions. The hypotheses are satisfiable. For the linear program , , , , , , , , system (11) has the unique solution , , . Statements that hold only because a junk value appears are ruled out: every statement requires and , where , the inverse Hessian and the conjugate barrier take their true values. A formalization that drops from the inner products, or that fixes one solution of (18) instead of quantifying over all, would be a different lemma and does not count.
Welcome contributions: the general sum rule for products of cones, a Fin.append splitting library for
EuclideanSpace, and proofs of the homogeneity identities that can be reused by the series' other missions.
The explicit Euler–Maruyama scheme is the standard way to simulate a stochastic differential equation
on driven by a -dimensional Brownian motion. When and are globally Lipschitz it converges strongly with order in the step size (Kloeden and Platen 1992). Many models of interest in physics, chemistry and statistics have a drift that grows faster than linearly but points inwards, such as . For these the SDE is well posed and its solution has finite moments of all orders, but the uniform-step scheme does not: for , Hutzenthaler, Jentzen and Kloeden proved that as the step size , for every and (Proc. R. Soc. A 2011).
Several remedies have been proposed: implicit schemes (Higham, Mao and Stuart 2002; Mao and Szpruch 2013), the tamed Euler scheme (Hutzenthaler, Jentzen and Kloeden 2012), truncated schemes (Mao 2015). Fang and Giles (Ann. Appl. Probab. 2020) keep the explicit Euler–Maruyama update and change only the step: the timestep is a function of the current state, small where the drift is large. This mission formalizes their finite-time results: stability of the adaptive scheme (Theorem 1) and strong convergence of order (Theorem 3).
Let and be the Euclidean norm and inner product on , and the Frobenius norm of an matrix. Given a timestep function , the scheme (5) starts from , and sets ,
The grid is random: it depends on the path. For a time , is the last grid time not after ; the piecewise constant interpolant is and the continuous interpolant is
The hypotheses (Assumptions 1–4, pp. 528–530):
For in one dimension, satisfies Assumption 2.
Under Assumption 4, with satisfying Assumption 3 for an satisfying Assumption 2, for every there is such that for all
Theorem 1 shows that an explicit scheme, at the cost of one drift and one diffusion evaluation per step, is stable for one-sided Lipschitz drifts of polynomial growth, the class where the uniform-step scheme fails. Theorem 3 shows that refining the timestep function keeps the classical order . Combined with the paper's bound on the expected number of steps (Lemma 2) this gives order in terms of computational cost, and the results underpin the paper's adaptive multilevel Monte Carlo estimators. The uniform-in- form of Theorem 1 is what lets Theorem 3 apply the stability bound to the whole family .
The paper's proofs are complete on paper; none of these results has a machine-checked proof. Formalizing them needs a theory of Euler schemes on a random, state-dependent grid, which is not in Mathlib and is not covered by uniform-grid formalizations of tamed or implicit schemes. The definitions here (the scheme on random times, the projected K-scheme) are reusable for the infinite-time companion mission and for other adaptive schemes.
The obvious argument for the uniform-step scheme bounds moments step by step, using deterministic step sizes and independent Gaussian increments. Here the step depends on , so the grid times are stopping times and the increments have random length. Sums over steps become Itô integrals only after the scheme is written as the solution of , and moment bounds for those integrals need the Burkholder–Davis–Gundy inequality on a random grid. A second difficulty is that need not be reached: if decays fast enough, could converge below . Excluding this needs a positive lower bound on over bounded sets together with moment bounds, which the paper obtains by first analysing a version of the scheme projected onto a ball.
Lean conventions: is the published SDEState m (EuclideanSpace ℝ (Fin m)); matrices are the published Diffusion m d, whose norm is the Frobenius norm; is a standard -dimensional -Brownian motion in the sense of the published IsWienerMartingale; the SDE solution is any process satisfying the published IsSolution on (existence and uniqueness are not claimed). Times are in , indices start at , and is deterministic. The scheme is defined pathwise; the index of is a junk value when the grid never passes , an event of probability zero (Theorem 1). and are real-valued and their positivity is a hypothesis; each is assumed measurable. Moments are -valued integrals of extended norms, never Bochner integrals. Every existential constant is chosen before the parameter it must not depend on: before in Theorem 3 and its milestones, before (and ) in Theorem 1 and Step 3. Results the paper proves for inside its proofs are stated for . Pages are the journal's printed pages (PDF page + 525).
A formalization that places the constant after , uses a deterministic grid, or allows would be trivially true or a different theorem; these are ruled out by the statements.
Contributions welcome: proofs of the milestones, and of general facts they need (Burkholder–Davis–Gundy, moments of Brownian increments over stopping-time intervals, Grönwall's inequality for -valued functions).