Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Solving a linear system with a large symmetric positive definite matrix is a basic task of scientific computing: it arises from discretized elliptic equations, least-squares problems and the Newton steps of optimization methods. In 1952 Magnus Hestenes and Eduard Stiefel published the conjugate gradient method (cg-method) (J. Res. Natl. Bur. Stand. 49 (1952) 409–436). The method uses only through matrix–vector products and stores a few vectors. The paper's abstract states its central property in one sentence: "The solution is given in steps."
The paper obtains this property from a more general scheme, the method of conjugate directions (cd-method), which also contains Gaussian elimination as a special case. Its argument has two parts. Every cd-method with nonzero directions reaches the solution within steps (Theorem 4:2). The cg-method is a cd-method (Theorem 5:2), which follows from the orthogonality and conjugacy relations of Theorem 5:1. This mission formalizes that chain.
Vectors are real -tuples, with scalar product and squared length . The matrix is real, , symmetric and positive definite, which is the paper's standing assumption (p. 410). The solution satisfies . The residual of an estimate is . Two vectors are conjugate when .
The cg-method (eq. (3:1), p. 411) starts from an arbitrary estimate and sets . Given , , , it computes
In Lean the iterates are cgIter A k x₀ i, a structure with fields x, r, p. The step length is cgA.
The cd-method (Section 4, p. 412) chooses an arbitrary first direction and then sets with and . Each new direction may be any vector conjugate to . Because the directions are free, a cd-run is a property of sequences: IsCDRun A k x r p.
For every , every symmetric positive definite , every and with , and every initial estimate ,
where is the -th cg iterate. This is the statement of the abstract and of Section 3 (p. 410): "one will reach an estimate () at which . This estimate is the desired solution ."
IsCDRun.Finite termination is the property that distinguishes the conjugate gradient method from stationary iterations such as Jacobi or Gauss–Seidel. It explains why the method can be used as a direct solver in exact arithmetic. It is the starting point for the later theory of Krylov subspace methods. The relations of Theorem 5:1 are the checks the paper recommends for monitoring a computation (eq. (3:3)). They are also the input to the paper's further results on the monotone decrease of the error (Section 6) and on the connection with orthogonal polynomials (Sections 14–18).
The result has been proved since 1952 and appears in every numerical linear algebra textbook. As far as a search of the Prove2Me catalog shows (September 2026), it has no machine-checked proof there. The only conjugate gradient material on the platform is a Hilbert-space convergence result for a different recurrence. This mission adds a faithful formal version of the original recursion (3:1) and of the cd-method. It also adds the complete termination argument, organized as in the paper. The definitions and the Theorem 5:1 relations are reusable by any later formalization of Krylov methods, including the second mission of this series on the decrease of the error .
The obvious argument says that the residuals are mutually orthogonal, so at most of them are nonzero. That argument is only as good as the orthogonality, and Theorem 5:1 must be established by a simultaneous induction over four families of relations. The recursion defines by an update, not as , so even needs a proof. Orthogonality of to the earlier residuals needs the conjugacy of the earlier directions, and conjugacy of needs the orthogonality of the earlier residuals. Neither family can be proved first.
A second obstacle is the passage from orthogonality to termination. A cd-run with a zero direction stalls, so Theorem 4:2 needs the directions to be nonzero. The cg directions become zero exactly when the solution is reached, so applying Theorem 4:2 to cg needs a case split at the first vanishing residual.
Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), and is Matrix.mulVec (*ᵥ). The hypothesis on is Mathlib's Matrix.PosDef, which includes symmetry. The solution enters only through the hypothesis A *ᵥ h = k. Indices are 0-based, as in the paper.
The cg iteration is total and has no stopping test. Once , Lean's convention gives and . From then on the iteration stays at , with zero residuals and directions. For this reason the relations of Theorem 5:1 are stated for all indices without guards: after termination they hold trivially.
Two formulations would make the goal trivial, and neither is used. One is a stopping test or step that refers to or to . The other replaces (3:1b), (3:1d) or (3:1e) by the equivalent formulas (3:2a), (3:2b) or , which would move Theorem 5:5 and part of Theorem 5:2 into the definition. The iteration is (3:1) literally.
The cd-method's implicit hypothesis, that the directions are nonzero, is an explicit binder of Theorem 4:2. Without it the statement fails (take ). The hypothesis is satisfiable: the cg run with nonzero residuals is one example.
A complete development needs the standard facts that mutually conjugate nonzero vectors are linearly independent and that independent vectors span . It also needs the induction behind Theorem 5:1. Contributions welcome beyond the milestones include the converse half of Theorem 5:2, the relation (5:2) expressing through , and Theorem 4:5 (the cd-method computes ).
In online convex optimization a player repeatedly chooses a point from a convex set , after which an adversary reveals a convex cost function and the player pays . The player's regret after rounds is its total cost minus the cost of the best fixed point in hindsight. The model covers online portfolio selection, online regression and prediction with expert advice, and it underlies the analysis of stochastic and adaptive optimization methods (Zinkevich 2003; Cesa-Bianchi and Lugosi 2006).
For general convex costs the best achievable regret is of order . Hazan, Agarwal and Kale (Mach Learn 69, 2007) showed that a curvature condition, -exp-concavity, brings the regret down to order , and gave several algorithms that achieve it. This mission concerns the simplest of them, Exponentially Weighted Online Optimization (EWOO), which needs nothing beyond exp-concavity: no bound on gradients and no bound on the diameter of .
Timeline.
Fix and a set that is nonempty, closed, bounded and convex, with positive Lebesgue volume . Fix . The cost functions are , each continuous on and -exp-concave on : the function is concave on (LogRegretOCO.EWOO.IsExpConcave).
EWOO keeps the weights
and on round plays the -weighted mean of ,
(LogRegretOCO.EWOO.ewooPoint). In particular is the centroid of , and each depends only on . The regret against a comparator is .
For every and every ,
This is the paper's printed constant. The paper's proof yields the slightly sharper ; the printed form is the goal.
The proof in §3.4 (p. 187) passes through five displays, each a milestone:
The result. Theorem 7 shows that exp-concavity alone suffices for logarithmic regret, with a constant that does not depend on the size of or on the gradients of the costs. Specialised to the log-loss on the simplex, where , it recovers the regret of Cover's universal portfolio. The bound is the benchmark against which the computationally cheaper second-order methods of the same paper (Online Newton Step, Follow the Approximate Leader) are compared: those need a gradient bound and diameter and pay a factor .
Formalizing it. The theorem is proved in the paper, and a textbook version with a different constant, , appears in Hazan's Introduction to Online Convex Optimization (Theorem 4.4). No machine-checked proof of either is known. The work here is to formalize the paper's proof: Jensen's inequality for a weighted Lebesgue average in , the change of volume under homothety, and the elementary inequality . A companion draft of the textbook version exists on the platform as a private item (OnlineConvexOpt.SecondOrder.ewoo_regret) with another constant; it is not reused.
The pieces are classical, but they have to be assembled in measure-theoretic form. The point is a Bochner integral of a vector-valued function over , and its membership in and the Jensen inequality both require the normalised weight to be a genuine probability measure on , with every integrand integrable. The obvious one-dimensional intuition — "the weighted mean of a convex set lies in the set" — hides the requirement that be closed and have positive volume.
The second obstacle is that Eq. (18) compares the algorithm with an average of the product over all of , while the regret compares it with a single point. The natural attempt, bounding the average below by the value at the comparator, fails: the average can be far smaller than the maximum, and a lower bound that loses more than a factor polynomial in destroys the logarithmic rate. Controlling this loss in dimensions, with a constant independent of the shape and size of , is the heart of the argument.
Points live in EuclideanSpace ℝ (Fin n) with its Lebesgue (Haar) measure volume. Rounds are numbered from : the weights sum over Finset.Ico 1 t, the regret over Finset.Icc 1 T. Cost functions are defined on all of ; only their values on enter. The algorithm is the total function ewooPoint P α f t, and the goal is stated for equal to it — not for an arbitrary sequence satisfying a Jensen-type inequality.
Conventions and corrections relative to the printed text:
⨅ or sInf over , which in Lean would return a junk value off its intended domain and trivialize the statement.volume P ≠ 0 is added: the algorithm divides by , which the paper leaves implicit. Without it Lean's convention would set .Infrastructure that a complete development needs, and that is reusable beyond this mission: Jensen's inequality for concave functions under a probability measure with a continuous density on a compact convex set (Mathlib has ConcaveOn.le_map_integral and Convex.integral_mem); the scaling identity for Haar measure (MeasureTheory.Measure.addHaar_smul); and the elementary bound . Proofs of any milestone, and a general weighted-Jensen lemma usable across the milestones, are welcome.
Online convex optimization models repeated decision making against an adversary: in each round a player chooses a point of a convex set, and only then learns the convex cost of that round. It covers online portfolio selection, online regression and routing, and it is the standard lens for analysing learning algorithms that must commit before seeing data. The figure of merit is regret, the player's total cost minus the cost of the best fixed decision in hindsight. For general convex costs regret over rounds is optimal; for costs with curvature it can be logarithmic.
Hazan, Agarwal and Kale (Mach Learn 69 (2007) 169–192) gave several algorithms with regret for -exp-concave costs, the class that contains the log-loss of portfolio selection. This mission formalizes one of them, Follow the Approximate Leader (FTAL). It connects to the oldest online algorithm, Follow the Leader (FTL), which plays the minimiser of all past costs: FTAL is FTL run on quadratic lower models of the costs, and the paper's analysis shows that FTL itself has logarithmic regret on a class of curved costs.
Timeline. Zinkevich (2003) proved regret for online gradient descent on convex costs. Cover (1991) gave a universal portfolio with logarithmic regret for the log-loss, at a running time exponential in the dimension. Kalai and Vempala (2005) analysed perturbed Follow the Leader through the "be the leader" argument. Hazan, Agarwal and Kale (2007) gave efficient algorithms (Online Newton Step, FTAL, EWOO) with regret for exp-concave costs.
The decision set is nonempty, convex, closed and bounded, and bounds its diameter: for . In rounds the player picks and then pays , where is a cost function differentiable at the points of with gradient norm on . The cost is -exp-concave () if is concave on . The regret over rounds against a comparator is .
Follow the Leader plays (any point of in round 1). Follow the Approximate Leader (version 1 of the paper's Fig. 3) with parameter plays FTL on the approximate costs
In the Lean development these are IsFTLRun P f x and IsFTALRun P β f x, predicates on a whole trajectory .
With , every FTAL run on -exp-concave costs satisfies, for every and ,
This is the paper's statement with its constant, stated for the algorithm as defined, and for every adversarial sequence of costs.
Theorem 6 shows that a simple rule, re-solving a convex quadratic program over all past linearized costs, achieves regret on exp-concave costs, matching the Online Newton Step up to constants. Theorem 5 is of independent interest: it shows that unmodified Follow the Leader, which has linear regret on linear costs, has logarithmic regret whenever each cost is a strongly curved function of one linear form. Portfolio selection is such a case. The appendix lemmas (log-determinant potential, elliptical potential) are standard tools reused throughout the bandit and online-learning literature.
On formalization: the results are proved on paper; none is formalized. The Lean development provides a reusable encoding of Follow the Leader as a trajectory predicate, the "be the leader" reduction, the surrogate reduction for regret, and the matrix potential inequalities, which the Online Newton Step analysis also needs. The paper's printed statements of Theorem 5 and Lemma 10 contain errors (see below); this mission states corrected versions that suffice for the goal.
The obvious attempt, bounding each term by how far the leader moves, requires knowing how far the minimiser of a constrained problem moves when one cost is added. For unconstrained strongly convex quadratics this is an explicit Newton step, but here the minimiser lies in a general convex set and each cost contributes curvature in only one direction, so the accumulated curvature can be singular for many rounds and no per-round strong convexity is available. Turning the per-round movement into a sum that grows only like , with the paper's explicit constant, is the core of the work; the printed Theorem 5 bound is negative for small , so the constants must be tracked exactly rather than asymptotically.
Points are in EuclideanSpace ℝ (Fin n) so that is the Euclidean norm; cost functions are functions on all of , differentiable at the points of , with Mathlib's gradient. Rounds are -based; and are unused. is any upper bound on pairwise distances in . Exp-concavity is ConcaveOn ℝ P (fun x => Real.exp (-α * f t x)). Algorithms are predicates on the trajectory, required at every round, so every tie-breaking rule is covered and adaptive adversaries are included.
Regret is always stated against every comparator . A formalization with a real-valued ⨅/sInf over , or one that bounds the regret of an arbitrary sequence of points rather than of an FTAL run with the paper's , would be trivial or false, and is excluded: the goal carries IsFTALRun with .
Corrections and conventions relative to the printed paper:
deriv with explicit differentiability at the points , .Needed infrastructure: first-order optimality for convex minimisation over a convex set, a mean-value theorem along segments, determinants and eigenvalues of symmetric positive definite matrices (Mathlib has most of this), and the matrix inequality . Contributions welcome: proofs of any milestone, and a proof of the goal from the milestones.
Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round a player picks a point of a convex set , and only then learns a convex cost function and pays . Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.
Many costs met in practice have more curvature than bare convexity. The log-loss of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.
Timeline:
The decision set is nonempty, closed, bounded and convex, and bounds its diameter: for all , with the Euclidean norm. The costs are real functions, differentiable at every point of , with gradient bound on . A cost is -exp-concave () if is concave on .
For a matrix , the generalized projection is a point of minimising over .
The Online Newton Step fixes
writes and , plays an arbitrary , and then
The regret after rounds against a comparator is ; the paper's regret is its maximum over .
In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.
For every run of ONS, every horizon with , and every ,
The added condition is what makes the printed constant correct (see Formalization scope).
Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in , at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.
The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with and a , a different statement) and the Euclidean case of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with and bound ) is an open private draft with different parameters.
The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes , needs a uniform lower bound on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential and a projection in the norm of rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.
Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index is unused. Cost functions are ambient functions , differentiable at the points of , with given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. enters only as an upper bound on distances in . The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.
Corrections and added hypotheses:
Regret is stated against every comparator , never as a real infimum ⨅ over , which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's , and . A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with , , , is a model.
A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, and ); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of .
Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.
The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.
A serial supply chain has stages. Stage is the demand node and stage supplies stage for . Time is discrete, with periods . Stage has a deterministic lead time and a base stock . It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.
The end-item demand in period is . The window demand is , which is when . The demand bound gives , the maximum possible end-item demand over periods, with .
The backlog is the amount the customer of stage has ordered but not yet received. It satisfies the recursion (A1):
Unrolling it gives the closed max-form (A2). The external customer receives 100% service when for all . When demand never exceeds its bound, this is ensured by the service constraints
Let be the holding cost at stage and the echelon holding cost. After constant terms are dropped, the expected holding cost gives program :
Demand is random, and is the expected backlog at stage in a period .
If the echelon holding costs are nonnegative and is nondecreasing, then an optimal solution of is
Formally, (A6) is feasible, and for every period its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible . The weaker claim that "some optimal solution binds all of (A3)" would not be enough.
The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.
The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.
The objective is not linear in . Each is a convex, nonsmooth function of through the maximum in (A2), and the objective subtracts these terms, so minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on , and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.
Stages are natural numbers read on the range . Lead times are natural numbers cast to . Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function , and only indices are read. The backlog is defined by the recursion (A1), computed in steps, with for . The closed form (A2) is a theorem. Randomness is a probability space with a demand path whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.
The page's informal words are read as follows:
Monotone D on .A non-integrable backlog would make its Bochner integral and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.
Useful contributions include a proof of (A2) by downward induction on stages, the integrability of , the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.
Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.
For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.
Let be a finite set with elements. A set function assigns a real number to every subset . It is submodular if
equivalently if the marginal value of an element does not increase as the set grows. It is symmetric if for every ; the cut function of an undirected graph is the standard example. The optimum is
For , denotes the random subset of containing each element independently with probability ; similarly is the random subset of a fixed . The Random Set Algorithm (RS) returns , a uniformly random subset of , without querying . Its expected value is the average of over all subsets,
where is the multilinear extension of , the expectation of on a random set that includes element independently with probability .
For every nonnegative submodular ,
and if is in addition symmetric,
Both parts form the goal, stated as one theorem. The constants and are exact, not asymptotic, and they are tight: the directed cut of a single arc attains , and the cut of a single edge attains .
The milestones need no sign on the function; nonnegativity enters only in the goal.
The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive -algorithm and its local search algorithms with factors and , followed by later work culminating in the tight -approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that is optimal among nonadaptive algorithms required to return one of the queried sets, and that is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.
Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.
The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.
Lemma 2.2 is not a pointwise statement: the random set can be any subset of , and can be smaller on it than both and . The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets and may overlap, and on the union contains an element with probability , so it is not the product distribution with probability on and on . Finally, the third milestone requires identifying the uniform random subset with the union of independent half-samples of and of its complement, as a statement about finite sums.
The obvious attempt at the goal, comparing with for an optimal set by set, fails: is not monotone, so a random set that contains most of may still have small value, and a random set can pick up elements that hurt.
The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption , is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.
Expectations are written as exact finite sums, not as integrals. is the multilinear extension F f (fun _ => 1/2). is , and is the double sum over independent samples , with the product of the two weights. The ranges and , implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.
Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all subsets, is the true maximum rather than the value at one fixed set, and is required to be both nonnegative and submodular.
Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.
Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with , and for multistage models it grows very fast, so is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.
Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional (an optimal transport cost). Scenario reduction then becomes: find a measure supported on a subset of the scenarios with small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.
Let be a set and a cost function with if and only if , and (conditions (C1)–(C2), p. 498). The original distribution has scenarios with weights and . Write .
A set of scenarios is deleted. The reduced measure is with reduced weights , . A transport plan from to is a nonnegative matrix with row sums and column sums . The Kantorovich functional (10) is the value of this transportation problem,
and is the best distance achievable once is fixed. The optimal deletion problem (13) asks for for a given .
In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue (), optWeightsValue () and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.
For every ,
and the minimum is attained at the optimal redistribution rule , where and , for every such choice of .
Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of , which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.
The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.
The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all , not over the kept scenarios.
Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: , (C1), (C2), and . Measurability of and conditions (C3) and (C4) concern and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis , implicit in Theorem 2, is stated explicitly; in Theorem 4, plays this role.
and are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. is defined as the transportation problem and is not defined by the closed form ; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force .
Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).
Nash's equilibrium existence theorem assumes that each player's set of available strategies is fixed. Many social and economic systems do not work that way: a consumer's budget set depends on prices, which are the choices of another agent, and a firm's feasible production may depend on what other firms do. Gerard Debreu's A Social Equilibrium Existence Theorem (PNAS 38(10), 1952) proves that an equilibrium exists in such a system, called a social system or abstract economy (today also a generalized game). Here each agent's feasible actions depend on the actions of all the others.
Arrow and Debreu used this theorem to prove the existence of a competitive equilibrium (Econometrica 22(3), 1954). It is the standard existence result for generalized Nash equilibrium problems in operations research, where the feasible sets are coupled by shared constraints.
Timeline.
There are finitely many agents . Agent chooses an action in a set , a subset of a finite-dimensional real space. A profile lies in . For each agent, denotes the actions of the others, ranging over .
Given , agent may only choose from a nonempty set , a multi-valued function of the others' actions. Its graph is . The payoff takes values in the completed real line . The best value available to agent and the set of constrained best responses are
An equilibrium point is a profile such that, for every , and .
The topological vocabulary is Debreu's §1:
A multi-valued function is semicontinuous if its graph is closed.
Assume that for every , is a contractible polyhedron, is closed, is continuous on , is continuous on , and is contractible for every . Then
The result. The theorem gives an equilibrium for games in which one agent's choices constrain another's. This is the step that makes competitive equilibrium an equilibrium of a game: the market participant's price choice constrains the consumers' budget sets. The same result gives existence for generalized Nash equilibrium problems, including games with shared constraints. Replacing convexity by contractibility also admits non-convex best-response sets: a contractible set such as a star-shaped region or an arc qualifies. Nash's theorem for finite games and von Neumann's minimax theorem are special cases. With values in , payoffs may take infinite values.
The formalization. The theorem was proved in 1952. None of it is formalized on the platform: neither the theorem itself, nor the LEMMA, nor the topological vocabulary of polyhedra and contractible sets used here. Brouwer's theorem is available on the platform as AGT.brouwer_fixed_point. Nash's existence theorem for finite games (AGT.nash_existence) and Sion's minimax theorem are also formalized. All of these assume convexity. The mission produces a machine-checked existence theorem for generalized games, together with a fixed-point theorem for set-valued maps with contractible values on polyhedra.
Most of the argument reduces to the LEMMA, which is a particular case of the Eilenberg–Montgomery fixed-point theorem. The usual route to Kakutani's theorem does not carry over: it approximates a convex-valued map by continuous selections and applies Brouwer's theorem on a convex set. Contractible values do not admit convex combinations of nearby values, and a contractible polyhedron need not be convex, so neither the selection step nor Brouwer on a simplex applies directly. Debreu cites the LEMMA without proof, and Mathlib has no fixed-point theorem for set-valued maps and none of the algebraic topology of polyhedra that the classical results rest on.
The remaining steps are point-set topology. The product milestones require building homeomorphisms and deformations on products of subspaces, and the closed-graph steps require care with continuity on as opposed to continuity everywhere.
Fintype. Profiles live in . The others' actions range over the product over the subtype , so cannot depend on agent 's own action. With a single agent this product is a point, and the theorem becomes the one-agent statement.EReal with its order topology. is a supremum (sSup) in EReal; under the hypotheses it is attained, so it is Debreu's Max. No arithmetic in EReal is used anywhere.Three formalizations would be easier but are not this theorem: one that replaces contractible by convex (that is the Kakutani–Nash setting), one that maximizes over all of instead of , and one that assumes a fixed point of or states only the closed-graph step. None of these is acceptable, and the LEMMA may not be weakened to convex domains or convex values.
The work needed includes a small library of polyhedra and contractible subsets, and closed-graph correspondences on products. The largest piece is a proof of the LEMMA, a fixed-point theorem that is reusable well beyond this mission. Proofs of any milestone, alternative routes to the LEMMA, and supporting lemmas on polyhedra, such as compactness, triangulation or being absolute neighbourhood retracts, are all welcome.
Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.
Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor over a -approximate one-machine schedule, which is when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio . In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.
Timeline of the relevant results:
There are jobs and identical machines. Job has a processing time and a weight ; every job is available at time (there are no release dates).
The precedence constraints form an in-tree (more generally, an in-forest): every job has at most one immediate successor , and following successors never returns to the start. Write if is reached from by following successors one or more times.
A feasible schedule on machines gives each job a start time and a machine; a job runs without interruption for time units; two jobs on the same machine do not overlap; and implies that starts no earlier than completes. The completion time is and the value of the schedule is .
The critical-path length (Definition 4.1 with no release dates) is if has no predecessors and otherwise.
A list is an ordering of the jobs that obeys the precedence constraints. It defines the one-machine schedule that runs the jobs in list order without idle time; its completion times are , the total processing time of the jobs up to and including in the list. An optimal one-machine schedule is a list minimizing .
List scheduling (Graham's rule, footnote 3 of the paper) on machines with list : whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.
Let be an optimal one-machine schedule and the list schedule on machines with list . Then for every feasible -machine schedule ,
Lemma 4.16 (any precedence-respecting list , with its idle-free one-machine schedule ): for every job ,
Lemma 4.10: , i.e. for an optimal list and every feasible .
Lemma 4.11: , i.e. for every feasible on any number of machines, and the value is attained by a feasible schedule on machines.
The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor for a strongly NP-hard problem, halving the factor that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a share of its one-machine completion time, so the same bound applies to other objectives built from completion times.
Formalizing it. The paper's proof is complete and short, but it argues about events at a time (jobs that finish exactly at , jobs that become ready at , machines freed at ) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.
List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form holds only if such idle time can be accounted for by 's own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.
Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits only in lower-bound instances elsewhere; the bounds here assume .succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.
Minimizing the sum of weighted completion times is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.
Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an -machine schedule, and proves that a -approximate one-machine schedule yields a -approximate -machine schedule for every . The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.
An instance has jobs . Job has processing time , release date and weight . Precedence constraints form a strict partial order : means that may start only after completes.
A feasible nonpreemptive schedule on machines assigns each job a start time and a machine; each job runs uninterrupted for time units on its machine, two jobs on one machine do not overlap, , and whenever . The completion time is and the value of the schedule is . A one-machine schedule is the case .
The critical-path length (Definition 4.1) is for a job without predecessors and otherwise; it is the earliest time could complete with unlimited machines.
A list is an ordering of the jobs. Delay List with parameter processes time continuously. A job is ready once it is released and all its predecessors have completed; is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:
For a job , is the set of jobs up to and including in the list, the set after it, the set of jobs of started before , and . Definition 4.4 builds from the schedule a backward path ending at , whose length is .
Let be a feasible one-machine schedule of the instance with for every feasible one-machine schedule . Let and . Every Delay List schedule built on the completion order of satisfies, for every feasible -machine schedule ,
A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.
The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an -machine algorithm at a bounded loss. With an optimal one-machine schedule and the factor is (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's -approximation for parallel machines with release dates (§4.5).
Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.
The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.
Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; , readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor of an optimal one-machine schedule" and "within a factor of an optimal -machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.
Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's is modelled by machines.
It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.
Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.
Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written ), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.
A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the machines are one machine that is times as fast, and allow preemption.
Timeline:
An instance has jobs and identical machines. Job has a processing time and a release date .
A feasible schedule gives each job a start time and a machine. Job runs without interruption on its machine during , and two jobs on the same machine never overlap. The completion times are and the objective is . denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.
The one-machine relaxation has the same jobs and a single machine. Job has processing time and release date in , and may be preempted. A preemptive schedule of gives each job a processing rate . The rates sum to at most at each time, and no job is processed before its release date. Each job receives units in total. Its completion time is the first time by which all of it has been processed. is optimal if is minimal among all such schedules.
A list is an ordering of the jobs, and the completion order of lists the jobs by nondecreasing . Two ways of turning a list into an -machine schedule are compared.
With optimal, its completion order, the strict-order list schedule of and a Delay List schedule of with , every feasible schedule satisfies
The printed lemma says . Its proof gives , which is stated here.
In the order the proof uses them:
Two existence statements accompany them. One says an optimal exists. The other says a Delay List schedule exists for every list and every .
The result gives a -approximation for that is simple to state and runs in time. It improves the bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.
The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.
All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.
The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.
The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the -machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first jobs of the list and the start of the -th job. Proving this needs the strict order.
The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.
Jobs are Fin n and machines Fin m with . Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and 's optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of .
Committed conventions:
Fin n ≃ Fin n. A list of may break ties in completion time in any way, and every such list is covered.The statement cannot be made easy by the hypotheses. Two existence items show that an optimal and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.
Not stated: the running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.
Matrix completion asks to recover a matrix from a small random subset of its entries. It models collaborative filtering (a ratings table with most entries missing), sensor-network localisation from partial distance data, and system identification. With no structure the task is hopeless, so one assumes the matrix has low rank and that its information is not concentrated in a few entries (incoherence).
Candès and Recht (Found. Comput. Math., 2009) showed that nuclear-norm minimisation recovers such a matrix from about random entries. Candès and Tao (IEEE Trans. Inf. Theory, 2010) lowered this to . The same paper also asks how few entries any method could possibly use, and answers it with a lower bound, Theorem 1.7: below about observed entries, no algorithm can succeed. This mission formalizes that lower bound. The two upper bounds of the same paper are separate missions of this series.
Work with real matrices. For a matrix , let be its column space and its row space, and let , be the orthogonal projections onto them. Let be the -th standard basis vector.
Fix an integer and a real . A matrix has rank at most and obeys the incoherence property with parameter (the paper's (I.18)) if and
Since , a matrix of rank exactly can satisfy this only when ; the smallest possible value means the column and row spaces are spread evenly over the coordinates.
Bernoulli sampling. Fix and set . The observed set contains each entry independently with probability , so is the expected number of observed entries. The sampling operator keeps the entries of a matrix that lie in and sets the others to . A recovery method sees only .
The sampling conditions are, with the natural logarithm,
Fix , , and , with an integer. If (I.20) fails, or (I.21) fails, then
On that event, the observations cannot tell from , so no method can recover every such matrix with probability greater than . The statement fixes no constant beyond those the paper prints.
The result. Theorem 1.7 shows that the sample complexity of the paper's upper bounds is close to optimal: about entries are necessary, however the matrix is reconstructed. The count exceeds the degrees of freedom of a rank- matrix by the factor . The logarithm is a coupon-collector effect: every row has to be sampled. The factor shows that the oversampling grows in proportion to the coherence. The bound is information-theoretic, and it holds even when the rank bound and the coherence are known in advance.
Formalizing it. The theorem and its proof in Section II are published. No machine-checked version is known to exist, and the platform has no lower bound for matrix completion. A formal proof would also check the printed argument, whose steps are compressed. It would yield reusable pieces: a Lean predicate for incoherence of matrices of bounded rank built on Mathlib's orthogonal projections, the independence computation for Bernoulli sampling over disjoint entry sets, and the elementary estimates that turn a success probability into a sampling rate.
The probabilistic and analytic parts are elementary. The difficulty is in building the hard instances as matrices and certifying them. For each observation set one has to exhibit, on an event of probability at least , an infinite family of distinct pairs that agree on . Every member must have rank at most and meet both incoherence bounds, measured through projections onto its column and row spaces, and the pairs must stay distinct across the family. The paper describes the instances only informally. They have to be pinned down so that whatever distinguishes from is really invisible on , while the incoherence bounds still hold for every admissible and . Computing the column space and the projection norms of an explicit matrix in Lean is the main infrastructure cost.
Matrices are Matrix (Fin n) (Fin n) ℝ (the platform's MatrixCompletion.RealMatrix n n). The observation model is the platform's bernoulliEventProb with rate , the sum over all of . The sampling operator is the platform's samplingProjection. Logarithms and exponentials are Real.log, Real.exp. The mission's own definitions are IncoherentRankAtMost r μ₀ M (rank at most , with the projection bounds computed from Mathlib's Submodule.starProjection onto the ranges of and in EuclideanSpace ℝ (Fin n)) and SamplingConditionI20, SamplingConditionI21.
The formalization commits to four readings:
The hypothesis "(I.20) fails or (I.21) fails" covers both parts of the theorem. The last sentence of Section II proves the second part from , which the paper states "whenever ". At the two sides are equal, so the strict inequality is false there; milestone 4 states the corrected range , which is all the paper uses, since its is positive.
Trivializing formalizations are ruled out. The set of pairs requires , so the diagonal pairs do not count. "Infinitely many" is Set.Infinite of a set of pairs, not "at least one". Incoherence uses the theorem's and the actual column and row spaces, so the class is the paper's. The hypotheses are satisfiable, for example , , , , , .
Contributions are welcome on every milestone. The Bernoulli independence computation and the incoherence predicate can be reused in the other two missions of this series and in any lower bound for sampling problems.
A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.
In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.
Demand for the season has law on , distribution function and density . As in §3 of the paper, , is strictly increasing on , on , and the generalized failure rate is strictly increasing (IGFR). The expected sales from available units are
The retail price is , the unit production cost , the salvage value , with .
A contract is a pair of wholesale prices . Before production the retailer submits a prebook order of units at . The supplier then produces . During the season, after running out of prebooked stock, the retailer places at-once orders at , filled from the supplier's remaining stock. Pull is ; an advance-purchase discount is . In §5.1 the supplier pays an extra shipping and handling cost per at-once unit. The profits are
A supplier best response to maximizes over . An outcome of is a pair with a best response to and maximizing when every alternative prebook is followed by a best response to it.
Fix and , and suppose the retailer does not prebook under the pull contract : is his unique best reply, followed by the supplier's best response . Then there is with
such that has an outcome, and every outcome of it satisfies
Without shipping costs, advance-purchase discounts with coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.
The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.
The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as . That limit involves , which the model does not provide: is differentiable only on , and for gamma demand with shape above the density vanishes at , so the paper's limit is . A proof of the goal must therefore not rest on the limit display alone.
The second obstacle is the retailer's global choice. The calculus concerns prebooks below the supplier's production . Once , the retailer might instead prefer a prebook at least , turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for close to requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at .
Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on only, so the exponential law is admitted. Quantities range over . Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for , and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue . The prebook function in milestones 5 and 6 is a function pinned on by Eq. (22), which determines it uniquely.
Readings of the paper's words:
A version of the goal that assumed , assumed , compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with , would be weaker than Theorem 8 and is not the target.
A complete development needs the concavity and first-order conditions for , the inverse-function derivative for , and the regime comparison between prebooks below and above . The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.
A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.
The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.
Demand is a random variable with distribution function and density . The paper assumes , strictly increasing, and an increasing generalized failure rate (IGFR): has . Production costs per unit, the retail price is , and leftover units are salvaged for , with . Expected sales with units available are
and the integrated supply chain's expected profit is . It is maximized at with ; write . The efficiency of a contract is , where is the quantity produced.
A contract is a pair of wholesale prices with . The retailer first prebooks units at each. The supplier, seeing , produces . During the season the retailer sells the prebook and, once it runs out, places at-once orders at per unit from the supplier's remaining stock, provided . The supplier's and retailer's expected profits are
with the at-once terms absent when . An outcome of a contract is a pair where maximizes the supplier's profit given , and maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push (), pull () and advance-purchase discount (). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).
For every with , the contract has an outcome and is Pareto; every outcome of every Pareto contract satisfies
and for every some contract with has an outcome with payoffs
A further draft theorem states the step of the proof in which the retailer's outcome profit along falls strictly from to as rises from to .
The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces ; the prebook price then acts as a pure transfer. Every division of is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.
The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.
The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when . Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook always being available and on . Third, the division claim is surjectivity of the retailer's equilibrium payoff over , which needs the solution of to vary continuously with , including at both ends ( at , at ).
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The standing assumptions are a structure: , strictly increasing on , on , and on . Differentiability is required only on , so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over . is a parameter with the hypothesis ; its existence is part of milestone 1.
Readings of informal words: "includes all" means every contract with has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the family; "any division is achievable" is surjectivity onto ; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is " is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when (p. 226, "with push , so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires (p. 228 sets aside as Pareto inferior); pull includes (the paper's remark in the proof) and advance-purchase discounts include (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.
Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of as would turn the goal into algebra, and is ruled out.
Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of , and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.
A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.
Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.
Demand has distribution function and density . The paper's standing assumptions (§3, p. 225) are: , strictly increasing, and the generalized failure rate strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost to produce, sell at the retail price , and are salvaged at .
Expected sales with units available are , and the integrated chain earns . It is maximized at the newsvendor quantity , , with ; the efficiency of a contract is .
A contract is described by the quantity it induces.
Write and (the hazard rate). The retailer's preferred pull contract is and the supplier's preferred push contract is .
A contract Pareto dominates if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.
A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks and the supplier then chooses her production to maximize . A pull contract survives the push challenge if the retailer's profit is strictly highest at .
There is a quantity , , the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that
and every pull contract with survives the push challenge.
The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ( for the supplier, for the retailer) is Pareto, and the least efficient Pareto contract, , is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself.
The results are proved in the paper, with the calculus informal, the unimodality of cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).
The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of (Lemma 1), and that fails to be routine at , where need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records , strictly increasing on , on , and for . Differentiability is not required at : the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy ; no sign is imposed on . Quantities range over . The paper's is a parameter characterized by , and the first milestone proves it exists and is unique.
Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.
Readings of informal words, each named in the item concerned:
The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. , , and are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.
Welcome contributions: basic facts about , and under the demand assumptions, reusable across the series' other two missions.
In the predict-then-optimize framework, a machine-learning model predicts the cost vector of a linear optimization problem , and a decision is made by solving that problem with the prediction. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed judging predictions by the SPO loss, the excess cost of the decision induced by when the true cost is . El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) develop generalization bounds for learning with the SPO loss.
The SPO loss is discontinuous in : its value jumps where the optimization problem has several optimal solutions. The paper's sharper bounds (its Theorems 4 and 5) therefore replace the SPO loss by a margin SPO loss that is Lipschitz, and they hold whenever the feasible region satisfies a geometric condition called the strength property. This mission formalizes the paper's first class of feasible regions for which that condition holds: strongly convex sets, such as Euclidean balls and balls with .
Let be a finite-dimensional real vector space with a norm (the paper's with a generic norm). A cost vector is a linear functional on ; its value at is written , and its dual norm is . The closed ball of radius around is .
The feasible region is nonempty, compact and convex. An optimization oracle is any map with and for all ; no tie-breaking rule is fixed.
If is compact, not a singleton, and -strongly convex for some , then for every oracle ,
The strength parameter equals the strong convexity constant.
Theorem 7 is what makes the paper's margin-based bounds usable for a concrete family of feasible regions. It says two things: the strength property holds with , so the Lipschitz constants in the margin analysis are explicit; and , so the margin of a prediction, and with it the empirical margin SPO loss, is as easy to compute as a dual norm. Combined with bounds on the multivariate Rademacher complexity, this gives generalization bounds for strongly convex regions whose dependence on the dimension improves on the paper's Natarajan-dimension bound. In dimension one it recovers the classical margin bounds for binary classification (Example 7, p. 24).
The results are proved in the paper; Proposition 1 is due to Vial (1983). None of them has a machine-checked proof known to this mission, and Mathlib has no notion of a strongly convex set (its StrongConvexOn concerns functions). The mission produces a formal definition of strongly convex sets for a general norm, the normal-cone characterization, and the connection to the predict-then-optimize strength property. It is one of four missions on this paper; the margin-based generalization bound itself is the subject of mission II, and polyhedral regions of mission IV.
Definition 5 speaks about balls around convex combinations, while Proposition 1 is a pointwise inequality with the exact constant . Evaluating the ball inclusion at any single convex combination loses that constant, since the admissible radius and the displacement of the centre both shrink with the mixing weight. Relating a ball to a linear functional also requires the maximum of over a ball to be attained and equal to , a fact about dual norms whose attainment depends on finite dimensionality.
For , comparing with gives only the inequality ; equality needs every nonzero cost vector to have a unique minimizer over . The oracle minimizes, whereas the normal cone is written for maximizers, so the signs in (5) and (8) do not match directly and are a common source of error.
StrongDual ℝ E), so is c w and the operator norm is the dual norm; balls are Metric.closedBall.S.Nontrivial. Proposition 1 and the ball identity carry no compactness hypothesis, as in the paper.Metric.infDist to the degenerate set; the parameter conditions and are hypotheses of the theorems, not parts of the predicates.In the predict-then-optimize paradigm a model first predicts the cost vector of a linear optimization problem from contextual features, and the prediction is then fed to an optimization solver that returns a decision. Examples include routing with predicted travel times and portfolio choice with predicted returns. The quality of a prediction is judged by the decision it produces. The Smart Predict-then-Optimize (SPO) loss of Elmachtoub and Grigas (Management Science 2022) measures exactly that: the excess cost of acting on the prediction instead of on the true cost vector.
El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) ask when a model with small empirical SPO loss also has small expected SPO loss. The SPO loss is non-convex and discontinuous, so standard Lipschitz-contraction arguments do not apply to it directly. Their Section 4 introduces a margin version of the SPO loss, in the spirit of the margin theory of Koltchinskii and Panchenko (Ann. Statist. 2002) for classification. They show that it is Lipschitz under a geometric condition on the feasible region, and derive a generalization bound in terms of the multivariate Rademacher complexity of the hypothesis class. This mission formalizes that bound.
Decisions live in with a norm ; cost vectors are linear functionals with the dual norm . The feasible region is nonempty, compact and convex, and throughout Section 4 it is not a singleton. An optimization oracle maps each cost vector to some minimizer . The SPO loss of a prediction against the realized cost is
and the linear optimization gap is , with and for the set of possible true costs.
A cost vector is degenerate if has more than one optimal solution; is the set of degenerate costs. The distance to degeneracy is . The region has the strength property with parameter if
For the -margin SPO loss equals when and otherwise. It dominates the SPO loss.
Data are drawn from a distribution on features and costs in , and is a class of prediction functions . The SPO risk is and the empirical margin risk is . The multivariate empirical Rademacher complexity is with i.i.d. Rademacher vectors , and is its expectation over the sample.
In the set-up, under the strength property with and for fixed , for every , with probability at least over an i.i.d. sample of size , for all :
Theorem 3 is stated for a general norm, as in the paper. Eq. (7), Theorem 4 and the goal are Euclidean. The paper's Theorem 5 (p. 20), a version of the goal uniform over , is not part of this mission.
The bound replaces the loss-class complexity of the SPO loss, which is controlled only through combinatorial dimensions (Natarajan dimension in the polyhedral case, Section 3 of the paper), by the multivariate Rademacher complexity of itself. For norm-bounded linear hypothesis classes this complexity has mild, even logarithmic, dependence on the dimensions and (Section 4.4). The result applies to every feasible region with the strength property. By Section 5 of the paper these include strongly convex sets and polytopes, where can also be computed. When most predictions stay far from degeneracy, and the bound is much sharper than the combinatorial one. It is also a strict generalization of margin bounds for binary classification (Example 7).
The theorem is proved in the paper, which imports two external tools without proof: the Rademacher generalization bound of Bartlett and Mendelson, applied to the margin loss, and Maurer's inequality. To our knowledge none of these results has a machine-checked proof. The mission produces a checked proof of the margin bound and a Lean statement of Maurer's inequality. It also formalizes the strength property and the Lipschitz estimates of Theorem 3, which the companion missions on strongly convex sets and polytopes rely on.
The SPO loss is discontinuous in at degenerate predictions. The standard route, scalar Ledoux–Talagrand contraction applied to the loss class, therefore fails at the first step. It would fail even for a Lipschitz loss, because it relates the loss class only to a scalar class, and is vector valued. Lipschitz continuity of the margin loss needs the oracle to be stable away from . Convexity and compactness of alone do not give that: for an ball with the strength property fails for every (p. 14). The vector contraction inequality of Maurer (2016) is a nontrivial probabilistic inequality, and its constant must not depend on the dimension . The final concentration step is McDiarmid's inequality for a supremum over a possibly uncountable class, which in a formal proof needs measurability of that supremum.
The decision space is a finite-dimensional real normed space E. Cost vectors and predictions are continuous linear functionals, StrongDual ℝ E, whose operator norm is the paper's dual norm. In the statements E = EuclideanSpace ℝ (Fin d), where the dual norm is Euclidean. Every statement carries the standing assumptions: nonempty, compact, convex and not a singleton, an arbitrary oracle (no tie-breaking rule), and , . The Lipschitz-like bounds of Theorem 3(a)–(b) are stated multiplied out, because the paper reads as . Expectations over signs are finite averages over sign patterns. and are suprema over a nonempty bounded containing the cost almost surely. "With probability at least " is the statement that the outer -measure of the failure event is at most .
Added hypotheses, all disclosed in the statements: the multivariate Rademacher sums are bounded above (almost surely in the goal) and is integrable, since otherwise Lean's junk value would replace an infinite complexity and make the bound false rather than vacuous. Hypotheses and measurable, and the uniform deviation and margin Rademacher suprema a.e.-measurable, are also added; the paper is silent on measurability. A singleton would make empty and the strength property hold for free; this is excluded explicitly, so the strength property is not vacuous.
A complete development needs the Bartlett–Mendelson symmetrization bound for bounded losses, McDiarmid's inequality, Maurer's inequality, and the Lipschitz and distance-to-degeneracy facts of Section 4.1. Maurer's inequality and the multivariate Rademacher complexity are reusable across vector-valued learning theory. Proofs of any milestone, and of Maurer's inequality in particular, are welcome.
Facility location asks where to open service points (warehouses, plants, servers) and how to connect customers to them so that the total opening cost plus the total connection cost is minimum. In the capacitated version each facility can serve only a limited number of customers, which is the situation in most applications: a warehouse has a floor area, a server a bandwidth. The problem is NP-hard, and the algorithms used in practice for it are often simple local search heuristics: start from a solution and repeatedly apply a small change that lowers the cost, until no such change exists.
The quality of such a heuristic is measured by its locality gap: the largest possible ratio between the cost of a solution that no allowed change can improve and the cost of an optimum solution. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave locality-gap analyses for k-median, uncapacitated facility location, and the capacitated problem in which several copies of a facility may be opened. This mission formalizes their §5, the capacitated case.
Timeline (as surveyed on pp. 545–546 of the paper). For the variant 1-CFL, where at most one facility may be opened at each location, Korupolu, Plaxton and Rajaraman (1998) showed that local search with add, drop and swap moves has locality gap at most 8 when capacities are uniform; Chudak and Williamson (IPCO 1999) refined this to 6, and Pál, Tardos and Wexler gave a local search with gap 9 for nonuniform capacities. For ∞-CFL, the variant with copies studied here, the known algorithms were LP-based: a 3-approximation of Chudak and Shmoys (1999) for uniform capacities, a 4-approximation of Jain and Vazirani for nonuniform capacities, and a 2-approximation of Mahdian, Ye and Zhang. Arya et al. (2004) analysed local search for ∞-CFL with nonuniform capacities: with a new move that drops any set of open copies and opens several copies of one facility, the locality gap is at most 4 (Theorem 5.5), and scaling the facility costs gives (p. 561). The tight example for uncapacitated facility location (§4.3) also shows a locally optimum solution of cost 3 times the optimum, so the locality gap of the procedure lies between 3 and 4; its exact value was left open (§6).
An instance consists of a finite set of clients, a set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality; is the cost of serving client from facility . Every facility has an opening cost and an integer capacity . Any number of copies of a facility may be opened; each copy of costs and serves at most clients.
A solution opens a finite list of copies, copy being a copy of facility , and assigns every client to a copy so that each copy serves at most clients. Write for the set of clients served by copy and for the clients served by a set of copies. Its costs are
The neighbourhood (9) of a solution whose multiset of open facilities is consists of
is locally optimum if no neighbour, with any feasible assignment of the clients, has smaller cost.
For every instance with at least one client, every locally optimum solution and every solution ,
In the order the paper's proof uses them:
A companion item states the scaled bound of p. 561: a local optimum for facility costs has cost at most in the original instance.
The result. Theorem 5.5 gives a constant locality gap for a local search procedure for capacitated facility location with copies and nonuniform capacities, a variant previously approached through LP-based algorithms; the drop-add move it analyses is the paper's new operation for this problem. The scaled bound gives an approximation algorithm once local search is run to approximate local optimality. The paper also shows (Figure 13, the procedure T-hunt) that the exponentially large neighbourhood can be searched with a knapsack oracle, so the analysis applies to an implementable algorithm.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a checked model of capacitated facility location with copies (solutions, costs, the multiset neighbourhood) and of the locality-gap argument. The per-copy model and the flow comparison of Lemma 5.4 are reusable for other capacitated location problems and for local search analyses that compare a local optimum with an optimum through a flow or a matching.
The obvious attempt imitates the uncapacitated analysis: close one copy of and send its clients to a nearby copy of . With capacities this fails, since that copy of may be too small to absorb them, and single-copy moves do not certify a constant bound. With the drop-add move a single copy of must be charged for a whole group of copies of , and the groups must be chosen so that the charges add up to a constant times ; the rounding of the number of new copies costs an additional that has to be absorbed as well.
CFLSol Cl Fa u: a number n of open copies, a map loc : Fin n → Fa giving the facility of each copy, and an assignment σ : Cl → Fin n with the capacity constraint for every copy. Copies are separate indices because is per copy. Its multiset of facilities is the image multiset of loc.Contributions are welcome at every level: proofs of the milestones, alternative proofs of Lemma 5.4 or (10) (for instance through a matching argument instead of flows), and general infrastructure for multiset neighbourhoods and assignment problems.
The k-median problem asks where to open facilities so that the total distance from a set of clients to their nearest open facility is as small as possible. It is a basic model of facility location in operations research (placing depots, warehouses or servers) and of clustering with representative centres, and it is NP-hard, so the question of interest is how close a polynomial-time method can come to the optimum.
Local search is among the most widely used heuristics for it: start from any facilities and repeatedly exchange one open facility for a closed one while the cost decreases. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first constant-factor guarantee for this heuristic on metric instances: every local optimum of the single-swap local search costs at most five times any solution with facilities. This mission formalizes that result.
Timeline of the relevant bounds:
A metric instance consists of a finite set of clients, a finite set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality. Write for the cost of serving client by facility .
For a nonempty set of open facilities every client is served by its nearest open facility, and the cost of is
The k-median problem asks for a set of at most facilities of minimum cost.
A swap closes a facility and opens a facility , giving . The neighbourhood of is
and is locally optimum if for every . The local search starts from an arbitrary set of facilities and applies improving swaps until none exists; swaps preserve the number of facilities, so it stops at a locally optimum set of exactly facilities. The locality gap is the supremum, over instances, of the ratio between the cost of a worst local optimum and the optimal cost.
The analysis uses the following notation. For a solution , let assign each client to a nearest facility of , let be the service cost of client , and let be the set of clients served by . For two solutions and put . A facility captures if ; is bad if it captures some and good otherwise.
For every metric instance, every , every locally optimum set of exactly facilities and every nonempty set of at most facilities,
The comparison solution is arbitrary, not an optimum; the statement is the locality gap bound in the form the proof gives.
Theorem 3.2 shows that the simplest exchange heuristic for k-median is a constant-factor approximation on every metric instance, and the paper states that the analysis is tight: its example of §3.5, given for swaps of two facilities, is said to generalize to swaps of facilities, where the bound is 5 for . Combined with the standard device of accepting only swaps that improve the cost by a factor , it yields a polynomial-time -approximation (p. 548). The same capture-and-reassignment argument is reused for multi-swap k-median, for uncapacitated and capacitated facility location in the same paper, and in later work on k-means and on local search for clustering; its milestones (the capture graph and the mapping ) are the reusable part.
The result has been proved since 2001 and is textbook material (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, Chapter 9). No machine-checked proof of it is known; Mathlib has no k-median problem and no locality-gap result for any clustering objective. The work remaining is to formalize the known proof.
The obvious argument adds up the inequalities over a pairing of with , rerouting the clients of the closed facility to the nearest remaining facility. This fails when a single facility of serves most clients of several facilities of : closing it leaves those clients with no nearby open facility, and no bound in terms of follows. The analysis must choose which swaps to consider so that such facilities are never closed, and must reroute the displaced clients of the facilities it does close to a facility other than the closed one while paying only a constant multiple of their own service costs. Both choices must work for arbitrary ties in the nearest-facility assignments and when and share facilities.
Namespace LocalSearchFL.KMedian. Clients and facilities are types Cl, Fa with Fintype and DecidableEq; the distance is a real-valued function on Cl ⊕ Fa with fields for nonnegativity, symmetry and the triangle inequality, and is not assumed. Solutions are Finset Fa. The cost is defined only for nonempty sets, from a nonemptiness proof, so no value is assigned to the empty solution; the goal takes nonempty with S.card = k, which is the paper's . Local optimality quantifies over every swap with and , exactly the neighbourhood of Theorem 3.2, and not only over the swaps with that the proof uses. The inequality is stated multiplied out, , so it is meaningful when .
The milestones quantify over nearest-facility assignments , with arbitrary ties. Capture is stated in integers as . The bijection of is a permutation of all clients fixing every client outside ; in inequality (2) it is a single permutation preserving every . Milestones 1–3 are purely combinatorial and are stated for arbitrary assignments, which contains the paper's case.
A formalization in which local optimality ranges over the swaps , , only, or in which or optimal is assumed, or in which the cost of the empty set is , is a different statement and is ruled out.
A complete development needs the finite-sum and Finset.inf' API of Mathlib, permutations (Equiv.Perm) and finite counting. The capture machinery and the mapping are reusable for the multi-swap and facility location missions of this series. Proofs of individual milestones are welcome independently of the goal.
Bilinear programs, which minimize an objective containing a term over constraints on and , model pooling and blending in petroleum refining, location–allocation, certain dynamic production problems and many other applications (Konno 1971, surveyed in Al-Khayyal and Falk 1983, p. 274). The term is not convex, so such problems can have local minima that are not global. For example, has local solutions at and . When and are constrained separately, a solution lies at an extreme point of the feasible region, and vertex-enumeration and cutting-plane methods apply. When the constraints couple and , this property is lost.
Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) gave a branch-and-bound algorithm for this jointly constrained case. It lower-bounds the objective on each box by the convex envelope of the bilinear term, and they proved that it converges to a global solution. The closed form of that envelope, found independently by McCormick (1976) and now called the McCormick envelope, underlies the bilinear relaxations of modern global solvers.
Timeline:
Fix and a box with coordinate rectangles . Problem is
with , convex (and continuous) on their boxes, closed and convex, and . Its optimal value is .
The convex envelope of a function over a set is the pointwise supremum of all convex functions that underestimate on . For a box , the node function is convex and lies below on . The subproblem at node , minimizing over , is a convex program.
A run of the algorithm is a sequence of stages. Stage has the single open node . At stage the Best Bound Rule selects an open node whose subproblem value is least, and the stage point is its subproblem solution. The best lower bound is and the best upper bound is . The selected node is then split. The algorithm picks the coordinate with the largest gap and replaces the rectangle by the four subrectangles cut out by the point (Figure 1 of the paper). All other rectangles are kept. The stage function assigns to each point of the least node value among the open boxes containing it.
For every run,
In attack order:
Theorem 4 of the paper, on the envelope of with concave , is included as a further target.
The convergence theorem certifies that the algorithm computes the global optimum of a nonconvex problem. It is not a local search. Its ingredients carry over to spatial branch-and-bound in general: envelopes that are exact on the boundary of their box, a subdivision at the relaxation's solution, and best-bound selection. Theorem 2 and its separable extension are the building block of McCormick relaxations, used for bilinear terms throughout global optimization.
As far as is known, none of these results is formalized. The mission produces a formal model of a spatial branch-and-bound procedure with rectangular subdivision at the relaxation solution, together with the convex-envelope facts it rests on. The paper's convergence proof is informal and, as printed, passes through two claims that do not hold (see Formalization scope). A machine-checked proof of the convergence theorem would settle the result on firm ground.
The algorithm splits at the relaxation's solution, not at the midpoint, so the boxes of a run need not shrink to points. The usual "exhaustive subdivision" argument, in which the diameters of nested boxes tend to zero, does not apply. What makes the gap close is Theorem 3: after a split, the split point sits on the boundary of the new rectangles in the split coordinate, where the envelope is exact. That exactness has to be carried from the selected points to their accumulation points, across coordinates that may be split finitely or infinitely often. The obvious route through a continuous limit of the stage functions is not available, because the stage functions are not continuous in general.
Vectors are Fin n → ℝ, points are pairs in (Fin n → ℝ) × (Fin n → ℝ), and boxes are four bound vectors, degenerate boxes allowed. The convex envelope is the paper's definition, the real supremum of values of convex minorants, and is used only at points of convex boxes. The McCormick closed form is Theorem 2, a target, and is not built into any definition. A run is a predicate on four sequences: open nodes as a multiset of boxes, selected node, branching index, stage point. Stages are numbered from and runs are infinite: the stopping test is ignored, so a run stopped by the paper is a prefix of one. The optional pruning of p. 278 is omitted, and ties are arbitrary. The optimal value enters through IsMinOn, not through an infimum. The Euclidean distance on is written out explicitly.
Hypotheses and corrections relative to the page:
Two trivializations are excluded. The goal is not a statement about an arbitrary sequence of boxes and points whose gap tends to zero: it quantifies over runs of the algorithm as defined, and a separate well-posedness item, run_exists, asserts that runs exist for every instance. Theorem 2 is about the supremum of convex minorants, not about a function defined by the closed form.
Reusable beyond this mission: the convex envelope and its bilinear closed form, and the box-splitting model. Contributions welcome: proofs of the envelope theorems, a proof of run_exists, and a convergence proof that avoids the false intermediate claims.
The bilinear program
with and polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on and on are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.
Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set of pairs , so that constraints may couple and . They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.
Write points of as , and let be a nonempty compact set. No convexity of is assumed. Let be continuous on .
The function is biconcave over (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside : for every fixed , the map is concave on every convex set with ; and for every fixed , the map is concave on every convex set with . Equivalently, is concave along every segment of that is parallel to the -block or to the -block. A bilinear objective with and concave is biconcave; joint concavity of is not required.
The boundary is the topological frontier of in : the closure of minus its interior. A solution of is a point with for all (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is .
If () is nonempty and compact, and is continuous on and biconcave over , then
The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on (a constant is a counterexample to that).
Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to , and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.
The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.
The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. need not be convex, so it has no useful extreme-point structure, and is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.
What remains is local geometry around an interior minimizer: one must find points of around it at which biconcavity can be applied in both blocks, and control their membership in without convexity. The feasibility of the mixed points and , which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.
EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on ), and BiconcaveOn S φ. One hypothesis is added: . For the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.IsLocalMinOn relative to the box, and non-globality of records the paper's word "proper".IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.A set of integers is a Sidon set if all of its pairwise sums () are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let
A counting argument shows , and the true order was settled early: . What remains open is the size of the error term . Erdős and Turán asked whether it is smaller than every power of ; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.
Timeline.
No upper bound with an error exponent below is known, and no lower bound of the form for every is known either.
A set in an additive commutative monoid is Sidon if for all ,
For a finite set , is the largest size of a Sidon subset of (the empty set is Sidon, so this is well defined), and
The first values are (OEIS A143824).
This is a two-sided statement: it asks both for an upper bound and for a matching lower bound for large . Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.
The result itself. An affirmative answer would pin down to up to a sub-polynomial error, in both directions; Erdős even speculated that might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of . Either answer would be the first change in the exponent of the error term since 1941.
Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this . The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.
For the upper bound, every known argument counts differences in short windows and loses at the scale ; improvements since 1941 only change the constant in front of . For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about in a modulus of size about , and the loss comes from the gap between and the nearest admissible modulus; bringing it below requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.
Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value is a natural number cast to ; is the real square root and , are real powers of . The goal's is Mathlib's Asymptotics.IsBigO along atTop on . The goal is not trivialized by any junk value: is a genuine finite maximum, and the statement concerns all large .
Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for with ; a prime number theorem in short intervals is needed for ). Contributions of reusable Sidon-set lemmas are welcome.
FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjecturesWhich sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every with contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: , so a positive answer would contain the Green–Tao theorem.
Timeline.
The problem is open for every .
A set is an arithmetic progression of length if and for some (for the size condition forces ). For , denotes the largest size of a subset of containing no arithmetic progression of length . A set has divergent reciprocal sum if .
For every ,
This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.
A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of : bounds of the shape for every would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.
Divergence of is a very weak condition: such sets can have density zero, and the natural approach through requires bounds just past . For this barrier was only broken in 2020. For the best known bounds (Leng–Sah–Sawhney) save only a power of in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.
All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over ). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element , if present, contributes . "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with are written without a multiplicative constant and with "for all sufficiently large "; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every " forms are welcome.
A set of positive integers is pairwise coprime if for all distinct . The primes are the model example, and a recurring theme in Erdős's combinatorial number theory is that pairwise coprime sets cannot do much better than the primes on natural additive or harmonic statistics. Erdős Problem 1210 asks for a sharp version of this principle for the harmonic weight , which measures how densely a coprime set can crowd the point from below.
Timeline.
Fix a natural number . Consider finite sets of integers with for every , and with for all distinct . For such a set define the reciprocal gap sum
Every term is at most , and the element contributes . Write for the sum of reciprocals of the primes below ; by Mertens' theorem it equals . Throughout, denotes the number of primes .
The goal of the mission is the affirmative answer to Problem 1210: there is an absolute constant such that
for every and every pairwise coprime . A negative answer is equally welcome and is recorded by disproving the goal statement.
The milestones are:
The result itself. An affirmative answer would say that, for the weight , no pairwise coprime set beats the primes by more than a constant, and would give a quantitative form of the heuristic that coprime sets behave like sets of primes near a point. A negative answer would exhibit coprime sets that concentrate near more efficiently than the primes do in the harmonic sense. The [Er77c] variant concerns only primes, and relates the distribution of primes just above to the primes below the interval length .
Formalizing it. Neither the goal nor the [Er77c] variant is known. The mission produces Lean statements checked against the source, a reduction (milestone 2), to be verified in Lean, that isolates exactly which counting estimate would suffice, and the elementary coprimality lemma (milestone 1). These pin down what a proof or disproof must supply.
The natural first attempt splits into elements with a prime factor , of which there are at most , and -rough elements, and then hopes that sieve bounds make the rough part . The obstruction is that may contain many primes in . Bounding the number of primes in a short interval by is a form of the second Hardy–Littlewood conjecture , which is open and known to be incompatible, in its exact form, with the prime -tuples conjecture. So the counting route in milestone 2 needs input on primes in short intervals beyond current knowledge, and any proof of the goal must either supply such input or avoid pointwise counting.
All objects are elementary: is a Finset ℕ, coprimality is Nat.Coprime, primes are Nat.Prime, is Nat.primeCounting, and the sums are real-valued. The source's is encoded as an existentially quantified real constant chosen before and . The source asks a yes/no question; each statement is posed in its affirmative form, and a disproof (a proof of the negation) settles the negative answer. The standing hypothesis means every denominator is at least , so no division-by-zero default can make the statement trivial. The window is written as with truncated natural subtraction together with .
No new definitions are required. Useful reusable contributions include Mertens-type estimates for , partial summation lemmas for finite sums over , and upper bounds for primes in short intervals.
ErdosProblems/1210.lean, https://github.com/google-deepmind/formal-conjecturesAddition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.
Timeline.
The conjecture itself remains open.
For a finite set define the sumset and product set
For nonempty both contain at least elements and at most . The quantity of interest is as a function of .
For every there is such that for every finite set ,
The cannot be removed: there is no with for all (take ; the multiplication table is by Erdős).
A proof of the goal would settle the sharp form of the sum–product phenomenon over . Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over have come together with new incidence-geometric tools.
Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.
Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near , and passing beyond has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to ; even over , where arithmetic structure is available, the best general bounds are the real-number ones.
Sets are Finset ℤ; and are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to . Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis keeps every exponent positive, so the empty set contributes the trivial inequality rather than a junk value . The constant may depend on but not on . The Solymosi milestone is stated for so that .
The statements are for integer sets only; results proved over specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over , multiplicative energy, bounds for the multiplication table) are welcome.