Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Training data describe one probability distribution, while a deployed prediction rule may be evaluated under a nearby distribution. Distributionally robust learning measures a rule by its worst expected loss over a specified set of nearby laws. This changes the question from how well the rule fits the observed sample to how well it performs when probability mass can move. Wasserstein distance supplies a geometric notion of “nearby”: moving mass farther across the instance space costs more. The setting is relevant to the domain drift discussed by Lee and Raginsky and to Wasserstein robust optimization as developed by Mohajerin Esfahani and Kuhn.
Theorem 1 of Lee and Raginsky's 2018 paper gives a finite-sample answer. It controls the local worst-case risk at the true population law using quantities computed from the empirical law, and also controls the empirical local worst-case risk using population quantities. Both assertions are simultaneous over the entire loss class. This mission concerns exactly those two probability inequalities and the displayed claims in Appendix C.1 that support them. The source is the pinned arXiv:1705.07815v2 preprint, containing the NeurIPS 2018 paper and its supplementary appendix.
The instance space is a bounded Polish metric space with distance . A probability measure generates independent observations . Their empirical distribution is . A loss has risk under a probability law . The class consists of upper semicontinuous losses satisfying for every and , as in Assumption 2 of the paper.
For , the -Wasserstein distance is the least th-power transport cost over couplings of and , raised to the power . The Wasserstein ball consists of probability laws with , where . The local worst-case risk is
The dual expression uses the envelope for . To measure the size of , let be its uniform-metric covering number at radius . The entropy integral is . These symbols match the local Lean setting and the source's notation.
For every , the mission goal is the conjunction of the paper's two displays:
The seven milestones preserve displayed claims from Appendix C.1: the deterministic comparison through the supremum deviation , its concentration and symmetrization bounds, the entropy-integral estimate with constant , the fixed- probability bound, and the integer-grid union and comparison with real multipliers. They are statements from the author's argument, ordered by their appearance. The goal retains both directions of the published theorem and every printed constant.
The first bound provides a sample-dependent certificate for the worst-case population loss of every member of at once. The second compares the robust empirical quantity with a population envelope. Together they make it possible to assess what a local Wasserstein ambiguity set buys in finite samples, rather than relying only on asymptotic convergence. The complexity term depends on the geometry of the loss class through its covering numbers, following a line of empirical-process bounds also seen in Bartlett and Mendelson's study of Rademacher complexity. Lee and Raginsky emphasize that this class complexity can reflect hypotheses outside the support of the data-generating law.
The mathematical theorem is proved in the 2018 paper; the particular declarations in this mission remain open Lean goals. A complete formal development would connect probability inequalities for supremum processes to the published Wasserstein distance and ball, make the entropy integral and its measurability consequences explicit, and verify both directions of the final bound. The reusable output includes a precise internal uniform covering number and a finite-sample Rademacher process for metric-space loss classes.
A fixed multiplier is easier to control than the infimum over all . A pointwise concentration bound alone does not produce a simultaneous statement over an uncountable multiplier set. The source's final formula contains a logarithmic multiplier penalty, and retaining its coefficient and the probability factor requires accounting for that parameter range exactly. Independently, the supremum over an arbitrary loss class is a genuine random variable only with enough regularity. The boundedness of individual losses does not by itself settle the measurability of their unrestricted supremum.
The envelope also mixes the metric geometry with empirical-process complexity. Estimating a class of envelopes must remain tied to the covering properties of the original class . Replacing the envelope class by a finite hand-picked subclass or assuming the desired concentration inequality as a new hypothesis would change the theorem being formalized.
Lean uses a metric space with its Borel measurable structure and a Polish-space instance, together with boundedness of the whole carrier. The Wasserstein distance and ball are imported from the published WassersteinLinOpt.Ball definitions. Because the carrier is bounded, every probability measure has a finite th moment, matching the source's . The ball is a subtype of probability measures; its supremum is taken only over feasible laws. Sample outcomes are functions Fin n → 𝒵, and the product measure gives their independent common law. The empirical law is a normalized finite sum of Dirac masses, while is written as its equal finite average.
The paper does not specify whether covering centres must lie in . This formalization uses the internal covering number, whose centres do; its value is at least the external covering number. The entropy integral is extended nonnegative and is required to be finite in statements that convert it to a real number. This disclosed restriction avoids the default conversion of to zero and supports the separability needed for expected suprema. Milestones using also require to be nonempty, so a real supremum never acquires the empty-family default value. The empty-class case of Theorem 1 remains valid because its failure events are empty.
The source writes minima over nonnegative real multipliers and positive integers. The Lean statements use bounded-below real infima; for the final bound, the appendix's comparison holds at every multiplier, so this reading is at least as strong as the printed minimum. All radii are positive, , , and where it appears. Failure probabilities use outer measure of the sample event directly, with no conversion through toReal. The goal never quantifies over arbitrary distributions outside the Wasserstein ball, and expectations of supremum processes are guarded by the finite-entropy hypothesis. Contributions are welcome on the concentration, symmetrization, covering-number, and transport-risk interfaces as well as the goal itself.
Best subset selection asks for the linear model that fits a response best using only a few of many candidate predictors. In its penalized form it is the least-squares problem with an penalty, the number of nonzero coefficients. The problem is NP-hard. Mixed-integer optimization can solve it to certified optimality at moderate sizes (Bertsimas, King, Mazumder 2016), but statisticians who fit whole regularization paths with tens of thousands of predictors need something faster. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed cyclic coordinate descent for the -penalized problem, the method that glmnet made standard for the lasso. Their algorithm underlies the L0Learn software package.
Coordinate descent on a convex smooth-plus-separable objective converges by classical arguments (Tseng 2001). Those arguments do not cover the penalty, which is discontinuous. The paper adds occasional spacer steps to plain cyclic coordinate descent and proves that the modified algorithm converges to a coordinate-wise minimum. This mission formalizes that convergence theorem.
Let be a model matrix whose columns have unit Euclidean norm, and let . For let
with and ; counts the nonzero coordinates. Problem (2) is . Its three named cases are (L0) (), (L0L1) () and (L0L2) (). .
Fix all coordinates but the -th. With unit-norm columns, minimizing over amounts to minimizing a scalar function of . The minimizer set is (7). The thresholding operator (12) picks one element of it:
A coordinate-wise (CW) minimum is a such that every minimizes in coordinate with the others fixed (Definition 2). A stationary solution is a whose lower directional derivative is nonnegative in every direction (Definition 1).
Algorithm 1 (CDSS) takes an initial point and a positive integer . It sweeps the coordinates cyclically. Each non-spacer step sets the current coordinate to and increments a counter for the resulting support. When the counter of a support reaches , a spacer step follows: one sequential pass over the coordinates of with the term switched off, . The counter of is then reset. The iterates count both kinds of step.
For (L0) and (L0L1) the paper adds Assumption 1: every columns of are linearly independent. It also adds Assumption 2, which constrains the initial point when : for (L0), and for (L0L1).
For (L0), (L0L1) and (L0L2), under Assumptions 1–2 in the first two cases, there are and a support with
The two parts share : the support stabilizes, and the limit is a CW minimum on that support.
Theorem 2 guarantees that exact cyclic coordinate descent on Problem (2), with spacer steps, has a limit, and that the limit is a CW minimum. That class is strictly smaller than the stationary solutions and the fixed points of iterative hard thresholding ((4), p. 5). It also serves as the inner solver of the paper's local combinatorial search (Algorithm 2, Theorem 4). So the guarantee transfers to the partial-swap-inescapable minima studied in the companion mission. Support stabilization (part 1) is also what reduces the asymptotic analysis to smooth strongly convex coordinate descent on a fixed support (Theorem 3).
The result is proved in the paper; no machine-checked version exists. A formalization would check the convergence argument for a discontinuous objective, where the bookkeeping of supports, counters and step indices is easy to get wrong. It would also provide a reusable Lean model of -penalized least squares and its thresholding operators.
The standard proof for cyclic coordinate descent needs a uniform decrease per step or a continuous objective. Neither holds here. A coordinate may switch between zero and a nonzero value infinitely often while decreases by arbitrarily small amounts, so the descent property alone gives neither support stabilization nor convergence of the iterates. Coordinates dropped infinitely often and coordinates added infinitely often must both be excluded. The tie-breaking rule in matters here: with the other choice on ties the algorithm is different. The exclusion of coordinates added infinitely often is only sketched in the paper (p. 43), and a complete proof has to supply it.
Vectors are Fin p → ℝ with 0-based indices. Every norm is written as an explicit sum; Mathlib's sup norm on function types is never used. Unit-norm columns, , and are hypotheses. The case , which the paper never names, is excluded from the statements about the algorithm's limits. is Real.sign. chooses the nonzero solution on ties, as in (12). The lower directional derivative takes values in EReal, since it is in directions leaving the support. Lemma 3 is stated with the condition on the support, taken from (5). The printed condition (8) omits it, and without it the equivalence fails for . Indices and pages throughout are those of arXiv:1803.01454v3.
Algorithm 1 is a deterministic state machine: iterate, cyclic pointer, the counter array Count, and a flag for a pending spacer step. The iterates are therefore defined from and , not quantified over. The pointer advances only on non-spacer steps, following the pseudocode box; the prose formula on p. 10 contradicts it. A statement about an arbitrary sequence satisfying a step predicate, or one that adds a step size or a sufficient-decrease hypothesis, would describe a different algorithm and is ruled out.
Useful infrastructure includes the scalar thresholding lemmas and coercivity of under Assumption 1 on supports of size at most . Contributions of proofs for any milestone are welcome, as are lemmas on the state machine (descent of each step type, the counter bookkeeping).
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At each step it keeps an exponential moving average of stochastic gradients and an exponential moving average of their squared coordinates, corrects both for their initialization at zero (the bias correction), and moves the iterate by coordinatewise.
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size with and , the interpolated iterates follow a non-autonomous ordinary differential equation. Their Theorem 3.2 shows that the trajectory of this ODE approaches the critical set of the objective. That leaves open whether the trajectory settles at a single critical point, and how fast. For gradient-like systems the classical answer goes through the Łojasiewicz gradient inequality (Łojasiewicz, 1963, for real-analytic functions), and the dissipative-systems framework of Haraux and Jendoubi (2015) turns such an inequality into convergence with a rate. This mission formalizes the paper's Theorem 3.4, which brings that conclusion to the continuous-time Adam dynamics.
Timeline.
Let be continuously differentiable with locally Lipschitz gradient , and let be locally Lipschitz. In the paper and . Its §7 uses only the two properties above, and so does this mission. Assume is coercive ( as ) and coordinatewise for every . Fix constants with .
The state is , and all vector operations are coordinatewise. The Adam field (3.3) is, for ,
and (ODE) is . A global solution with initial condition is a continuous that is continuously differentiable on , satisfies (ODE) for every , and has . The critical set is .
A number is a Łojasiewicz exponent of at if there are and with
Assumption 3.3 (the Łojasiewicz property) requires an exponent at every . It holds for real-analytic and semialgebraic .
The proof uses the Lyapunov function , where (3.4)–(3.5). It also uses its perturbation (7.11) and .
Assume Assumption 3.3 and that has empty interior in . Let be a global solution with initial condition . Then there is with as . Moreover, if is a Łojasiewicz exponent of at , then
for a constant (and, in the second case, some ) depending on the trajectory, and but not on .
The milestones follow the proof in §7.4:
Theorem 3.2 only places the limit points of the trajectory in . When contains a continuum of critical points, the trajectory could in principle drift along it forever. Theorem 3.4 excludes this under the Łojasiewicz property. It shows that continuous-time Adam has finite length and converges to one critical point, and it makes the speed explicit. The speed is polynomial with exponent in general and exponential when , which holds for instance at a nondegenerate critical point. The theorem places continuous-time Adam in the same class as gradient flow, heavy-ball dynamics and proximal methods.
The result is proved in the paper (§7.4, with the final integration delegated to arguments of Haraux and Jendoubi). It has not, to current knowledge, been machine-checked. The mission produces a formal proof, together with formal statements of the Lyapunov estimates (7.12)–(7.13) for the Adam ODE. The Łojasiewicz-rate step is reusable for other perturbed gradient-like systems.
The standard Łojasiewicz argument for gradient flow uses itself as the Lyapunov function, whose derivative is . For the Adam ODE neither nor works. decreases only at the rate , which says nothing about when the momentum is small. The system is also non-autonomous, with a field that is singular at and only locally Lipschitz in . As a result is only absolutely continuous, so all derivative inequalities hold only almost everywhere. A further obstacle is that the Łojasiewicz inequality at a single critical point does not by itself control the trajectory: the limit set is a connected compact subset of , and the inequality has to be made uniform on a neighbourhood of it. Finally, the rate has to be stated for an arbitrary exponent at the limit point, not only for the uniform exponent the argument produces.
is EuclideanSpace ℝ (Fin d) and is the product E × E × E, whose Mathlib norm is the maximum of the three Euclidean norms. This does not change any statement here, which concern , , separately. and are abstract, under the hypotheses of §7 (ContDiff ℝ 1 F, LocallyLipschitz (gradient F), LocallyLipschitz S, coordinatewise, coercivity as Tendsto F (cocompact _) atTop). Under Assumption 2.2 the paper's and satisfy these, so the statements imply the printed ones. A solution is a map ℝ → E × E × E constrained only on . The field uses in place of (the paper's extension, p. 12) and is never evaluated at . Statements are made for every global solution; there is exactly one (Theorem 3.1, a separate mission).
The polynomial bound is stated for , because Lean's real power gives while the paper's right-hand side is at . The constant is quantified before . A version with chosen after , or one that assumes converges, would be trivial and is not the theorem. (7.13) states absolute continuity of on every together with the almost-everywhere derivative bound, since an almost-everywhere bound alone says nothing about .
A complete development needs the Lyapunov calculus of §7.1, compactness of the trajectory, the limit-set theory behind Theorem 3.2, the uniformisation of the Łojasiewicz inequality on a compact connected set of critical points, and the Haraux–Jendoubi integration lemmas. Contributions to the last two are reusable beyond this mission and are welcome, as are proofs of the individual milestones.
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.
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.
Norms are the most common nonsmooth terms in convex optimization models. The norm promotes sparsity in the lasso and in compressed sensing, the Euclidean norm of blocks of variables promotes group sparsity in the group lasso, and the nuclear norm promotes low rank. First-order methods for such models, notably the proximal gradient method, ADMM and their accelerated and parallel variants, handle a norm term through a single operation: its proximal operator. Each iteration of these methods needs for some point and step , so a description of this operator for an arbitrary norm is needed in practice.
The monograph of N. Parikh and S. Boyd, Proximal Algorithms (Found. Trends Optim. 1(3), 2014), records this description twice. In §2.5 it derives it from Moreau decomposition, and in §6.5 it states the general scaled form: the proximal operator of a norm is the identity minus a scaled Euclidean projection onto the unit ball of the dual norm. The underlying decomposition is due to J.-J. Moreau (Proximité et dualité dans un espace hilbertien, Bull. SMF 93, 1965). The norm case is standard in convex analysis texts; Parikh and Boyd present it as the bridge between proximal operators of norms and projections onto norm balls.
Work in with the Euclidean inner product and Euclidean norm .
A function is closed proper convex if its epigraph is a nonempty closed convex set. For such and , the proximal operator is
which has a unique minimizer for every . The convex conjugate is . For a set , the indicator function is on and off , and the Euclidean projection onto a nonempty closed convex is .
Let be a general norm on , possibly different from . Its dual norm and the dual unit ball are
In the Lean development the space is EuclideanSpace ℝ (Fin n), the general norm is a seminorm N with the definiteness hypothesis IsNorm N, is dualNorm N z, is dualBall N, is indicator C, and is normFun N.
For every general norm on , every and every ,
Stated as: if and only if , for all .
MoreauProx.Decomposition.moreau_decomposition.The goal reduces evaluating the proximal operator of any norm to projecting onto one convex set, the unit ball of the dual norm. All the familiar closed forms are instances: soft thresholding for (whose dual ball is the box), block soft thresholding for (whose dual ball is the Euclidean ball), and the prox via projection onto the ball. Conversely, it lets a projection onto a norm ball be computed from the norm's proximal operator. Milestone 4, the scaled Moreau decomposition, is here stated for norms; its general form is an identity used throughout splitting methods whenever a dual or conjugate prox is cheaper than the primal one.
The results are classical and proved in the literature; the work here is formalization. Moreau's decomposition is already formalized on the platform (Moreau 1965 series, proved). Several norm-specific corollaries are posed as open problems in other series: soft thresholding (BoydADMM.Prox.prox_l1_eq_softThreshold), block soft thresholding (BoydADMM.L1.group_lasso_z_update) and projection onto a Euclidean ball (Pegasos.Analysis.projBall_isProj). A proof of the goal here gives a uniform route to such statements for any norm. The general-norm statements, the conjugate of a norm and the scaled decomposition are not formalized elsewhere on the platform.
The derivation in the monograph is two lines, but each line hides a step. Computing for a norm requires the inequality and, for , a direction along which grows without bound; the dual norm is a supremum, so finiteness and attainment have to be argued from finite dimensionality and definiteness of the norm. The scaling step requires knowing how the conjugate and the proximal operator transform under and , in extended-real arithmetic where values must be tracked. The proximal operator of an indicator being the projection is an unfolding of definitions, but the minimizer predicates on both sides must be matched, including the factor and squared versus unsquared distances.
A tempting shortcut is to work only with the Euclidean norm, where is the Euclidean unit ball; that proves a special case, not the goal.
EuclideanSpace ℝ (Fin n) for arbitrary , including . The general norm is an arbitrary Seminorm ℝ (EuclideanSpace ℝ (Fin n)) with definiteness (IsNorm); the Euclidean norm of the space is used only in the proximal objective and the projection, as in (1.1) and (1.3).EReal. The dual norm is computed in EReal as the supremum of the printed set, so it has no junk value. and are products with the positive reals , , and is a hypothesis everywhere (p. 124).IsProx g z x ( minimizes ) and "" is IsProj C z x. With , Moreau's objective is times the objective of (1.2), so it has the same minimizers. Both minimizers exist and are unique, so an equivalence over all candidate points states the printed equations exactly.conj, IsProx and IsProj come from the published Moreau 1965 series definitions MoreauProx.Decomposition.ConvexDuality and MoreauProx.Decomposition.Cones.Useful contributions include lemmas on conjugates of positively homogeneous functions, on the behaviour of IsProx under scaling, and the identity in the predicate form; all are reusable beyond this mission.
The lost-sales inventory model with a positive lead time is one of the basic models of inventory theory. A retailer reviews stock once per period, places an order that arrives periods later, and loses (rather than backlogs) any demand that cannot be met from stock on hand. Lost sales are the norm in retail, where a customer facing an empty shelf buys elsewhere. The optimal policy is the solution of a dynamic program whose state is the on-hand inventory together with the whole pipeline of outstanding orders. The state dimension therefore grows with the lead time, and computing the optimal policy is intractable beyond small : for a lead time of four and geometric demand the dynamic program already has 228,581 states (Zipkin 2008a, Operations Research 56(5), 1256–1263).
Heuristics (base-stock, myopic, cost-balancing) have been studied at length. Reiman (2004) analyzed an open-loop policy that orders one unit at fixed intervals in a continuous-review lost-sales model with Poisson demand. Zipkin (2008a) observed numerically that ordering the same constant amount every period performs well already at lead time four. Huh, Janakiraman, Muckstadt and Rusmevichientong (2009) proved that order-up-to policies are asymptotically optimal as the lost-sales penalty grows. Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante proved that a constant-order policy is asymptotically optimal as the lead time grows, with an explicit threshold. This mission formalizes that result, Theorem 1 of their paper.
Fix a holding cost per unit left over at the end of a period, a lost-demand penalty per unit of unmet demand, a lead time , and a horizon . Demands are i.i.d. with a law on that has a finite third moment and is not deterministic. At the start of period the system holds inventory and a pipeline of outstanding orders. First arrives; then an order is placed and joins the end of the pipeline; then is realized, and
The system starts empty. A policy chooses each order from the information available before the period's demand, possibly with randomization. Problem (1) is
For let , the steady-state waiting time of a GI/D/1 queue. For the constant-order policy orders the random amount (drawn independently of the demands) in the first period and in every later period. The best constant is (the smallest minimizer). With the quantile of , , the standard deviation and the skewness of , set and
For all , and ,
The milestones follow the paper's argument in its order:
The theorem says that the policy which ignores the state entirely, ordering the same amount every period after a single randomized first order, loses at most a factor against the optimal policy once the lead time exceeds an explicit threshold. The threshold depends only on , and the demand law. Optimal policies are out of computational reach precisely when is large, so this is the first guarantee of near-optimality whose computation does not grow with the lead time. The paper's Corollary 2 (the ratio tends to as ) follows directly.
The result is proved in the paper (up to the correction below); this platform holds no formalization of it or of its lemmas. A formalization would produce reusable statements about suprema of random walks with negative drift (Lemma 9, (26)), a quantitative central limit theorem for Lipschitz test functions (Theorem 11), and the finite-horizon lost-sales problem built on the published model of this platform.
The obvious comparison fails. An optimal policy may vary its orders arbitrarily over time, so its pipeline need not look like a constant stream. Comparing it period by period with gives nothing, because the inventory of is driven by an unbounded random-walk supremum.
The paper instead bounds the optimal cost over any consecutive periods by the cost from the most favourable state. It then has to show that the average of that state's pipeline stays bounded away from uniformly in . This last step is the crux. The components of may vary considerably over the window, and a qualitative central limit theorem is not enough: the argument needs an explicit rate (Theorem 11) with constants that survive summation over windows. On the probabilistic side, the expectations of random indices at which random walks attain their maxima are not adapted to the demand filtration. They are controlled only through the distributional identity of Lemma 9 and the geometric tail (26).
The model is the published CappedBaseStock_Model. Its parameter record supplies , and the penalty (field p; the record is called prm). Its demand law supplies a probability law on with finite positive mean. The finite third moment and non-determinism are explicit hypotheses. and are the published newsvendorLevel and backorderCost. The conventions:
A correction. As printed, the second term of (p. 5) and of Corollary 12 (p. 14) lack a factor . The proof of Corollary 12 establishes , and the printed bounds are not invariant under rescaling the demand. Both are stated here with the factor restored, and each item's note says so.
Neither a long-run average cost nor a restricted comparator (stationary, Markov, or bounded-order) may replace the finite-horizon OPT. The demand law may not be specialized, and may not order in its first period: each change makes the goal a different, easier theorem.
A complete development needs Lindley-type recursions and the stationarity of the GI/D/1 waiting time, Chernoff and moment bounds for random-walk maxima, a Stein-method CLT rate, and the existence of optimal policies for a finite-horizon problem with a continuous state. The random-walk and CLT parts are independent of inventory theory and reusable. Proofs of any milestone are welcome, as are alternative proofs of the goal.
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.
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.
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).
A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture: a minimal counterexample to any of them, if one exists, is a snark. Lists of all small snarks are therefore used to test such conjectures by computer.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, 2013) generated all snarks on up to 36 vertices. Testing 3-edge-colourability is NP-complete, and only a vanishing fraction of cubic graphs are snarks (0.00044% of the cubic graphs of girth at least 5 on 28 vertices, p. 4), so the generation algorithm needs cheap criteria that recognise, before a graph is built, that it will be colourable and can be skipped. Section 3.1 of the paper supplies such a criterion for the last construction step, and this mission formalizes it.
All graphs are finite and simple. A graph is cubic if every vertex has degree 3. A 3-colouring of a graph is a map that gives different colours to any two distinct edges sharing an end-vertex; is colourable if it has one, i.e. its chromatic index satisfies (p. 2, Isaacs' terminology).
A 2-factor of is a spanning 2-regular subgraph (p. 4); each connected component of is a cycle. is an even 2-factor if all its cycles have even length (p. 5). For a 3-colouring and colours , write for the spanning subgraph whose edges are those coloured or .
The edge insertion operation (Figure 1(d), p. 5) takes two distinct edges and of , which may share an end-vertex, subdivides by a new vertex and by a new vertex , and adds the edge . The resulting graph has vertex set and edge set
If is cubic, so is . In the generation algorithm every graph of girth at least 4 is produced from a graph with two fewer vertices by this operation.
Let be a cubic graph with a 3-colouring , let be colours, and let , be distinct edges of lying on the same cycle of . Then
Theorem 3.4 (p. 6, stated as folklore without proof). If is a colourable cubic graph and the inserted edge lies on a 4-cycle of , then is colourable.
The result. Theorem 3.3 is the look-ahead of the snark generator: one 3-colouring of a graph on vertices excludes, at once, every pair of edges lying on a common cycle of one of its three bicoloured 2-factors. For 28 vertices the first colouring alone discards on average 85% of the candidate edge pairs (p. 6), and the overall ratio of weak snarks among generated graphs on the last level improves by a factor of 85 (p. 4). The enumeration of all snarks up to 36 vertices, on which the paper's counterexamples and statistics rest, depends on this pruning being sound: a wrong pruning rule would silently delete snarks from the lists. Theorem 3.4 is a second pruning rule of the same kind.
Formalizing it. The results are proved (Lemma 3.1 is classical; the paper gives the argument for Lemma 3.2 in one sentence and for Theorem 3.3 by combination). None of them, and no statement about 3-edge-colourings of cubic graphs and their 2-factors, is formalized on the platform. The mission produces a machine-checked soundness proof of the pruning criterion and, along the way, a reusable development of the equivalence between 3-edge-colourings and even 2-factors in Lean's SimpleGraph library. Theorem 3.4 has no proof in the paper.
The combinatorial content is short; the difficulty lies in graph-theoretic infrastructure that Mathlib does not have. Lemma 3.1 relates a global object (a proper colouring of all edges) to the cycle structure of a spanning 2-regular subgraph, and either direction needs the description of a finite 2-regular graph as a disjoint union of cycles together with parity information along each cycle. Mathlib has walks, cycles and connected components, but no decomposition of a 2-regular graph into cycles and no notion of the length of a component as a cycle.
Lemma 3.2 and Theorem 3.3 change the vertex type: lives on , so 2-factors, connected components and cycle lengths must be transported from to , and the case where and share an end-vertex (allowed by Figure 1(d)) has to be handled alongside the generic one. A first idea, to extend a given 3-colouring of directly to , does not work in general: the colours forced on the edges at and by the old colours of and can conflict, and the hypothesis "same cycle" is what has to be used to avoid the conflict.
Vertices form a type V with [Fintype V] [DecidableEq V]; graphs are SimpleGraph V with decidable adjacency, and "cubic" is Mathlib's G.IsRegularOfDegree 3. Colourability is G.lineGraph.Colorable 3 (an edge colouring, not a vertex colouring), and a 3-colouring is G.lineGraph.Coloring (Fin 3). A 2-factor is a graph F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2; it is even if every connected component has an even number of vertices (Nat.card). The edge insertion operation produces a graph on V ⊕ Fin 2, with Sum.inr 0 subdividing and Sum.inr 1 subdividing ; edges are unordered pairs Sym2 V. "On the same cycle" is encoded as membership of both edges in the 2-factor plus reachability of their end-vertices inside the 2-factor. Oddness is not defined as a number; Lemma 3.1 is stated in its second form.
Dropping "on the same cycle" would make Theorem 3.3 and Lemma 3.2 false (inserting edges between different cycles of a bicoloured 2-factor is exactly how snarks are produced), and both statements require the two edges to be distinct; a formalization without either hypothesis is ruled out. Every statement assumes cubicity, without which Lemma 3.1 fails.
Out of scope: the algorithmic content of §3 (isomorphism rejection, the look-ahead implementation, recolouring along non-hamiltonian cycles, the 85% / 11% / 3.4% statistics), the generation counts, and every exhaustive-search claim of the paper. The remaining results of the paper are covered by three sibling missions of this series.
Reusable beyond this mission: the 2-factor and even-2-factor definitions, the two-colour 2-factor of an edge colouring, and Lemma 3.1 itself. Contributions welcome: the cycle decomposition of finite 2-regular graphs, alternating colourings of even cycles, and a proof of Theorem 3.4.
Quasi-Newton methods replace the Hessian of an objective by a matrix that is updated from observed pairs of steps and gradient changes. The secant equation asks the new matrix to map the observed steps to the observed changes . The best-known update is BFGS, which for simultaneous pairs reads
Schnabel (Quasi-Newton methods using multiple secant equations, technical report, University of Colorado at Boulder, 1983, reference [25] of the paper) studied such multiple-secant updates; one of his results is that a positive definite with exists exactly when .
Dahl and Andersen (Math. Program. 194:341–370, 2022) use multiple-secant BFGS updates to build primal-dual scaling matrices for an interior-point algorithm on the nonsymmetric exponential cone, following Tunçel (Found. Comput. Math. 1:229–254, 2001) and Myklebust and Tunçel (arXiv:1411.2129). In their setting , and they need the update in factored, low-rank form. Their Theorem 2 supplies it: the term , and its counterpart for the inverse update, are computed by rank-one steps. These steps resemble single-secant quasi-Newton updates, and no inverse is formed. This mission formalizes Theorem 2 and the steps of its proof.
Let and . Write for the -th unit vector of and for the inner product of , so that . The hypothesis of the theorem is
meaning that the matrix is symmetric and positive definite.
For the recursions (25)–(26) are
Both updates of step use the previous pair . Collect the vectors into and .
The proof uses two more objects. The first is the matrix
The second is , the principal submatrix formed by the last rows and columns of . In Lean these are ExpConeIPM.Secant.Ys, Ss, d, V, U, L and Ψ, all in one definition item.
The first identity of the goal follows from milestones 4 and 5. The paper says the second "follows similarly". The analogous identity is not displayed in the paper, so it is not a milestone.
The result. Theorem 2 expresses the multiple-secant part of the BFGS update (23), and of its inverse, as a sum of rank-one terms and . Each term comes from a recursion that touches one column at a time. On pp. 359–360 Dahl and Andersen apply it twice with . This gives the BFGS scaling of their exponential-cone algorithm as an explicit rank-3 update of , which is how the algorithm implemented in MOSEK computes its scaling matrices (§6, p. 361 of the paper). The argument is a Cholesky factorization of carried out implicitly on the factors and .
Formalizing it. The theorem is proved in the paper, in under a page. Its proof leaves two steps implicit. The first is that the symmetry of every , which (27) and the step to use, propagates from . The second is the second identity, which the paper does not prove. A machine-checked proof records both. To our knowledge no proof assistant has a formal treatment of multiple-secant updates. The recursion also gives a reusable statement: a column-by-column Schur-complement process on a product produces its Cholesky factor.
The obvious route expands directly and compares it with . This leads nowhere, because depends on all earlier steps through and . The step that carries the proof is an invariant over the recursion. The trailing blocks of must stay symmetric positive definite, and the leading columns of and must stay zero. Both must be maintained together through a pair of coupled updates, in which is updated with the old . A second difficulty is bookkeeping: the paper's 1-based columns, the step count , and the trailing block of size shift relative to each other.
The hypothesis needs care. If is only assumed to satisfy for , without symmetry, the identities are false in general. A instance whose symmetric part is positive definite, with a small antisymmetric part, violates the first identity by in the largest entry.
Everything is real matrix algebra over Matrix (Fin n) (Fin p) ℝ, with arbitrary (including , where both sides are zero). The formalization commits to the following conventions.
Matrix.PosDef, which includes symmetry. The inverse is Matrix.inv. It is a genuine inverse under this hypothesis.j : Fin p is the paper's . Ys Y₀ S₀ k and Ss Y₀ S₀ k are and after steps, and they are left unchanged after step . d Y₀ S₀ j is .Real.sqrt. The division by it is multiplication by an inverse. Both return junk values on non-positive arguments, which never occur under the hypothesis; milestone 2 states this.No repair of the printed statements was needed. On p. 359 two misprints are not copied: for , and for . The definition of uses .
A complete development needs rank-one updates of products, Schur complements of a positive definite matrix in its leading entry, and inverses of for an invertible . Schnabel's existence theorem (Theorem 1 of the paper) and the applications on pp. 359–360 are outside the mission. A general lemma on Schur-complement recursions producing Cholesky factors would be reusable on its own. Contributions on the U-side identity are welcome.
Nonnegative matrix factorization (NMF) approximates a data matrix by a product of two nonnegative factors. Adding a cap on the number of nonzero entries of each factor gives sparse NMF, used in signal separation, text mining and image analysis because sparse nonnegative factors are easier to interpret. Bolte, Sabach and Teboulle (Math. Program. 146 (2014)) introduced the algorithm PALM (proximal alternating linearized minimization) for problems of the form with nonconvex, nonsmooth and , and proved that its bounded runs converge to critical points when the objective has the Kurdyka–Łojasiewicz property. Sparse NMF is the paper's main application (§4).
PALM is only implementable when the proximal map of each nonsmooth term can be computed. For sparse NMF the nonsmooth term is the indicator of the nonconvex set of nonnegative matrices with at most nonzero entries. Proposition 4.1 of the paper computes that proximal map in closed form. This mission formalizes Proposition 4.1 and the steps of its proof. The convergence theory of PALM is a separate mission of the same series.
Matrices are real arrays . The squared Frobenius norm is . The sparsity count is the number of nonzero entries of , and means for every .
For a set , the indicator is on and off . For a natural number , set
the function that is on nonnegative matrices with at most nonzero entries and elsewhere.
For and , the proximal map (2.2) of the paper is the set
Throughout, is the set of all points of where attains its smallest value on .
The hard-thresholding operator of Definition 4.1 is
which is multi-valued when the largest entries of in absolute value are not uniquely determined. The projection onto the nonnegative orthant is , componentwise.
In the proof, is fixed and , , with partial squared norms .
For every and every ,
Both equalities are equalities of sets, and both are part of the goal.
The result. Proposition 4.1 says that the proximal step for the nonnegative sparsity constraint is computed by clipping the negative entries of to zero and then hard-thresholding: keeping entries of largest magnitude and zeroing the rest. The paper remarks that this costs operations. It is what turns PALM into the explicit algorithm PALM-Sparse NMF, and the same formula applies to any method that needs a projection onto nonnegative sparse matrices (projected gradient methods, iterative hard thresholding with sign constraints).
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The platform has a projection-onto-sparse-vectors statement without nonnegativity and stated as a single inclusion, which is a different theorem. The mission produces a set-level statement that handles ties, the degenerate cases and , and the interaction of the sign and the sparsity constraints, all of which the informal proof passes over quickly.
The obvious argument is: "project onto the nonnegative orthant, then onto the sparse matrices". Composing two projections onto nonconvex sets is not in general the projection onto their intersection, so this argument is not valid as it stands; the equality holds here because of the specific coordinate structure, and the proof must show it. The second obstacle is that everything is set-valued: when several entries of tie for the -th largest magnitude, has several elements, and the equality must account for every one of them, in both directions. The step "(4.1) = (4.2)" and the removal of are dismissed in the paper as "a simple contradiction argument" and "arguing in a similar way"; each needs an explicit modification of a feasible point that preserves sparsity and does not increase the objective.
Matrices are Matrix (Fin m) (Fin n) ℝ, with 0-based indices (harmless relabelling of ). is the Frobenius inner product of the published definition CaiCandesShen.ProximalLimit.Basic. The indicators and take values in EReal, with ; membership in is the inequality in EReal for every . The proximal map carries the weight of (2.2), not . is defined by the componentwise formula. No restriction is placed on .
Every operator in the statement is a set of minimizers. A formalization that selects one element (for instance "keep the largest entries with a fixed tie-break") proves only one inclusion of a weaker statement and does not count.
The development needs only finite sums and the argmin-set definition shared by all items; no further library is required. Lemmas about hard thresholding on matrices (the description of by largest entries, nonnegativity of of a nonnegative matrix) are reusable well beyond this mission, and contributions of such lemmas are welcome.
Theorem numbers and page numbers refer to the author version of the paper (36 pages, printed page = PDF page), not to the Springer typesetting.
In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.
Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation of a set-partitioning formulation , rather than on the LP relaxation of that formulation. Their Theorem 2 is the justification for that design choice: the best bound can deliver is never weaker than , and can be strictly stronger. This mission formalizes that comparison.
An instance has a depot , satellites and customers , a symmetric travel cost (in which the fixed vehicle costs have already been folded into the depot–satellite and satellite–customer entries), positive integer demands , capacities for first- and second-level vehicles, a bound on first-level vehicles, second-level vehicles at satellite , a global bound on second-level vehicles, a capacity and a unit handling cost for each satellite.
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the cost of that closed walk. A second-level route leaves satellite , visits a set of customers and returns; its load is , counts its visits to customer , and its cost is its closed-walk cost plus .
Formulation uses binaries (route of satellite is used), binaries , and nonnegative integers (quantity route delivers to satellite ). It minimizes subject to: each customer is covered exactly once (2); at most routes at satellite (3) and overall (4); the load delivered from satellite is at most (5); at most first-level routes (6); what first-level routes bring to satellite equals what its second-level routes carry (7); and (8).
The LP relaxation replaces the integrality of by , . Its value is , equal to when is infeasible.
The relaxation relaxes (2)–(4) with penalties , and , and replaces the second-level routes by marginal routing costs that must satisfy, for every route ,
Its variables are binaries (customer is supplied from satellite ), and ; it minimizes
subject to single assignment of each customer, flow balance , satellite capacity , and (6), (8). A choice with and (12) is admissible.
Formally: (1) for every instance and route families whose is feasible, some admissible satisfies ; (2) some instance, route families and admissible choice give .
Theorem 2 places the relaxation in the hierarchy of bounds for the 2E-CVRP. The remark on explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so degrades as first-level routing costs grow. keeps binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through . The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation of the paper worth computing.
The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on needs positive first-level route costs, and the "max" in Theorem 2 is attained only when is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than .
is not the Lagrangean dual of in the textbook sense: it changes the variables (customer-to-satellite assignments instead of routes ), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of , an admissible that is compatible with the flow-balance and capacity constraints of . For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, , route loads at most , ), and must be feasible, so that the gap is a genuine gap between finite bounds.
Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families , are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, variables real. Optimal values are infima over the feasible set in EReal, for an infeasible problem; there is no junk value .
Part 1 of the goal assumes feasible: when is infeasible the printed relation would read "", which is not attained by any single choice of penalties. Part 2 requires , which rules out the trivial witness of an instance with infeasible; admissibility includes , without which the supremum is for trivial reasons.
The definitions (instance, route systems, , , (12), ) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect to the platform's general-form LP and its strong duality theorem are welcome.
Differential privacy (Dwork, McSherry, Nissim, Smith 2006) asks that a randomized algorithm run on a database behave almost identically whether or not any single record is changed. A central question for data curators is non-interactive release: publish, once, a sanitized object (ideally a synthetic database) from which analysts can answer many statistical queries accurately. Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that over a discrete data universe this is possible for every class of counting queries of bounded VC-dimension, with accuracy governed by the VC-dimension and the logarithm of the universe size.
That dependence on the universe size raises an obvious question: can the discretization be removed? For real-valued data the class of interval queries ("what fraction of the records lies in ?") has VC-dimension 2, so a learning-theoretic intuition suggests that releasing a database accurate for all intervals should be easy. Section 5 of the paper shows that it is impossible under differential privacy. This mission formalizes that impossibility.
The phenomenon was later quantified: Bun, Nissim, Stemmer and Vadhan (FOCS 2015) showed that for approximate differential privacy, releasing threshold queries over a finite ordered domain of size requires sample size growing with , so that the infinite case is impossible for approximate privacy as well. The present result is the pure-privacy statement for the real line.
A real-valued database of size is a tuple . Two databases are neighbours if they differ in exactly one coordinate. A mechanism maps each database to a probability distribution on a measurable output space . It is -differentially private if for all neighbours and all measurable ,
For real the interval query is . A mechanism with a readout (the answer that output gives to ; for synthetic data , ) is -useful for interval queries if for every database ,
A real number is a -percentile point of (the paper's " percentile" with ) if at least entries satisfy and at least entries satisfy . A mechanism with real outputs answers median queries usefully with positive probability if on every database its output is a -percentile point with positive probability.
In Lean, databases are Fin n → ℝ; neighbours and differential privacy are the published PrivLearn.Generic.Neighbors and PrivLearn.Generic.IsDP; the new objects are intervalQuery, IsPercentile, AnswersMedianUsefully and UsefulIntervals in PrivateRelease.Continuous.
For every , and , no -differentially private mechanism with a measurable readout is -useful for interval queries on :
No constant is hard-coded; the thresholds are the paper's.
For every , and real , no -differentially private mechanism answers median queries usefully with positive probability on every database:
The result. Corollary 5.2 is the reason the paper's general release mechanism needs a discretized data universe and why its halfspace mechanism (§6) relaxes usefulness to large-margin queries. More broadly it separates private release from non-private learning: the class of intervals is learnable from samples without privacy, yet no pure-private mechanism can release it at all over . It anticipates the line of work on private learning of thresholds and the role of the domain size in private query release.
Formalizing it. Both statements are proved in the paper; neither is, to our knowledge, machine-checked. A formal proof needs the countability of the atoms of a finite measure on , the stability of differential privacy under measurable post-processing, and a measurable selection of a percentile point from approximate interval answers. These pieces (especially post-processing for general measurable outputs) are reusable across formalized differential privacy.
The obvious argument for Theorem 5.1, a direct comparison of two neighbouring databases, gives nothing: changing one record moves the percentile set only slightly, and differential privacy allows each probability to change by a factor , so no single pair of neighbours yields a contradiction. A naive appeal to "the median reveals a record" also fails, since the statement must exclude even mechanisms that are correct with tiny positive probability.
For Corollary 5.2 the difficulty is measure-theoretic: the usefulness event intersects uncountably many conditions, the release must be converted into a single real output measurably, and the converted output must be a percentile point on the useful event for every real database, not only those in .
Conventions committed to in Lean:
Fin n → ℝ with ; the paper's neighbour relation "" is read as replace-one-entry.IsProbabilityMeasure (A z) is a hypothesis). Theorem 5.1's outputs live in with its Borel σ-algebra.Contributions welcome: a proof of Theorem 5.1; a general post-processing lemma for IsDP; the reduction from interval usefulness to median answers.
Many problems in data analysis and signal processing are posed as minimizing a sum of three terms over two blocks of variables: a nonsmooth function of the first block, a nonsmooth function of the second block, and a smooth coupling term. Nonnegative and sparse matrix factorization, blind deconvolution and dictionary learning all have this form, with constraints or sparsity penalties as the nonsmooth parts. The functions involved are usually nonconvex, so convexity-based convergence theory does not apply, and the classical alternating minimization (Gauss–Seidel) scheme requires solving an exact nonconvex subproblem in each block.
Bolte, Sabach and Teboulle (Math. Program. 146 (2014)) introduced Proximal Alternating Linearized Minimization (PALM), which replaces each exact block minimization by one proximal-gradient step, and proved that every bounded sequence it generates converges to a critical point whenever the objective has the Kurdyka–Łojasiewicz property. The result became a standard template for the convergence analysis of first-order methods on nonconvex, nonsmooth problems.
Timeline.
Let and , let , and set
The product carries the Euclidean norm . Assumption A: and are proper (never , finite somewhere) and lower semicontinuous, and is . Assumption B:
The proximal map of with parameter is the set
Fix . A sequence is generated by PALM if, from an arbitrary , with and ,
The limiting subdifferential consists of the limits of Fréchet subgradients at points with ; is critical if . Let be the class of continuous concave functions with , on and there. A proper lsc has the KL property at if there are , a neighbourhood of and with
and is a KL function if it has this property at every point where is nonempty.
If is a KL function, Assumptions A and B hold and is a bounded sequence generated by PALM, then
The result. Theorem 3.1 gives convergence of the whole sequence, not only subsequential convergence, for a method whose steps are explicit: a gradient step on followed by a proximal step on or . The KL hypothesis holds for semi-algebraic, subanalytic and o-minimal data, which covers penalties, rank constraints and polynomial couplings. The paper applies the theorem to sparse nonnegative matrix factorization (Theorem 4.1), and the same scheme (sufficient decrease, relative error, KL) underlies many later convergence proofs for nonconvex splitting and alternating methods.
Formalizing it. The result is proved on paper; no machine-checked proof is known to exist. A formalization produces reusable components: the nonconvex proximal-gradient decrease lemma, the structure of limit point sets of sequences with vanishing steps, and the uniformized KL lemma, which is independent of PALM and is used in essentially every KL-based convergence proof.
Lemmas 3.2–3.5 are estimates and compactness arguments; the core difficulty is in passing from them to convergence. Square-summability of the steps (Lemma 3.3) does not give summability of the steps themselves, and a bounded sequence with vanishing steps may wander along a continuum of limit points. The KL inequality supplies the missing control, but only near each critical point separately, with point-dependent and ; the iterates are known only to approach the compact set , not a single point. Combining Lemma 3.6 with the decrease and relative-error estimates requires handling the concave function along the sequence and an extended-valued whose subdifferential is a limiting construction. Lemma 3.5(i) also needs along subsequences, which lower semicontinuity alone does not give.
, are EuclideanSpace ℝ (Fin n), EuclideanSpace ℝ (Fin m), and the product is the product WithLp 2 (… × …) of the published setting ProxAltMin.Conv.Setting, not Lean's default product with the sup norm. Values in are EReal. The prox map is a set with weight , exactly as in (2.2). Iterates are selections from it, and the starting point is arbitrary, so is allowed; inequalities between values of are stated with the difference moved across. are given modulus functions and fixed constants. The limiting subdifferential and the KL notions are the published definitions NonconvexSplitting.Shared.LimitingSubdiff and NonconvexSplitting.ADMMKL.KLProperty, with real and the KL inequality read for every (equivalent to the form). Assumption A together with B(iv) is AssumptionH; B(i)–(iii) and the PALM run are defined in PALM.Conv.Setting. The satisfiability of all hypotheses of the goal has been checked on a concrete instance.
The goal is not weakened: it asserts summability of and convergence of the full sequence to one critical point, not that every cluster point is critical (that is Lemma 3.5(i)). The constants and are explicit as in the paper, with chosen once for all .
Theorem numbers and pages are those of the author version (source PDF), whose page numbers coincide with its printed pages; they may differ from the Springer typesetting.
Welcome contributions: proofs of any milestone; a general-space version of Lemma 3.2; a proof of the published Proposition 2.1 (ProxAltMin.Conv.proposition_3, still open), which Lemma 3.4 relies on.