Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A retailer that sells products in several categories has to decide which products to put on display. Under the nested logit model a customer first picks a category (a nest) and then a product inside it, so offering a product changes the purchase probabilities of every other product. Choosing the assortment that maximizes expected revenue is assortment optimization, a standard problem of revenue management. Gallego and Topaloglu (Management Science, 2014) study it when every nest carries its own constraint on the assortment. With a limit on the shelf space of each nest the problem is NP-hard even for a single nest, so the paper builds an assortment that is guaranteed to earn at least half of the optimum.
A worst-case factor of two says little about one concrete instance. For its computational study (§7.1) the paper therefore needs, instance by instance, a number that is provably at least the optimal expected revenue, and it obtains one from a linear program, (13), whose constraints come from the linear programming relaxations of knapsack problems. Proposition 7 (Online Supplement A, p. 33) proves that this linear program does give an upper bound. This mission formalizes that proposition.
There are nests and products in each nest. Product of nest has a preference weight and a revenue (any real number); is the preference weight of buying nothing, and is the dissimilarity parameter of nest . For an assortment of nest put
with for the empty assortment . The expected revenue of is
Under space constraints product of nest uses units of space and nest has capacity , with for every product, so the feasible assortments are . Problem (1) is .
For a scalar , the knapsack problem (10) of nest maximizes over with . Its linear programming relaxation allows . The paper partitions into finitely many intervals , , on each of which one vector solves the relaxation. For a fractional vector it writes and .
The linear program (13) in the variables is
If is an optimal solution of (13), then
The proposition makes the optimality gaps of §7 meaningful: the expected revenue of any assortment that respects the space constraints, divided by the optimal value of (13), is a certified lower bound on its fraction of . The bound is a linear program with variables and one constraint per interval solution, so it can be solved for instances where itself, an NP-hard quantity, cannot be computed.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it checks the interplay of three ingredients that the paper treats briefly: the role of the interval solutions (only their feasibility and their optimality for every matter), the extension of and to fractional vectors, and the concavity of . A related but different program is Davis, Gallego and Topaloglu's LP (16) (NestedLogitVariants.LP.lp16_upper_bound), which bounds the unconstrained problem by another argument.
The constraints of (13) are indexed by finitely many fractional vectors, while is attained at an integral assortment that need not be among them. The obvious argument, that (13) is a relaxation of an exact linear-programming formulation of problem (1), does not apply: no constraint of (13) involves directly. The link between the two has to be made nest by nest, through the knapsack relaxations at values of that depend on the unknown optimum, and the fractional vectors are compared with integral assortments through the nonlinear map .
The formalization references the published nested logit model NestedLogitVariants.General.Model (instance, , , , ) and NestedLogitVariants.General.Relaxation (the unit box and the term of the constraints of (13)). The conventions are:
Fin n, indexed from ; assortments are finite sets of products and is the empty set;Real.rpow, and , which gives as in the paper and makes the constraint term at equal to ;The statement is not to be trivialized: setting , taking to be the whole box (not a finite set and not LP (13)), assuming , or proving the bound for one particular feasible point are all excluded.
A complete development needs the concavity (tangent-line) inequality of at a positive point and elementary facts about fractional knapsack relaxations; both are reusable. Proofs of the milestones and of the goal are welcome.
The Frank–Wolfe algorithm minimizes a smooth convex objective over a compact convex domain by choosing an atom through a linear optimization problem and moving toward it. On a domain that is the convex hull of atoms, each ordinary iteration introduces at most one new atom. That makes the method useful when a solution represented with few atoms is valuable, but it raises a basic question: how much accuracy can a solution with only a few atoms attain? Jaggi's 2013 analysis gives upper bounds on primal error and duality gap for four Frank–Wolfe variants. Its sparsity section supplies a matching obstruction on the unit simplex. This mission isolates that obstruction so the claimed dependence on sparsity can be checked independently of any particular implementation of the algorithm.
The paper calls the number of used atoms the sparsity of an iterate. It proves two lower bounds for one quadratic objective: a sparse point cannot have arbitrarily small objective value, and, with fewer active coordinates than the simplex dimension, it cannot have arbitrarily small duality gap. These are worst-case statements about feasible points themselves. Consequently, any method whose iterates retain the stated sparsity is subject to them, regardless of how it selects its next atom. The source statements and constants are Lemma 3 and Lemma 4, PDF p. 5.
Let be a positive integer and let the unit simplex be
For a vector , let be the number of nonzero coordinates. The objective is the squared Euclidean norm . Its minimum on the full simplex is , reached at the uniform point. The paper compares that optimum with the best value permitted by a bound on . The dimension and sparsity budget are separate: the goal assumes , so at least one coordinate must be zero at every eligible point.
The duality gap at a feasible is
For a convex objective, this gap bounds the difference between the current objective value and the optimum; the paper introduces that certificate in display (2), PDF p. 2. Here the maximum exists because the simplex is nonempty and compact and the expression is continuous in . It is the same certificate computed by minimizing a linear function over the domain in a Frank–Wolfe step. The paper's Table 1, PDF p. 6 identifies the simplex linear subproblem with choosing a coordinate having the largest coefficient.
For , Lemma 3 asserts an attained minimum:
The associated primal-error statement says that a point with exactly nonzero coordinates has , where is an optimizer on the full simplex. The minimum and the primal-error reading are both included as draft theorems.
For every natural number , Lemma 4 states the mission goal:
The threshold is essential to this exact value. If all coordinates may be active, the uniform optimizer has zero gap. The case is formally allowed by the paper's natural-number wording, but has no eligible simplex point. The formal statement keeps the paper's quantifier order and does not add a positive- hypothesis.
Three milestones accompany the goal. The first records that an atomic set and its convex hull have the same support function. The second records the simplex support value from Table 1. The third is Lemma 3's attained sparse minimum. They are stated as mathematical claims independent of any algorithmic running-time assertion.
The source's convergence analysis gives error guarantees that decrease with the number of iterations, while its simplex example shows that using only atoms leaves primal error at least and, for , gap at least . Together they delimit what the paper's sparsity guarantees can achieve. The duality-gap claim concerns a certificate of approximation quality, so it applies even when the optimal value is unavailable to an algorithm. The result is already proved in the 2013 paper; the open work here is its Lean formalization and the finite-dimensional facts needed to connect sparse coordinates, linear optimization, and the gap.
The formalization also produces reusable interfaces for sparse simplex optimization: a coordinate-count notion of sparsity, an attained minimum formulation, and a support-function statement that avoids making a real supremum silently return a default value on an empty or unbounded set. These can serve later work on atomic methods without tying that work to one choice of Frank–Wolfe steps.
Bounding the quadratic objective alone does not establish the duality-gap statement. The gap also involves the best linear comparison point in the simplex. The unrestricted simplex optimum, the optimum under a sparsity budget, and the best linear comparison are different objects and must retain their respective domains. An encoding that replaces the gap's domain with the sparse feasible set would change the theorem. Another easy mistake is to use the ambient norm of a function as the objective: that norm is the supremum norm, whereas the paper uses the Euclidean squared norm.
The paper's displayed curvature value is included as a companion statement. It uses the Euclidean diameter of the simplex, which is for . The one-dimensional simplex is a single point, so extending that equality to would be false. The formalized companion makes the dimension condition explicit.
Vectors are functions . The domain is Mathlib's ; the objective is an explicit sum of coordinate squares, and sparsity counts nonzero coordinates. The gradient pairing in the source is represented by the Fréchet derivative applied to a direction. For this quadratic, the two agree coordinate by coordinate. The duality gap is a real supremum of those derivative values over the simplex. Its use in the goal is guarded by , which implies and makes the simplex nonempty; compactness makes the supremum a maximum. The support-function milestone states equality through all upper bounds, so it also has a meaningful reading for empty or unbounded atomic sets.
The curvature set follows display (3), PDF p. 3, with step size because the printed quotient has no value at zero. The companion assumes , a necessary dimension pin beyond the paper's sentence. Other standing conditions of the general problem are discharged by the chosen quadratic and simplex, rather than added as free hypotheses. No theorem assumes the quadratic minimum, a gap maximizer, or a zero coordinate as a premise; those are consequences to be established from feasibility and sparsity. The source PDF contains the statements but not its cited appendix proofs, so formal proof contributions may use other valid arguments. The simplex support, sparse minimum, and curvature interfaces are reusable beyond this mission.
An assortment planner chooses which products to offer to arriving customers. When products are grouped into nests, a customer's choice of nest depends on all the assortments offered at once. A planner may nevertheless be able to generate only a short list of promising assortments for each nest. The remaining task is to choose one assortment from each list so that their combined expected revenue is as large as possible. Testing every combination requires a number of evaluations equal to the product of the list sizes. Gallego and Topaloglu show that the choice can instead be described through a linear program whose number of constraints grows with the sum of those sizes; this is Theorem 2 of their 2014 paper, in the authors' September 11, 2013 manuscript, pp. 10–12.
This mission isolates that selection result. Later parts of the paper address how to construct useful candidate lists under cardinality, space, and pricing constraints. Here the candidates are already given, and the question is which combination earns the most. The result matters whenever the candidate lists are much smaller than the space of all assortments: it makes the last step of those algorithms an exact optimization over the candidates, without enumerating their Cartesian product.
Let be a finite set of nests and a finite set of products available in each nest. An assortment is the set offered in nest . Product in nest has preference weight and revenue . The empty assortment is allowed. The main model has no within-nest no-purchase option, so its total offered weight is . The conditional revenue in nest is , with under the paper's convention.
The weight of no purchase outside the nests is . Each nest has a dissimilarity parameter . Its attraction weight is . The expected revenue of a combined assortment is
For each nest, is a finite nonempty collection of candidate assortments. The paper obtains these from a feasible set , which may impose a cardinality or space constraint; Theorem 2 compares only combinations drawn from the supplied candidates. Equation (2) defines a real scalar through the maximum, over separately, of . Problem (3) selects a maximizing candidate in each nest at that scalar. Linear program (4) has decision variables , minimizes , and imposes and for every and every .
The goal is the exact candidate-selection claim of Theorem 2. If minimizes among all feasible pairs of program (4), and every solves problem (3) at , then
The milestones record three statements from pp. 11–12: equation (2) has a unique real root; the balance equation and its inequality form characterize the expected revenue of a fixed assortment; and Lemma 1 identifies the root as the best revenue attainable from candidate combinations while showing that local maximizers attain it. They separate the paper's numerical characterization of the best candidate revenue from its LP formulation. The target does not prescribe how the candidate lists were generated or claim that the selected combination is best among assortments outside those lists.
The theorem gives an exact, compact choice rule for assembling nestwise candidates. If the lists contain useful assortments under the original constraints, their best combination can be selected through program (4). The rest of the paper establishes candidate-generation and approximation results under particular constraint families; the stitching theorem supplies the common final selection step for those results. A larger candidate list may improve the obtainable revenue, but its Cartesian product need not be searched explicitly. The authors' manuscript, p. 12, states that program (4) has variables and constraints when the candidates are indexed by .
Formalizing the theorem yields a reusable statement about the interaction of a fractional revenue objective, independent nestwise candidate families, and a shared scalar LP. The published Prove2Me definition NestedLogitVariants.LP.Model already supplies the instance, , , , and the feasibility and optimality predicates for program (4). Its previously proved lp4_opt_binding concerns an equality at an LP optimum under ordered, nonnegative revenues; it does not contain Theorem 2's maximality claim under this paper's revenue assumptions. The four statements in this mission are draft targets awaiting machine-checked proofs.
Optimizing a candidate independently in every nest at an arbitrary value of does not generally optimize the combined revenue: the revenue denominator couples all nests. Likewise, an LP-feasible value need not be its minimum, and using such a value in problem (3) does not establish the theorem. The substantive assertion is that choosing the local maximizers at the optimal LP value solves the combined selection problem. The unique-root statement also needs care at empty assortments, where a nest contributes zero attraction and the conditional revenue uses the paper's convention.
Nests are represented by any finite type, and products by Fin n, indexed rather than the paper's . A Boolean offer vector is represented by Finset (Fin n); is the empty finset. Each is a finite set of such assortments. There is no single-nest or specialization, and no substitution of all possible assortments for the supplied candidates. The LP assumption is its full minimum objective property, not merely feasibility. The imported LP4Optimal predicate uses a set of candidates, supplied by coercing each finite to a set.
The source's main model is selected from the imported general instance by setting . In the paper's later extension, ; this is different from the imported unmodified when , so the extension is outside this mission. Positive and product weights are stated explicitly to keep the probability denominator positive and to match the model's preference interpretation. Revenues remain arbitrary real numbers: neither an order nor nonnegativity is assumed. The dissimilarities satisfy the paper's range. The paper states candidate feasibility ; this mission's claim holds for arbitrary candidate collections because no step compares against . The definitions of revenue and LP feasibility are imported, so useful contributions include proofs of the balance characterization, the root result, Lemma 1, and the final LP statement.
A retailer that sells through a choice model decides two things at once: which products to put on the shelf and at what price. Under the nested logit model of discrete choice, products are grouped into nests (brands, categories, store sections); a customer first picks a nest, or leaves without buying, and then picks a product inside the nest. The price of a product changes its attractiveness, and the attractiveness of every product changes the purchase probabilities of all the others, so assortment and price interact.
Gallego and Topaloglu (Management Science, 2014) study assortment optimization under the nested logit model with constraints on what may be offered in each nest. Their §6 treats joint assortment and pricing when each product can be sold at one of finitely many price levels. Earlier work on nested logit pricing, by Li and Huh (2011) and Gallego and Wang (2011), assumes that a product priced at has preference weight . With a finite menu of price levels, no parametric link between price and preference weight is required, and the prices can be restricted to a range or a grid (for example $49.99, $59.99, …), as retail practice often demands.
There are nests . In each nest there are products , and each product can be offered at one of price levels . Offering product at level in nest earns the price and gives the product the preference weight . The relation between and is arbitrary.
Each pair (product, price level) is a virtual product. Nest has virtual products ; is the set of the virtual products of product , and the sets are disjoint. Virtual product at level has revenue and preference weight . An assortment of nest is a set , and the feasible assortments are
so each product is offered at no more than one price, or not at all.
For an assortment write and , with . For a number , problem (7) of the paper is
Its objective equals with ; under this is problem (12) of the paper.
For every nest there is a collection , fixed independently of , with
such that for every some is an optimal solution of problem (7). The page states ; the explicit bound is the count of intervals left by the intersection points of the lines , , with .
The paper's Theorem 4 shows that a collection containing an optimal solution of (7) for every yields an optimal solution of the full nested logit problem, and its Theorem 2 that the best combination of candidates solves a linear program with variables and constraints. With the goal above, the joint assortment and pricing problem is solved exactly by a linear program of polynomial size, constraints, for arbitrary price–weight relations. This is one of the paper's three headline results.
The result is proved in the paper in prose, without a numbered statement. No machine-checked proof of it is known. The mission fixes the constant hidden in , states the feasible set exactly, and isolates the two steps of the argument as separate statements.
The naive candidate set is all of , which has members; the content of the goal is the polynomial bound with the collection fixed before . The argument must handle ties between coefficients, lines that coincide or never cross, intersection points at negative , and the boundary points between intervals, where several assortments are optimal at once. The count must be made per product: a count over all pairs of virtual products gives and misses the stated bound.
ι; virtual products are Fin n and products Fin p, both 0-based. is the fiber of a map prod : Fin n → Fin p; the hypothesis that every fiber has exactly elements is IsVirtualProductMap prod b. The price level of a virtual product is left implicit.NestedLogitVariants.LP.Instance fields r i j and v i j; there is no parametric price–weight relation and no ordering of prices.Finset (Fin n); the empty assortment is allowed and has objective .0 ≤ u).A complete development needs the reduction of (7) to the linear objective (identity (8)), the per-product optimality of problem (12), and a counting argument for the intersection points of finitely many lines on . The last one is reusable beyond this mission: the paper's cardinality-constrained result uses the same kind of argument. Proofs of the milestones, and lemmas such as (8) for the published V and R, are welcome.
The scalar Bernstein and Bennett inequalities bound the upper tail of a sum of independent, zero-mean random variables that are bounded above: the tail is governed by the total variance at moderate deviations and by the uniform bound in the far tail. Many questions in randomized numerical linear algebra, matrix completion, covariance estimation, graph sparsification and statistical learning reduce to the same question for a sum of independent random matrices, where the quantity of interest is the largest eigenvalue or the spectral norm of the sum rather than a scalar.
Ahlswede and Winter (2002) introduced a matrix Laplace transform method based on the Golden–Thompson inequality. Oliveira (2010) and Gross (2011) proved matrix Bernstein-type bounds with this method. Tropp (arXiv:1004.4389, Found. Comput. Math. 12 (2012)) replaced the Golden–Thompson step with Lieb's concavity theorem, obtaining a master tail bound for independent sums (Theorem 3.6) from which matrix Bennett and Bernstein inequalities follow with the variance parameter , the natural analogue of the scalar variance. This mission formalizes §6 of that paper.
Timeline:
All matrices are complex matrices with . For a self-adjoint (Hermitian) matrix , is its largest eigenvalue and its spectral norm. The semidefinite order means that is positive semidefinite. Functions of a self-adjoint matrix are defined spectrally: if , then ; this gives the matrix exponential and, on positive-definite matrices, the matrix logarithm . The trace is .
A random matrix is a measurable map on a probability space ; its expectation is taken entrywise. A finite sequence of random self-adjoint matrices is independent if the maps are mutually independent.
The setting of the goal: are independent random self-adjoint matrices with
and the total variance is . Bennett's function is for .
For every , the following chain holds:
and the last term is at most for and at most for . The first inequality is the matrix Bennett inequality, the second the matrix Bernstein inequality, and the case split the split Bernstein inequality.
Lemma 6.8 (the matrix mgf bound under ) and Theorem 6.2 (matrix Bernstein, subexponential case: , split as and ) are included as further theorems.
Matrix Bernstein is the most used inequality of the paper: it bounds the spectral norm of a sum of independent bounded random matrices with only a logarithmic dimensional factor, and it is the standard tool behind sampling bounds for matrix completion, randomized low-rank approximation, spectral sparsification, covariance estimation and the analysis of random features. Theorem 6.1 assumes only an upper bound on the largest eigenvalue of each summand, so it applies to summands with unbounded smallest eigenvalues; applied to and separately it controls both tails.
The results are proved in the paper. As far as the local catalog shows, no machine-checked proof of the matrix Bennett or Bernstein inequality for complex Hermitian matrices exists; the platform has a matrix Bernstein statement for real symmetric matrices in a different form (Wainwright, Theorem 6.17), still open, and scalar Bennett and Bernstein inequalities. Formalizing Theorem 6.1 produces a reusable matrix concentration inequality together with its two ingredients, the matrix mgf bound of Lemma 6.7 and the scalar inequality relating Bennett's and Bernstein's exponents.
The scalar argument multiplies moment generating functions of independent summands. For matrices, unless and commute, so does not factor; the master bound of Theorem 3.6 rests on Lieb's concavity theorem for , which is not in Mathlib. The mgf bound of Lemma 6.7 needs a semidefinite comparison between functions of a random matrix, the transfer rule on the spectrum , and the operator monotonicity of the logarithm. The remaining steps (optimizing over , the inequality between and the Bernstein exponent) are real analysis.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; is the supremum of the real spectrum; is the operator norm on ; and are Mathlib's continuous functional calculus cfc; the semidefinite order is Mathlib's MatrixOrder; expectation is entrywise. A random matrix is a measurable map, each is Hermitian at every , independence is iIndepFun, and the measure is a probability measure. The bound is assumed almost surely; no lower bound on the eigenvalues is assumed. The paper's standing regularity (§2.2) is made explicit as integrability of the entries of and (and of where its expectation is taken). The infimum over in Theorem 3.6 and Corollary 3.7 is stated for every admissible .
The printed formulas divide by and , so and are hypotheses of Theorems 6.1 and 6.2; with Lean's convention , the case would turn the Bennett bound into the trivial value , so the statement is not allowed to degenerate there. The chain is a conjunction of the probability bound and the inequalities between consecutive bounds, so the weaker reading "the probability is below each bound" does not satisfy it.
A complete development needs the matrix Laplace transform method, Lieb's theorem (or a substitute), operator monotonicity of the logarithm, the transfer rule for the functional calculus, and the scalar inequality . The first four are reusable for every matrix concentration inequality of this paper and beyond. Contributions to any milestone are welcome.
Regularized loss minimization over linear predictors is the training problem behind support vector machines, logistic regression, ridge regression and their many variants. Given examples , one minimizes an average of convex losses of the predictions plus a quadratic penalty. Dual coordinate ascent (DCA) solves the Fenchel dual of this problem by optimizing one dual variable at a time; it has been the workhorse of linear SVM solvers such as LIBLINEAR (Hsieh et al., ICML 2008). Before Shalev-Shwartz and Zhang's work, the available analyses of DCA either gave linear rates with constants depending on unknown problem quantities or did not control the duality gap, which is the quantity a practitioner can actually monitor as a stopping criterion.
Shalev-Shwartz and Zhang (2013) analysed stochastic dual coordinate ascent (SDCA), where the coordinate is picked uniformly at random, and proved explicit bounds on the expected duality gap. For Lipschitz losses (hinge loss, absolute loss) the bound is iterations, which matches stochastic gradient descent when the accuracy is low and improves on it when is small compared with . This mission formalizes that result, Theorem 1 of the paper, together with the lemmas of its proof.
Timeline. Hsieh, Chang, Lin, Keerthi and Sundararajan (2008) proposed dual coordinate descent for linear SVMs and proved linear convergence with an unspecified constant. Shalev-Shwartz and Zhang (arXiv 2012, JMLR 2013) gave the first explicit duality-gap rates for SDCA, for Lipschitz and for smooth losses. Proximal and accelerated variants followed (Shalev-Shwartz and Zhang, Math. Program. 2016).
Fix examples (Euclidean norm), convex losses and a regularization parameter . The primal problem (1) is to minimize
The convex conjugate of a scalar function is . The dual problem (2) is to maximize, over ,
Weak duality gives for all , so the duality gap bounds the primal sub-optimality of .
A loss is -Lipschitz if for all . The paper's standing assumptions are , and .
Procedure SDCA starts from . At iteration it picks a coordinate uniformly at random, chooses maximizing
and sets and . The averaging option outputs and . Let maximize and write for the dual sub-optimality.
For convex -Lipschitz losses under the standing assumptions, if and
then
The constants and are the paper's.
In the order the proof uses them: the one-coordinate increase (10); the identity ; Lemma 1 (expected dual increase at least times the gap minus ); Lemma 2 (, ); Lemma 3 ( outside ); Lemma 4 (); the recursion after (13); the rate (14), ; and the averaged duality-gap bound of p. 16.
Theorem 1 makes the duality gap of SDCA a certified stopping criterion with an explicit iteration count. Because the gap upper-bounds the primal sub-optimality, it also gives a primal guarantee for the averaged output . It covers non-smooth losses, the hinge loss in particular, where linear rates are not available. The analysis pattern, a lower bound on the expected dual increase by the duality gap (Lemma 1) followed by a recursion for the dual sub-optimality, was reused in the analyses of proximal, accelerated and mini-batch dual methods.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. The mission produces a formal account of the primal–dual pair of regularized loss minimization with extended-real conjugates, a formal SDCA run with uniformly random coordinates, and the complete chain of lemmas. Lemma 1 is stated with a general strong-convexity modulus , as in the paper, so it serves the smooth-loss analysis as well.
The obvious first idea is to treat SDCA as stochastic coordinate ascent on a concave function and import a standard rate. That fails: is neither smooth nor strongly concave for Lipschitz losses, and its domain is a box, so the per-coordinate progress cannot be bounded by a gradient norm. The argument instead compares the exact coordinate maximizer with an explicit interpolation towards a sub-gradient, which needs the conjugate's value at a sub-gradient (Fenchel–Young equality) and its infinite values outside .
The rate (14) is not a plain geometric recursion. It needs a burn-in phase and then an induction with a step size that changes with , and the duality gap of the output has to be recovered from the dual progress by Jensen's inequality over the averaged iterates. Everything happens in expectation over the coordinate sequence, while the dual values have to be kept finite along every run.
Lean conventions:
EuclideanSpace ℝ (Fin d), examples and losses are indexed by Fin n, and is inner ℝ w x.EReal supremum, and is EReal-valued. Real values of are used only where the same statement asserts that they are finite.Δ : (Fin n → ℝ) → Fin n → ℝ constrained by an arg-max predicate (IsSDCAStep). Any maximizer is admissible, and one exists for convex real losses.js : Fin T → Fin n, started at , with .SAGA.Convex.expectIdx, a published definition).A real-valued conjugate, which returns where the supremum is infinite, or an unconstrained step map would make the statements false or vacuous. The EReal conjugate and the arg-max predicate rule both out.
Infrastructure needed: Fenchel–Young for scalar convex functions, the existence of sub-gradients of convex real functions and their bound by the Lipschitz constant, Jensen's inequality for the convex and the concave , and the algebra of uniform averages over . The conjugate and sub-differential definitions and the duality-gap identity can be reused beyond this mission. Proofs of any milestone are welcome, as are lemmas on EReal sums that keep the finiteness bookkeeping short.
Stochastic differential equations (SDEs) model physical, biological and financial systems whose drift often grows superlinearly: the stochastic Lorenz equation, the stochastic van der Pol and Duffing–van der Pol oscillators, Langevin dynamics. Solutions are rarely explicit, so they are simulated by time-stepping schemes. For multilevel Monte Carlo methods (Giles 2008) the cost of a simulation is governed by the strong convergence rate, the speed at which tends to as the step size shrinks.
For superlinearly growing coefficients the classical Euler–Maruyama method diverges in (Hutzenthaler, Jentzen, Kloeden 2011). Tamed schemes repair this, and rate was proved for them under a global monotonicity condition: for all (Hutzenthaler, Jentzen, Kloeden 2012; Sabanis 2016). Most of the examples above violate that condition. Before this paper no strong rate was known for any time-discrete scheme for a multidimensional SDE with non-globally monotone coefficients.
Timeline. 2011: divergence of explicit Euler for superlinear drifts. 2012: tamed Euler, rate under one-sided Lipschitz drift and globally Lipschitz diffusion. 2012–2013: strong convergence without rates for non-globally monotone SDEs (stopped and tamed schemes). 2014: this paper (arXiv:1401.0295), rate for the stopped-tamed Euler–Maruyama scheme under the conditions below; published in Ann. Probab. 48 (2020).
Fix and . On a probability space with a normal filtration , is a standard -dimensional -Brownian motion. Matrices carry the Hilbert–Schmidt norm . Given coefficients and , is an adapted continuous process with
The taming map is . The stopped-tamed Euler–Maruyama scheme with steps is and
The whole increment, drift and noise together, is tamed, and the scheme freezes once it leaves a ball whose radius grows slowly as .
The conditions use a Lyapunov-type function and a function . The generator is , where is the -th column of . For partitions with mesh , the same recursion run in continuous time on defines interpolations .
Let , , and with . Let be with polynomially growing derivatives. Let satisfy , , and , and assume for
Then there is such that for all ,
The constant is not specified. Only the rate is asserted, and that is the stable content of the result.
In the proof's order:
Theorem 1.3 gives strong rate , and with it the complexity bounds of multilevel Monte Carlo, for SDEs with non-globally monotone coefficients. The paper's applications include the stochastic Lorenz equation with bounded noise, the stochastic van der Pol and Duffing–van der Pol oscillators, a model from experimental psychology and overdamped Langevin dynamics. The perturbation estimate, Theorem 2.10, is a separate tool. It compares a solution with any Itô process, so it also gives local Lipschitz dependence on the initial value and, in the paper's §3.2, rates for Galerkin approximations of SPDEs.
All results listed here are proved in the paper, and none has been machine-checked so far. This mission produces Lean statements of the goal and of every numbered step of its proof. The development needs Itô calculus for , a localization argument, exponential-moment bounds via Lyapunov functions, and calculus for the taming map. Several of these pieces are reusable well beyond this paper.
The obvious argument is Gronwall's lemma applied to . It needs the global bound , which fails for the Lorenz and van der Pol drifts: there the one-sided Lipschitz "constant" grows with . The difficulty is to control a random, state-dependent Gronwall exponent . That requires exponential integrability of and along both the solution and the scheme. For the scheme it holds only because of the taming and the stopping, and only up to an error of the right order.
EuclideanSpace ℝ (Fin d). Diffusion values are the published Diffusion d m, whose norm is the Hilbert–Schmidt norm the paper uses throughout. Time is .SabanisEuler.Shared.IsSolution / IsItoProcess. The normal filtration is right-continuity plus completion, and is the published IsWienerMartingale, a Brownian motion on . For , the paper's cylindrical Wiener process is exactly such a Brownian motion. All processes are hypotheses; existence is never claimed.Many equilibrium problems in operations research, such as networked Cournot competition, power markets and communication networks, are stochastic Nash games: each player minimizes an expected cost that depends on the rivals' strategies and on a random vector whose law is accessible only through samples. Best-response schemes, in which every player in turn solves its own optimization problem given the others' latest strategies, are the natural distributed method for such games. In the stochastic setting no player can compute an exact best response, because evaluating requires the expectation itself. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in which each best response is approximated by a finite number of stochastic gradient steps, and they ask how many sampled gradients each player needs to reach an approximate equilibrium.
The deterministic theory of proximal best responses, including the contraction matrix used here, is due to Facchinei and Pang (Nash equilibria: the variational approach, 2009, §12.6; reference [19] of the paper). The present mission covers the paper's first scheme, the synchronous one, in which all players update simultaneously.
There are players. Player chooses from a closed, compact, convex, nonempty set ; a profile is , and is the profile with its -th block replaced by . A Nash equilibrium is a profile such that every minimizes over .
Assumption 1 asks that each be convex in and twice continuously differentiable near , that the sampled gradients be unbiased for , and that . For the proximal best response is
The matrix has entries and , where is the least eigenvalue of over and the largest spectral norm of the mixed block over . Assumption 2 is (spectral norm).
Algorithm 1 starts from a deterministic . At major iteration every player computes with , by running projected stochastic gradient steps
and setting . A random profile is an -NE if .
With , , , , , , and , the iterate after major iterations is an -NE, and player uses at most
projected stochastic gradient steps. The goal fixes the paper's explicit expression, not its summary.
Theorem 1(a) shows that the synchronous inexact scheme keeps the linear rate of the exact best-response iteration, with factor arbitrarily close to , and turns it into a sample complexity explicit in , in the number of players and in the game's constants. Choosing gives a bound of order for any (Theorem 1(b)), close to the of a single stochastic convex program; the dependence on is mild, which matters for games with many players. The same building blocks (the contraction (5), Lemma 2, Lemma 3 and (30)) are reused by the randomized and asynchronous schemes of the same paper.
The result is proved in the paper; it has not been machine-checked. A formalization adds a verified proof of the complexity bound together with fully explicit hypotheses: several conditions that the paper leaves implicit or states imprecisely (listed under Formalization scope) are made exact, and the Lean statement records which version of each is used.
The arithmetic of Theorem 1(a) from Proposition 4, Lemma 3 and (30) is routine. The weight lies elsewhere. The contraction (5) is quoted from Facchinei–Pang and not proved in the paper; it needs the variational optimality conditions of the two proximal problems and a mean-value argument along a segment of for the partial gradient, which mixes the Hessian blocks and . Lemma 3 is a conditional-expectation argument about a stochastic approximation recursion: the iterate must be shown measurable for the nested -fields generated by the samples, and the conditional unbiasedness and moment hypotheses must be combined with the tower property and the projection's nonexpansiveness. Proposition 4 then needs conditional Jensen to pass from (8) to the Euclidean norm of block errors.
Players are Fin N, player 's space is EuclideanSpace ℝ (Fin (n i)), profiles are dependent functions, and is Function.update y i z. The Euclidean norm of the vector of block distances is written out (blockDist), since Mathlib's norm on profiles is the sup norm; is the operator norm of Matrix.toEuclideanCLM Γ. and are the infimum and supremum of Rayleigh-type quotients of the second derivative over and unit vectors. The proximal BR is any map minimizing the proximal objective on (unique there), and is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. The -fields and are generated by the samples. Every expectation carries an integrability hypothesis.
Statement repairs, each recorded in the item's Formalization Note:
The goal is not trivialized by deterministic gradients: the sampled gradients are random, constrained only by conditional unbiasedness and a conditional second-moment bound, the proximal BR is tied to by its argmin property, must be a Nash equilibrium, and the norms are Euclidean. A deterministic instance (, on a ball, exact gradients) satisfies every hypothesis jointly.
Needed infrastructure: optimality conditions for constrained strongly convex minimization, the mean-value inequality for partial gradients of functions on convex sets, conditional expectation of vector-valued functions with the tower property and conditional Jensen, and the nonexpansiveness of Euclidean projection. The contraction (5) and Lemma 3 are reusable beyond this mission. Proofs of any milestone are welcome.
For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.
Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.
Let be a simple graph on , . A set of vertices is stable if no two of its members are adjacent; the stability number is the size of a largest stable set, so .
Put and write a vector of as , with indexed by vertices and indexed by pairs of vertices. The tensor has entry at the six orderings of the triple of coordinates for every non-adjacent pair , and elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.
For a real 3-tensor the cubic form is , and a real is a unit -eigenvalue of if
Finally, for . In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and is Mathlib's SimpleGraph.indepNum.
That is, is an eigenvalue of , and no with is. This is the statement on which the paper's -query reduction rests; nothing is claimed about .
both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.
The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.
Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.
The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing and maximizing over by Cauchy–Schwarz, reduces the cubic problem to a quartic one in , whose value still has to be identified with ; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.
ι → ι → ι → ℝ on a finite index type. For the index type is the disjoint union of the vertices Fin v and the pairs ; this is with coordinates labelled by name instead of by the paper's enumeration . Vertices are .SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.The rank of a matrix does not depend on the field in which its entries are read: a rational matrix has the same rank over , and , because rank is computed by Gaussian elimination, which never leaves the field of the entries. For 3-tensors, arrays with three indices, this fails. Tensor rank governs the complexity of bilinear maps (the exponent of matrix multiplication is a statement about the rank of one tensor), the uniqueness of the CANDECOMP/PARAFAC decompositions used in psychometrics and signal processing, and the identifiability of latent-variable models. In each application the field matters: algorithms are run over or , while complexity results are often proved over or finite fields.
Håstad (1990) proved that deciding is NP-complete over finite fields and NP-hard over . De Silva and Lim (2008) gave real tensors whose rank over is strictly smaller than their rank over . Hillar and Lim (2013, Theorem 1.14) showed that the same phenomenon already occurs between and , for a tensor with integer entries, so that Håstad's result over does not by itself say anything about rank over .
Let be a field. The outer product of , , is the tensor with entries . The rank of over is
If has entries in a subfield , both and are defined, and .
The paper's example uses , and
A decomposition with , is equivalent to the eight cubic equations (30) in the twelve unknowns , one for each entry of .
In Lean, outer x y z and rankOver E A implement the two definitions, tensorA is , and System30 is (30).
The theorem shows that tensor rank, unlike matrix rank, is not invariant under field extension even between and , and even for the smallest nontrivial format . Its consequence for complexity is that a hardness result for rank over cannot be transferred to by reading the same instance in a larger field; the paper accordingly re-examines Håstad's construction to obtain hardness over and (Theorem 8.2), which is outside this mission.
The result is proved in the paper, with the decisive algebraic step delegated to a computer-algebra computation (Appendix). A machine-checked proof replaces that computation by a certificate verified in Lean, and it settles a printed error: one of the two consequences of (30) in the proof of Lemma 8.1 is printed with the wrong sign (see Formalization scope). No formalization of array tensor rank over a field, or of its field dependence, is known to exist in Mathlib or on this platform.
The upper bound is an identity among explicit arrays. The lower bound is the substance: one must show that the cubic system (30), which has real solutions, has no rational one. Since (30) is solvable over , no argument by signs, inequalities or real geometry can work; the obstruction is arithmetic, coming from the irrationality of . The step that fails in a naive attempt is the elimination: eliminating ten of the twelve unknowns from eight cubic equations by hand is impractical. A second, smaller difficulty is the reduction from "" to two terms of the special form (29), which requires absorbing the scalars and padding a decomposition with fewer than two terms.
Fin l → Fin m → Fin n → E, with 0-based indices: the paper's is A (i-1) (j-1) (k-1). Vectors are Fin n → E.rankOver E A is the sInf over of the lengths of decompositions . The set is nonempty (one term per entry), so this is the paper's minimum. Zero summands are allowed; this gives the same minimum as the paper's sum of nonzero rank-1 tensors.rankOver ℝ of its entrywise cast to ; is rankOver ℚ, whose witnesses are rational. A formalization in which both ranks range over real witnesses would make the theorem false.Needed infrastructure: finite sums of arrays, Real.sqrt and irrational_sqrt_two, and an ideal-membership certificate for milestone 3. The array rank rankOver is reusable for any statement about tensor rank over a field. The platform's mme_tensor_rank (restriction-based rank of a TensorObj over a single field, from the matrix-multiplication exponent series) is a different object and is not reused. Proofs of any milestone, and alternative certificates for Lemma 8.1, are welcome.
Interior-point methods for conic optimization are best understood on symmetric cones: the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices. On these cones the barrier functions are self-scaled, and Nesterov and Todd showed that every primal-dual pair then has a unique scaling point with and . The resulting primal-dual algorithms, implemented in solvers such as SeDuMi and MOSEK, combine long steps with good worst-case complexity.
Many models in statistics, geometric programming, entropy maximization and logistic regression need the exponential cone, which is not symmetric. Dahl and Andersen (Math. Program. 194, 2022) designed the primal-dual algorithm behind MOSEK's exponential-cone support. To explain why they cannot simply transplant the Nesterov–Todd construction, they use a property that sits between "self-scaled" and "arbitrary": negative curvature of the barrier. Barriers of symmetric cones have it; a barrier is self-scaled if and only if both it and its conjugate have it (Nesterov–Tunçel, 2016); and barriers with negative curvature still admit a unique scaling point satisfying one secant equation. Dahl and Andersen observe in §5 that the exponential-cone barrier lies outside this class, by an explicit witness. This mission formalizes that observation and the derivative formulas of their Appendix A it rests on.
Timeline:
Points of are written . The exponential cone is the closure
whose interior is . Its standard barrier is
defined and smooth on . Appendix A of the paper writes with
For a smooth on an open set, is its Hessian, a symmetric linear map of , and the third directional derivative is the symmetric linear map
A barrier of a cone has negative curvature if for all and for
where is the Loewner order: for every . The direction ranges over the closed cone , including its boundary.
The goal asserts only the qualitative failure, so it does not depend on the particular witness.
The result. Negative curvature is the property that gives symmetric-cone barriers their long-step Hessian estimates and a unique scaling point with one secant equation. Its failure for the exponential-cone barrier means that none of these consequences can be invoked for the exponential cone. An algorithm for this cone has to obtain its scalings by other means; Dahl and Andersen take them from Tunçel's framework, via the quasi-Newton secant updates of §5. The witness also shows that the failure occurs already for a direction on the boundary of the cone, at an interior point with simple coordinates.
Formalizing it. The claim is proved in the paper by a computation "using the expressions in the appendix", with the details left to the reader. The appendix formulas for the gradient, Hessian and third directional derivative of the exponential-cone barrier are the ones an implementation evaluates, including the higher-order corrector term . A machine-checked version certifies these closed forms, including the zero padding of the "leading parts" in (33), and gives a reusable definition of negative curvature that applies to any cone and barrier. As far as is known, none of these statements has a machine-checked proof.
The obstacle is computational, not conceptual. The barrier is a composition of logarithms with a function that is itself a perspective of the logarithm, so its third derivative is a sum of terms with denominators , and . Stating it as a derivative of the Hessian map requires showing that the Hessian is differentiable on the open interior, which in turn requires a description of that interior, a set defined as the interior of a closure. The membership claims about are not definitional either: lies on the boundary, reached only as a limit of points of the generating set, and its non-interiority needs a neighbourhood argument. Finally, the cone condition on matters: replacing by makes the claim nearly trivial, because .
EuclideanSpace ℝ (Fin 3); the paper's are (x 0, x 1, x 2), and vectors are written !₂[·, ·, ·].Real.log; every statement evaluates them, and their derivatives, only at points of , where all logarithms are the genuine ones. The appendix formulas carry the hypothesis .SelfScaledIPM.ShortStep.hess (derivative of the gradient), and is fderiv ℝ (hess F) x u. The Loewner order is stated through the quadratic form for every . Matrices act through the standard basis (Matrix.toEuclideanCLM).The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).
The proof is a reduction from the clique number of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding is one of Karp's (1972) NP-complete problems.
A real 3-tensor is an array with trilinear form . With the Euclidean norm , its spectral norm is
A real is a unit -singular value of if there are unit vectors with
for all : the stationarity conditions of on a product of unit spheres.
Let be a simple graph on , , with edges , , and clique number . Let be the standard simplex, the adjacency matrix and the all-ones matrix. For a positive integer set and . Let , and let be the maximum over unit , of the multilinear form
The graph tensor has as entry the coefficient of in (26).
For every graph on vertices and every enumeration of its edges:
so is the largest for which is a unit singular value of . The paper's -query Turing reductions rest on exactly this.
The result. The goal shows that a single comparison with of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size encodes whether . It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.
Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.
The construction of is explicit, and the comparison with is arithmetic once is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.
Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with , clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. is a rational tensor, read over by casting.
Explicit readings of the paper:
This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of , the -query procedure, the scaling to a general fixed , and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.
Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.
Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.
Conic optimization over the exponential cone models entropy, relative entropy, logistic regression, log-sum-exp and geometric programming. Unlike the nonnegative orthant, the second-order cone and the semidefinite cone, the exponential cone is not symmetric (self-scaled), so the Nesterov–Todd primal-dual machinery that makes solvers such as SeDuMi and MOSEK fast does not apply as is. Dahl and Andersen (Math. Program. 194 (2022) 341–370) describe the nonsymmetric-cone algorithm implemented in MOSEK (version 9.2 in the paper's experiments). Its central new ingredient is a corrector for nonsymmetric cones, an analogue of Mehrotra's predictor-corrector that is responsible for much of the practical performance of symmetric-cone solvers. The paper reports that the corrector gives a substantial and consistent reduction in iteration counts across its test sets.
Timeline. Nesterov and Todd (1997, 1998) built primal-dual methods for self-scaled cones. Nesterov, Todd and Ye (1999) and Tunçel (2001) studied primal-dual scalings for general cones, Tunçel proving polynomial complexity of an infeasible method without a corrector under bounded scalings. Skajaa and Ye (2015) gave a homogeneous method for nonsymmetric cones with a Runge–Kutta corrector. Myklebust and Tunçel (2014) analysed BFGS-type scalings. Dahl and Andersen (2022) introduced the third-order corrector studied in this mission.
Let be linear with full row rank, , , and let be a proper cone (pointed, closed, convex, with nonempty interior). A -logarithmically homogeneous self-concordant barrier (LHSCB) for is a convex function on with and . The primal problem minimizes subject to , ; the dual maximizes subject to .
The homogeneous model adds : , , , , . With , the residual is
a linear map whose -block is skew-symmetric. An iterate has , , and . The shadow iterates are and , with the conjugate barrier. A scaling is a nonsingular with and (the double secant equations (8)).
The affine direction solves , (11). The corrector is (16). For a centering parameter , the combined direction solves
Every solution of (18) satisfies
and for all
The goal fixes no constants beyond those of the direction itself. It holds for every solution of (18), not a chosen one.
The result. Lemma 4 says that a step of any length along the combined direction reduces the infeasibility residuals and the complementarity gap by exactly the same factor. Starting from a point with , the iterates satisfy and , so the algorithm needs no merit function to balance feasibility against optimality, in contrast with earlier nonsymmetric methods. The lemma also shows that adding the third-order corrector does not cost this property, which is what justifies using the corrector in MOSEK's exponential-cone solver.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of Lemmas 2–4, the §2 homogeneity identities or the barrier sum rule has a machine-checked proof. The mission produces a formal homogeneous model for a general proper cone with a general LHSCB and a formal account of third-derivative calculus for logarithmically homogeneous barriers. Both are reusable in any analysis of interior-point methods for nonsymmetric cones (power cones, generalized power cones, hyperbolicity cones).
The obvious reading of Lemma 4 as bookkeeping with the linear map stalls at the corrector: the term
in (18) involves the third derivative of the barrier, and nothing in linear algebra says how it
interacts with the complementarity gap. Controlling it needs the third-derivative calculus of logarithmically
homogeneous barriers. In Lean that means relating gradient, the Hessian as fderiv of the gradient, and the
third derivative as fderiv of the Hessian, and working with the symmetry of iterated Fréchet derivatives of a
function, for which the Mathlib interface is thin. A second obstacle is the augmented barrier: the
barrier properties of must be transported to on through the
splitting , including the boundary behaviour at the corner
, .
The first identity of Lemma 4 is misprinted in the paper as . A formalization following the printed statement would be false, not merely awkward.
Vectors of the augmented space are EuclideanSpace ℝ (Fin (n + 1)); is the first coordinates and
(resp. ) the last. is a continuous linear map and its Hilbert adjoint; full row rank
is surjectivity. Proper cones, the Hessian hess, the barrier class IsLogHomBarrier and the conjugate
conj are the published SelfScaledIPM.ShortStep.Setting. That barrier class adds three standard conditions
to the paper's two (boundary blow-up, the -inequality and a positive definite Hessian), which the
paper uses implicitly when it writes and calls a barrier. is a continuous linear
equivalence and the adjoint of . is fderiv ℝ (hess F) x u w and
is ContinuousLinearMap.inverse. Every inner product includes the homogenizing term .
Repairs, generalizations and specializations, each disclosed in the item statements:
The directions are predicates (" solves (11)"), and the lemmas quantify over all solutions. The hypotheses are satisfiable. For the linear program , , , , , , , , system (11) has the unique solution , , . Statements that hold only because a junk value appears are ruled out: every statement requires and , where , the inverse Hessian and the conjugate barrier take their true values. A formalization that drops from the inner products, or that fixes one solution of (18) instead of quantifying over all, would be a different lemma and does not count.
Welcome contributions: the general sum rule for products of cones, a Fin.append splitting library for
EuclideanSpace, and proofs of the homogeneity identities that can be reused by the series' other missions.
The explicit Euler–Maruyama scheme is the standard way to simulate a stochastic differential equation
on driven by a -dimensional Brownian motion. When and are globally Lipschitz it converges strongly with order in the step size (Kloeden and Platen 1992). Many models of interest in physics, chemistry and statistics have a drift that grows faster than linearly but points inwards, such as . For these the SDE is well posed and its solution has finite moments of all orders, but the uniform-step scheme does not: for , Hutzenthaler, Jentzen and Kloeden proved that as the step size , for every and (Proc. R. Soc. A 2011).
Several remedies have been proposed: implicit schemes (Higham, Mao and Stuart 2002; Mao and Szpruch 2013), the tamed Euler scheme (Hutzenthaler, Jentzen and Kloeden 2012), truncated schemes (Mao 2015). Fang and Giles (Ann. Appl. Probab. 2020) keep the explicit Euler–Maruyama update and change only the step: the timestep is a function of the current state, small where the drift is large. This mission formalizes their finite-time results: stability of the adaptive scheme (Theorem 1) and strong convergence of order (Theorem 3).
Let and be the Euclidean norm and inner product on , and the Frobenius norm of an matrix. Given a timestep function , the scheme (5) starts from , and sets ,
The grid is random: it depends on the path. For a time , is the last grid time not after ; the piecewise constant interpolant is and the continuous interpolant is
The hypotheses (Assumptions 1–4, pp. 528–530):
For in one dimension, satisfies Assumption 2.
Under Assumption 4, with satisfying Assumption 3 for an satisfying Assumption 2, for every there is such that for all
Theorem 1 shows that an explicit scheme, at the cost of one drift and one diffusion evaluation per step, is stable for one-sided Lipschitz drifts of polynomial growth, the class where the uniform-step scheme fails. Theorem 3 shows that refining the timestep function keeps the classical order . Combined with the paper's bound on the expected number of steps (Lemma 2) this gives order in terms of computational cost, and the results underpin the paper's adaptive multilevel Monte Carlo estimators. The uniform-in- form of Theorem 1 is what lets Theorem 3 apply the stability bound to the whole family .
The paper's proofs are complete on paper; none of these results has a machine-checked proof. Formalizing them needs a theory of Euler schemes on a random, state-dependent grid, which is not in Mathlib and is not covered by uniform-grid formalizations of tamed or implicit schemes. The definitions here (the scheme on random times, the projected K-scheme) are reusable for the infinite-time companion mission and for other adaptive schemes.
The obvious argument for the uniform-step scheme bounds moments step by step, using deterministic step sizes and independent Gaussian increments. Here the step depends on , so the grid times are stopping times and the increments have random length. Sums over steps become Itô integrals only after the scheme is written as the solution of , and moment bounds for those integrals need the Burkholder–Davis–Gundy inequality on a random grid. A second difficulty is that need not be reached: if decays fast enough, could converge below . Excluding this needs a positive lower bound on over bounded sets together with moment bounds, which the paper obtains by first analysing a version of the scheme projected onto a ball.
Lean conventions: is the published SDEState m (EuclideanSpace ℝ (Fin m)); matrices are the published Diffusion m d, whose norm is the Frobenius norm; is a standard -dimensional -Brownian motion in the sense of the published IsWienerMartingale; the SDE solution is any process satisfying the published IsSolution on (existence and uniqueness are not claimed). Times are in , indices start at , and is deterministic. The scheme is defined pathwise; the index of is a junk value when the grid never passes , an event of probability zero (Theorem 1). and are real-valued and their positivity is a hypothesis; each is assumed measurable. Moments are -valued integrals of extended norms, never Bochner integrals. Every existential constant is chosen before the parameter it must not depend on: before in Theorem 3 and its milestones, before (and ) in Theorem 1 and Step 3. Results the paper proves for inside its proofs are stated for . Pages are the journal's printed pages (PDF page + 525).
A formalization that places the constant after , uses a deterministic grid, or allows would be trivially true or a different theorem; these are ruled out by the statements.
Contributions welcome: proofs of the milestones, and of general facts they need (Burkholder–Davis–Gundy, moments of Brownian increments over stopping-time intervals, Grönwall's inequality for -valued functions).
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.
The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.
Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.
Timeline:
All matrices are complex matrices with . For a self-adjoint (Hermitian) matrix , and are its algebraically largest and smallest eigenvalues. The semidefinite order means that is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if then ; this gives the matrix exponential and, on positive-definite matrices, the matrix logarithm .
A random matrix is a measurable map on a probability space , and its expectation is taken entrywise. The matrix moment generating function of is .
The objects of the mission are independent random Hermitian matrices that are almost surely psd contractions: and . Their average expectation has extreme eigenvalues
and the binary information divergence is
In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.
Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with , the extreme eigenvalues of ,
Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor , which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound .
The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.
The scalar Chernoff argument uses for independent . For matrices unless and commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. , are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "" hold almost surely. The sequence has terms wherever an average appears. An infimum over is stated as a bound for every admissible ; integrability of is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean , so at the boundary values the divergence is finite where the paper's is ; this only weakens the stated bound.
A formalization in which (empty spectrum, ) or (the average ) were allowed, or in which the range of were dropped, would state a different, partly false theorem; these cases are excluded.
A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in . Contributions of any of these as stand-alone lemmas are welcome.
A matrix Gaussian series , a sum of fixed self-adjoint matrices each multiplied by an independent standard normal variable, is the simplest sum of independent random matrices. It already appears in the analysis of random designs, in compressed sensing, in randomized numerical linear algebra and in quantum information, wherever one needs to know how large the spectrum of a random linear combination of matrices can be. Its Rademacher analogue , with random signs, plays the same role in symmetrization arguments.
For real coefficients the answer is classical: is normal with variance , so its upper tail is at most . Tropp's paper (arXiv:1004.4389v7) shows that the same bound holds for the largest eigenvalue of a matrix series, with an explicit dimensional factor and with the variance parameter .
Timeline. Noncommutative Khintchine inequalities (Lust-Piquard 1986; Lust-Piquard and Pisier 1991) control the moments of matrix Rademacher and Gaussian series and imply tail bounds of this type. Ahlswede and Winter (2002, arXiv:quant-ph/0012127) introduced the matrix Laplace transform method, whose bounds depend on the sum of the norms . Oliveira (2010, arXiv:1004.3821) obtained bounds of the same form as Theorem 4.1. Tropp (2012) derived the result from a master inequality built on Lieb's concavity theorem (1973), which produces the norm of the sum, , as variance parameter. The paper itself notes that Theorem 4.1 and Corollary 4.2 are not new results; the contribution is the route through the master bound.
Fix a dimension . Matrices are complex arrays; a matrix is self-adjoint if it equals its conjugate transpose. For a self-adjoint , is its largest eigenvalue, and is the spectral norm, the operator norm on with the Euclidean norm. Functions of a self-adjoint matrix are defined through its eigen-decomposition: , (for positive-definite ), . The semidefinite order means that is positive semidefinite.
A random matrix is a measurable map from a probability space into the complex matrices; its expectation is taken entry by entry. A Rademacher variable takes the values with probability each; a standard normal variable has law .
The data of the mission are fixed self-adjoint matrices and independent scalar variables , all standard normal or all Rademacher. The variance parameter is
For all ,
For fixed matrices and ,
The result. Theorem 4.1 is the template for every inequality in the paper: a scalar tail bound carried over to matrices at the cost of a factor , with a variance parameter that is the norm of a sum rather than a sum of norms. The difference matters: can exceed by a factor of , and §4 of the paper shows that both the variance parameter and the dimensional factor in (4.3) are needed in general. Corollary 4.2 transfers the bound to the largest singular value of a rectangular series, which covers Gaussian matrices with nonuniform variances (§4.3).
Formalizing it. The theorem is proved in the paper; the work here is to formalize that proof. The milestones are reusable beyond this mission: Theorem 3.6 and Corollary 3.7 are the common entry point of the Chernoff, Bernstein and Azuma missions of this series, and the Rademacher half of Lemma 4.3 is used again in the matrix Azuma mission. No machine-checked proof of these matrix inequalities was found in Mathlib or on the platform when this mission was drafted.
The scalar argument bounds by the product of the individual mgfs, using . For matrices this identity fails when the summands do not commute, and the trace inequality that replaces it for two matrices (Golden–Thompson) has no analogue for three or more. Controlling the trace mgf of a sum of many noncommuting independent matrices therefore requires a genuinely matrix-analytic input with no scalar counterpart; the naive product bound is not available. A second difficulty is infrastructural: matrix functions, the semidefinite order and expectations of random matrices must be combined in a single setting.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; self-adjointness is IsHermitian; , , are Mathlib's continuous functional calculus cfc; is Mathlib's Loewner order under MatrixOrder; is the supremum of the real spectrum; is the operator norm on . Expectation is entrywise, and the paper's standing regularity assumption is made explicit as entrywise integrability of every matrix whose expectation is taken. The infimum over is stated pointwise: the bound is asserted for every at which the mgfs exist, which is equivalent to the infimum form. Independence is iIndepFun of the scalar variables, and "Gaussian or Rademacher" is the disjunction of two hypotheses, never a mixture of laws.
The variance parameter is the norm of the sum ; a formalization with , with a constant different from , or with the dimensional factor omitted is a different theorem. At , Lean's division by zero makes the bound the trivial ; this is the only degenerate case and it is valid.
The development needs: the spectral calculus for Hermitian matrices, monotonicity of the trace exponential, operator monotonicity of the matrix logarithm, Lieb's theorem, and moments of the Gaussian. These are reusable well beyond this paper; proofs of the milestones, of supporting matrix-analysis lemmas, and alternative routes (for instance through noncommutative Khintchine inequalities) are all welcome.
A data curator holds a database of individual records and wants to publish something from which many statistics can be computed, while guaranteeing differential privacy: no single record should noticeably change what is published (Dwork, McSherry, Nissim, Smith 2006). Interactive mechanisms answer queries one at a time and add noise to each answer, so their accuracy degrades as more queries are asked; Dinur and Nissim showed that answering too many arbitrary queries accurately reveals the database (Dinur, Nissim 2003).
Blum, Ligett and Roth asked a different question: can a curator release, once and non-interactively, a synthetic database that is accurate simultaneously for every query of a large, structured class, while remaining differentially private? Their answer (arXiv:1109.2229; JACM 60(2), 2013; conference version STOC 2008) is yes for every class of counting queries over a discretized universe, with accuracy governed by the class's VC-dimension rather than its cardinality. The mechanism it introduces, the Net mechanism, became the starting point of the literature on private query release (SmallDB, private multiplicative weights, and the lower bounds that followed).
Fix a finite data universe (for instance ). The curator's input is an -tuple , read as a multiset of records. Two inputs are neighbouring if they differ in exactly one entry.
A database of arbitrary size is a finite nonempty multiset of elements of . For a predicate the counting query is
the fraction of records satisfying . A class of predicates is identified with its class of counting queries, and its VC-dimension is the size of the largest set of points that shatters.
A randomized mechanism , whose output on input is a random database , is -differentially private if for all neighbouring and all sets of outputs. It is -useful for if for every input , with probability at least , for every .
The global sensitivity of is over neighbouring pairs. An -net for is a finite set such that every has some with for all ; denotes a net of minimum size.
The exponential mechanism with quality score over a finite range outputs with probability proportional to . The Net mechanism is the exponential mechanism over with score .
There is an absolute constant such that, for every finite , , , , , , whenever
a minimum -net exists and the Net mechanism run on any minimum -net is -useful for . The constant is left unspecified, as in the paper; the goal asserts the shape of the bound, not a value of .
The result. Theorem 3.10 shows that a database of size roughly suffices to release, privately, a synthetic database answering every query of to within . This is only a polynomial factor above what sampling needs without privacy, and it covers classes with exponentially many queries in , which interactive noise addition cannot. Together with Property 3.3 it is the first general feasibility result for non-interactive private release, and it identified VC-dimension as the governing parameter.
Formalizing it. The result is proved in the paper, modulo the cited uniform-convergence lemma (Lemma 3.8). No part of it is machine-checked on the platform. A complete development would give a formal exponential mechanism with a general score and its privacy proof, a formal utility analysis of a mechanism with a finite range, and a formal ε-approximation theorem for VC classes, which is the deepest dependency and reusable across learning theory.
The privacy and utility of the exponential mechanism (Theorem 3.2, Property 3.4) are short ratio arguments. The difficulty is concentrated in bounding the size of the net. For finite classes a random-sampling and union-bound argument suffices (Lemma 3.7). For infinite classes the union bound over is unavailable, and Lemma 3.8 needs uniform convergence over a class of finite VC-dimension, uniformly over every finite multiset : a symmetrization or chaining argument together with the Sauer–Shelah lemma, none of which is in Mathlib in this form. The obvious route of applying the finite-class bound to the restriction of to the support of gives a size depending on and fails.
Fin n → X with X : Type finite; neighbouring means "replace one entry", the platform's PrivLearn.Generic.Neighbors. The paper's "" read literally for equal-size multisets forces and would make every mechanism private.Database X), with every set measurable. Queries are real functions on multisets, so the same query reads inputs and outputs. Predicates are X → Bool; VC-dimension is the platform's HighDimProb.Chaining.vcDim (valued in ℕ∞; the theorems take it finite, equal to ).Welcome contributions: a general ε-approximation theorem for VC classes (Lemma 3.8), reusable well beyond this mission; a reusable exponential-mechanism privacy proof; the finite-range utility analysis of Property 3.4.
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 estimation problems in signal processing and statistics look for a vector with few nonzero entries that fits data well. Compressed sensing (Donoho 2006) recovers a sparse from linear measurements by minimizing over sparse vectors. Sub-wavelength optical imaging and phase retrieval (Shechtman, Eldar, Szameit, Segev 2011) lead to the same task with a quartic, nonconvex objective, because the measurements are quadratic in the unknown image. Beck and Eldar (SIAM J. Optim. 2013) treat the common abstraction: minimize a general smooth function under a cardinality constraint.
For linear least squares, greedy methods such as matching pursuit (Mallat, Zhang 1993) and orthogonal matching pursuit (Tropp 2004) add one coordinate at a time, and iterative hard thresholding (Blumensath, Davies 2008) is a projected gradient method. For a general nonconvex objective the question is which optimality condition an algorithm can actually guarantee at its limit points. Beck and Eldar introduce the greedy sparse-simplex method, a coordinate-descent scheme that never leaves the feasible set, and prove that its limit points satisfy coordinate-wise optimality, the strongest of the necessary conditions studied in their paper. This mission formalizes that convergence theorem.
Let and be integers with , and let be continuously differentiable and bounded below: there is with for all (Assumption 1, a standing assumption of the paper). The problem is
where the norm counts the nonzero components of . Write for the support of , for its complement, for the feasible set, and for the -th unit vector.
A feasible is a coordinate-wise (CW) minimum of (P) (Definition 2.4) if
Below the sparsity level no single coordinate can be changed profitably; at the sparsity level no support coordinate can be profitably swapped for any coordinate carrying any value.
The greedy sparse-simplex method starts from . If , it minimizes over all points (all , all ); if , it minimizes over all points with , any and any . If the best candidate strictly improves on it becomes ; otherwise the method stops. A run is any sequence produced this way, for any choice of minimizers.
For every run of the greedy sparse-simplex method and every accumulation point of ,
No Lipschitz assumption on is made.
Milestones 2–4 together with closedness of give the goal.
The theorem certifies what a cheap, feasible-point method achieves on a nonconvex, discontinuously constrained problem: its limit points cannot be improved by changing a single coordinate or by swapping a single support coordinate. Combined with Theorem 2.4 of the same paper (every CW-minimum is an -stationary point), it gives Corollary 3.2: when is Lipschitz, the limit points are -stationary, where is a local Lipschitz constant that can be much smaller than the global one used by iterative hard thresholding, and the method needs no knowledge of either constant. For quartic objectives arising in phase retrieval each inner step reduces to minimizing a scalar quartic, so the guarantee applies to a practical algorithm.
The result is proved in the paper (§4.2.1). As far as a search of the Prove2Me library shows, neither coordinate-wise optimality for sparsity constrained problems nor any convergence theorem for sparse-simplex methods has a machine-checked proof. The mission produces a formal model of the method that is faithful to its selection rules and stopping rule, and a formal proof of the convergence theorem. The companion missions of the series formalize Theorem 2.4 and the partial sparse-simplex method.
The obvious argument passes to the limit in the inequality "the next iterate is at least as good as every candidate move from the current iterate" along a subsequence converging to . This works directly when the candidate moves from converge to the candidate moves from . It fails in the case while the iterates near sit at the sparsity level : there the method cannot simply add a coordinate , only swap one out, and the candidate set from is not the candidate set from . The discontinuity of means that the regime of the iterates (below or at the sparsity level) need not be that of the limit.
Vectors live in EuclideanSpace ℝ (Fin n); indices are in Lean and on the page, and is EuclideanSpace.single i t. The function is ContDiff ℝ 1, Assumption 1 is the hypothesis ∃ γ, ∀ x, γ ≤ f x, and 0 < s, s < n are hypotheses, as in (P). No Lipschitz hypothesis appears anywhere.
A run is a predicate IsGreedyRun f s x on a sequence x : ℕ → EuclideanSpace ℝ (Fin n): , and each step is either a move to a point that strictly decreases and attains the minimum of over all candidate points, or a STOP, in which is at most every candidate value and the sequence stays put, (the convention behind Lemma 3.2). The argmin selections are therefore arbitrary, and every theorem holds for every run. An accumulation point is MapClusterPt xstar atTop x. Membership is part of the definition of a CW-minimum and has to be proved.
The predicate is not vacuous: a sorry-free check shows that on , , , the sequence , for is a run with one move followed by a STOP. A formalization in which the STOP branch is missing, or in which accumulation points are replaced by limits, would prove a weaker or empty statement and is ruled out by this encoding.
The needed infrastructure is small: closedness of , the behaviour of supports along convergent sequences (supports eventually contain the support of the limit), and continuity arguments for limits of inequalities. A lemma that the support of nearby points contains the support of the limit is reusable for any -constrained problem. Proofs of the milestones as stated, and alternative proofs of the goal, are welcome.
Theorem and page numbers refer to the arXiv version (arXiv:1203.4580v1), whose printed and PDF pages coincide; the published version is SIAM J. Optim. 23(3), 2013.
Differential privacy (Dwork, McSherry, Nissim and Smith 2006) is the standard guarantee for releasing statistics about a sensitive database: replacing one record changes the probability of any outcome by at most a factor . In their paper on non-interactive database privacy, Blum, Ligett and Roth propose an alternative motivated by learning theory, distributional privacy. When a database is a sample from a population, a release should reveal no more about the sample than is inherent in the population itself. Their example is a group of hospitals, each treating a random sample of the patients with a disease in a region: a hospital can publish information that describes the regional population without revealing which hospital's patients produced it.
The two notions look incomparable at first. Differential privacy protects only databases that differ in one record, but protects every such pair; distributional privacy can protect databases that differ in all their records, but only for typical pairs, and it tolerates a small failure probability . §7 of the paper (p. 19) shows that distributional privacy is the stronger notion once is small compared with . This mission formalizes that implication, Theorem 7.3.
Fix a data universe and a measurable space of outputs. In §7 a database of size is a set with ; databases are drawn without replacement, so they have no repeated elements. A mechanism assigns to each database of size the probability law of its random output, a measure on , and denotes .
The Lean development uses the same names: SetNeighbors, IsDPSet, GoodPair, badPairCount and IsDistPrivate in the namespace PrivateRelease.Distributional.
For a family of mechanisms , one per database size, and failure probabilities :
The goal keeps the paper's asymptotic hypothesis and leaves the rate of unfixed beyond .
For a single size , the threshold the paper's argument actually uses:
The goal follows from it, since forces eventually.
The result. Theorem 7.3 places distributional privacy above differential privacy: a mechanism designed for the distributional guarantee automatically inherits every consequence of differential privacy, including its composition properties and its robustness to auxiliary information about individuals. The paper complements it with a separation (Theorem 7.5), so the inclusion is strict. A footnote extends the conclusion to -privacy for databases that differ in elements.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The value of the formalization lies in fixing the definitions. Definition 7.2 is informal about the sampling model ("drawn at random without replacement"), about whether the guarantee holds for all events at once or event by event, and about what means for a mechanism defined on one database size. The proof's count "with probability " is also loose: the exact probability of a given unordered pair is . The mission records one precise reading of each and the theorem under it, and the definitions are reusable for further work on distributional privacy and on the paper's separation result.
The mathematics is short; the difficulty is in the encoding. The step that fails under a careless reading is the passage from "with probability " to "with certainty": it requires the population to be finite and small (the proof takes ), so that a single pair has probability bounded below. If the guarantee is read event by event (for each , most pairs satisfy the inequality for that ), the counting argument still applies to each event separately, but the definition is weaker than the paper's. If databases are allowed to repeat elements, the theorem is false, because distributional privacy never examines a database with repetitions while differential privacy does.
Finset X of cardinality ; a mechanism is A : Finset X → Measure R, and only its values on -element sets matter. [DecidableEq X] is assumed for set difference.(D \ D').card = 1). The paper's literal "" holds for equal-size sets only when ; the replace-one reading is the intended one.Tendsto (fun n => n^2 * β n) atTop (𝓝 0) and the conclusion is ∀ᶠ n in atTop; the claim for every would be false at small .Contributions welcome: proofs of the milestone and the goal, and the footnote's extension for databases differing in elements, stated as a new theorem.
A data curator holds a database of records and wants to publish answers to a large family of statistical questions about it without revealing any individual record. Differential privacy (Dwork, McSherry, Nissim, Smith 2006) makes the requirement precise, and the most basic questions are counting queries: what fraction of the records satisfy a given predicate? Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that a single private release can answer every query of a class to error once the database has size roughly , so that the sample size depends on the class only through its VC-dimension, a quantity from learning theory.
This mission formalizes the converse in §3.1 of that paper: the dependence on the VC-dimension cannot be removed. On databases of fewer than records, every differentially private mechanism has constant error on some query of . The argument is an early instance of the reconstruction attack idea of Dinur and Nissim (2003): accurate answers to many counting queries determine the database, and a mechanism that determines its input cannot be private.
Let be a set (the data universe). An input database of size is a tuple . A predicate is a map , and its counting query is
A class of predicates is identified with its class of counting queries. A finite set is shattered by if every function is the restriction of some ; the VC-dimension is the supremum of the sizes of shattered sets.
A mechanism maps each input to a probability distribution on an output space ; an output is read through an answer map . Two inputs are neighbours if they differ in exactly one entry. The mechanism is -differentially private if for all neighbours and all measurable events . It is -useful for if for every input , with probability at least over , every query is answered to within :
In the paper the output is a synthetic database and .
There is an absolute constant such that for every universe , class , size with , and : every -differentially private mechanism that is -useful for on databases of size satisfies
Theorem 3.11 shows that the VC-dimension term in the paper's upper bound is necessary: for a class of VC-dimension , no private mechanism is accurate on databases of size below , whatever its running time. It thereby locates the sample complexity of private query release between and up to accuracy and privacy factors, a gap that later work on private learning and on fingerprinting codes studied in detail (Bun, Ullman, Vadhan 2014).
The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a checked reconstruction-attack lower bound for differential privacy, together with the corrected statement disclosed below: the printed proof drops the failure probability of the two reconstructions, and keeping it shows that the conclusion requires below , not merely "bounded away from 1". Milestone 3 records the inequality the argument actually yields.
The combinatorial core (Lemmas 3.12 and 3.13) is elementary. The difficulty lies in the last step, which compares the output distributions on two different inputs. The paper argues about a uniformly random , a random element and a random , and the swapped set . Privacy applies to one fixed pair of neighbouring inputs and one fixed event, while the reconstruction guarantee only controls , not whether a particular element is recovered. The "probabilities" of the printed proof mix the mechanism's randomness with the random choice of , , , and they are not the probability of any single event under any single , so the privacy inequality cannot be applied to them as written. The reconstruction event must also be measurable, which depends on the readout, and the failure probability must be carried through both reconstructions. A proof that sets , as the printed one does, does not prove the stated theorem.
Fin n → X with ; the empty database is excluded because every mechanism is private on it and there. In the proof, a set is given to the mechanism as any injective listing of its elements.PrivLearn.Generic.Neighbors); read literally, it would make every mechanism private and the theorem false. Under this reading and are neighbours, so the paper's factor becomes .ans. Synthetic-data mechanisms are the special case databases, so the lower bound covers a larger class of mechanisms. The hypotheses require IsProbabilityMeasure (M z) and the measurability of o ↦ ans o φ for . Without the first, the zero measure is private; without the second, a mechanism into a trivial -algebra would be private and "useful".PrivLearn.Generic.Privacy (neighbours, IsDP) and Vershynin's HighDimProb.Chaining.Shatters and vcDim. Contributions needed: subsets of shattered sets are shattered, and yields a shattered set of size exactly ; measurability of the argmin reconstruction; the averaging/bijection argument. The first two are reusable beyond this mission.