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?
The nearest common ancestor problem asks, for a rooted tree and two of its vertices and , for the deepest vertex that is an ancestor of both, written . It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.
Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: steps are needed in the worst case. This mission formalizes that lower bound.
Timeline.
A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex is represented by a single node , distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on and , the machine is given pointers to and and must return a pointer to .
The node is accessible from in steps or less if it can be reached from by following at most pointers. Write for the set of such nodes. A run of steps from input nodes and is a sequence in which each is the content of a pointer field of a node among . A query with answer is answered in steps if some run of at most steps holds .
The tree is the complete binary tree of height , with leaves. Its vertices are the words (the root-to-vertex path, = left), the ancestors of are its prefixes, the depth of is and its height is . Then is the longest common prefix of and . Logarithms are binary: .
For every , every node type, every list structure with two pointers per node and every injective representation of the complete binary tree with leaves: if every nca query on two leaves is answered in steps, then
This is the last display of the proof (p. 341), which is what the paper's means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.
where is the set of leaves.
The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).
Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.
The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.
N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of steps, AnsweredIn asks for some run of at most steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. counts leaves, not vertices.Real.logb 2. For Lean's gives the true statement ; for , .Set.encard in , so finiteness is part of each claim. Divisions are cleared: .AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.Many estimation problems in statistics, signal processing and bioinformatics minimize a composite function : a smooth convex loss plus a convex but nonsmooth penalty or constraint , such as the lasso's norm or the indicator of a convex set. Proximal Newton-type methods handle such problems by minimizing, at each iterate , a model in which is replaced by its second-order Taylor expansion. Widely used solvers of this kind (glmnet, newGLMNET, QUIC) never solve these model subproblems exactly; they stop an inner iterative solver early by some heuristic. Lee, Sun and Saunders (arXiv:1206.1623v13, 2014) proposed an adaptive stopping rule for the inner solver and proved that it preserves fast local convergence. This mission formalizes that local convergence theory (§3.4 of the paper).
Timeline:
Work in with the Euclidean inner product. The smooth part is twice continuously differentiable and strongly convex with constant : for all . Its gradient is Lipschitz with constant , its Hessian is Lipschitz with constant , and for a constant . The nonsmooth part is proper, closed and convex, and may take the value ; it is given by its domain and its values on . The problem is , and denotes its (unique) optimal solution.
The proximal mapping of is . The composite gradient step with step length is
with ; it vanishes exactly at minimizers of and plays the role of the gradient. The step is the unit step on . The model at is with .
The inexact proximal Newton method with unit step lengths produces , where the direction is any point satisfying the adaptive stopping condition
for a forcing term . The Eisenstat–Walker choice is
Both parts are asserted together. The statement fixes no constant beyond the existence of , and .
Theorem 3.10 justifies stopping the inner solver of a proximal Newton method at a relative accuracy that is set by the current optimality measure : a constant small forcing term keeps linear convergence, and forcing terms that decay to zero recover superlinear convergence, with no sufficient-descent condition on the subproblem and for a generic nonsmooth . Theorem 3.11 shows that the self-adjusting choice (2.25) achieves the superlinear regime automatically. Together they are the composite analogue of the inexact Newton theory used in most large-scale smooth solvers.
The results are proved in the paper. No machine-checked proof of any of them is known, and the platform contains no proximal mapping, composite gradient step or inexact Newton condition. A formalization adds a checked proximal-operator toolkit (existence and nonexpansiveness of , the optimality characterization of , strong monotonicity of ) and a precise form of the theorem: the paper's proofs mix two scalings of the composite step and cite a lemma where another is meant, so the formal proof settles which constants are valid.
The obvious argument compares the inexact step with the exact proximal Newton step and treats the gap as a perturbation. For composite functions this fails: the exact step is defined by a nonsmooth inclusion, and the stopping condition bounds a residual of the model's composite gradient step, not the distance to the model's minimizer. The link between the two is strong monotonicity of the composite gradient step (Lemma 3.9), which requires controlling the proximal mapping of a general closed convex jointly with the curvature of ; for it is immediate, and for general it is the central step. A second difficulty is that the threshold on is not scale invariant: a threshold below chosen arbitrarily does not give convergence, so the admissible has to come out of the analysis.
The space is EuclideanSpace ℝ (Fin n). The nonsmooth part is a pair : nonempty and convex, convex on , and the extended function ( on , off ) lower semicontinuous; indicator functions of closed convex sets are included. The proximal mapping is a total function chosen among the minimizers over , which exist uniquely under these hypotheses. , and are functions of the split and a scalar, never of alone. The Hessian is the derivative of the gradient map, measured in operator norm. Sequences are indexed from ; a run requires and . Rates are stated without quotients.
" sufficiently close to " is an existential radius chosen before the run; assuming , letting the radius depend on the run, or reading part 1 as "for every " (which is false: , , diverges) are ruled out. The forcing sequence of Theorem 3.10 is fixed in advance; that of Theorem 3.11 depends on the iterates through (2.25), with a free first term .
A complete development needs existence, uniqueness and firm nonexpansiveness of the proximal mapping of an extended-valued closed convex function, the subgradient characterization of , and a second-order Taylor bound for functions with Lipschitz Hessian. These are reusable well beyond this mission. Contributions of any of them, of the milestones, or of alternative proofs of Lemma 3.9 are welcome.
The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges carry capacities. It is a basic model of operations research. Transportation, scheduling, bipartite matching and image segmentation reduce to it, and it is the inner step of many combinatorial algorithms.
Goldberg and Tarjan introduced the push–relabel (preflow) method in A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988). Ford–Fulkerson-type algorithms augment along whole source–sink paths. The push–relabel method instead moves excess flow across single edges, guided by integer distance labels on the vertices. Whatever order its local operations are applied in, it is correct and performs of them (§3 of the paper). Section 4 shows that one particular order, processing the active vertices first-in, first-out, cuts the dominant term, the number of nonsaturating pushes, to . The method and its FIFO and highest-label variants are the standard practical maximum-flow codes.
Timeline:
A flow network has a finite vertex set with , a capacity on every ordered pair, a source and a sink . The edges are the pairs with , and there are no loops. A preflow is a function on vertex pairs with and . Its excess must be nonnegative at every . The residual capacity is . A labeling assigns each vertex a value in . A vertex is active if and .
The two basic operations (Fig. 1 of the paper) are:
The algorithm starts by saturating every edge leaving , with and for .
In the first-in, first-out algorithm (§4), each vertex scans a fixed list of its neighbours through a current edge. The push/relabel operation pushes through the current edge if possible. Otherwise it advances the current edge, or, at the end of the list, returns to the first edge and relabels . Active vertices wait in a queue , initially . The discharge operation removes the front vertex and repeats push/relabel until or increases. Every vertex that becomes active meanwhile is appended to , and is appended too if it is still active. Passes over the queue are defined inductively. Pass 1 consists of the discharges of the initially queued vertices. Pass consists of the discharges of vertices added during pass .
For every network, every edge-list order, every initial queue order, and every run of the FIFO algorithm,
The constant is the printed one.
Corollary 4.4 is the combinatorial core of Theorem 4.5, which states that the FIFO algorithm runs in time. Theorem 4.2 shows that the remaining work of the implementation is plus constant time per nonsaturating push. The bound of Corollary 4.4 is therefore what separates the FIFO method from the bound of the generic method, which matters on dense networks. The same pass-counting argument is reused for the parallel algorithm of §6 and underlies later analyses of highest-label and wave variants.
The results are proved in the paper. Formalizing them adds an analysis of a push–relabel algorithm, which the platform does not yet have. Its existing network-flow material states max-flow min-cut and Ford–Fulkerson termination in an arc-based model with nonnegative flows (the Introduction to Linear Optimization missions). The mission builds a precise operational model of the FIFO implementation, with edge lists, current edges and a queue carrying pass numbers, and states an explicit operation count for it. A companion mission in this series treats the generic algorithm's correctness and its operation bound.
The obvious argument is the potential-function count of §3, over the sum of the labels of active vertices. It yields only and does not use the queue discipline at all. The bound has to charge nonsaturating pushes to passes over the queue, and then bound the number of passes by the total growth of the labels. Neither step is visible in the generic algorithm, because both depend on the order in which vertices are processed.
Making this rigorous requires invariants of the implementation that the paper uses silently:
Lemma 4.1 in particular depends on the current-edge scan: an edge passed over earlier stays inadmissible until is relabeled.
The Lean development works in namespace GoldbergTarjan.FIFO. Vertices form a type V with [Fintype V] [DecidableEq V], and is Fintype.card V. Capacities are c : V → V → ℝ with c ≥ 0 and c v v = 0. Flows are antisymmetric real functions on all ordered pairs, not nonnegative arc flows. Excess is computed from the flow. Labels are in ℕ∞, and the empty minimum in relabel is ⊤.
The state of the algorithm consists of the flow, the labels, the current-edge index cur v into the edge list L v, and the queue Q : List (V × ℕ), each entry tagged with its pass number. Push/relabel (Fig. 3) is a total function, and a discharge (Fig. 4) is a relation carrying the number of push/relabel operations it performs. A run consists of the states S 0, …, S K with S 0 the initial state and consecutive states related by one discharge. The printed variant of Fig. 4, which stops as soon as is relabeled, is the one formalized. Counts are natural numbers over all push/relabel operations of all discharges. The number of passes is the largest pass tag of a discharged entry.
All constants are explicit, exactly as printed:
No asymptotic notation is used, and no assumption is made.
A model without current edges, where relabeling happens whenever no push applies, would make Lemma 4.1 vacuous and change the algorithm. Pass numbers that are not propagated by the "added during pass " rule would make the pass count arbitrary. Both are ruled out by the definitions. A sorry-free check, outside the proposal, exhibits a three-vertex network with two legal discharges, two passes and no nonsaturating push, so the run hypotheses are satisfiable.
Reusable beyond this mission are the network, preflow, push and relabel definitions and Lemma 3.5, which is about an arbitrary preflow. Contributions welcome: invariants of FIFO runs (preflow, valid labeling, queue = active set, cur within bounds), proofs of the milestones, and the reduction of Corollary 4.4 to Lemma 4.3.
Many estimation problems in statistics, machine learning and signal processing minimize a composite function, the sum of a smooth loss and a convex but nonsmooth regularizer or constraint: the lasso and -regularized logistic regression, the graphical lasso for sparse inverse covariance estimation, and constrained least squares, where the nonsmooth part is the indicator function of a convex set. First-order proximal gradient methods (ISTA, FISTA, SpaRSA) are the standard tools, and their convergence is at best linear. Practical solvers such as glmnet, newGLMNET and QUIC instead minimize a local quadratic model of the smooth part plus the nonsmooth part at every iteration, and in practice they need far fewer iterations.
Lee, Sun and Saunders (arXiv:1206.1623, SIAM J. Optim. 2014) put these methods into one framework, proximal Newton-type methods, and proved that they inherit the local convergence rates of Newton and quasi-Newton methods for smooth problems. This mission formalizes the exact-subproblem half of their analysis, ending with q-superlinear convergence of proximal quasi-Newton methods whose Hessian approximations satisfy the Dennis–Moré criterion.
Timeline. Dennis and Moré (1974) characterized superlinear convergence of quasi-Newton methods for smooth equations and minimization by what is now called the Dennis–Moré condition. Tseng and Yun (2009) analyzed coordinate gradient descent for composite problems with a scaled quadratic model. Byrd, Nocedal and Oztoprak (2013) studied inexact proximal Newton methods for -regularized problems. Lee, Sun and Saunders (2012–2014) proved quadratic and superlinear local convergence for a generic closed convex .
The problem is
The smooth part is twice continuously differentiable and strongly convex with constant , meaning for all (Definition 3.2). Its gradient and Hessian are Lipschitz continuous with constants and . The nonsmooth part is a proper closed convex function that may take the value . Its effective domain is nonempty and convex, and denotes the optimal solution of (1.1), which is unique by strong convexity.
At an iterate the method chooses a symmetric positive definite matrix and computes the search direction , the minimizer of the model subproblem
The predicted decrease is . A step length satisfies the sufficient descent condition (2.19) if for a fixed . A backtracking line search with factor takes for the least that passes, so the unit step is tried first. The update is (Algorithm 1). With this is the proximal Newton method. With any other choice of it is a proximal quasi-Newton method. The sequence satisfies the Dennis–Moré criterion if
If for all , with , and satisfies (3.2), then every run of Algorithm 1 from any satisfies
The goal fixes no rate constant. It asserts only the shape of the convergence.
In the order the proof uses them:
The result. Theorem 3.7 is the composite counterpart of the Dennis–Moré theorem. It says that the rate of a proximal quasi-Newton method is governed by how well approximates the Hessian of the smooth part along the steps actually taken, whatever the nonsmooth part is. It covers proximal BFGS-type methods for -regularized and constrained problems, and it explains why solvers built on these methods reach high accuracy in few iterations. Theorem 3.4 gives the corresponding quadratic rate when the exact Hessian is used.
Formalizing it. The results are proved in the paper. None of them has a machine-checked proof: the platform currently has Newton's method only for smooth objectives (Boyd–Vandenberghe's quadratic phase in the mission Convex Optimization V: Newton's Method), and nothing on proximal or composite Newton-type methods. The formalization also settles two defects of the printed text. Theorem 3.1 is false as printed, since it lacks an upper bound on : with , and the iterates stall at about . It is therefore stated here under the assumptions of §3.3. Proposition 3.6 uses an undefined constant (read as ), and the first-order inequalities in its printed proof contain a typo. The explicit constant in Theorem 3.4 is the one the paper's proof derives.
The difficulty is the nonsmooth part. For smooth the Newton step solves a linear system, and the classical analysis works with that closed form. Here is defined only as the minimizer of a nonsmooth subproblem, and every estimate on it has to come from the optimality of that minimizer, i.e. from the firm nonexpansiveness of scaled proximal maps in a norm that changes with . A natural first idea is to apply the smooth Dennis–Moré argument to . It fails because is not differentiable and may be outside . The superlinear rate also depends on the line search eventually accepting the unit step. That acceptance comes only from a third-order Taylor bound combined with (2.15) and the Dennis–Moré residual, and a line search that may return any admissible step does not give it.
EuclideanSpace ℝ (Fin n), and matrices are continuous linear operators. is Mathlib's gradient, and is fderiv ℝ (gradient g). "Positive definite" includes symmetry, and is stated through quadratic forms of a symmetric .EReal, never arithmetic. Replacing by a real-valued function on all of would exclude indicator functions and is not the paper's setting.The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges have capacities. It is a basic model in operations research (transportation, scheduling, bipartite matching) and a standard subroutine in combinatorial optimization.
Classical algorithms, from Ford and Fulkerson (1956) through Edmonds–Karp and Dinic (1970–1972) and Karzanov (1974), increase a feasible flow along augmenting paths or blocking flows. Goldberg and Tarjan, A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988, doi:10.1145/48014.61051), replaced this global view by a local one: the push-relabel method maintains a preflow, which may violate conservation at intermediate vertices, and moves excess along edges toward vertices with smaller distance labels. The generic method, with the basic operations applied in any order, is the starting point of the FIFO, highest-label and dynamic-tree implementations analysed later in the same paper, and push-relabel codes remain among the fastest practical maximum-flow solvers.
This mission formalizes §2–§3 of the paper: the generic algorithm is correct, and it stops after a number of basic operations bounded by an explicit polynomial in the numbers of vertices and edges, whatever order of operations is chosen.
A flow network has a finite vertex set with , a source and a sink , and a capacity for every ordered pair of vertices, positive exactly on the edges ; , and there are no loops, .
Flows are real functions on all vertex pairs. A function satisfies the capacity constraint if and antisymmetry if for all pairs. The excess of is . A flow also has for ; a preflow only for . The value of a flow is , and a maximum flow is a flow of maximum value.
The residual capacity is ; pairs with are the edges of the residual graph . A valid labeling is with , and on every residual edge. A vertex is active if , and .
The two basic operations (Fig. 1 of the paper) are:
The generic algorithm (Fig. 2) starts from the preflow that saturates every edge leaving and is zero elsewhere, with the simple labeling , otherwise, and applies applicable basic operations in any order while one exists. An execution with basic operations is a sequence of states from the initial state, each obtained from the previous one by one applicable operation.
Assume the paper's standing assumption . For every execution with basic operations,
and if no basic operation applies in the final state, then is a maximum flow. The paper states the bound as and proves it as "immediate from Lemmas 3.8, 3.9, and 3.10"; the goal states the sum of those three printed bounds. Since every execution is this short, no order of operations runs forever.
In the order the proof uses them: Lemma 2.1 (at an active vertex a push or a relabel applies); Lemma 3.1 (the labeling stays valid); Theorem 3.2 (Ford–Fulkerson: a flow is maximum iff is unreachable from in ); Lemma 3.3 (under a valid labeling is unreachable from ); Lemma 3.5 (from any vertex with positive excess, is reachable); Lemma 3.6 (labels never decrease; a relabeling increases the label); Lemma 3.7 ( throughout); Theorem 3.4 (termination with finite labels gives a maximum flow); Lemma 3.8 ( relabelings per vertex, in total); Lemma 3.9 ( saturating pushes); Lemma 3.10 ( nonsaturating pushes, under ). A further, non-milestone item states the unnumbered invariant that every is a preflow.
The generic bound shows that push-relabel terminates in a polynomial number of steps without any rule for choosing the next operation; the specific orderings of §4–§5 of the paper (first-in first-out, ; dynamic trees, ) refine only the count of nonsaturating pushes, and reuse Lemmas 3.1–3.9 unchanged. The correctness argument, a valid labeling excludes augmenting paths, is the template for the push-relabel minimum-cost flow and assignment algorithms that followed.
These results are proved in the paper and are textbook material. Their machine-checked counterparts are, as far as is known here, not on the Prove2Me platform: the platform's network-flow statements (from Introduction to Linear Optimization, e.g. LinearOptimization.max_flow_min_cut) use a different model, with arc-indexed nonnegative flows and extended-real capacities, and contain nothing about preflows, labels or operation counts. This mission produces a formal account of the antisymmetric-flow model, of Ford–Fulkerson in that model, and of the amortized counting arguments, with the constants the paper prints.
The correctness half is short once the invariants are in place; the difficulty is in the counting. The label bound (Lemma 3.7) is a statement about the whole execution, and it depends on a structural fact about preflows (Lemma 3.5) whose truth rests on antisymmetry and on the nonnegativity of excesses. The obvious first idea for the push counts, bounding pushes per edge or per vertex locally, fails for nonsaturating pushes: flow pushed across a pair can be pushed back later, and nothing local limits how often this happens, so Lemma 3.10 holds only as an amortized statement over the entire execution and depends on both earlier counts. Saturating pushes on a pair can also recur, in both directions, and Lemma 3.9 has to control the interaction between the two directions.
Formally, all of this is reasoning about arbitrary interleavings of operations, with labels in and real-valued flows.
ℕ∞, with ; the relabel value is an infimum, which is on the empty set.σ : ℕ → State V with a length , starting at the Fig. 2 state with the simple labeling (the paper's own assumption for its proofs), each step an applicable push or relabel. "Terminates" means that no basic operation applies, the loop guard of Fig. 2. The three counts are cardinalities of the sets of step indices of each kind.Welcome contributions: proofs of the invariants (preflow, valid labeling, label monotonicity), of Ford–Fulkerson for antisymmetric flows (reusable beyond this mission), and of the counting lemmas. The FIFO bound of §4 is the subject of a companion mission.
Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.
Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.
Demand has density , distribution function and ; on with the upper end of the support, is continuous there, the mean is finite, and the failure rate is strictly increasing. Write for expected sales and .
A retailer (the leader) sets a wholesale price , and a capital-constrained supplier (the follower) chooses a production quantity ; the retail price exceeds the unit cost . Each firm has a credit rating , a default probability with strictly decreasing, and an interest premium with decreasing. The lead time is , the payment term , and are the liquidity risks.
Under a post-shipment scheme with coefficient the supplier earns
with (recourse factoring), (non-recourse factoring) and (reverse factoring with payment extension ). The retailer earns under factoring and
under reverse factoring, where is the supplier's best response. Its first-order condition is (Eq. (12)).
Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium , when , and recourse, with , when . The retailer keeps the existing wholesale price and solves problem (13): maximize over , subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). is the rating at which , and .
(i) If , reverse factoring is dominated by recourse factoring. (ii) If , reverse factoring should be offered with
where with in the non-recourse case, and with in the recourse case.
A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when .
Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).
The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.
The retailer's objective depends on through two opposing channels: the liquidity factor increases, while expected sales decrease because the supplier's effective cost rises. Neither factor is concave in , and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of along the implicitly defined response , which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at against the existing equilibrium). Reducing it to requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.
The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on with a density , and is an extended real. "Continuous p.d.f. with in " is read as continuity on , with outside the support. Credit functions are real functions constrained on . The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.
Readings of informal words, each also recorded in the item's Formalization Note:
Three misprints of the paper are corrected: "if " is read as "if "; "the retailer's maximization problem in (16)" refers to (13); the middle line of the display on p. 6082 carries a stray factor , and the last line is used.
The hypotheses on cannot be met when , and the goal then says nothing about the case, as in the paper. The existing equilibrium, and are never free parameters: is the paper's explicit formula, and the reduction of acceptance to is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to or assumed unimodality would be trivial and is excluded.
The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas (, and increasing) and the explicit best response of a newsvendor-type follower.
Arrival processes to call centers and hospital emergency departments are routinely modeled as nonhomogeneous Poisson processes (NHPPs): Poisson processes whose arrival rate varies over the day. Staffing and queueing models built on this assumption are only as good as the assumption itself, so practitioners test it on data. The standard test, going back to Brown et al. (2005, doi:10.1198/016214504000001808), divides the day into short subintervals, treats the rate as constant on each, rescales the arrival times within each subinterval to , combines all the rescaled data, and applies a Kolmogorov–Smirnov (KS) test of uniformity.
Kim and Whitt (2014, doi:10.1287/msom.2014.0490) ask when this piecewise-constant approximation is justified. If the true rate is not constant on a subinterval, the rescaled arrival times are not uniform, and with enough data the KS test rejects the Poisson hypothesis even when the process really is an NHPP. Section 3 of the paper quantifies this effect through a single number, the degree of nonhomogeneity, and shows how it behaves when the interval is cut into equal pieces. This mission formalizes that section's exact computations for a linear arrival rate.
An arrival rate function on an interval , , is nonnegative, integrable, and strictly positive except at finitely many points. Its cumulative arrival rate is
Conditionally on arrivals in , the arrival times of an NHPP with rate , divided by , are distributed as the order statistics of independent random variables on with the conditional cdf
The degree of nonhomogeneity is the Kolmogorov distance of from the uniform cdf,
It is zero exactly when is constant, and it is the limit of the KS test statistic as the amount of data grows.
For , divide into subintervals of length . For the -th subinterval has cumulative rate , conditional cdf , and share of arrivals . The data of all subintervals, each rescaled to and combined, have the conditional cdf (LEMMA 1).
The linear arrival rate is with and , not identically zero. When its relative slope is ; on the -th subinterval the relative slope is .
In the Lean development these are cumRate, condCdf, degree, subCum, subCdf, weight, mixCdf, linRate and subSlope, in the namespace NHPPArrivals.LinearRate.
For the linear rate, there is a constant such that for every
with, if ,
and, if ,
and in both cases . The constant may depend on , and , but not on ; its value is left open, as in the paper.
The result gives a quantitative criterion for the piecewise-constant approximation: for a linear rate, cutting the interval into equal pieces reduces the degree of nonhomogeneity of the combined data by a factor of order . Since the KS critical value at sample size is of order , this tells a practitioner how fine the subintervals must be, relative to the amount of data, before a KS test of the Poisson hypothesis stops rejecting merely because the rate varies within subintervals. The paper's later THEOREM 6 and its practical guidelines (§3.4, §3.6) rest on these formulas.
The results are proved in the paper by direct calculation; none of them has a machine-checked proof. The mission produces a verified library of the conditional-cdf calculus for NHPPs on an interval (the conditional cdf, its degree of nonhomogeneity, the subinterval decomposition) and the exact linear-rate formulas that the testing literature cites.
The computations are elementary, but two steps are not immediate. First, the supremum of over is a supremum of a nonsmooth function; showing that it is attained at requires knowing the sign of on the whole interval, and for the combined cdf it requires that all the pieces attain their maximal deviation at the same point, which is special to linear rates. For a general rate the naive identity fails: the sup of a sum is at most the sum of the sups, with equality only when the maximizers coincide. Second, LEMMA 1 is a statement about the law of a rescaled random variable (the fractional part of ), which requires splitting a measure along the subintervals and handling their boundary points.
Rates are real functions ; only their values on enter. is an interval integral, subintervals are indexed by with natural numbers cast to reals, and is computed in . All quotients are real divisions; the hypotheses of every statement (, , , and or for the linear rate; integrability, nonnegativity and a finite zero set for a general rate) make every denominator and positive. is the paper's standing assumption of §3.3; excluding is §3.2's requirement that the rate be positive except at finitely many points. The degree of nonhomogeneity is sSup of the image of , and every statement that uses it also asserts that the supremum is attained, so no default value of sSup can make a statement true. The constant of THEOREM 5 is quantified before ; choosing it after would make the bound empty. The statements are about the general definitions of (17) applied to , not about the closed forms (18)–(19), which are separate milestones. The formula for in (19) is stated for only: is undefined when .
The Poisson process itself is not formalized. LEMMA 1's "i.i.d. random variables" is the paper's THEOREM 1 (the conditioning property) applied to each arrival; LEMMA 1 is stated for the law of one arrival time, the probability measure with density on . THEOREM 1, THEOREMS 2–3 and COROLLARY 1 (limits of the empirical cdf and of the KS statistic) are out of scope: they need a point-process layer, the Glivenko–Cantelli theorem and KS critical values, none of which exists in Mathlib. THEOREM 6 is out of scope because the paper gives only a sketch comparing with the KS critical value.
Contributions welcome: proofs of the milestones, general lemmas on sups of for convex cdfs, and the measure-splitting argument of LEMMA 1, which is reusable for any subinterval-based test of the Poisson hypothesis.
Dynamic programming, as introduced by Bellman in the early 1950s, solves sequential decision problems through a functional equation: the value of a problem started in a given state equals the best one-stage return plus the value of the problem started in the state that decision leads to. In practice the argument usually runs backwards. One writes down the functional equation, finds or characterizes a solution, and reads off the structure of optimal decisions from that solution. This is legitimate only if two things hold: an optimal policy exists at all, and the solution of the functional equation that was found is the optimal value, not some other solution of the same equation.
Samuel Karlin's 1955 paper The Structure of Dynamic Programing Models (Naval Research Logistics Quarterly 2(4):285–294) gives an abstract deterministic model in which both questions can be posed precisely. It proves existence of optimal strategies by a compactness argument (Theorem 1), derives the functional equation, which it calls the Principle of Optimality, and identifies the condition under which a solution of that equation is the optimal return: a tail term must vanish. Later treatments of dynamic programming on general state spaces, such as Blackwell's discounted and positive programming (1965–1967) and the monographs of Bertsekas and Shreve, state their verification theorems in the same form, with a solution of the optimality equation plus a condition at infinity.
The model has a state space , a Hausdorff topological space, and a decision space , a nonempty compact Hausdorff space. A strategy is a sequence of decisions, one per stage. The strategy space carries the product topology and is compact by Tychonoff's theorem.
The data are:
From an initial state , a strategy generates the trajectory , , and the weights with . The total yield is
and the optimal return is . The standing assumption of the paper, display (1), is that the partial sums converge uniformly in for each .
Let solve the functional equation
with the maximum attained, and suppose that for every
Then for every , and the maximum is attained (pp. 290–291, §Uniqueness).
Milestone 3 says that the optimal return solves the functional equation. The goal gives the converse on a class of candidate solutions: any solution with a vanishing tail is the optimal return. Together they justify solving a dynamic program by solving its functional equation. The paper's two examples, a two-operation allocation problem with discounting and a resource allocation model driving the state to the origin, obtain uniqueness among bounded solutions and among continuous solutions vanishing at the origin respectively, by checking the tail condition. Without the tail condition the conclusion fails; the paper notes that the limit term "need not be true in general for any solution to the functional equation".
All four milestones and the goal are classical results with published proofs. None of them has a machine-checked proof on this platform: its existing Bellman-equation theorems concern finite-state stochastic models with a constant discount factor, and this model has neither restriction. The mission produces a formal version of the general deterministic model on topological state spaces, with optimality characterized by a verification theorem, which later missions on the paper's examples can reuse.
Existence rests on continuity of on the product space. Each term depends on the first decisions through the composite map , and continuity of that composite in all decisions at once does not follow from separate continuity of in and in . The limit of the series is continuous only because the convergence is uniform.
For uniqueness, the paper's display "" is not an identity: a maximum of a sum is not the sum of the maxima. A proof has to bound from above by the yield of every strategy and from below by the yield of one particular strategy, and the lower bound fails if the tail term is controlled only from above. Attainment of the maximum in the conclusion needs a strategy to be exhibited, not only a supremum computed.
A strategy is a function s : ℕ → D, with the product topology. Lean's 0-based index is the paper's stage : s 0 is , trajectory T ω s 0 is , and weight P s k is , so weight P s 0 = 1. The total yield is a tsum and the optimal return a supremum over all strategies. "Maximum" is encoded as IsGreatest of a range, so every stated maximum is attained. Uniform convergence of (1) is TendstoUniformly of the partial sums to along atTop.
The formalization commits to the following, relative to the page:
Lean's tsum of a non-summable series is , and a supremum of an unbounded family is . Neither default can make a statement trivially true. The uniform-convergence hypothesis forces the series to converge, and under Theorem 1's hypotheses is continuous on a compact space, so the supremum is a maximum. The goal's conclusion is stated without a supremum. A sorry-free check confirms that all hypotheses of the goal hold on a concrete instance with non-zero return: two decisions, constant return , , and .
Needed infrastructure: Tychonoff's theorem, continuity of uniform limits, and attainment of maxima on compact spaces, all in Mathlib. The mission's own definitions are the trajectory, weights, partial and total yield, and the optimal return. Contributions of intermediate lemmas are welcome, for example continuity of , summability from uniform convergence, and the upper and lower tail estimates for . So are formalizations of the paper's Remarks 1 and 3 (Dini's theorem and convergence of the -stage optimal returns).
Integer programming asks whether a system of linear inequalities has a solution . In fixed dimension it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in operations, and runs integer programming in arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.
Timeline.
is Euclidean space with dot product and length , and is the set of integer vectors. For linearly independent , the lattice is the set of integer combinations , , and is a basis. Gram–Schmidt orthogonalisation gives and unit vectors , and , so and . The determinant is . is the length of a shortest nonzero vector of . The projected lattice is the image of under orthogonal projection onto the complement of . A basis is reduced (Definition 2.6) if for every and for .
A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets with .
In Lean, is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), is gsLen b j, is gsCoeff b i j, is latticeDet b, is lambdaOne, is projLattice b j, and a reduced basis is IsReduced b.
For and every bounded convex set with nonempty interior and there is a subspace spanned by integer vectors with and
The printed theorem allows "an dimensional space " with and bound . Taken literally that is trivial (, one translate). The proof on the same page takes , of dimension , and remarks that this "ensures that the subspace is always of dimension at least 1". The goal states that reading.
Theorem (5.5) is a structural form of the flatness theorem. For it says that a lattice-free convex body meets fewer than consecutive integer hyperplanes of some integral direction. For smaller it gives a finer decomposition of into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.
The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.
The naive route to (5.5) is to take a flat direction directly: bound the lattice width of and count hyperplanes. That needs a flatness theorem with an explicit bound below , which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its -fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.
Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of on every projected lattice and a lifting argument (Proposition 1.9).
Conventions: indices are 0-based (Fin m), so the paper's is projLattice b (j-1) and its bound is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. is assumed convex, bounded and with nonempty interior, but not closed.
Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.
Trivializing formalizations are ruled out: the goal forbids , which gives one translate, and , where no translate meets . It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become ).
Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.
A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality (LMI) . In applications the coefficient matrices are measured, estimated or rounded. A solution that is feasible for the nominal data can become infeasible for data that differ from it by an arbitrarily small amount.
El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) introduced robust semidefinite programs (RSDPs): the constraint must hold for every admissible perturbation of the data, and the robust solution is the best point that survives all of them. Their §5 works out the examples in which the robust counterpart has a closed form. The simplest and most widely quoted is the case where every coefficient matrix is perturbed independently and without structure (§5.1): the robust LMI becomes the single convex constraint . The same computation gives closed-form robust versions of linear programs (§5.3), of largest-eigenvalue minimization (§5.4) and of matrix-norm minimization (§5.6), each of which is the nominal problem plus a Tikhonov-type term . Robust linear programming under ellipsoidal uncertainty was developed at the same time by Ben-Tal and Nemirovski (Math. Oper. Res., 1998); robust least squares, the prototype of §5.6, by El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl., 1997).
Fix , a level , and symmetric matrices . For write and (the Euclidean norm). For a matrix , is its spectral norm, the largest singular value, and means that is symmetric positive semidefinite.
An unstructured perturbation is a block row of blocks, viewed as one matrix. It perturbs each coefficient independently:
The robust feasible set is
and the RSDP is: minimize over . With , the matrix whose -th block is for , the perturbation reads (the paper's (19)).
Three further models use the same pattern. In a robust LP, the data of each constraint are shifted by an independent with . In robust eigenvalue minimization one minimizes the worst case over of . In robust maximum-norm minimization, with , , and one minimizes .
For every ,
The RSDP and problem (21), "minimize subject to ", therefore have the same feasible set, optimal value and solutions. The goal fixes no numerical data: , , and are arbitrary.
The goal shows that robustness against unstructured perturbations costs no more than the nominal problem: the robust counterpart is an LMI of the same size , with a right-hand side that is a convex function of and grows like . The sets have no flat faces, which the paper's §5.2 uses to define the robust center of an LMI and which underlies the uniqueness and continuity of the robust solution (the second sentences of Theorems 5.1–5.4, from §4 under hypotheses H1–H3). Theorems 5.3 and 5.4 exhibit robustification as a Tikhonov regularization with parameter or , and Theorem 5.2 turns a robust LP into a second-order cone program.
All four closed forms are proved in the paper, partly by appeal to the general SDP reformulation of its §3. No machine-checked version of any of them exists, to our knowledge. The mission produces the robust counterparts as identities of feasible sets, stated for every , together with the three intermediate steps of §5.1, so that later missions on the uniqueness and stability halves can import them.
The goal is an exchange of a universal quantifier over an infinite family of matrices with a single matrix inequality. The inequality bounds each perturbation, but the converse needs, for each failing direction, one admissible perturbation that attains the bound; the constant comes from the two copies and , and the constant is the spectral norm of , which holds only because is normed as one block row. Normed block by block, the worst case and the constant change. In the milestone route, the positivity of needs a separate argument before any Schur complement can be taken, since the Schur complement with respect to is undefined at , and the elimination of needs the attainment of . For Theorem 5.4 the difficulty is the attainment: an upper bound on the maximum is immediate, while the lower bound requires exhibiting an admissible perturbation that attains it.
Matrices are Matrix (Fin r) (Fin c) ℝ. Coefficients are indexed by Fin (m + 1) with index 0 the constant term. A block row is one matrix with columns indexed by pairs (i, b) : Fin (m + 1) × Fin n (or Fin q), and is Mathlib's operator norm (open scoped Matrix.Norms.L2Operator), the largest singular value, never the default entrywise norm. The vector norm is written as , never as Mathlib's sup norm on Fin m → ℝ. is (A - B).PosSemidef. Standing assumptions made explicit: symmetric; (§3, p. 36); in milestone 2 (at every is feasible); in Theorem 5.4 (empty matrices have norm ).
Readings and corrections of the printed text:
A formalization in which is an entrywise or blockwise norm, is the sup norm, or the robust set quantifies over a single block, changes the constant and is not this theorem; the statements here rule these out by construction.
Useful, reusable infrastructure: the spectral norm of , Schur complements for positive semidefinite block matrices, and spectral norms of rank-one matrices. Proofs of the three §5.1 milestones and direct proofs of the goal are both welcome.
A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality (LMI) . SDPs model problems in control, combinatorial optimization, statistics and engineering design, and they are solved efficiently by interior-point methods. In applications the data are rarely known exactly: they come from measurements, from linearized models, or from rounding. A solution that is optimal for the nominal data may violate the constraint for data that differ only slightly.
El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for robust solutions: points that satisfy the constraint for every admissible value of an unknown but bounded perturbation, and among them one that minimizes . Their paper, together with the contemporaneous work of Ben-Tal and Nemirovski on robust convex optimization (Math. Oper. Res. 23(4), 1998), founded robust semidefinite programming. The perturbation model they use, the linear-fractional representation (LFR), is the standard uncertainty model of robust control, where the same exact reformulation appears as the multiplier characterization of quadratic stability under norm-bounded uncertainty.
This mission formalizes the first main result of the paper: when the perturbation is full (an arbitrary matrix of bounded spectral norm), the robust problem is exactly an SDP with one extra scalar variable.
Fix natural numbers and a decision vector . The data are:
For a matrix , denotes its largest singular value (the spectral norm), and means that is symmetric positive semidefinite. A perturbation is a matrix . The perturbed constraint matrix is the LFR (5)
which is well defined exactly when . For a linear subspace of , the robust feasible set (2) is
and the robust SDP (4) is: minimize subject to , for a given . In this mission , the full perturbation case, and the paper's standing assumption of §3.1 is .
Under , , and , for every ,
The paper states that the robust SDP and a corresponding solution can be computed by solving the SDP "minimize subject to (10)" in the variables . Both problems have the objective , so the identity above, between and the -projection of the feasible set of (10), is the content of that sentence. A companion item states the solution correspondence explicitly: is optimal for the robust SDP if and only if is optimal for (10) for some .
The paper cites the S-procedure as the classical result behind Lemma 3.1; it is already proved on the platform (ConvexOptimization.s_procedure) and is included as a reference item.
The robust feasible set is defined by infinitely many matrix inequalities, one per perturbation, each rational in ; in general such a set is convex but has no tractable description, and the paper notes that the structured version of the problem is NP-hard. Theorem 3.1 shows that for full perturbations nothing is lost by replacing that semi-infinite constraint with a single LMI of size in one extra variable. Consequences: the robust problem is solved by a standard SDP solver; the largest admissible perturbation level is a generalized eigenvalue problem; and the exact result is the benchmark against which the paper's sufficient conditions for structured perturbations (Theorem 3.2) and its closed-form counterparts for unstructured perturbations (Theorem 5.1) are measured.
The result is proved in the paper (from the S-procedure, with the details deferred to a cited report). To the best of available knowledge it has no machine-checked proof. The mission produces a formal statement of the LFR model and of the robust feasible set that later missions on robust SDPs can reuse, a formal proof of the well-posedness condition, and a formal proof of the exact reformulation built on the platform's S-procedure. Formalizing it also records two points the printed statement leaves implicit: the result needs and a nonempty perturbation output dimension .
The direction from the LMI to robust feasibility is elementary. The converse is the substance: robust feasibility is a statement about a continuum of perturbations, each entering rationally, and testing the LMI against finitely many extreme perturbations does not produce a multiplier . The exactness of the reformulation rests on a lossless certificate for an implication between quadratic inequalities, which holds only under a strict feasibility condition; that condition is where enters, and without it the lemma is false. The well-posedness milestone requires showing that is also necessary, which is not a norm estimate but needs a perturbation that makes singular.
Matrices are Mathlib Matrix (Fin a) (Fin b) ℝ. The affine maps are given by coefficient lists indexed by Fin (m + 1), the constant term first. The norm on matrices is the operator norm, opened with open scoped Matrix.Norms.L2Operator; it is the largest singular value, and no other matrix norm is used. is Matrix.PosSemidef, which includes symmetry. Block matrices are Matrix.fromBlocks over the index type Fin n ⊕ Fin q, with top-right and bottom-left. Mathlib's matrix inverse returns at a singular matrix, so the condition appears in the robust feasible set in the same universally quantified clause as positive semidefiniteness, as the paper's "well defined" requires; dropping it, or using an entrywise matrix norm, would change the set and is excluded.
Readings and corrections of the printed statements:
Welcome contributions: proofs of the well-posedness milestone (a spectral-norm and singular-vector argument, reusable wherever must be invertible); of Lemma 3.1 from the S-procedure (the reachability lemma for norm-bounded perturbations is reusable in robust control); of the goal from Lemma 3.1 by rescaling; and general lemmas on the spectral norm of rank-one matrices and on Schur complements of block matrices.
The subgradient method maximizes a concave, piecewise-linear function by moving along a subgradient of an active piece with a prescribed step. Held, Wolfe and Crowder's 1974 paper Validation of subgradient optimization tested the method on three families of Lagrangean duals from combinatorial optimization — the assignment problem, a relaxation of the travelling salesman problem in the style of Held and Karp, and multicommodity flows — and gave the first systematic account of when the method works in practice.
On randomly generated assignment problems of order the authors observed that the method usually did not merely converge: it stopped, after finitely many steps, at an iterate whose subgradient was exactly zero. Their explanation is a structural fact about the assignment dual, Theorem 3.1 of the paper: when the optimal assignment is unique — the typical case for random integer costs — the set of optimal dual prices has full dimension , so a sequence of steps of decreasing length can land inside it. This mission formalizes that theorem and the steps of its proof.
There are men and jobs, and a real cost matrix : is the cost for which man does job . A one-to-one assignment is a permutation of , where is the man doing job ; its cost is . The assignment problem (3.1) asks for a permutation of minimal cost; the assignment is unique if exactly one permutation attains that minimum.
The linear relaxation of (3.1), over doubly stochastic matrices , has the dual linear program (3.2), . For fixed prices on the men the best is , which leaves the dual function (3.3)
the inner minimum being over the men for each job . The optimal set is .
To put in the form the paper uses assignments in a weaker sense: arbitrary functions , of them, with cost and vector (3.4). The subgradient step raises the price of a man assigned no job and lowers the price of a man assigned several; exactly when is a permutation.
In the Lean development these are assignCost, assignVec, IsOptimalAssignment, w and optSet in the namespace HeldWolfeCrowder.Assignment.
If the assignment problem has a unique optimal permutation, then
The hypothesis is uniqueness among permutations; the conclusion is the dimension of the affine hull of the optimal set.
The theorem turns an empirical observation into a statement about the problem: finite termination of the subgradient method on assignment problems is a property of the dual, not luck. Since is unchanged by adding the same constant to every price, always contains a line; Theorem 3.1 says that, under uniqueness, it is as large as it can be. The paper (p. 70) cites the argument of its Section 2 that, with a full-dimensional optimal set, termination of the method is "nearly certain".
The result is proved in the paper; none of it is known to be machine-checked. What the formalization adds is a checked link between three classical ingredients: the integrality of the assignment polytope (Birkhoff–von Neumann, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix), linear-programming duality, and strict complementary slackness, which neither Mathlib nor the platform has in the form needed. The piecewise-linear representation (3.4) is reusable wherever the assignment dual appears as a Lagrangean subproblem.
The inclusion is elementary; the substance is that is nonempty. The obvious candidate — any optimal dual solution — fails: an optimal may leave ties for some , so it sits on the boundary of and shows nothing about dimension. What is needed is an optimal price vector with all these inequalities strict at once, and uniqueness of the optimal permutation is a statement about the primal side only; transferring it to the dual side goes through the linear relaxation (3.1), whose uniqueness is not the hypothesis, and through a strict complementarity property that is not available in Mathlib or on the platform.
Men and jobs are both Fin n; the costs are a : Matrix (Fin n) (Fin n) ℝ with a i r the cost of man i on job r; prices are π : Fin n → ℝ (no inner product or norm is needed, so no EuclideanSpace). The inner minimum of (3.3) is Finset.univ.inf' over the men, well defined for every n. One-to-one assignments are Equiv.Perm (Fin n) with σ r the man doing job r, so the orientation of the matrix matches (3.3); arbitrary assignments are functions Fin n → Fin n. "Of dimension " is Module.finrank ℝ (vectorSpan ℝ (optSet a)) = n. The page prints the index condition of (3.6) as ""; the formalization uses , which is what the argument requires. The case is allowed and trivial.
A statement asserting only that is nonempty, or that it has dimension at least one, is not this theorem: both hold for every cost matrix, the second because is invariant under adding a constant to all prices. The goal requires the full value , and its hypothesis is uniqueness of the optimal permutation, not of the optimal linear-programming solution.
A complete development needs: the assignment linear program and its integrality (Mathlib's Birkhoff–von Neumann theorem), weak and strong duality between (3.1) and (3.2) or directly , and a strict complementarity statement for this primal–dual pair; the last two are reusable beyond this mission. Contributions of any of these, and of alternative arguments for (3.5) that avoid strict complementary slackness, are welcome.
Mathlib/Analysis/Convex/Birkhoff.lean (Birkhoff–von Neumann theorem, doublyStochastic_eq_convexHull_permMatrix). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Convex/Birkhoff.leanMany convex sets that appear in optimization have complicated descriptions in their own space but simple descriptions as projections of higher-dimensional sets. A polytope with exponentially many facets can be the shadow of a polyhedron with polynomially many; the unit disk is the projection of a slice of the cone of positive semidefinite matrices. Such a representation, a lift, turns linear optimization over the original set into a linear or semidefinite program over the lifted one, so the size of the smallest lift measures how hard the set is for conic optimization.
For polytopes and polyhedral lifts, Yannakakis (Yannakakis 1991) showed that the minimal size of a lift equals the nonnegative rank of the polytope's slack matrix. This turned questions about extended formulations into questions about matrix factorizations, and it is the basis of the lower bounds of Fiorini, Massar, Pokutta, Tiwary and de Wolf (2012) for the cut, stable set and traveling salesman polytopes. Lift-and-project hierarchies (Sherali–Adams, Lovász–Schrijver, Lasserre) all produce lifts to nonnegative orthants or positive semidefinite cones, so a criterion for the existence of a lift is also a criterion for when such a hierarchy can succeed.
Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 38(2), 2013) extended Yannakakis' theorem from polytopes and polyhedral cones to arbitrary convex bodies and arbitrary closed convex cones. Their Theorem 2.4 is the target of this mission.
Timeline:
Throughout, carries the Euclidean inner product .
A convex body is a set that is convex, compact, and contains the origin in its interior. Its polar is
A point is an extreme point if with forces ; is the set of extreme points. The slack operator of is
It is nonnegative, and for a polytope it is the slack matrix: rows indexed by vertices, columns by facet normals.
Let be a full-dimensional closed convex cone: closed, convex, closed under nonnegative scaling, with nonempty interior. Its dual is .
In Lean these are IsConvexBody, IsClosedConvexCone, HasLift, HasProperLift and SlackFactorizable in the namespace ConeLifts.Factorization, together with the series' shared ConeLifts.Shared.polar and ConeLifts.Shared.dualCone.
For , a convex body and a full-dimensional closed convex cone :
The two implications are not an equivalence: the forward one assumes properness, and the lift produced by the converse may be improper.
In the order the paper's proof uses them:
with the minimum attained. 4. (proof, p. 5) For and its projection to : . 5. (proof, p. 5) If maps into , and , then . 6. (proof, p. 5) For each there is a unique with .
The result. Theorem 2.4 makes the existence of a lift of a convex body to a given cone a purely algebraic question about its slack operator. Every lower bound on lift size in the paper and its successors goes through it: the nonnegative-rank bounds for polytopes (Section 4 of the paper), the proof that the stable set polytope of an -vertex graph has no lift to (Section 5), and the later psd-rank literature. It also puts Yannakakis' theorem and its semidefinite analogue under a single statement.
Formalizing it. The theorem is proved on paper; no machine-checked version is known to exist. Formalizing it requires conic strong duality with dual attainment under a Slater condition, which Mathlib does not have, and finite-dimensional Krein–Milman for the polar body. The companion missions of this series (nonnegative-rank lower bounds; stable set polytopes and psd lifts) use the correspondence as their entry point.
The converse half is elementary once the extreme points of are known to generate it. The forward half is not: must be an element of that certifies on through the lift. A separating functional gives this certificate on , but writing it as with , and exactly is conic duality with a zero gap and an attained dual optimum. For closed convex cones the gap can be positive or the dual unattained unless a constraint qualification holds; this is why properness is assumed. Weak duality alone gives only , and a dual sequence approaching does not yield a factor. The paper notes (p. 5) that, since the proof uses strong duality, it is not obvious how to remove properness for a general closed convex cone.
Conventions fixed by the Lean statements:
EuclideanSpace ℝ (Fin k); every pairing, in , in and in the factorization, is its inner product.(interior K).Nonempty. Pointedness is not assumed.AffineSubspace and a linear map; the lift condition is the set equality .L.directionᗮ and LinearMap.adjoint π; minima and maxima are stated with IsLeast/IsGreatest, so attainment is part of every claim.Trivializing readings are excluded: is linear, not an arbitrary function (with an arbitrary function every set is a "lift"); is an affine subspace, not an arbitrary set; and takes values in , not , which for a cone that is not self-dual would be a different and generally false statement.
Needed infrastructure: finite-dimensional Krein–Milman in the form for compact convex sets (Mathlib has the closure form); the bipolar theorem for closed convex with the one-sided polar; compactness of when ; and conic linear programming duality with a Slater point, including dual attainment. The last two are reusable well beyond this mission. Proofs of individual milestones, and of these general facts as separate lemmas, are welcome.
A forecaster who announces "70% chance of rain" is calibrated if, among the days on which that number was announced, it rained on about 70% of them. Dawid (The well-calibrated Bayesian, JASA 1982) proposed calibration as the minimal requirement of an honest probability forecaster. Oakes (Self-calibrating priors do not exist, JASA 1985) showed that no deterministic forecasting rule can be calibrated against every sequence of outcomes: an adversary who knows the rule can always choose the outcome that contradicts the forecast.
Foster and Vohra (Calibrated learning and correlated equilibrium, Games Econ. Behav. 21 (1997) 40–55) use calibration as the bridge between learning and equilibrium in repeated games. Their Theorem 1 says that if each player best-responds to calibrated forecasts of the opponent, the empirical distribution of play converges to the set of correlated equilibria. That theorem is only useful if calibrated forecasts can actually be produced whatever the opponent does. Theorem 3 of the paper, credited to an unpublished 1991 manuscript of the same authors and proved in the paper's Appendix, says they can, provided the forecaster randomizes.
Timeline. Dawid (1982) defines calibration. Oakes (1985) rules out deterministic calibrated forecasting against arbitrary sequences. Foster and Vohra (1991 manuscript; 1997 paper, Theorem 3 and Appendix) give a randomized forecaster calibrated against any opponent, through a pairwise ("internal") no-regret property. The full argument appeared in Foster and Vohra, Asymptotic calibration, Biometrika 85 (1998). Hart and Mas-Colell (A simple adaptive procedure leading to correlated equilibrium, Econometrica 2000) later made internal regret the standard route to correlated equilibrium.
Player 2 has pure strategies . In every round, player 1 announces a forecast , a probability vector (, ), and player 2 plays a strategy . The two moves are simultaneous: player 2 does not see the current forecast.
A history of length is the list of the pairs (forecast, play), oldest first. For a forecast vector and a strategy :
A randomized forecaster maps each history to a probability distribution on forecasts. A learning rule of player 2 maps each history to a probability distribution on strategies. In round the forecast is drawn from and the play from , independently given the history of the first rounds. This defines the law of the first rounds (histLaw F A t).
For the Appendix: with forecasts, losses and mixing weights , the pairwise regret of replacing forecast by forecast is
There is a forecaster , with probability-vector forecasts, such that for every learning rule of player 2 and every ,
The forecaster is fixed before the opponent; no rate is claimed, and the rate may depend on .
with the fractional L-2 calibration score. 4. L-1 versus L-2 (p. 54). For each , .
The result. Theorem 3 makes the hypothesis of Theorem 1 attainable: combined, they show that there are learning procedures under which play converges in probability to the set of correlated equilibria of any finite game (the paper's Corollary, p. 49). The intermediate Lemma 1 is an early internal-regret bound; internal (swap) regret minimization later became the standard algorithmic route to correlated equilibria and to calibrated prediction in online learning.
Formalizing it. The result is proved, in the 1997 Appendix in telegraphic form and in full in Foster and Vohra (1998). The Appendix leaves several steps informal (see Formalization scope), so a machine-checked proof must supply them. No formalization of calibration or of internal regret was found on Prove2Me as of 2026-09-26. The mission produces a formal model of randomized forecasters against adaptive opponents, a checked internal-regret bound with an explicit constant, and the passage from regret to calibration.
The obvious approach is to pick, at each round, a forecast that corrects the current miscalibration. This is a deterministic rule, and by Oakes' theorem an opponent can defeat it. Randomization alone does not help either: the forecaster must randomize in a way that controls every pairwise regret at once, not only the regret against the best fixed forecast. External no-regret does not imply calibration.
Two further gaps separate Lemma 1 from Theorem 3. First, the Appendix controls a fractional score in which the event "forecast was issued" is replaced by its probability . The realized calibration score involves the random choices, so a concentration argument is needed against an adaptive opponent. Second, a fixed grid gives calibration only up to its mesh . Exact convergence requires letting the grid size grow and shrink over time, and the scores of the different phases must be combined.
Fin n; forecasts are vectors Fin n → ℝ that are probability vectors (IsDist). Histories are Lean lists of (forecast, play) pairs, oldest first. Forecaster and opponent are maps from histories to Mathlib PMFs. The history law is built with PMF.bind/PMF.map, with the two draws independent given the past. is the toOuterMeasure of the law, in ℝ≥0∞; no σ-algebra on histories is used.∃ F, ∀ A). The reverse order is trivial, since one can forecast 's next play.MarkovChain.exists_isStationary for row-stochastic matrices. Also useful: martingale concentration for PMF-built processes, and Cauchy–Schwarz with weights. The history-law construction is reusable for any repeated forecasting game.Least squares fits a model as if the data were exact. In practice they are measured, rounded or estimated, and the least-squares solution can be very sensitive to such errors. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to treat the errors as deterministic, unknown but bounded, and to choose minimizing the worst-case residual over all admissible data. For unstructured perturbations of bounded in Frobenius norm this leads to a second-order cone program (missions I and II of this series).
In many applications the perturbations have a known structure: a Toeplitz matrix stays Toeplitz, a parameter enters several entries at once, or only some entries are uncertain. An unstructured bound then over-estimates the worst case. The paper's §4 treats perturbations that are affine in a parameter vector bounded in Euclidean norm, and shows that the resulting structured robust least-squares (SRLS) problem is still solved exactly, now by a semidefinite program (SDP). This model of uncertainty (an ellipsoid of affinely parametrized data) is the one later adopted as the basic uncertainty set of robust optimization; see Ben-Tal and Nemirovski, Math. Oper. Res. 23(4), 1998.
Vectors carry the Euclidean norm . Given matrices and vectors , define for every
For and the structured worst-case residual is
and is an SRLS solution if it minimizes over . The paper takes throughout §4 and writes .
For fixed let and
Since , the squared residual at is the quadratic function . Finally, for scalars ,
With and , consider the SDP in
The goal states that (a) for all and , some makes feasible if and only if ; and (b) is optimal for (32) if and only if is an SRLS solution, , and is feasible. This is the precise content of the paper's "the SRLS can be solved by computing an optimal solution of (32)".
The result shows that a min–max problem over a nonconvex worst case (the inner problem maximizes a convex quadratic over a ball) is equivalent to a single convex SDP whose size is linear in , and , and hence solvable in polynomial time by interior-point methods. It covers as special cases the unstructured problem of §3, least squares with uncertainty in selected entries, and Toeplitz or otherwise patterned perturbations. The exactness contrasts with the next section of the paper, where the linear-fractional and -bounded versions are in general only bounded from above, or shown NP-hard.
The result is proved in the paper; to the best of current knowledge it has not been formalized. The platform already has the one-constraint S-procedure (ConvexOptimization.s_procedure, proved, in a different sign and block convention); this mission adds the robust least-squares objects, the reduction to the S-procedure, the Schur-complement step, and the optimal-solution correspondence of Theorem 4.2. The worst-case residual and SDP (32) definitions are reusable by later robust-regression missions.
The obvious approach is to compute the inner maximum directly. The function is convex, so its maximum over the unit ball is attained on the boundary, but it is not given by any closed-form expression in general, and maximizing a convex function is not a convex problem. Exactness therefore rests on the lossless S-procedure for one quadratic constraint, a nonconvex duality statement that fails for two or more constraints; the sufficient direction alone only yields an upper bound.
A second point is passing from "for fixed " (Theorem 4.1) to "optimal over " (Theorem 4.2): is quadratic in , and only the Schur-complement lift (32) is jointly affine in . The correspondence of optimal solutions must then be checked in both directions, including that the optimal is the squared residual and not the residual.
A0 : Matrix (Fin n) (Fin m) ℝ, A : Fin p → Matrix (Fin n) (Fin m) ℝ, b0 : Fin n → ℝ, b : Fin p → Fin n → ℝ; A i is the paper's (0-based index). Vectors live in Fin k → ℝ with the Euclidean norm written out as , never Mathlib's sup norm.sSup of the set of attained residuals over the closed ball; for this set is nonempty and bounded, so sSup is the true maximum. The theorems use , as the paper does; the paper derives general by scaling and that is not stated here.Matrix.fromBlocks in the printed order (scalar block first: Unit ⊕ Fin p; for (32), (Unit ⊕ Fin p) ⊕ Fin n). "" is Mathlib's PosSemidef, which includes symmetry; all matrices here are symmetric by construction.Matrix.PosSemidef.fromBlocks₂₂ and relatives in LinearAlgebra.Matrix.SchurComplement); the platform's ConvexOptimization.s_procedure and ConvexOptimization.single_constraint_quadratic_strong_duality with their definitions ConvexOptimization_quadraticForms, included as reference items. A bridge lemma between the platform's block convention and this mission's is a welcome contribution, as is a general- version.The least-squares (LS) problem assumes that the data , are exact. In applications they rarely are: they come from measurements, from linearizations, or from models with neglected dynamics. A classical response is sensitivity analysis or regularization (Tikhonov), where a weight trades the size of the solution against the fit, and the choice of that weight is left to the user. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) take a deterministic view instead: the true data lie in a known ball around , and the solution should minimize the residual it can be forced to have in the worst case over that ball. The paper shows that this robust least-squares (RLS) problem is solvable exactly, in the unstructured case by a second-order cone program (SOCP). The same worst-case idea, applied to regression, underlies the later equivalence between robustness and regularization (Xu, Caramanis and Mannor, 2009) and is a standard entry point to robust optimization (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009).
This mission formalizes the first main result of the paper, Theorem 3.1: the worst-case residual has a closed form, its minimizer is unique, and minimizing it is an SOCP.
Vectors carry the Euclidean norm . For a matrix , is the Frobenius norm and the largest singular value, i.e. the smallest with for all .
Fix and . A perturbation is a pair , , collected in the augmented matrix . For a bound and , the worst-case residual is (paper, eq. (1))
and is an RLS solution if it minimizes . The bound constrains the augmented matrix jointly, not and separately. The paper normalizes and writes . Finally, denotes stacked over . In the Lean development these are RobustLS.Unstructured.eucNorm, frobNorm, specNorm, augment, stackOne, worstCaseResidual A b ρ x, its largest-singular-value variant worstCaseResidualSpec, and the SOCP constraint predicate SocpFeasible A b x λ τ.
For , every , :
the problem has exactly one solution , and it is the SOCP
in the sense that is the least for which some makes feasible.
The closed form replaces a maximization over a matrix ball of dimension by two Euclidean norms. It shows that the RLS objective is the LS residual plus a penalty that does not depend on or , which is the starting point for the paper's Theorem 3.2 (the RLS solution is a Tikhonov-regularized LS solution with a data-dependent weight) and its analysis of continuity and conditioning. The SOCP formulation places the problem in the class solved by interior-point methods, at a cost the paper compares with one singular value decomposition of . The spectral-norm statement says the worst case does not depend on which of the two standard matrix norms bounds the perturbation.
The result is proved in the paper; the proof is short. To the best of the planning survey (September 2026), no machine-checked proof exists, and Prove2Me has no statement about worst-case residuals or robust least squares. The mission produces a verified closed form that later missions of this series (Tikhonov form of the solution, structured and linear-fractional perturbations) and any formalization of robust regression can import.
The upper bound alone does not give the theorem: the statement is an equality, and the equality needs an explicit maximizer. The paper's printed maximizer is wrong by a sign: with in place of the perturbation does not attain the bound (for , , it gives residual instead of ), so a transcription of the printed proof fails. Two further points are silent in the paper. The operator norm of a rank-one matrix has to be computed from the definition of the largest singular value. Uniqueness of the minimizer needs existence first, which follows from growth of at infinity and is not stated. Working with the sSup definition of the worst case requires showing the set of residuals is bounded, which is milestone 1.
Fin n, Fin m; is Matrix (Fin n) (Fin m) ℝ, and are functions Fin n → ℝ, Fin m → ℝ. The augmented matrix is indexed by Fin m ⊕ Unit, and so is .eucNorm), never Mathlib's ‖·‖ on Fin n → ℝ, which is the sup norm. The Frobenius norm and the largest singular value are explicit definitions (frobNorm, specNorm); specNorm is the infimum of admissible operator constants.sSup of the set of attained residuals. For the set is nonempty and bounded, so this is the true maximum; milestones 1 and 2 state the bound and the attaining perturbation directly, so no statement relies on the value of sSup on an unbounded set.∃! of a global minimizer over all of .Contributions welcome: lemmas on Frobenius and operator norms of rank-one matrices, the inequality in this explicit setting, and strict convexity of ; these are reusable beyond the mission.
Paging is the problem of managing a two-level memory: a cache holds of the pages a program uses, every request must find its page in the cache, and a request to a page outside the cache (a page fault) forces the algorithm to bring the page in and evict another. An on-line algorithm chooses what to evict without seeing future requests. Sleator and Tarjan (CACM 1985) measured on-line paging algorithms against the optimal off-line algorithm, which knows the whole request sequence, and showed that no deterministic on-line algorithm can be within a factor smaller than of it.
Randomization changes that picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) gave a randomized algorithm, the marking algorithm, whose expected number of faults is within of the optimum, where . This mission formalizes the other half of their paper's picture: no randomized paging algorithm can do better than . The bound says that the logarithmic behaviour is not an artefact of one algorithm but a property of the problem.
Timeline:
Let be a set of vertices with the uniform metric: any two distinct vertices are at distance . A configuration of servers is a map ; server sits at , and a vertex is covered when some server sits on it. A request sequence is a finite list of vertices. A deterministic on-line algorithm assigns to every prefix of requests the configuration after serving it, in such a way that the vertex just requested is covered; its cost on is the total distance travelled by its servers, which on the uniform metric is the number of server moves. Paging with cache slots and pages is exactly this -server problem on uniform vertices.
The optimal off-line cost is the least cost of any schedule of configurations that starts at and covers each request of in turn.
A randomized on-line algorithm is a probability space of coin outcomes together with a deterministic on-line algorithm for each outcome . Its expected cost is the average of the cost of on over . The request sequence is fixed in advance and does not depend on the coins (an oblivious adversary). Following the paper, is -competitive from the initial configuration if there is a constant such that
For the lower-bound argument, the probability vector after a prefix has equal to the probability, over , that vertex is not covered by after serving . A set of marked vertices and the number of unmarked vertices are bookkeeping of the adversary, updated as the marking algorithm would update them.
For , every randomized on-line algorithm with servers on uniform vertices, every initial configuration and every real ,
The case : no randomized algorithm for the uniform -server problem on vertices is -competitive with .
With the probability vector, the marked set, and :
The result. Together with the marking algorithm's upper bound, the corollary pins the randomized competitive ratio of paging to , an exponential improvement over the deterministic ratio that no randomized algorithm can push below . For the marking algorithm itself is -competitive, so Theorem 4 makes it optimal there. The bound is the benchmark every later randomized paging algorithm is measured against, including the -competitive algorithm of McGeoch and Sleator, and it is the uniform-metric base case of the randomized -server conjecture.
Formalizing it. The theorem is proved and classical; no machine-checked proof is known to exist. The platform already has the deterministic bound (KServer.uniform_not_competitive_below_k, ratio ) and a formal Yao averaging principle for randomized -server algorithms (KServer.randomized_yao_averaging), but no randomized paging lower bound. This mission produces the first formal lower bound, stated against the published randomized -server model, and a formal version of the paper's adversary argument. Either route — the paper's adaptive construction of a nemesis sequence from the probability vector, or Raghavan's distributional argument through Yao's principle — is welcome.
The adversary may not look at the coins, yet it must build one fixed sequence against which the expected cost is high in every phase. Requesting an uncovered vertex is not available, since which vertex is uncovered depends on the coins; requesting the vertex with the largest uncovered probability gives only per request and loses the harmonic sum. Lifting the per-phase bound to the asymptotic statement also requires handling the additive constant , the initial configuration of the off-line algorithm, and, for Corollary 5, the reduction from vertices to of them for an algorithm that may still place servers on the others.
The Lean development reuses the published definitions KServer_model (configurations Fin k → M, deterministic on-line algorithms as functions of the request prefix, offlineCost) and KServer_randomized (RandomizedAlgorithm: a probability measure on coin outcomes, a deterministic algorithm per outcome, measurable costs; expCost as a lower Lebesgue integral in ; IsCompetitiveFrom C₀ c: every drawn algorithm starts at and there is one constant , fixed before the sequence, with expCost σ ≤ ENNReal.ofReal (c * offlineCost C₀ σ + a)). The clamp at in ENNReal.ofReal only weakens the property the goal refutes. The vertex set is an abstract type with an equivalence Fin n ≃ M and the uniform metric as a hypothesis, never the line metric of Fin n. is Mathlib's harmonic k cast to . The goal quantifies over every algorithm and every initial configuration, with no laziness or distinct-positions assumption, and over every real , including .
A formalization in which competitiveness is vacuous (a model with no algorithms, or a cost that is always infinite), in which the adversary may choose the sequence after seeing the coins, or which fixes or the additive constant, would be a different statement and is ruled out by the published definitions used here.
The probability vector is the one new definition, uncoveredProb A σ i. Milestones about it assume the uncovered events measurable, the standing convention that is a probability; the model itself only guarantees measurable costs. The milestone assumes the servers occupy distinct vertices, as in the paper; in general . The arithmetic milestones are stated for an arbitrary probability vector on a finite set. Reusable pieces: the probability vector and the cost lemma apply to any randomized -server algorithm on a uniform metric, and a restriction lemma (from vertices to ) would serve other paging lower bounds.
Paging is the problem of managing a two-level memory: a fast cache holding pages and a slow memory holding the rest. When a requested page is not in the cache (a page fault), it must be brought in and, if the cache is full, some page must be evicted. An on-line paging algorithm decides which page to evict without knowing future requests. Sleator and Tarjan (CACM 1985) compared on-line algorithms with the optimal off-line algorithm on every request sequence and showed that the best deterministic algorithms (LRU, FIFO) lose a factor of exactly , and that no deterministic on-line algorithm does better.
Randomization changes this picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) showed that the randomized marking algorithm is -competitive, where , and that no randomized algorithm is better than -competitive. For the marking algorithm does not reach , already for and . For two servers the same paper gives a different algorithm, EATR ("end after twice requested"), and proves it -competitive. Since , EATR is strongly competitive for : no randomized algorithm has a smaller competitive factor. This mission formalizes that result.
Timeline:
The uniform -server problem has a finite set of vertices, any two distinct vertices at distance , and two servers. A request sequence is a list of vertices; each request must be covered by a server when it is served, and the cost is the number of server moves. This is paging with a cache of two pages: vertices are pages and the covered vertices are the cache.
A deterministic algorithm has a cost ; a randomized algorithm has an expected cost , averaged over its random choices. is -competitive if there is a constant such that for every request sequence and every deterministic algorithm (on-line or off-line),
Algorithm EATR. The servers start on the vertices and . The algorithm divides into phases; the first phase starts at the first request to a vertex other than and . Let be the set of vertices occupied by the servers at the end of the previous phase ( before the first phase). During a phase, a vertex is clean if it is not in and has not been requested during this phase; a vertex is stale if it is neither clean nor the most recently requested vertex . EATR keeps one server on and the other uniformly at random on the stale set. When a stale vertex is requested, the servers are placed on and and the phase ends; the next phase starts at the next request to a vertex not covered by a server. Requests between phases, and repeated requests to , move nothing.
For a phase, denotes the number of clean vertices requested in it. For a deterministic algorithm , and denote the numbers of 's servers that do not coincide with any of EATR's servers at the beginning and at the end of the phase. An algorithm is lazy if it moves no server on a request to a covered vertex and exactly one server on a request to an uncovered one.
With the optimal off-line cost of serving from the servers' starting position , there is a constant such that for all
The constant is left free; the factor is the paper's and is optimal.
The result. Theorem 3 settles the randomized competitive ratio of paging with two cache slots: combined with the paper's lower bound (Corollary 5, the subject of a companion mission), the optimal factor for is exactly , against for every deterministic algorithm. The general case was settled later by McGeoch and Sleator's -competitive partitioning algorithm, which is considerably more complicated.
Formalizing it. The result has been proved since 1991; no machine-checked proof of it is on the platform (a search for EATR, randomized paging and two-server results on 2026-09-26 found only deterministic -server theorems). The mission produces a formal model of a randomized on-line algorithm as a probability distribution over states evolving with the request sequence, a formal treatment of the phase decomposition and of the telescoping amortization that relates expected on-line cost to the optimal off-line cost, and a first strongly competitive randomized paging result on the platform, alongside the deterministic -server results already there.
The per-phase computations are short. The main difficulty is the global accounting. The adversary's cost in a phase is bounded only in amortized form, , where and compare the adversary's servers with EATR's at the phase boundaries; the bound becomes a statement about only after the and terms telescope across phases. This needs care with the requests that lie outside every phase (before the first phase, between phases, and in an unfinished last phase), during which the adversary may move. A further difficulty is that the off-line optimum ranges over arbitrary schedules, which may move several servers on one request, while the phase bound is proved for lazy on-line algorithms: the reduction from one to the other must be made explicit. Finally, the uniform law of the stale server is an invariant of a Markov chain on states that must be tracked through the whole phase.
The vertices are an abstract metric space with an enumeration , , and the hypothesis that distinct points are at distance ; the metric of is not used. The starting vertices are . is KServer.offlineCost of the published KServer model: the infimum of total movement over all schedules serving from . Comparing with this infimum covers every deterministic starting from EATR's position; a starting elsewhere differs by at most , which the constant absorbs. The constant is quantified before .
EATR is a PMF over states: a deterministic record (the set , whether a phase is in progress, the last requested vertex, the vertices requested in the phase) and the random position of the second server. Its expected cost is the expected number of server moves, summed over the requests. The paper fixes only that the second server is uniform on the stale set; when a clean request enlarges the stale set, the formalization moves one server by a fixed coupling that keeps the law uniform, and this choice is stated in the definition. A formalization that defines EATR's expected cost by the closed formula of the proof, or that restricts to complete phases, would make the goal a different statement; neither is done here. The pre-phase prefix and an unfinished last phase belong to and are covered by the constant.
Needed infrastructure: finite probability distributions (Mathlib's PMF), the published KServer model and its laziness theorem, and bookkeeping lemmas on the deterministic phase record. The phase record and the amortization argument are reusable for the marking algorithm of the companion mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.
Max -cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number ; the task is to choose subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.
The greedy algorithm covers at least a fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any , max -cover cannot be approximated in polynomial time within a ratio of , unless ." Together with the greedy bound, it makes the exact approximation threshold of max -cover.
Timeline:
An instance consists of points , a list of subsets of the points, and a number . Its value is the largest number of points covered by at most of the sets. Instances are written over a three-letter alphabet:
Following p. 648, a polynomial-time algorithm approximates max -cover within a ratio if on every input it outputs a number with
The algorithm need not name the sets. This is the non-constructive notion of approximation.
The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a -prover proof system for such a formula with clauses:
The max -cover instance of §5 attaches to every random string a copy of the explicit partition system. Its points are the vectors in with , so . Its partitions are labelled by the -bit strings, and each splits the points by the value of one coordinate. There are points in all. For each prover , question and answer , the set collects, for every on which receives , the th part of the partition of labelled by the values that gives to the distinguished variables of . The budget is , where is the number of questions a single prover can receive.
conditional on the two cited results below. The ratio is left free (any ), so the goal records the shape of the threshold and not a particular constant.
The result closes the approximability of max -cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:
Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:
The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.
The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly , a concave function of the number of sets used. Since the sets meet a random string times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about , which tends to . A further obstacle is that the reduction must run in polynomial time. The paper therefore takes and constant (unlike the set-cover reduction, where ), and the soundness bound must beat at a constant . The quantifier order ( large first, then large) is part of the difficulty.
A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.
CookPvsNP_defs (a published platform definition): one-tape Turing machines, , , polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the -fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most . This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max -cover is assumed.A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max -cover, and the approximation hypothesis is satisfiable for ratios up to .
Needed infrastructure, reusable beyond this mission:
Contributions to any of these, or to either cited theorem, are welcome.
A risk measure assigns to a random financial position a capital requirement : the amount of cash that must be added to to make it acceptable. The axiomatic theory of convex risk measures (Föllmer–Schied 2002; Frittelli–Rosazza Gianin 2002) treats this number as computed with no information beyond the model. In practice a regulator or a risk manager revises the requirement as information arrives, so the requirement becomes a random variable measurable with respect to the information available at the time of measurement. Detlefsen and Scandolo (SFB 649 Discussion Paper 2005-006; published in Finance and Stochastics 9(4), 2005, doi:10.1007/s00780-005-0159-6) develop this conditional theory: axioms, a robust representation, and a treatment of dynamic risk measurement.
The entropic risk measure is the standard example of a convex risk measure that is not coherent. It is the capital requirement of an agent with exponential utility , and its penalty function in the robust representation is the relative entropy (Föllmer–Schied, Stochastic Finance, Example 4.60, as cited by the paper). Section 5 of the paper carries this example to the conditional setting and shows that its penalty is a conditional relative entropy. The same identity appears in dynamic entropic risk measures, exponential-utility indifference pricing and recursive utility, where one-period conditional entropic measures are composed over time.
Fix a probability space and a sub--algebra , the information available at the time of measurement. is the space of essentially bounded random variables and its -measurable part. All equalities and inequalities between random variables hold -almost surely.
A conditional convex risk measure is a map that is translation invariant ( for ), monotone (), conditionally convex ( for , ), and satisfies .
The relevant probability models are
The essential supremum of a family of -valued random variables is the a.s. smallest random variable that dominates every member a.s.; the essential infimum is defined symmetrically. The minimal penalty of is
For a risk aversion , the conditional entropic risk measure is
the capital requirement for the acceptance set . For with density , the conditional relative entropy is
For every :
The first identity is representability with the minimal penalty as the penalty; the second identifies that penalty.
The result gives the conditional entropic risk measure an explicit dual description: the capital requirement is a worst case over conditional models, each penalized by its conditional relative entropy. This duality is what makes entropic risk measures computable in dynamic settings. Recursive compositions of over a filtration are time consistent, and their penalties add up by the chain rule for conditional relative entropy. Lemma 5.5 is also the conditional form of the Donsker–Varadhan (Gibbs) variational principle, which is used on its own in large deviations and in PAC-Bayesian bounds.
On status: the results are proved in the paper, and the unconditional versions are textbook material. Mathlib has unconditional Kullback–Leibler divergence, tilted measures, conditional Jensen's inequality and a -valued conditional expectation. As far as the platform search could establish, neither the conditional relative entropy nor the conditional Donsker–Varadhan formula nor any conditional risk measure has been formalized. This mission produces the first machine-checked conditional version, with allowed to be infinite.
In the unconditional case both sides of Lemma 5.5 are numbers, and the supremum is a supremum over reals. Conditionally, both sides are random variables. The supremum over the uncountable family indexed by must be taken in the essential sense, and a pointwise supremum is neither measurable nor meaningful. The conditional relative entropy can be on a set of positive probability. The integrand need not be integrable, so the usual conditional expectation of is not available for it, and the "" direction must reach an unbounded target through bounded test variables while controlling at the same time. The ess.sup in the goal ranges over measures, not random variables, and each is a conditional expectation under a different measure. These are identified with -a.s. objects through the condition on .
IsProbabilityMeasure P), and is m : MeasurableSpace Ω with hm : m ≤ mΩ. Payoffs are real functions with MemLp X ⊤ P. membership is StronglyMeasurable[m] plus MemLp ⊤. Every (in)equality between random variables is -a.e.P[·|m] and Q[·|m]. Bounded variables are integrable under every , so no junk value arises.Q.rnDeriv P. and are generalized conditional expectations, , built from Mathlib's -valued condLExp and valued in EReal. The negative parts are integrable, so never arises. In EReal, a real number minus is , which is how a model with infinite entropy drops out of the supremum.IsEssSup, IsEssInf) on a candidate -a.e. measurable EReal-valued function. The candidate must dominate every member a.s. and lie a.s. below every a.s. upper bound.P[φ * log φ | m] (which returns when is not integrable) or through a pointwise supremum would make the goal false or vacuous, and so would stating it for an abstract convex risk measure in place of . The formalization uses the extended-valued , the essential supremum, and the explicit .CondConvexRisk.Entropic and does not assume the general representation theorem (Theorem 3.2). The generalized conditional expectation and the conditional Donsker–Varadhan formula are reusable beyond risk measures. Contributions are welcome on the ess.sup API (existence, upward-directed families), on conditional monotone convergence for condExp, and on the conditional Jensen step for .Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about times larger than the optimum on an instance with points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.
Timeline of the lower bounds:
This mission formalizes Feige's theorem, the result that fixed as the threshold.
An instance consists of points and a list of subsets . A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some . It is written as a string: in unary, then each subset as its characteristic vector.
A deterministic polynomial-time algorithm approximates set cover within if, for some threshold and every coverable instance with points, the value it outputs satisfies , where is the size of a smallest cover.
is the class of languages that a deterministic one-tape Turing machine decides within steps, for some constant . Machines, and are those of the published definition CookPvsNP_defs.
The proof passes through three objects, each defined in the mission:
The statement fixes no constant beyond . The parameters , and of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.
The result. Combined with the greedy algorithm, Theorem 4.4 shows that is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The -prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.
Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any inapproximability of set cover is known. This mission contributes:
Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.NaorPartitionSystems relaxes "time linear in " to polynomial time and renders " polynomial in " as . Both relaxations weaken the hypothesis.Gradient descent needs a step size, and the classical choices each ask for something the user may not have. A constant step needs the Lipschitz constant of the gradient, which is rarely known and often pessimistic. Backtracking needs repeated function evaluations. The exact line search needs a one-dimensional minimization at every iteration. Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021, doi:10.1137/20M1329858) proposed a step size for the static linear-quadratic regulator (their rule (4.8), §4.3, p. 11). In §6.1 they point out that the same rule applies to any smooth unconstrained problem . The rule divides the squared gradient norm by the Hessian quadratic form along the gradient. It needs one Hessian–vector product per iteration and neither nor the strong convexity constant . In the paper's LQR experiment (§5, Figure 8, p. 13) the algorithm built on this step converges much faster than gradient descent with a constant step tuned at the first iterations.
The paper proves the method converges linearly for strongly convex functions (Theorem 6.1, p. 13). The proof takes one page (Appendix D.4, p. 19). This mission formalizes that theorem. It is the third mission of a series on this paper; the other two concern the LQR gradient method and gradient flow, and this one uses none of their control-theoretic objects.
Let be twice differentiable, with gradient and Hessian . Three constants describe it.
Let be the global minimizer of . The Hessian step size at a point is
the minimizer of the second-order Taylor model of along . The method (6.1) runs
from a starting point . The damped method with factor runs . For a quadratic the method (6.1) is steepest descent with exact line search.
Under the hypotheses above:
The constants are the paper's, stated exactly.
Theorem 6.1 gives a rate for a step size computed from local second-order information alone. Part 1 says that near the minimizer the method converges at least as fast as gradient descent with step , with no step-size parameter to tune. Part 2 gives convergence from every starting point, at the price of knowing a lower bound on for the damping. The same step appears in the paper's LQR method (rule (4.8)) and in gradient projection methods (p. 13, citing [37]), so the one-step inequalities are reusable beyond this theorem.
The result is proved in the paper. As of this writing none of it has a machine-checked proof. The formal work is the full development: the cubic Taylor bound from a Lipschitz second derivative on , the two one-step inequalities, and the inductions that give the rates.
The obvious argument for gradient descent uses the quadratic upper bound and a step no larger than . The Hessian step can be as large as , far outside that range, so the quadratic bound in the Euclidean norm gives no decrease. Two different replacements are needed. For the undamped method, the cubic Taylor error must be controlled along the whole trajectory, and condition (6.2) is imposed only on : the proof must show the gradient stays small enough at every later iterate. For the damped method, the upper bound must be measured in the local Hessian norm (D.1), which trades the step's size for the condition number .
On the Lean side, Mathlib has Taylor's theorem in one variable. The cubic bound for a function on with a Lipschitz Fréchet second derivative must be assembled from it or from the integral form along a segment. Mathlib has no ready-made link between strong convexity and a lower bound on the Hessian either.
The space is EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient f. The Hessian quadratic form is fderiv ℝ (fderiv ℝ f) x v v. Twice differentiability is differentiability of f and of fderiv ℝ f everywhere. The Lipschitz constant of the Hessian is in the operator norm of the bilinear map, not the Frobenius norm. Strong convexity is StrongConvexOn Set.univ μ f with 0 < μ; Mathlib's modulus is . and are real constants in the Lipschitz inequalities. The minimizer is a hypothesis ( for all ), not constructed.
Deviations from the page, all recorded in the items' Formalization Notes:
At a stationary point the step is ; Lean evaluates it to , so the method stays at the minimizer, and both rates remain true.
The iterates are those of the defined recursions (6.1) and its damped version. A statement about an arbitrary sequence satisfying a descent inequality would be a different, weaker theorem and does not discharge the goal. Condition (6.2) is imposed on only; a version assuming it at every iterate is also not the goal.
Contributions welcome: the multivariate cubic Taylor bound (reusable wherever a Lipschitz Hessian appears, e.g. in cubic regularization of Newton's method); the Hessian bounds from strong convexity and a Lipschitz gradient; and the inequality .
A buyer and a seller negotiate over a single indivisible good. Each knows how much the good is worth to them, but not how much it is worth to the other side. Whether the two will trade, and at what price, then depends on how each party shades its offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this situation as a one-shot game in which both parties submit sealed offers simultaneously, and characterised its Bayesian equilibria.
The model became the standard reference point for bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) showed that no mechanism can guarantee efficient trade in this setting, and that the equilibrium of the Chatterjee–Samuelson game with and uniform values attains the second-best efficiency bound. Later work on the -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the continuum of equilibria of exactly this game. The object of the present mission, a pair of linked differential equations, is the tool these papers use to construct and classify equilibria.
A seller has reservation price and a buyer has reservation price . Each knows their own value. The buyer's belief about is a probability measure with distribution function ; the seller's belief about is with distribution function . The subscript names the player who holds the belief, not the variable. Each belief is regular: , , and is strictly increasing and differentiable on the value interval, with density (respectively ).
Under the Bargaining Rule, the seller asks and the buyer offers simultaneously. If the good is sold at for a fixed ; otherwise nothing happens. Profits are for the seller and for the buyer on trade, and zero otherwise.
An offer strategy is a function (for the seller) or (for the buyer) from values to offers. Against , a buyer with value offering earns in expectation
and symmetrically . The pair is an equilibrium if maximises over all real offers for every buyer value , and maximises for every seller value .
A strategy is of class if its offers are bounded, it is nondecreasing, it is strictly increasing except where it sits at its lowest offer or its highest offer , and it is differentiable wherever its offer lies strictly between and . A class equilibrium is an equilibrium in which both strategies are of class .
In a class equilibrium, wherever the seller's strategy is strictly increasing around and the buyer value offers ,
and wherever the buyer's strategy is strictly increasing around and the seller value asks ,
The paper writes in (3a) and in (3b).
The milestones assume (respectively ), which the paper's formula for the offer density needs. The goal does not assume it.
Theorem 2 reduces the search for equilibria to the analysis of a pair of ordinary differential equations. Every explicit equilibrium in the paper and in the later -double-auction literature is found as a solution of (3a)–(3b) with suitable boundary conditions: the linear equilibrium for uniform beliefs (the paper's Example 1), the one-parameter families of Satterthwaite–Williams, and the non-linear equilibria of Leininger–Linhart–Radner. The equations also expose how the split parameter distributes bargaining power: at equation (3b) forces the seller to ask their own value, and at equation (3a) forces the buyer to bid theirs.
The result is proved in the paper. To the best of a search of the platform, no formalization of it or of the bargaining model exists. This mission produces a machine-checked version of the necessary conditions. Its definitions of beliefs, expected profits, equilibrium and class are also the basis for companion missions on the uniform linear equilibrium and its trade probability.
The paper's proof is four lines: differentiate the expected profit, set the derivative to zero, substitute. Three steps of that argument do not survive a careful reading.
First, the paper differentiates under an offer density that exists only if is strictly increasing and has a positive derivative. Class allows to be flat at its bounds, to jump between them, and to have zero derivative. The formal goal assumes none of this. It must handle the case , where the offer distribution has an infinite density at and the first-order condition becomes a one-sided argument.
Second, identifying with requires that no seller value outside a neighbourhood of makes the same offer. That is a global statement about , and it is where monotonicity on the whole interval and the "flat only at the bounds" clause of class enter.
Third, the first-order condition needs the equilibrium offer to be an interior maximiser of a function of that is differentiable there. The profit is an integral over the belief, and its differentiability at must be derived from the differentiability of at the single point and of . Neither nor is assumed continuous elsewhere.
Values, offers and are real numbers. Beliefs are probability measures on , with distribution function Mathlib's ProbabilityTheory.cdf. Expected profits are Bochner integrals over the opponent's value, not over an offer density. The two agree whenever the density exists, and the integral form needs none. Integrability is not assumed: for a class strategy and a regular belief supported on the value interval, the integrand is bounded and almost everywhere measurable. Ties () trade. Deviations range over all real offers. Strategies are arbitrary functions whose values outside the value interval play no role.
The derivative is deriv S y. The paper's inverses and are not introduced as functions. The matching value is a universally quantified variable with , so no junk value of an inverse can make an equation true or false. The equations are asserted only at values interior to an open subinterval on which is strictly increasing. A formalization that assumed the first-order condition, or restricted to strategies with everywhere, would be a different and weaker theorem.
A complete development needs: differentiation of parametric integrals of indicator type (the derivative of ), the change of variables from values to offers under a strictly increasing strategy, and Fermat's rule (IsLocalMax.hasDerivAt_eq_zero). The first two are reusable for auctions and other Bayesian games with monotone strategies. Proofs of the milestones, alternative proofs of the goal, and general lemmas about monotone strategies are welcome.
Variational inequalities and complementarity problems are the standard formulation of equilibrium in operations research and mathematical economics: traffic equilibria, spatial price equilibria, Nash equilibria of convex games, and the optimality conditions of constrained optimization all take this form. Many applications have two features that the classical theory does not cover. The feasible set of a player or a flow can depend on the current state (a quasi-variational inequality, as in generalized Nash games with shared constraints), and the response map can be set-valued (a subdifferential, or a best-response correspondence). D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the generalized quasi-variational inequality covering both, proved existence theorems for it, and derived existence for a new generalized implicit complementarity problem.
Timeline of the results this mission builds on:
Throughout, carries the Euclidean inner product and norm . A point-to-set mapping assigns to each a set . Given point-to-set mappings and , the problem asks for vectors with
A cone is a convex set containing and closed under nonnegative scaling. The dual cone of a set is . For a point-to-point map , a cone-valued map and a point-to-set map , the problem asks for with
A mapping is upper semicontinuous on a set at if for each open there is a neighbourhood of with for ; lower semicontinuous if for each open meeting , meets for all near in ; continuous if both. A set is contractible if some point and a continuous satisfy , . is the closed ball of radius about the origin, its boundary sphere. For point-to-set maps and , the coercivity function is
with . The map is strongly copositive with respect to at if and for some and , for all and . For and , .
Let be a closed cone with nonempty interior, continuous, , and a mapping with nonempty contractible compact values, upper semicontinuous on . If some satisfies for all , and is strongly copositive with respect to at , then for every
Theorem 4.2 gives existence for complementarity problems whose cone is translated by a state-dependent map and whose response map is set-valued. It contains existence for the implicit complementarity problem of Capuzzo-Dolcetta, Mosco and Pang () with strongly monotone data (Corollary 4.2 of the paper), and Saigal's generalized complementarity problem (). Theorems 3.2 and 4.1 are general-purpose existence tools for quasi-variational inequalities with set-valued maps; Theorem 3.2 reduces to the Fang–Peterson theorem when is constant, and Corollary 3.1 to the Hartman–Stampacchia theorem when in addition is single-valued.
All results of the paper are proved; none is open. To our knowledge none of them has been formalized: no proof assistant library contains quasi-variational inequalities with set-valued maps, and Mathlib has neither Kakutani's nor the Eilenberg–Montgomery fixed point theorem (nor Brouwer's). A formal proof of the goal therefore also produces a reusable library of set-valued existence theory.
The whole chain rests on Theorem 3.1, whose proof applies the Eilenberg–Montgomery fixed point theorem for upper semicontinuous maps with acyclic (here contractible) compact values; this in turn needs either singular homology or an approximation argument, neither of which is available in Mathlib. Replacing "contractible" by "convex" to use Kakutani's theorem would prove a strictly weaker theorem: the paper states contractible values deliberately. The second difficulty is that the fixed point only solves the problem on the truncation ; turning it into a solution over all of needs the boundary argument of Theorem 3.2, and for Theorem 4.2 the continuity of , which is where the solidity of is used. The obvious approach of applying Theorem 3.2 directly with fails because must be compact.
The space is EuclideanSpace ℝ (Fin n), so all norms and balls are Euclidean (not the sup norm of Fin n → ℝ). Point-to-set mappings are functions into Set; semicontinuity "on " is Mathlib's UpperHemicontinuousOn/LowerHemicontinuousOn with neighbourhoods relative to , and "on " is UpperHemicontinuous. Cones are PointedCone ℝ _ (convex, containing , as footnote 1 of the paper says). Balls are centred at the origin.
Conventions that the Lean statements make explicit:
A trivializing formalization is ruled out: the GQVI solution tests over all of , not over , and the GICP solution keeps both the dual-cone condition and the complementarity equation. Dropping any of these would turn the goal into a restatement of Theorem 3.1.
A complete development needs: an Eilenberg–Montgomery (or at least Kakutani plus an acyclicity argument) fixed point theorem for set-valued maps, Berge's maximum theorem, and basic facts on hemicontinuity of intersections and translates of set-valued maps. The fixed point theorems, the maximum theorem and the hemicontinuity lemmas are reusable far beyond this mission. Contributions of any of these as separate theorems are welcome.
The gradient projection method minimizes a continuously differentiable function over a closed convex set by alternating a gradient step with a projection back onto the set. It was proposed by Goldstein (1964) and by Levitin and Polyak (1966), and it is the basic step of many algorithms for bound constrained and linearly constrained optimization, including large-scale quadratic programming codes.
The classical convergence results either need a Lipschitz constant for the gradient to choose the step (Goldstein; Levitin–Polyak), or assume a bounded sequence of iterates and conclude only that limit points are stationary (Bertsekas, 1976, for the Armijo rule on a box; Dunn, 1981). Calamai and Moré (1987) introduced a general step-size rule that contains the Armijo procedure, and proved a convergence statement that needs no boundedness of the iterates: the projected gradients tend to zero. This statement is what later results on finite identification of the active constraints use as their hypothesis, so it is the natural entry point to the paper.
Let be a finite-dimensional real inner product space with norm , let be nonempty, closed and convex, and let be continuously differentiable on , with gradient taken with respect to the inner product. The problem is
A run of the gradient projection method is a pair of sequences , with , and , where . For fixed constants and , the steps satisfy the sufficient decrease condition
and the condition that the step is not too small: either , or for some at which sufficient decrease fails,
In Lean these objects are proj, projGrad and IsGradientProjectionRun in the namespace CalamaiMore.Convergence, together with the shared definitions tangentCone and IsStationaryPoint in CalamaiMore.Shared.
If, in addition, the steps are bounded, for some constant (3.2), is bounded below on , and is uniformly continuous on , then
No boundedness of is assumed, and no specific step rule beyond (2.1)–(2.3).
By Lemma 3.1, vanishes exactly at stationary points, so Theorem 3.2 says that the method approaches stationarity in a quantitative sense even when the iterates are unbounded. With Lemma 3.3 it gives that every limit point is stationary. For polyhedral it is the hypothesis of the paper's Theorem 4.1: any sequence with converging to a nondegenerate point identifies the active constraints in finitely many iterations, which is the basis of active-set methods that switch between gradient projection steps and subspace minimization.
The results are proved in the paper. To our knowledge they have no machine-checked proof. This mission produces a formal account of the gradient projection method with a general step rule, a reusable projected gradient and tangent cone on a general finite-dimensional inner product space, and the standard projection estimates of §2, which are also the starting point of the paper's other two main results.
The obvious argument fails at two places. First, the continuity of cannot be used: the map is not continuous, and can be bounded away from zero in every neighborhood of a stationary point, because the tangent cone changes discontinuously at the boundary of . So with stationary does not by itself force , and here the iterates need not converge at all. Second, the steps may tend to zero along a subsequence; the step rule gives information only through a trial step , at a point other than , and comparing the two projected steps is where the argument must work.
The space is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; is Mathlib's gradient f. "Continuously differentiable on " is ∀ x ∈ Ω, DifferentiableAt ℝ f x together with ContinuousOn (gradient f) Ω. Bounded below is BddBelow (f '' Ω), uniform continuity is UniformContinuousOn (gradient f) Ω. Sequences are ℕ → E indexed from ; a subsequence is an infinite K : Set ℕ with limits along atTop ⊓ 𝓟 K; a limit point is a MapClusterPt. The projection and the projected gradient are total functions through a nearest-point map that returns when no nearest point exists; every theorem assumes nonempty, closed and convex, and evaluates only at points of , where the nearest point exists and is unique. The step rule is a predicate on the pair of sequences, so the theorems cover every rule satisfying (2.1)–(2.3); the auxiliary condition , which the paper uses only to show that an admissible step exists, is not imposed.
The run predicate is satisfiable: for a constant , the constant sequence with is a run, so the goal is not vacuous. A formalization that states the goal for an arbitrary map in place of the projection, drops the bound , or replaces by proves a different theorem and is not accepted.
Contributions welcome: the projection estimates (reusable for any projection-based method), existence and uniqueness of the projected gradient, the characterization of stationarity, and the two limit theorems.