Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.
Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least . Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in .
Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most . Singh and Lau (STOC 2007) improved this to , which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.
Let be a finite simple graph with edge costs ; no sign or triangle inequality is assumed. Let be a forest on with no edge in common with . A set is an -tree if is a spanning tree of , and is the number of edges of at . Integer lower bounds are given on and integer upper bounds on . The minimum bounded degree connecting tree problem asks for a cheapest -tree with on and on ; with it is the spanning-tree problem.
The supernodes are the vertex sets of the components of , isolated vertices included, and is the family of unions of supernodes. For , and are the edges with both endpoints in , the edges with exactly one endpoint in , and . The linear relaxation LP-MBDCT minimizes subject to
MBDCT Algorithm2 (Figure 5 of the paper) repeats: if is a spanning tree, stop; otherwise take a basic optimal solution , delete the edges with , move one edge with (if any) into and lower and by one at its endpoints, and otherwise remove from and one vertex whose support degree is at most two.
For every well-formed instance whose LP is feasible, MBDCT Algorithm2
The statement fixes no constants beyond the paper's , and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.
In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with ); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value on the edges between the members of , and when a set is special); Lemma 5.6 (every set of keeps at least three tokens, exactly three only if it is special or ); and Lemma 5.1 (a basic solution has an edge with or a vertex of with support degree two).
The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the guarantee, which cannot be improved to unless P = NP, since a Hamiltonian path is the case . With lower bounds it also covers prescribed minimum degrees.
The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.
The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of , , , and along the run.
Vertices form a Fintype; edges are elements of Sym2 V with no loops, and , are finite sets of edges with acyclic and disjoint from . LP vectors are functions on Sym2 V that vanish off . Right-hand sides are computed in , degree bounds are integers, and the subtour rows range over nonempty (at the literal row would make the LP empty). A basic solution is a feasible that is the only vector on satisfying with equality every constraint tight at , including the tight rows . Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.
The paper's loose phrases are made explicit as follows.
Two trivializations are ruled out. Existence of a cheap tree with degrees in is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.
Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.
A G/GI/N queue has identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution of mean . In the Halfin–Whitt regime the number of servers grows while the traffic intensity approaches at rate ; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.
Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against is replaced by a convolution against the renewal function of . With exponential service the renewal function is , and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.
Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.
Let be a probability measure on with mean (the service-time law), its distribution function and its tail. The equilibrium distribution is
Let be the -fold convolution of (the law of the th renewal epoch ). The renewal measure is and the renewal function is , the expected number of renewals by time .
A path is càdlàg on if it is right continuous at every with finite left limits at every ; only its values on matter. Fix a càdlàg driving path (in the paper , (5.40)) and . Write and . The two equations are
All Stieltjes integrals are over the closed interval .
For every service law , every càdlàg and every :
and (5.41) has a càdlàg solution that is unique on among càdlàg paths.
The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process and whose only nonlinearity is the idle-server term . This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that , the solution of (5.41).
The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity ; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.
The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when may have an atom at , and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at . The converse direction, (5.41) (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in . The uniqueness of (5.41) is not a contraction argument either: the atom of at has mass , which may exceed , so a naive Picard estimate on fails.
negPart.BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below ); ChenWhitt93.Reflection.Basic (càdlàg paths on ). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.Random partitions of the positive integers are the common language of population genetics, Bayesian nonparametrics and the theory of coalescent processes. When a sample of genes, customers or particles is grouped into classes, the grouping is a partition, and in most models its law is exchangeable: it does not depend on the labels. The best-known example is the Ewens sampling formula of population genetics (Ewens 1972); Kingman's representation theory (Kingman 1978) describes all exchangeable random partitions of .
Pitman's two-parameter family of exchangeable partitions, the partitions (Pitman 1995; Pitman and Yor 1997), contains Ewens' family as and is the partition counterpart of the two-parameter Poisson–Dirichlet distribution. Theorem 12 of Pitman 1999 shows that two natural random operations act on this family in a dual way: merging blocks of an partition according to an independent exchangeable partition (coagulation) and splitting each block of an partition by independent exchangeable partitions (fragmentation) produce the same joint law of a fine and a coarse partition. The paper uses it to describe the Bolthausen–Sznitman coalescent (Bolthausen and Sznitman 1998).
Timeline. 1972: Ewens' sampling formula, the case . 1978: Kingman's correspondence between exchangeable partitions and random mass partitions. 1995: Pitman introduces exchangeable partition probability functions and the formula (15). 1997: Pitman and Yor study the two-parameter Poisson–Dirichlet law. 1999: this paper proves the coagulation–fragmentation duality (Theorem 12) and its sharper converse, by reduction to an identity between explicit formulas. The duality is treated again in Pitman's lecture notes Combinatorial Stochastic Processes (2006).
A partition of a set is a collection of disjoint nonempty blocks whose union is the set. Write for the partitions of and for those of ; the restriction of to keeps the nonempty sets . carries the -algebra generated by the . Writing lists the blocks in increasing order of least elements.
A random partition of is exchangeable with EPF if for every and every partition of ,
For and the EPF is
with factors of and cancelled before evaluation when or . An partition is an exchangeable random partition with EPF .
Coagulation (Definition 5): for and , the -coagulation of has blocks . is a -coagulation of if, given , it is the -coagulation of for an independent with EPF . Fragmentation (Definition 11): is a -fragmentation of if, given , restricted to the -th block of equals restricted to that block, for independent with EPF . In Lean these are coag, frag, pdEPF and IsEPFLaw in LambdaCoalescent.CoagFrag.Setting.
For , , , the following are equivalent: (i) is an partition and is a -coagulation of ; (ii) is an partition and is an -fragmentation of . Formally, with laws of EPFs :
for every measurable .
Theorem 12 identifies one law of a nested pair of exchangeable partitions from both ends. Read from (i) to (ii), it shows that coagulating an partition by an independent partition yields an partition; read backwards, that an partition fragmented by partitions yields an partition. Through Kingman's correspondence it gives Corollary 13 on Poisson–Dirichlet laws, and with it connects the two-parameter family with Ewens' family. In the paper it is the tool for describing the Bolthausen–Sznitman coalescent through Poisson–Dirichlet laws. The sharper form shows the parameter relations (64) are forced.
The theorem has been proved since 1999. What this mission adds is a machine-checked development: exchangeable random partitions of with their EPFs, the coagulation and fragmentation kernels, and the reduction of identities between laws on to identities between finite-dimensional formulas. None of these objects is in Mathlib, and no formalization of the duality is known.
The algebraic heart, the EPF identity, is a finite computation with rising factorials. The difficulty is measure-theoretic and combinatorial. A law on must be pinned down by its values on the cylinder events . Computing under the coagulation kernel requires that the blocks of meeting are exactly the first blocks in order of least elements, and that the induced partition of has law given by the EPF; under the fragmentation kernel it requires the independence of the and that the restriction of an exchangeable partition to an arbitrary finite set (not an initial segment ) is governed by the same EPF. The converse in Lemmas 34 and 35 needs the bookkeeping that the formula on refining pairs exhausts total mass. Lemma 9 is an existence theorem for a projective family of laws, which the paper cites rather than proves.
A partition of is an equivalence relation on Lean's (PInf := Setoid ℕ), a partition of one on Fin n; labels shift by one, which preserves the order of least elements, and block indices are 0-based. The -algebra on PInf is generated by the coordinates , equivalently by the . Coagulation is stated with (Definition 5's case ). The EPF is the cancelled form
equal to (15) for ; this is needed because at . Conditional laws "for all " are encoded as joint laws, and equalities of laws are stated on preimages of measurable sets, so no Measure.map of an unproved-measurable map appears. Fragmenting partitions are one sample of Measure.infinitePi (fun _ => κ). In the sharper form, is written as , since PAR allows .
Not formalized: the stick-breaking characterization (12)–(13) in Lemma 9, Corollary 13 and Kingman's correspondence, and the auxiliary fact "", which as printed fails at .
A formalization in which no measure satisfies IsEPFLaw (pdEPF α θ) would make Theorem 12 and Lemmas 34–35 vacuous; Lemma 9 rules this out and must be proved for the parameters used, not assumed.
Infrastructure needed: cylinder-set uniqueness on PInf, the law of the restriction of an exchangeable partition to a finite set, block enumeration by least elements, and rising-factorial algebra (ascPochhammer). The partition, EPF and kernel definitions are reusable for any work on exchangeable partitions, Chinese restaurant processes or -coalescents. Proofs of Lemma 9, of Lemmas 34–35 and of the EPF identity are each welcome as independent contributions.
Many problems in optimization and equilibrium modelling reduce to a system of nonsmooth equations with locally Lipschitz but not differentiable: reformulations of nonlinear complementarity problems, variational inequalities and Karush–Kuhn–Tucker systems through the function or piecewise smooth maps. Newton-type methods for such systems replace the Jacobian by a directional derivative or a generalized Jacobian and globalize with a line search on the residual .
Global convergence theory for these methods typically shows that every accumulation point of the iterates is a zero of (or a stationary point of ). That leaves open whether the whole sequence converges. L. Qi's 1993 paper in Mathematics of Operations Research (DOI 10.1287/moor.18.1.227) answers this with an attraction theorem: a zero with a nondegenerate directional derivative, once approached, captures the whole sequence of any descent method whose steps are controlled by the residual.
Timeline. Robinson (1987) introduced the B-derivative (as recounted on p. 229 of Qi's paper); Pang (1990, DOI 10.1287/moor.15.2.311) proposed the damped B-derivative Newton method and proved a global convergence theorem under strong conditions at the limit point; Han, Pang and Rangaraj (1992, DOI 10.1287/moor.17.3.586) gave two further globally convergent descent algorithms; Qi and Sun (1993, DOI 10.1007/BF01581275) developed the semismooth Newton method. Qi's 1993 §5 shows that, for convergence of the entire sequence to a zero, BD-regularity at that zero suffices for all three methods, without semismoothness.
Throughout, is locally Lipschitz and is the Euclidean norm. The directional derivative of at in direction is the one-sided limit
is directionally differentiable at if this limit exists for every , and B-differentiable at if moreover
is BD-regular at if it is directionally differentiable there and for every .
A descent direction method produces iterates with step sizes and directions , and is monotone in the residual:
A point is a limiting point of if some subsequence converges to it.
The damped Newton method (Algorithm 4.1) is the special case where solves and is chosen by the Armijo rule on .
Let be locally Lipschitz and B-differentiable, a descent direction method satisfying (5.1), and a limiting point of with and BD-regular at . If there are such that implies and
then
The result. Global convergence theorems for line-search methods usually stop at "every accumulation point is a zero". The attraction theorem upgrades that to convergence of the entire sequence whenever the zero is BD-regular, under assumptions that are checked locally and that hold for several algorithms at once. For the damped Newton method it removes the semismoothness assumption needed for the superlinear local theory, at the price of saying nothing about the rate. The same pattern (local error bound plus residual-controlled steps gives capture) recurs in the convergence analysis of Levenberg–Marquardt and projection-type methods.
Formalizing it. The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization needs the one-sided directional derivative and B-differentiability, the passage from BD-regularity to a uniform constant, and the trapping argument for sequences with cluster points. These pieces are reusable for any convergence proof of nonsmooth Newton-type methods.
The obvious argument says: near , steps are small because is small, so the iterates cannot leave. This fails as stated: a small residual at does not by itself prevent from being far from , and without a lower bound of in terms of the iterates could drift along a set where is small. The step that needs work is the error bound (5.5), which requires a uniform constant from the pointwise condition , valid in a whole neighbourhood of and not only along the directions the iterates happen to take. The set must also be chosen so that both its defining inequalities are preserved, which ties the radius to the residual through .
Points of are EuclideanSpace ℝ (Fin n); norms are 2-norms; is allowed. The directional derivative is the published one-sided NonsmoothNewton.Local.dirDeriv; every statement that evaluates it does so at a point where existence is assumed (BD-regularity, B-differentiability), so the junk value of an undefined limit never enters. "Limiting point" is a cluster point of the sequence, not its limit. Condition (5.2) is assumed only for iterates within of , as on the page.
Standing assumption and added hypotheses:
A trivializing formalization is ruled out: the goal does not assume that converges, that is bounded, that (5.2) holds globally, or that is semismooth; the hypotheses are jointly satisfiable (for , , , ).
Definitions needed: directional differentiability, B-differentiability, BD-regularity, and for Corollary 5.2 the norm function, the Armijo test (4.1) and runs of Algorithm 4.1. Contributions to the general theory of one-sided directional derivatives of locally Lipschitz maps (Lipschitz continuity and positive homogeneity of ) are welcome and will serve the companion missions of this series.
In a labor market where firms hire sets of workers and salaries are negotiated pair by pair, the natural stability notion is the core: an assignment of workers to firms, with salaries, that no firm and group of workers can improve upon by agreeing among themselves. Kelso and Crawford (Econometrica 50 (1982) 1483–1504) proved that the core is nonempty, and that an ascending salary-adjustment process reaches it, when every firm regards workers as gross substitutes (GS): raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. The condition later became central to the theory of matching with contracts, combinatorial auctions and Walrasian equilibrium with indivisible goods (Gul and Stacchetti, J. Econ. Theory 87 (1999); Hatfield and Milgrom, Amer. Econ. Rev. 95 (2005)).
The question this mission addresses is whether (GS) is needed at all. Section 6 of the paper answers it with a concrete market with two firms and three workers in which every other assumption of the paper holds, each firm's technology is even subadditive, and the core is empty.
There are workers and firms , both finite. Worker 's utility of working for firm at salary is ; firm produces with the set of workers , and its profit at the salary vector is
A set is demanded at if it maximizes . Each pair has a reservation salary .
An allocation assigns each worker to a firm with salary ; . It is individually rational if and for all , . A firm and a set of workers strictly improve upon it if some salaries give every strictly more utility than at the allocation and give firm strictly more profit than . A core allocation (definition D3 of the paper) is an individually rational allocation that no such coalition can strictly improve upon. When salaries vary continuously, the range over .
The example. Workers ; firms ; ; (equation (23)); and
Firm is firm with workers and interchanged. In Lean, noCoreMarket : Market (Fin 3) (Fin 2) is this market, techJ and techK are the two technologies, and Market.IsCore anySalary is D3 with real salaries.
The goal then follows by the symmetry of the example.
The paper's existence results (Theorems 1 and 2: the salary-adjustment process converges to a core allocation; a strict core allocation exists with continuous salaries) all assume (GS). This example shows that the assumption cannot simply be dropped, and that the weaker and more familiar condition of subadditivity does not replace it once there are three or more workers, although it does with two (p. 1500). It is the reason gross substitutes, rather than a convexity-like condition on technologies, became the standard hypothesis for existence of equilibrium with indivisibilities.
The result is proved in the paper by a short computation. It has not been machine-checked before: nothing of this paper was on Prove2Me before this series. The mission contributes a checked counterexample, a general efficiency lemma for core allocations with transferable utility (milestone 3), and the computational facts about firm that show (GS) fails. The paper's further remark that the example also has no competitive equilibrium relies on the core–equilibrium equivalence of p. 1487 and is not part of this mission.
This is mission 7 of a series on the same paper; missions 1–6 treat the salary-adjustment process (1), the continuous strict core (2), one-sided markets (3), the firm-optimal allocation (4), comparative statics (5) and the characterization of (GS) for identical workers (6). This mission does not depend on them.
The obstacle is the quantifier over all allocations with real salaries: emptiness of the core is a claim about infinitely many candidates, and checking finitely many salary vectors proves nothing. A direct attempt to find an improving coalition for each allocation by case analysis on salaries does not close, because which coalition improves depends on the salaries. The printed inequality (24) also carries a sign misprint ( in place of ), and copying it would break the contradiction.
0, 1, 2 : Fin 3; firms are 0, 1 : Fin 2. and .A trivializing formalization is ruled out: the core includes individual rationality and real-valued coalition salaries, the technologies are the printed tables, milestones 1, 2 and 4 have no hypotheses, and the hypotheses of milestones 3 and 5 are each satisfiable.
Contributions welcome: proofs of each milestone, and a statement and proof of the symmetry (workers , firms ) used to exclude the second efficient assignment.
Adding a firm changes the offers available to workers; removing a worker changes the pool from which firms hire. In markets with salary bargaining, those changes can alter both assignments and pay. Kelso and Crawford asked whether the direction of the change can nevertheless be predicted at the outcome selected by their salary-adjustment process. Their 1982 paper studies firms that may hire groups of workers whose joint product need not be the sum of individual products. Theorem 5 gives two comparative-statics conclusions for that setting: a new firm leaves each worker at least as well off, and retaining a worker leaves each firm at least as well off.
The result follows the paper's finite-termination and firm-optimality results for the salary-adjustment process. Its comparison is specific to the process equilibrium under the no-ties conditions of Section 5; the paper does not claim that every core allocation moves in the same direction. This mission is the fifth of seven on the paper. Mission 1 concerns termination and the discrete core, mission 2 the continuous strict core, mission 3 a one-sided market, mission 4 firm optimality, mission 6 returns to workers and gross substitutes, and mission 7 the example without a core. The statements here are drafted independently of the other missions' unpublished declarations. None of this paper's statements was previously available on Prove2Me when the series was planned.
A market has a finite set of workers and a finite, nonempty set of firms. Worker 's utility from employment at firm for salary is . Firm produces from a set and earns profit . Workers care about their own firm and salary; the firm's product may depend on the whole set it hires. Every worker–firm pair has a starting salary , and permitted salaries increase by a common unit : for .
Each round of the salary-adjustment process records permitted salaries, offers from firms, and one tentatively accepted offer for each worker who receives any. Firms choose profit-maximizing sets of workers at current permitted salaries and repeat offers that were not rejected. A worker keeps a favorite available offer. A rejected worker–firm offer causes that pair's permitted salary to rise by next round. The process stops when no offer is rejected. An allocation assigns each worker one firm and a salary at that firm; an outcome is the allocation read from a stopping round. The paper calls this a process equilibrium.
An allocation is in the discrete strict core when each worker's salary is permitted and meets the starting salary, each firm's profit is nonnegative, and no firm together with a set of workers can make every participant weakly better off and at least one strictly better off using permitted salaries. The weaker discrete core excludes coalitions that make everyone strictly better off. The paper assumes workers' utilities are continuous and strictly increasing in salary; marginal product (MP) makes hiring an additional worker at the starting salary weakly profitable; no free lunch (NFL) sets the product of the empty set to zero; and gross substitutes (GS) lets a firm keep workers whose salaries did not rise when other workers' salaries increase. Section 5 adds no-ties conditions (NTW) for workers and (NTF) for firms relative to discrete-core allocations. These assumptions and their domains come from Sections 2 and 5.
The preliminary target is the paper's Corollary to Theorem 4: under these assumptions, all legal runs that stop have the same outcome. A second target is the new-firm-on-the-block process claim stated in the proof of Theorem 5: starting from the original market's final salaries, its outcome is a firm-optimal discrete strict core allocation of the augmented market.
The goal is Theorem 5. Write , and for stopping outcomes in the original market, the market augmented by one firm, and the market without one named worker. The two conclusions are
The first comparison concerns every original worker's utility. The second concerns every original firm's profit. The augmented market retains the original firms' technologies, utilities and starting salaries, and the diminished market restricts those data to workers other than the removed one. All three markets use the same and satisfy the conditions of Theorem 4.
The theorem gives a direction for the effects of entry and worker exit even though assignments and salaries may both change and a firm's product may depend on its entire workforce. The comparisons are individual: every worker is covered by the entry conclusion and every firm by the exit conclusion. Process uniqueness makes these comparisons well-defined despite the choices of favorite sets and favorite offers that a legal run may make.
The mathematical claims were proved in the 1982 paper; the Lean statements in this mission are open proof obligations. The formal development would give reusable finite-market definitions of demand, gross substitutes, core blocking, and an explicit adjustment run. It would also make precise how outcomes in markets with different agent sets are compared. The Corollary and the new-firm process result are separate proof targets. Completing them would support the goal while keeping the paper's two comparative-statics conclusions together.
Firm entry changes which firm can make the best offer, and worker exit changes which subsets of workers a firm can hire profitably. A direct pointwise comparison of old and new assignments has no fixed correspondence: a worker may switch firms and a firm may hire a different group. Comparing arbitrary strict-core allocations is also insufficient, because Theorem 5 concerns the specific outcome chosen by the adjustment process. The formal proof must account for all legal tie choices and show that the identified stopping outcomes have the required utility and profit order. The paper's proof uses two modified processes; its take-my-marbles process raises the removed worker's salary to a value that need not belong to the discrete salary grid on which (GS) was assumed. This is a genuine modeling boundary for that intermediate statement.
Workers and firms are finite Lean types, with at least one firm. Salaries, utilities and products are real-valued; is positive. An allocation assigns every worker to a firm, as the paper's does. Option F represents firm entry: some j is an original firm and none is the entrant. The diminished worker set is the subtype of workers unequal to the removed worker. Gross substitutes is imposed only on the grid vectors each market permits, and (NTW) and (NTF) quantify over discrete-core allocations. Each theorem's assumptions explicitly include utility regularity, MP, NFL, GS, NTW and NTF wherever the paper says “the conditions of Theorem 4.” Section 5 allows starting salaries to vary independently of unemployment utility, so the reservation-salary equation from Section 2 is not imposed.
“The equilibrium” is represented by the outcome at any stopping round of any legal run; the Corollary states why this does not depend on those choices. “Converges in finite time” in the new-firm milestone means that each legal continuation has some stopping round. NFB's initial offers are fixed to the old firms' final offers and an offer from the new firm to every worker, a reading of the first round that NFB1 leaves implicit. The take-my-marbles convergence claim is not drafted because its off-grid starting salary requires a separate convention or a stronger GS assumption. These commitments exclude a vacuous market condition, a continuous-price substitution for the discrete theorem, and a comparison of unrelated markets. Contributions that establish the Corollary, the NFB claim, or the three-market comparison under these definitions are welcome; lemmas about demand and core allocation can be reused across the series.
Prediction with expert advice asks how a learner should combine the forecasts of a pool of prediction algorithms when nothing is assumed about the data: the instances and labels may be chosen by an adversary, and the learner's performance is compared with that of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) introduced the multiplicative-weights master algorithm WM for binary pool predictions and proved that its number of mistakes is at most logarithmic in the pool size plus a constant times the mistakes of the best pool member. The same multiplicative update now underlies boosting, online convex optimization and approximate solvers for linear programs and zero-sum games (Arora, Hazan, Kale 2012).
In many applications the pool members do not output a bit but a degree of confidence in , while the master must still commit to a binary decision. Section 5 of the paper treats exactly this setting with the algorithm WMG, and shows that WM's mistake bound survives unchanged.
A nonempty pool of prediction algorithms is run on a finite sequence of trials. In trial the pool member predicts , the master predicts , and then the binary label is revealed. The master keeps a non-negative weight per pool member, with positive initial weights. Write
and , the total weight after the last trial.
WMG with parameter predicts if and if ; at either prediction is allowed. A mistake is a trial with , and is the number of mistakes. An update step multiplies every weight by a factor
with . WMG executes an update step in every trial, or only in mistake trials; more generally (footnote 8 of the paper) in every mistake trial and possibly in others. Outside update steps the weights do not change. When the are binary, WMG coincides with WM.
For every run of WMG with , whatever the tie-breaking, the update criterion and the factors in (5.1), if then
The bound involves only the total weights, not the losses of individual pool members; Corollary 5.1 of the paper, which compares with the total absolute loss of each pool member, follows from it and from the lower bound in (5.1).
The paper gives two proofs of Theorem 5.1, one through each milestone; the second also uses Lemma 5.2, the potential lemma shared with the continuous master WMC, which is posed in the companion mission on WMC.
Theorem 5.1 says that the master's mistake count is controlled by how much total weight the pool loses, with the same constant as for binary pools. With equal initial weights it gives Corollary 5.1: WMG makes at most mistakes for every pool member , so pool members may report graded confidences at no cost in the master's guarantee. The same weight-potential argument is the template for the randomized master WMR of §6 and for later analyses of exponential weights.
The result is classical and proved in the paper. What this mission adds is a machine-checked statement and proof against the paper's own model: a relation that covers both update criteria, all tie-breaks at and the whole interval of admissible factors, rather than a single deterministic instance. No formalization of WMG or of Theorem 5.1 is known; the platform's existing weighted-majority results (Hazan's textbook version) concern binary experts, unit initial weights and a fixed update factor.
The obvious argument, copied from WM, tracks the weight of members predicting and the weight of members predicting . With predictions in a member supports both outcomes, and the update factor is only constrained to an interval, so the two-bucket bookkeeping must be redone for fractional contributions. The factor's upper bound is affine in , while the natural exponential factor is convex; the argument must use the right one of the two bounds of (5.1). A further subtlety is the case : a factor may be , the total weight can vanish, and both the logarithmic bound and the weighted average degenerate.
Fin n with , and the trials are Fin T, all trials of the sequence; weights are w : ℕ → Fin n → ℝ, with w 0 the initial and w T the final weights.Real.rpow (so ).Real.log is used.Real.log 0 = 0 would turn the paper's vacuous bound into the false claim ; with it, no Lean junk value enters the statement.A complete development needs only finite sums, real logarithms and real powers from Mathlib. Proofs of either milestone, of the existence of a run for every input (using Lemma 5.1, ), and of Corollary 5.1 on top of the goal are welcome.
The Shapley value (Shapley 1953) is the most widely used single-valued solution of cooperative games with transferable utility. It is usually justified axiomatically, from cooperative principles. A recurring question in game theory, sometimes called the Nash program, asks whether cooperative solution concepts can also be recovered from the strategic behaviour of players in a non-cooperative game.
Section 6 of Monderer and Shapley, Potential Games (Games and Economic Behavior 14, 1996), gives such a recovery through the notion of a potential game, the central object of that paper. With every solution , vector of outside options and TU game it associates a simple non-cooperative participation game, in which each player decides whether to join. The Shapley value is then characterised, among efficient solutions, as exactly the solution for which every such participation game is a potential game. The characterisation rests on the potential of a TU game introduced by Hart and Mas-Colell (1989), whose marginal contributions are the Shapley value; Monderer and Shapley connect that cooperative potential to the strategic one of their paper.
Let be a finite set of players.
A game in strategic form has strategy sets and payoff functions on . Writing for the profile with player 's strategy replaced by , a function is an exact potential if
for every , every and all (condition (2.2) with unit weights). A game with an exact potential is a potential game.
For a coalition , is the space of TU games on : real functions on the subsets of with . A solution assigns to every a payoff vector . It is efficient if for every and every . For , is its restriction to the subsets of . The Shapley value of is
Given a solution , a vector and , the participation game has player set and strategy sets . Player either stays out (0) and receives , or participates (1). With the set of participants at the profile ,
For , is the profile in which exactly the members of participate.
In Lean these are IsPotential, IsPotentialGame, Solution, IsEfficient, shapleyOn, joiners (), profileOf () and participationPayoff, all in the namespace MondererShapley.Participation.
For every efficient solution , every and every ,
An efficient is the Shapley value on all of iff is a potential game for every .
Theorem 6.1 is a local characterisation: for a single game it identifies the Shapley value of all subgames of through a property of one non-cooperative game, for any outside options . Theorem 6.2 turns it into a global axiomatisation of the Shapley value among efficient solutions, with "every participation game has a potential" in place of the usual symmetry, null-player and additivity axioms. It links the cooperative potential of Hart and Mas-Colell to the strategic potentials of Monderer and Shapley, and through the latter to the existence of pure equilibria and the convergence of improvement dynamics in the participation games.
Both theorems are proved in the paper, on the basis of Hart and Mas-Colell's Theorem A. To the curators' knowledge no machine-checked proof exists: neither the Hart–Mas-Colell potential nor its identification with the Shapley value of subgames is formalized on Prove2Me or in Mathlib. A complete development therefore formalizes the paper's reduction (milestones 1–3) and, as its substantial part, the Hart–Mas-Colell characterisation (milestone 4), which is reusable for any later work on cooperative potentials, consistency and the Shapley value.
Milestones 1–3 are bookkeeping on profiles in ; the obstacle is the identification of the potential of a game on with a function of coalitions, which is a translation between two indexings rather than an idea. The substance is milestone 4, which is Hart and Mas-Colell's Theorem A specialised to the subgames . The condition (6.3) speaks of marginal differences of an unknown function on coalitions, while the Shapley value is a closed weighted sum over subsets of whose weights depend on ; relating the two requires a genuine combinatorial identity over the subset lattice of every coalition, in both directions, and efficiency of on every subgame is used essentially. Unfolding the definitions does not suffice for either direction.
ι with decidable equality; the strategy set is Bool (false = 0, true = 1). is Function.update ε i x.Finset ι; a TU game is w : Finset ι → ℝ, with "" encoded as w ∅ = 0 and only the values on subsets of meant. A solution is ψ : Finset ι → (Finset ι → ℝ) → ι → ℝ, ψ S w standing for ; only the coordinates are read. This admits solutions that look at values of w outside , so the Lean statements cover every solution of the paper and more; " is the Shapley value on " is ∀ S, ∀ i ∈ S, ψ S v i = shapleyOn S v i.shapleyOn is supplied: the paper uses the Shapley value without defining it. Its weights use , the size of the subgame's player set.v ∅ = 0 is kept as the meaning of (without it, efficiency does not constrain ψ S v); and the potential is an exact potential on all of , not only on profiles of a special form.The probability that a sum of independent random variables exceeds a large level is a central quantity in large deviation theory. It appears, for example, when relating tail assumptions on individual summands to the tail of their sum. For summands with light (exponentially decaying) tails, exponential bounds are often effective. For heavier tails, a large value of the sum can instead be produced by one large summand. Nagaev's survey studies bounds that make the contribution of such summands explicit.
S. V. Nagaev's survey Large deviations of sums of independent random variables, Ann. Probab. 7 (1979) collects upper bounds of this type. Its best-known result, the Fuk–Nagaev inequality (Theorem 1.3, p. 749), bounds from above by plus an explicit term built from truncated moments. Upper bounds alone do not show that the one-summand term is necessary. At the end of §1 (pp. 758–759) the paper gives a complementary lower bound that needs neither identical distributions nor regular variation of the tails, only centred summands with finite variances. This mission formalizes that lower bound and the steps of its proof.
Timeline. Fuk and Nagaev (1971) proved truncation inequalities of this kind; the survey refers to that paper for the proofs of its Theorems 1.1 and 1.2 (p. 752). A. V. Nagaev (1969) obtained the asymptotics of Theorem 1.9 (p. 753) for identically distributed, centred summands with tails , , slowly varying; in the range where one summand dominates, the survey's own argument gives , display (1.46), p. 756. The lower bound treated here (1979, p. 759) drops both the identical-distribution and the regular-variation hypotheses in exchange for explicit constants (, and in place of ).
Let be a probability space and independent real random variables on it. The paper writes
Throughout, is the level (p. 747). For an index , the sum without the -th summand is
and the one-big-summand probability is
the probability that the sum reaches while is the only summand that does.
In the Lean development these are S n X, Sj n X j, Bn2 P X and Pj P X x j, in the namespace NagaevLD.LowerBound.
Assume for every and . Then for
The result. Set beside the Fuk–Nagaev upper bound, the lower bound shows that in the range the probability is at least a fixed fraction of a one-summand term, , for any centred summands with finite variances. It is valid for every and every family of independent, centred, square-integrable summands, with no asymptotic regime and no tail regularity. It is a non-asymptotic counterpart of the asymptotics for regularly varying tails, and it indicates that the term in upper bounds of Fuk–Nagaev type cannot be removed.
Formalizing it. The result is proved in the 1979 paper; the local Prove2Me catalogue search found no exact formal statement of this bound. A formal proof would produce a reusable lower bound for tails of sums of independent variables and the decomposition (1.57) into one-big-summand events, which applies to any family of real random variables.
The individual steps are short. The step that needs care is the bound on : it requires the event to be independent of the event , which is generated by the other summands. Deriving this from mutual independence of means grouping the summands into and its complement and passing to a function of the complementary block. The first Chebyshev bound similarly needs the variance of to equal , again by independence of a sub-family. A naive union bound for one alone does not give the sum over : the decomposition into the disjoint events of (1.57) is what makes the sum appear.
X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); the paper's are X 0, …, X (n-1). Probabilities are P.real of sets, with , and exactly as printed.MemLp (X i) 2 P). Mathlib's variance returns for a variable that is not square integrable, so without this hypothesis could be while the summands have infinite variance, and the goal would be false. is stated as .The Nelder–Mead simplex method (Nelder and Mead, 1965) is a derivative-free method for unconstrained minimization. It keeps a simplex of points in and replaces the worst vertex by a reflected, expanded or contracted trial point, using only comparisons of function values. It is one of the most widely used methods in practice, available in standard numerical libraries and scientific software, and it is also known for having very little supporting theory. McKinnon (1998) gave a strictly convex function in dimension 2 on which the method converges to a nonstationary point.
Lagarias, Reeds, Wright and Wright (1998) gave the first convergence results for the method as originally stated. In dimension 1 they proved that, for a strictly convex function with bounded level sets, both endpoints of the Nelder–Mead interval converge to the minimizer when (their Theorem 4.1). For the standard reflection coefficient they proved more: the convergence is eventually M-step linear, with a number of steps that depends only on the expansion and contraction coefficients (their Theorem 4.2). This mission formalizes that rate result and the move-sequence lemmas it rests on.
Let . A one-dimensional simplex is a pair of vertices ordered so that : is the best and the worst vertex. The method has four coefficients satisfying
This mission fixes , so (2.1) becomes , , . The trial points are
With , , and so on, one iteration is:
A shrink replaces by . The worst vertex is discarded and the accepted point joins ; it becomes the best vertex exactly when . Iterating from a nondegenerate initial pair () gives the run , and . A contraction means an outside or inside contraction.
Under each move multiplies the diameter by a fixed factor: for a reflection, for an expansion and for either contraction. The paper's bracketing index (its Lemma 4.2) is the first iteration with . Two integers control the move sequences after :
For all and there is an integer such that for every , every strictly convex with bounded level sets and every nondegenerate ordered , the index exists and
The goal fixes no value of ; the paper's proof gives one, but any depending only on and proves the theorem.
Theorem 4.2 is a rate statement for a method whose global behaviour is mostly unexplained. It shows that in dimension 1 with the method behaves like a bracketing line search: once the minimizer is bracketed, the interval shrinks geometrically, and the number of iterations per halving is bounded independently of and of the starting interval. With the standard coefficients , the value of constructed in the paper's proof is . The intermediate lemmas describe which move sequences the method can produce after the minimizer is bracketed.
The paper's results are proved; to our knowledge none of them has a machine-checked proof. This mission produces a formal model of the one-dimensional method with the paper's tie-breaking rules, and formal statements of the rate theorem and its supporting lemmas. Proving them is the remaining work, including the one-dimensional bracketing and proximity results of the paper's §4.2, which the proofs use and which are posed as a separate mission of this series.
The rate does not follow from a per-iteration bound: a reflection keeps the diameter and an expansion multiplies it by , so the diameter can grow for several consecutive iterations. A contraction-only argument fails for this reason. The theorem needs a bound on how long the method can avoid contracting and on how much expansion can happen between two contractions. Both bounds come from strict convexity applied along the line through the current interval, together with the location of the minimizer relative to the vertices (the proximity property of §4.2), and they must hold uniformly in . Making the constants uniform, so that and depend only on and , is the delicate part. Before no such control holds, which is why the theorem only speaks about .
The state is an ordered pair p : ℝ × ℝ with p.1 the best vertex and p.2 the worst vertex ; run f 1 χ γ σ p0 k is , and moveAt f χ γ σ p0 k is the type of iteration . The coefficient is substituted into the algorithm. The ordering rule is the paper's insertion rule (new point first iff , ties to the higher index); the printed formula contradicts the paper's own example on p. 118 and is read as its words describe. The expansion step accepts the better of and , the outside contraction is accepted on , the inside contraction on .
Standing assumptions carried by every statement: (2.1) with ; strictly convex on (StrictConvexOn ℝ Set.univ f); bounded level sets ( bounded for every ); and nondegenerate and ordered. Corollary 4.1 prints only ; the remaining conditions of (2.1) are the section's standing assumptions. is the natural-number ceiling ; is computed by a bounded search over , which loses nothing for . The uniformity of in Theorem 4.2 and of in Lemma 4.8 is encoded by quantifier order: they are chosen after and before , , .
The goal's conclusion includes the existence of the bracketing index (the paper's Lemma 4.2), so the halving claim cannot hold vacuously for a run that is never bracketed; a statement that lets depend on or is a different and much weaker theorem and is ruled out by the quantifier order.
A complete development needs: the one-dimensional facts about strictly convex functions (the paper's Lemma 4.1), the absence of shrink steps under strict convexity (Lemma 3.5 for ), the bracketing and proximity lemmas of §4.2, and the move-sequence and diameter-product arguments of §4.3. The model of the one-dimensional method and the convexity lemmas are reusable for the series' first mission (convergence of both endpoints). Proofs of individual milestones, and of the §4.2 lemmas as local results, are welcome.
Improve deterministic integer 3SUM to time in the foundation mission’s word-RAM model.
The existing Corollary 26 routine admits the tighter bound . Keep and change the grouping parameter to , implemented using the integer root of of order . Balancing the instance costs and scans gives an Exact Triangle saving of , and the verified 3SUM reduction gives time.
The supporting theorem establishes every rational exponent , including . This changes the algorithm’s grouping parameter and improves the earlier cutoff . All other model definitions and the shared reduction lemmas are reused.
Prove deterministic time for 3SUM on polynomially bounded integers, using the same word-RAM model and definitions as the foundation mission.
The existing uniform Exact Triangle bound has saving . The verified 3SUM reduction yields time, so every fixed rational exponent above is attainable, including . This mission sharpens the bound extracted from the existing algorithm.
The supporting theorem covers all rational ; it does not assert an exact bound. The proof reuses the shared, proved APSP and 3SUM lemmas from Anthropic’s formalization.
Conditional value-at-risk (CVaR) is the expected loss in the worst fraction of outcomes. Rockafellar and Uryasev showed that, for a finite set of scenarios, minimizing CVaR is a linear program whenever the loss is linear in the decision (Rockafellar–Uryasev 2000; 2002). That linear program needs the scenario probabilities, and in practice they are estimates. Zhu and Fukushima (2009) replace the single distribution by a set of distributions and minimize the worst-case CVaR over that set. The resulting problem, (16)–(20) below, contains a maximization over distributions inside a constraint, which no standard solver accepts directly.
This mission treats the first of the two cases the paper works out explicitly: the scenario probabilities are only known to lie in a box around a nominal distribution. Proposition 2 of the paper shows that the worst-case problem is then equivalent to a single problem, (24)–(30), with finitely many explicit constraints. The tool is linear programming duality applied to the inner maximization.
A decision is chosen from a set . The random vector takes one of values , and is the loss of decision in outcome . A distribution over the scenarios is a vector . Vectors are compared componentwise, is the all-ones vector, and is the confidence level.
The box uncertainty set (21) is built from a nominal distribution and bounds :
Problem (16)–(20) minimizes over subject to
By Theorem 2 of the paper its optimal value is the minimum of the worst-case CVaR over .
For fixed , the worst case over the box involves the linear program (22) and its dual (23):
Problem (24)–(30) minimizes over subject to ,
and the same constraints , . A point solves a problem when it is feasible and no feasible point has a smaller .
and both maxima are attained.
Proposition 2 makes worst-case CVaR minimization under box uncertainty computable with standard software. When is linear in and is a polyhedron, (24)–(30) is a linear program whose size grows only linearly in , and when is convex in and is convex it is a convex program. The robust portfolio models of §3 of the paper rest on this reformulation. Setting recovers the Rockafellar–Uryasev linear program (Remark 2 of the paper).
Proposition 2 is proved in the paper. As far as is known, neither it nor the duality pair (22)–(23) has a machine-checked proof; this mission would supply one. The development also exercises LP duality for a specific bounded-variable program, one with a single equality constraint, in a form that can be reused by other robust-optimization reformulations over boxes.
The obvious argument says "replace the max by its dual". Two steps need care. First, the inner maximum is over a polytope that may be empty, and the substitution of (18) by (26)–(28) is correct only when the box is nonempty; it must be shown that an optimal solution of either problem forces the box to be nonempty. Second, the equivalence is a statement about optimal solutions, not feasible ones, so both directions need the comparison of objective values over all feasible points of the other problem. The printed proof assumes in each direction that some optimal solution with a smaller objective exists, where only a feasible one is available; the argument must be run with feasible points. Strong duality for (22)–(23) is a genuine LP duality theorem: Mathlib does not provide it in this form, and it must be derived from a general duality or Farkas-type result.
Vectors are Fin S → ℝ and Fin n → ℝ, compared pointwise, with zero-based indices. Dot products are ⬝ᵥ, and is ∑ k, η k. Points of the three problems are structures (Var16, Var24, Dual23) with fields named as in the paper. The factor is (1 - β)⁻¹, and every theorem assumes .
Committed readings:
IsMinOn). Feasibility alone would make the proposition trivial and is ruled out.Needed infrastructure: LP strong duality for the pair (22)–(23), derivable from Mathlib's Farkas lemma or from LP duality theorems already on the platform; finite sums and dot products. Proofs of the milestones, of the goal from the milestones, and of a general bounded-variable LP duality lemma are all welcome.
Not in scope: the ellipsoidal case (31)–(40), Remark 2, and the portfolio instances of §3.
The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an -dimensional state space.
Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class that contains the usual heuristics. This mission formalizes that section: the reduced state space , the policy class , and Claim 1, which says that states outside are transient.
Fix the lead time . The state is the -vector : is the stock on hand after this period's delivery, and () is the order that arrives periods later, so is the most recent order. Given the state , an order and a demand , the next state is
Demands in successive periods are independent with a common law on .
The pipeline partial sums are for and ; is the inventory position and the most recent order. A level vector is with . For a level vector ,
and is the set of stationary policies (an order in each state ) with for and for and . The vector base-stock policy with parameter is
equation (5) of the paper with a general in place of Morton's . Under a stationary policy , from an initial state and along a demand path , the state process is , with order and demand . In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.
For a level vector , a policy , i.i.d. demands with law on and , and any initial state , almost surely
The paper's word is "transient"; the statement above says that every state outside , indeed the whole complement, is visited only finitely often.
A further item records the paper's remark that and are increasing in .
Claim 1 lets the dynamic program be solved on the compact set with policies restricted to , which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since contains the vector base-stock policies and, for large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.
The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of . Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.
The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside the policy orders nothing, so the process can only reach through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with fixed forever) and holds only almost surely, from independence and . The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.
Fin L → ℝ with in the goal; theorems quantify over nonnegative states. The vector is Fin.snoc x z; takes a natural-number index and vanishes at , so .Fin (L+1) → ℝ, antitone with nonnegative last entry. constrains ; constrains for .Measure.infinitePi (fun _ : ℕ => D). The hypothesis is added to the paper's assumptions; without it the claim is false.A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.
The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an -dimensional vector, and no simple policy is optimal.
Its structure has a long history:
Time is discrete. In each period the order due arrives, a new order is placed, demand occurs, and a holding or penalty cost is charged. The lead time is an integer. The original state records on-hand inventory followed by the orders in transit. Demands are independent with a common law . The costs are linear and stationary: unit procurement cost , unit holding cost , unit lost-sales penalty , and discount factor .
The transformed state is the vector of partial sums , , with the convention . It ranges over the cone
The transformed order is . With the all-ones vector, the state moves to
The one-period cost is on , where is the on-hand stock, and . With periods to go, the optimal cost functions are
A function is submodular on a set if for all , with the componentwise maximum and minimum. A function is L♮-convex if is submodular on . A function on is L♮-convex if is submodular in over , .
For every number of periods to go ,
The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.
The result. L♮-convexity of implies that is submodular and convex in the transformed state. L♮-convexity of yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order is nonincreasing in and changes by at most when every component of increases by . These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:
The obvious argument works with ordinary convexity and submodularity in the original state . It stalls: the lost-sales transition is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in . The paper's structure appears only in the partial sums . Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over (Lemma 2). Proving plain submodularity of on therefore does not close the induction.
A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.
A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of , and these come from the model rather than from the definitions.
Fin L → ℝ, indexed as in the paper. A helper returns for and at . A function is encoded on Fin (L+1) → ℝ with last. The objective of (4) is encoded on Fin (L+2) → ℝ with coordinates . The order is componentwise.DiscreteConvex.LConvexFunctions.*) works on with values in , a different domain and definition, and is not reused.Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection and risk-averse optimization: for a confidence level it is, roughly, the expected loss in the worst fraction of outcomes. Its practical appeal comes from the representation of Rockafellar and Uryasev (2000, 2002), which writes CVaR as the minimum over a scalar threshold of a convex function, so that minimizing CVaR over decisions becomes a single convex (often linear) program.
That representation presupposes that the distribution of the uncertain data is known exactly. In practice the scenario probabilities are estimated, and decisions that are optimal for the estimate can perform poorly under a nearby distribution. Zhu and Fukushima (Oper. Res. 57(5), 2009) study the worst-case CVaR: the largest CVaR over a set of distributions that the decision maker considers plausible. For a finite scenario model they show (Theorem 2) that when the plausible set of probability vectors is compact and convex, the worst-case CVaR again has a min–max representation in the threshold . This is what makes worst-case CVaR minimization tractable: under box uncertainty it becomes a linear program and under ellipsoidal uncertainty a second-order cone program (§2.2.1–2.2.2 of the paper).
A decision incurs the loss , where is random. In the discrete model takes the finitely many values , the scenarios, with probabilities , where and . Fix a confidence level and write . The Rockafellar–Uryasev function for the distribution is
and the CVaR of the loss at under is
The distribution is not known; it is only known to lie in an ambiguity set of probability vectors. The worst-case CVaR at is
In the Lean development these objects are WorstCaseCVaR.Discrete.G, cvar and wcvar, with the scenarios given as ys : Fin S → (Fin m → ℝ) and as a set P of vectors Fin S → ℝ.
If is a nonempty compact convex set of probability vectors, then for each
with the inner maximum attained for every and the outer minimum attained at some . The statement fixes no constants and no particular ambiguity set.
Theorem 2 converts a supremum over distributions of a minimum over thresholds into a minimum over thresholds of a worst case of a function that is affine in . Minimizing over decisions is therefore the single minimization problem (16)–(20) of the paper in the variables , whose only nonstandard constraint is . For box and ellipsoidal ambiguity sets that constraint is dualized into linear or conic constraints, which gives the robust portfolio models of §§2.2.1–3 of the paper. The same exchange of and underlies many later distributionally robust CVaR models.
The result is proved in the paper (appendix, p. 1167) and is not open. The mission produces a machine-checked proof of it, which to our knowledge does not exist. Mathlib contains Sion's minimax theorem (Sion.exists_isSaddlePointOn), which covers Lemma 1; what is missing is the CVaR-specific part: the convexity of in , the reduction of the threshold to a compact interval uniform over , and the passage from the compact interval back to all of .
The obvious approach applies a minimax theorem directly to on . That fails because is not compact, and minimax equalities on a noncompact factor can fail; the threshold must first be confined to a bounded interval, and the interval must work for every simultaneously. After the exchange on the interval, the minimum over the interval has to be identified with the infimum over all of , which needs the min-max inequality on the unrestricted line. A second subtlety is attainment: every "min" and "max" in the statement is a claim that an extremum exists, and in the real-valued formalization each must be exhibited rather than read off from a supremum.
Conventions committed to in the Lean statements:
Fin S; probability vectors are elements of stdSimplex ℝ (Fin S).No vacuous version of the goal is admissible: the ambiguity set must be nonempty and consist of probability vectors, and the minimum over must be witnessed.
The development needs only finite sums, convexity on and on the simplex, compactness of and of closed intervals, and Mathlib's minimax theorem. The reduction to a bounded interval and the min-max inequality are reusable for other finite-scenario CVaR results. Proofs of any milestone are welcome, as are alternative proofs of the goal that avoid the interval reduction.
Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection, insurance and stochastic programming. Its practical appeal comes from a variational formula of Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002): CVaR at level is the minimum over a scalar of a convex function, so that minimizing CVaR over decisions becomes a single convex program, a linear program when the distribution is given by scenarios.
The formula needs the distribution of the random returns, and in practice that distribution is estimated and uncertain. Zhu and Fukushima (Oper. Res. 57(5), 2009) introduce the worst-case CVaR: the supremum of CVaR over a set of candidate distributions. They show it is again a coherent risk measure and that, for several natural choices of , minimizing it remains a tractable convex program. This mission formalizes the first of these results, for the set of all mixtures of finitely many given distributions, a model used in robust statistics and in finance to describe returns under several market regimes.
A decision and a random vector determine a loss . A confidence level satisfies (in applications ). Write .
For a probability distribution of under which is integrable, the Rockafellar–Uryasev function is
and CVaR is its minimum over :
Fix likelihood distributions on and let be the probability simplex. The ambiguity set is the set of mixtures
and the worst-case CVaR of is
Write for the function (1) with , with , and for the function (1) of the mixture .
For every with integrable under every ,
with the minimum attained. The supremum over infinitely many distributions on the left becomes a minimum of the pointwise maximum of functions on the right.
The milestones follow the paper's appendix proof (pp. 1166–1167) in order:
An additional item states Corollary 1: minimizes over exactly when minimizes over and minimizes .
The result. Theorem 1 makes worst-case CVaR under mixture uncertainty no harder to optimize than ordinary CVaR. Since each is jointly convex in when is convex in , is convex, and Corollary 1 turns robust CVaR minimization into one convex program in ; with sampled scenarios it is a linear program (the paper's (10)–(15)). It is the starting point for the paper's robust portfolio models (§3), whose ambiguity sets are mixtures of a few estimated return distributions.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof contributes a measure-theoretic treatment of the Rockafellar–Uryasev function for arbitrary distributions (the paper argues with densities and appeals to Remark 1 for the general case), a reusable statement that the minimizer set of is a compact interval, and a worked instance of the minimax theorem in Mathlib (Sion) applied to a problem with an unbounded variable.
The obvious argument is to exchange and in , since the function is convex in and affine in . Minimax theorems for this exchange need compactness of one of the two sets, and the variable ranges over all of . The step that has to be supplied is a localization: all minimizers in , for every at once, lie in one compact interval determined by the minimizer sets of the components. This in turn requires knowing that each has a nonempty bounded minimizer set, which uses and integrability of the loss: at the minimizer set can be a half-line and the localization fails. A second point is attainment: the outer supremum over is a maximum only because the inner minimum depends continuously on .
Fin m → ℝ (not densities); Remark 1 of the paper extends all results to general distributions, and a density is a special case. Decisions are Fin n → ℝ, the loss is f : (Fin n → ℝ) → (Fin m → ℝ) → ℝ, and the likelihood distributions are P : Fin l → Measure (Fin m → ℝ) with indices zero-based and [NeZero l].stdSimplex, and WCVaR is the supremum of the image of .min and max in the paper is stated as attained, with an explicit minimizer or as IsGreatest/IsLeast; no real sInf or sSup is evaluated on an empty or unbounded set, so no statement can hold through Lean's junk value .Many optimization models combine a smooth loss with a convex penalty or constraint. The penalty can be nonsmooth: an absolute-value penalty encourages sparse solutions, while an indicator function enforces a feasible set. A coordinate gradient descent (CGD) method updates selected coordinates by minimizing a quadratic model and then applies a line search. Tseng and Yun studied this method for an extended-valued convex penalty, including penalties that separate by blocks of coordinates. Their global convergence result addresses a basic question for such an iteration: if its iterates have an accumulation point, must that point satisfy the first-order stationarity condition? The result and examples appear in Tseng and Yun (2009).
Coordinate updates are appealing when changing a small block is cheaper than changing the whole vector. Their convergence is delicate when the penalty is nonsmooth: a direction can be useful on one block without revealing whether the full point is stationary. The paper's Theorem 1(e) establishes a guarantee for a generalized Gauss–Seidel selection rule and a block-separable penalty. The authors note that this rules out cycling on Powell's coordinate-minimization example under their stated conditions Tseng and Yun (2009), p. 404.
Let , , and let be proper, convex and lower semicontinuous. Its effective domain contains precisely the points where is finite. Let be continuously differentiable on an open set containing . The objective is , with value outside . No convexity of is assumed.
At iteration , choose a nonempty set of coordinates and a positive-definite symmetric matrix . The search direction minimizes
The next iterate is . The Armijo rule tests the geometric sequence and takes its largest accepted member, using the paper's decrease quantity . Its parameters satisfy , , and . The accepted step obeys .
The generalized Gauss–Seidel rule means that some fixed number of consecutive coordinate sets covers every coordinate, starting at every iteration. The penalty is block-separable with respect to when it is the sum of a proper closed convex function of the selected coordinates and another of their complement. A point is stationary when it lies in and the one-sided directional derivative is nonnegative for every direction .
The goal is Theorem 1(e) Tseng and Yun (2009), p. 399. Under the CGD and Armijo rules, Assumption 1's uniform matrix bounds, a positive lower bound on the initial trial steps, block separability for each chosen coordinate set, and a finite upper bound on the accepted steps,
The mission milestones state the paper's Lemma 1, its Armijo existence claim after equation (10), Lemmas 2 and 3, and Theorem 1(a) and (b). They connect the direction subproblem, descent, stationarity and subsequence behavior to the goal. The theorem asserts stationarity of every cluster point; it does not assert that a cluster point exists or that the full sequence converges.
The result supplies a global first-order guarantee for a block update method even when the smooth part is nonconvex. It applies to extended-valued convex penalties, so the same statement covers both nonsmooth regularization and constraints represented by indicator functions. The bounded-window coverage condition allows varying coordinate sets rather than a fixed cyclic schedule Tseng and Yun (2009), Theorem 1(e).
The paper proves the theorem. This mission asks for a machine-checked Lean proof of that known claim and its selected supporting results. The reusable output includes a precise interface for an extended-valued penalty, the exact quadratic coordinate subproblem, Armijo backtracking with first accepted exponent, and the distinction between a convergent subsequence and a cluster point. The current draft statements compile with proof placeholders; they are proof obligations, not completed machine-checked results.
The descent bound alone controls decrease in objective value; it does not directly show that every coordinate has a vanishing stationarity residual. The coordinate set may vary at each iteration, and the penalty need only separate with respect to the current block. A cluster point may be reached along a subsequence that samples only one of those blocks. The argument therefore has to connect behavior along a convergent subsequence to nearby iterations within a full coverage window. The nonsmooth penalty also prevents replacing directional stationarity by a statement solely about an ordinary gradient.
Vectors use EuclideanSpace ℝ (Fin n) and its Euclidean norm; Fin n starts at zero, whereas the paper numbers coordinates from one. A penalty is represented by its effective domain and finite values on D+\inftyDd_H(x;\mathcal J)xDH$ positive definite. A CGD run records the chosen minimizers, so it does not rely on any unspecified value of that choice outside its valid inputs.
The Armijo predicate records the first successful geometric trial, including rejection of all earlier trials. The matrix bounds in Assumption 1 are quadratic-form bounds. Lemma 3 represents eigenvalue extremes by Rayleigh quotients on the selected coordinates; its generalized spectrum is that of the pair of principal submatrices. These extrema are used only with a nonempty block and positive-definite matrices. The paper's is represented by a remainder whose quotient by tends to zero from the right. In Lemma 1 the line segment remains in . A convergent subsequence is indexed by a strictly increasing map; a cluster point is represented separately by MapClusterPt.
No convergence of the entire iterate sequence is assumed. Stationarity requires the nonnegative directional derivative in every direction, not only the coordinates selected at one step. A valid development needs convex analysis of the subproblem, estimates for positive-definite quadratic forms, properties of lower semicontinuity and directional derivatives, and finite-dimensional subsequence arguments. Contributions proving those reusable facts and the named milestones are within scope.
A binary classifier is learned from a sample of a distribution on , and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function .
Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.
Let be compact and let be a distribution on with marginal and regression function . The classes of are , and , all intersected with . The distance to the decision boundary is
with the Euclidean distance of to (equation (7), p. 7).
In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.
If has an envelope of order and Tsybakov noise exponent , then
Both clauses are stated, as one conjunction.
Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of at the decision boundary. Example: with , , uniform and , the distribution has envelope order and Tsybakov exponent , hence geometric noise exponent .
The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.
The case is elementary once the right splitting level is chosen: the expectation is split at a level of , and is then tuned to . Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value , but not the critical value itself: a logarithmic factor is lost.
Reaching the critical exponent when is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces and and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of . The obvious approach, the same splitting as for , does not work: it always loses the logarithm.
EuclideanSpace ℝ (Fin d) with , and a measurable version of the regression function with values in everywhere. Every Borel distribution on has this form, and the paper defines "for some choice of ".Metric.infDist gives . For Theorem 2.6 both readings give a true statement. Under the reading , the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of with an empty class. The convention is chosen for agreement with the companion mission.lintegral), so a bound can never hold through a junk value of a non-integrable function.The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.
The newsvendor problem is the basic single-period inventory model: a decision maker orders units at unit cost before a random demand is observed, sells units at price , and loses unsold units. Its optimal order is the critical fractile of the demand distribution . Laboratory experiments show that human subjects do not order . Schweitzer and Cachon (Management Science 46(3), 2000) gave subjects uniform demand on and found that the average order lay below for a high-margin product and above for a low-margin product: orders are pulled toward the center of the demand range.
Su (Manufacturing & Service Operations Management 10(4), 2008) explains this pattern with a model of bounded rationality: the decision maker does not pick the best order with certainty, but picks better orders more often, through a logit choice rule. This mission formalizes the first results of that paper, the case of uniform demand, where the logit order has an explicit law and the pull toward the center can be proved exactly. The source is the published MSOM 2008 article; all page numbers are its printed pages.
A decision maker with utility over an interval and bounded-rationality parameter makes a random choice with the logit density
and off (eq. (2), p. 571). Large means noisy choices; small concentrates the choice near the maximizer of .
In the newsvendor problem the price and unit cost satisfy . Demand has density and distribution function . The expected profit of ordering units is
and the optimal solution is its maximizer. The behavioral solution is the logit choice with utility over the decision domain , the smallest interval containing the support of (eq. (4), p. 572).
This mission takes uniform demand with : on and . The midpoint of the demand range is . Two parameters recur:
A truncated normal law on with parameters has density proportional to on and zero elsewhere (eq. (37), p. 586). Write and for the standard normal density and distribution function.
The goal is stated for every and every , with any maximizer of over ; it fixes only the sign of the bias, not its size.
Proposition 3 gives a single mechanism, noise in the choice of the order, that produces both directions of the bias observed by Schweitzer and Cachon: under uniform demand, a high-profit product () is underordered on average and a low-profit product () is overordered. Proposition 1 gives the full law of the boundedly rational order, which is what makes the model testable: the paper fits the truncated normal law to experimental order data and estimates (§5). Corollary 1 is the closed-form mean used in that fit and in Proposition 3.
These results are proved in the paper by direct computation; none of them has a machine-checked proof. The mission adds a checked development of the continuous logit choice model on an interval, of the truncated normal law and its mean, and of the uniform-demand newsvendor profit, together with exact statements of what the paper's informal phrases mean (see Formalization scope).
Each step is elementary on paper, but the formal content sits in the integrals. Expected sales must be computed as a piecewise integral to obtain eq. (5), and the maximizer must be identified over all of , not only on , which needs the profit outside the support as well. Proposition 1 is an identity between two normalized densities, so both normalizing integrals must be shown positive and finite. Corollary 1 requires the mean of a truncated Gaussian in terms of Mathlib's Gaussian density and distribution function, which is not in Mathlib. For Proposition 3, the natural shortcut "the mean of a truncated normal is " is false whenever , and it is exactly the asymmetry of the truncation that produces the bias.
All quantities are real numbers, with the paper's standing assumptions as hypotheses: , (the page states ; is read so that lies inside ), and (eq. (2) divides by ; , perfect rationality, is a limit, not a value of the formula). The decision domain is the closed interval ; the logit density is zero off it, and expectations are integrals over . The parameter is the positive square root of , and , are Mathlib's gaussianPDFReal 0 1 and the distribution function of gaussianReal 0 1.
Corrections and readings relative to the printed text:
The optimal solution in the goal is a hypothesis that maximizes over , never a variable set to a closed form by fiat; milestone 2 shows the hypothesis is satisfiable and identifies . No statement holds vacuously through a junk value: on with the logit normalizer is the integral of a continuous positive function over an interval of positive length, and the denominator of (8) is positive because .
Reusable beyond this mission: the logit density on an interval, the truncated normal density, and its mean formula. Proofs of any milestone, and of the mean of a truncated normal law in general, are welcome.
A service system with several servers can use a larger fraction of its capacity than a single-server system while still giving customers an acceptable wait. The design question is how much unused capacity is needed as the number of servers grows. Ward Whitt's study begins with a factory manager deciding whether to put four machines in one work area. It uses queueing models to connect the number of machines, their utilization, and the delays customers experience. The proposed utilization rule, , keeps the unused fraction proportional to as the number of servers changes (Whitt 1992, pp. 708–710).
The paper distinguishes the chance that a customer waits at all from the length of the wait once a delay occurs. That distinction matters when a staffing choice must control a long wait rather than merely the fraction of customers who wait. The exact result in §3.1 gives a benchmark for the paper's later approximations to more general arrival and service processes (Whitt 1992, pp. 719–720).
An queue has Poisson arrivals at rate , identical servers, independent exponential service times, unlimited waiting room, and first-come first-served service. Time is measured so that each server's service rate is one. The server utilization is . We consider and , so the queue has a stationary distribution. Let be the stationary probability that customers are in the system. Its state process is a birth–death process: arrivals occur at rate and departures from state occur at rate .
Let be an arriving customer's steady-state time in the queue before service begins. An arrival finding fewer than customers starts service at once. An arrival finding customers waits for service completions while all servers are occupied. In the formal model, the law of has an atom at zero of mass and, for each , a gamma component with shape , rate , and weight . The arrival-state weights use the Poisson-arrivals-see-time-averages property. This construction represents the FCFS waiting time independently of any claim about its eventual conditional distribution.
For an event of positive probability, denotes the conditional waiting-time law. The paper calls a customer delayed exactly when . The scale parameter is defined by the utilization equation ; because , this equation makes positive.
The supporting target is the §3.1 statement that a delayed customer's waiting time is exponential with rate , equivalently with mean :
The goal is Proposition 3.1 under the utilization equation. It records both the entire conditional tail and its mean, for every :
The goal also asserts , so these conditional quantities are defined. The scan of Proposition 3.1 prints the exponent without and the mean denominator with ; the statement here uses the values determined by the preceding exponential-law sentence and by the paragraph following the proposition (Whitt 1992, pp. 719–720).
The result gives an exact delay distribution for the Markovian multi-server system. With servers and the utilization equation held fixed, the conditional tail at any positive threshold and the mean wait of a delayed customer both depend on through . Thus the same rule that organizes the probability-of-delay discussion has a definite implication for customers who actually wait. It is also the exact comparison point for the paper's later, explicitly approximate analysis of general queues (Whitt 1992, §3.2).
Formalizing this result supplies a reusable representation of the stationary FCFS waiting-time law as a mixture of Erlang distributions, together with a precise connection between birth–death state probabilities and delay. The related platform items QueueingFundamentals.BirthDeath.mmc_steady_state and QueueingFundamentals.BirthDeath.erlang_c_formula state the stationary state probabilities and the probability of delay, respectively; both are open and neither states this waiting-time law. The open QueueingFundamentals.BirthDeath.halfin_whitt concerns the heavy-traffic limit for the case, a different target. The current result is known mathematically from Whitt's 1992 paper; this mission asks for its machine-checked proof in the specified model.
The conditional distribution is not immediate from an individual service time. A delayed arrival can encounter any queue length , so its waiting time is a gamma law whose shape varies with . The stationary probabilities provide the weights of infinitely many such components. Showing that this whole mixture has one exponential law requires a relation among the stationary tail probabilities and control of the infinite sum. The same mixture must have a well-defined first moment for the conditional mean formula.
Lean uses a natural number , a real arrival rate , and a real sequence satisfying the published QueueingFundamentals.BirthDeath.IsSteadyState predicate with constant birth rate and death rate . That predicate includes nonnegativity, total mass one, and the global balance equations. Its published definition is imported as a reference. Service rate is exactly one, as fixed in §2.1 of the paper. The conditional waiting-time law is a measure on real time, with a point mass at zero and a countable gamma mixture. The positive-time restriction of this measure expresses conditioning in the milestone; real measure values and an integral express the tail and mean in the goal.
The formal hypotheses spell out positive arrival rate, at least one server, and subcritical utilization. These make the stationary law and the positive exponential rate meaningful. The goal states positive delay probability before dividing by it. The waiting-time law is built from stationary queue lengths and service completions, rather than being defined as exponential; proving that it becomes exponential is the mathematical task. Solvers may develop reusable measure-mixture identities, stationary-tail facts, and gamma or exponential distribution results. The approximation formulas of §3.2 and the paper's numerical tables are outside this mission.
J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259) introduced the two criteria that still organise traffic assignment. When a flow of traffic can choose between several routes from one origin to one destination, the paper (p. 345) considers two ways the traffic might divide:
The first is now called Wardrop's first principle, or user equilibrium: no driver can shorten their trip by switching route. The second, Wardrop's second principle, is the system optimum: it "minimizes the vehicle-hours spent on the journey". The gap between the two is the quantity later studied as the price of anarchy of selfish routing (Roughgarden and Tardos, J. ACM 2002), and the marginal-cost characterisation of the system optimum underlies congestion pricing (Beckmann, McGuire and Winsten, Studies in the Economics of Transportation, 1956).
This mission formalizes the paper's solution of criterion (2) on parallel routes, section (2) Minimum Average Time, pp. 345–347. Mission II of the same series treats criterion (1) on the same model.
A total additional flow is divided among alternative routes . Route carries an additional flow and has journey time, equation (22),
where is the journey time on route with no additional flow and is the additional flow at which its speed would fall to zero (routeTime b p i x). A feasible split of is a vector with for every and (IsFeasible p Q q).
The number of additional vehicles on route at an instant is , and (totalExtra b p q). The average journey time is, equations (25)–(26),
(avgTime b p Q q). Criterion (2) asks for a feasible split with for every feasible split (IsMinAvgTime b p Q q).
The marginal journey time of route is , the rate at which grows when flow is added to that route. For a threshold , (usedSet b ε) is the set of routes whose marginal time at zero flow lies below ; with the routes labelled so that it is the paper's "first routes".
For and , every split minimizing admits a threshold with , where , such that
A companion theorem states that a minimizing split exists whenever .
The closed forms give the system-optimal assignment on parallel routes with the travel-time law (22) explicitly: which routes carry traffic, how much, and the resulting average time. Together with the equal-times solution (23)–(24) of mission II they quantify, for this model, how much average time selfish route choice costs; the paper's Fig. 8 compares the two numerically and finds the difference small in its example. The marginal-time conditions (27)–(28) are the parallel-route instance of the general statement that a system optimum is an equilibrium with respect to marginal costs.
The derivation on pp. 346–347 is a first-order argument that the paper does not make rigorous: it assumes a minimizer exists, that it satisfies the stationarity condition, and leaves (32)–(33) to "a few lines of algebra". This mission produces the rigorous version, including existence. No machine-checked statement of (27)–(33) is on the platform; the related platform items on Wardrop equilibria concern the Beckmann potential and atomic congestion games, not the system optimum of this model.
The stationarity condition (27) comes from moving an infinitesimal flow between two routes in use. Turning this into a theorem needs the one-sided version at unused routes, since is a boundary point and the condition there is an inequality, and needs the constraint to be preserved by the perturbation. The step "only the first routes will be in use" is the converse direction: a route with that carries no flow must be shown to contradict minimality, not just to violate the equal-marginals equation.
Existence is not a compactness argument on a closed set: the feasible set is open in the direction , where , and that coercivity has to be used. The algebra from (31) to (32)–(33) is routine once the set and the value of are fixed.
Routes are indexed by Fin D; all quantities are real. The standing hypotheses are , , and ; without the last the feasible set is empty and every statement about a minimizer is vacuous, and with the average time is undefined. Feasibility requires , of the minimizer and of every competitor: at Lean evaluates as , which would let a "minimizer" place flow at capacity for free. The paper's labelling is not assumed; "the first routes" is . Marginal times are written in the closed form (29), and milestone 1 identifies that form with the derivative via HasDerivAt. Minimality is stated for , the paper's criterion, not for .
Corrected slip. The paper prints the denominator of (33) as . The formalization uses : from (31), , and . The printed form is not dimensionally consistent and gives wrong flows, e.g. for , , . Equation (32) is correct as printed.
The goal cannot be satisfied trivially: the threshold is existential and the flows and are pinned to explicit formulas, and the companion existence theorem shows the hypothesis IsMinAvgTime is met for every admissible . The route time and feasible split come from the shared WardropTraffic.EqualTimes.Setting definition; this mission adds the total and average time and criterion (2). Proofs of any item, including the existence theorem and a uniqueness statement (the objective is strictly convex), are welcome.
A network designer may need a cheap connection that keeps the number of links at each site within a local capacity. The minimum bounded-degree spanning tree problem asks for the cheapest spanning tree of a weighted, undirected graph whose vertex degrees respect prescribed upper bounds. The capacity constraints matter in settings where a low-cost tree alone can overload a few hubs. They also make the optimization problem difficult: even with unit edge weights and a bound of two at every vertex, feasibility includes the Hamiltonian path problem. Singh and Lau study the useful relaxation in which the returned tree may exceed each degree bound by one while its cost stays no greater than the best tree satisfying every original bound Singh–Lau 2007.
The weighted result settled the bounded-degree form of a conjecture discussed in their paper. Goemans had obtained a cost-preserving degree guarantee of ; an earlier unweighted local-search result attained a degree allowance but did not cover arbitrary real costs. Singh and Lau's Theorem 1.2 gives the allowance in the weighted setting, without assuming nonnegative costs or triangle inequalities Singh–Lau 2007, pp. 661–662. The platform's open WilliamsonShmoys.minimum_degree_tree_local_search_approximation concerns the related unweighted minimum-degree local-search problem, with a different objective and guarantee.
Let be a finite vertex set and a finite set of unordered, non-loop edges. A spanning tree connects every vertex without a cycle. Every edge has a real cost , so . Each vertex has an integer upper bound on its tree degree . A feasible original solution has for all .
The paper studies a broader connecting-tree problem. A forest is already selected; its connected components, including isolated vertices, are supernodes. The remaining graph has edges disjoint from . A set is an -tree if is a spanning tree. Degree bounds are active only at vertices in , and counts edges of , not edges of . The initial spanning-tree problem is the case and Singh–Lau 2007, p. 665.
For an edge set and vertex set , write for edges of with both endpoints in , and for edges of incident to . The LP-MBDCT relaxation has a nonnegative variable for each . It requires , requires for every nonempty union of supernodes, and requires for . Its objective is . At , , this is the spanning-tree LP in equations (1)–(5) Singh–Lau 2007, pp. 662, 665.
For every feasible initial LP, the paper's Figure 4 algorithm has a terminating run. Every possible run returns a spanning tree satisfying
In particular, is at most the cost of every spanning tree satisfying the original bounds, and thus at most the original optimum. Every run has at most iterations. The cost comparison against every LP-feasible vector states the stronger bound used by Theorem 4.2 Singh–Lau 2007, pp. 661, 666.
The connecting-tree theorem makes the same cost and degree guarantee for an arbitrary feasible state , with only for . The attack path follows the paper's numbered results: Lemma 4.3 describes tight constraints by a laminar family, Claim 4.5 classifies vertices with one excess token, Lemma 4.6 bounds tokens inside a laminar subtree, and Lemma 4.1 says each nonterminal basic solution has either a unit-valued edge or a removable degree constraint. Theorem 4.2 then supplies the general guarantee Singh–Lau 2007, pp. 666–667.
The result allows one unit of violation at each local degree bound while preserving the cost benchmark exactly. It applies even when negative edge costs make standard multiplicative cost ratios awkward. The connecting-tree statement is useful beyond the initial instance because it covers a forest already accumulated and a subset of degree constraints still active.
This mission formalizes the known 2007 result as an open Lean proof target; the paper proves the mathematics, while the declarations here currently have no machine-checked proofs. A completed development would provide a reusable account of a spanning-tree LP with forest contraction, basic solutions defined by tight rows, and a finite relational algorithm with all choices exposed. These objects could support the paper's lower-and-upper-bound extension and other iterative-rounding results.
Rounding an arbitrary fractional edge upward can increase cost beyond the LP benchmark. Restricting the algorithm to edges with value exactly one protects that benchmark, but a nonterminal basic solution need not present a unit-valued edge. The central structural question is then whether some active degree constraint can be removed with only a one-unit effect on the final degree. The tight subtour rows and degree rows overlap, so counting edges from the support alone is insufficient; Lemmas 4.3–4.6 resolve the dependency and token-counting issues that make the direct argument fail Singh–Lau 2007, pp. 666–667.
Lean represents edges as Sym2 V in finite sets, excluding diagonal edges. It represents LP vectors on all unordered pairs but requires zero values outside the current edge set. A forest is acyclic on the full vertex set. A compatible subtour set is a union of its connected components. Subtour right-hand sides are real numbers, so subtraction does not truncate at zero; the empty set is excluded because the literal row would make the LP infeasible. Degree bounds are integers so the algorithm's decrements are total. A basic feasible solution is determined uniquely by its tight equality rows among vectors supported on the current edge set. Linear independence in Lemma 4.3 is checked on the positive support.
Figure 4 is a relation because the LP optimum, a unit-valued edge, and a qualifying vertex may each be chosen in several ways. Its edge and vertex tests are mandatory when their conditions hold. The vertex test uses the support before deleting the selected edge and bounds after decrementing its endpoints, following the printed order. “The algorithm returns” is represented by existence of a run, an iteration bound on every step chain, and guarantees for every returned set. “Cost at most the LP optimum” means cost no greater than the objective at every feasible LP vector. “Polynomial time” is represented by the iteration count; the ellipsoid LP solver and separation-oracle complexity are outside this mission. Lemma 4.6's token distribution is expressed as its explicit counting inequality.
The goal asserts the Figure 4 output and its LP cost guarantee. Bare existence of a tree with cost at most the optimum and degrees at most would be witnessed by an original optimal tree and would lose the algorithmic theorem. A return guarantee without run existence would hold vacuously for a stuck relation. Contributions that prove the stated structural lemmas, establish the LP oracle's basic-optimum availability, or close the algorithm invariant are within scope. No existing platform item treats this bounded-degree LP and iterative-rounding algorithm under these conventions; the plain minimum-spanning-tree LP definition uses a different edge representation and no forest or degree constraints.
A many-server queue has identical servers, a stream of arriving customers, and a buffer in which customers wait when every server is busy. It models call centres, hospital wards and server farms, and the regime of practical interest is the Halfin–Whitt or quality-and-efficiency-driven regime, in which the number of servers grows with the arrival rate so that : servers are almost fully used, yet only a vanishing fraction of customers waits.
This mission formalizes that identity and the proposition that yields it.
Fix one realisation of the queue (Reed, §2, p. 6).
The number in system is (2.2):
Centring each indicator at its (conditional) mean produces the terms
and , the analogous centred sum (2.5) over the customers who entered service after time . is the conditional mean number in a queue fed by the same arrivals.
A sample path is non-idling if for every
that is, the customers waiting at time are exactly those who have arrived and not yet entered service. This holds for every first-come-first-served -server path that never idles a server while a customer waits; the paper uses it at the start of the proof of Proposition 2.1 (p. 8).
For a non-idling sample path and every ,
The result. Equation (2.8) is the paper's starting point for both of its limit theorems. Writing with shows that the number in system is the image of the infinite-server quantities under the regulator map of the paper's §3, the unique solution of . The fluid limit (Theorem 4.1, p. 12) and the diffusion limit (Theorem 5.1, p. 23) then follow from limit theorems for the infinite-server terms and the continuity of that map. Without (2.8), the -server queue has no closed equation in terms of quantities whose limits are known.
Formalizing it. The identity is proved in the paper on pp. 7–9; to our knowledge it has not been machine-checked. This mission produces a sample-path model of the queue (initial customers, arrivals, FCFS service order, waiting times) together with the decomposition of its number in system, reusable for other many-server results stated pathwise. The limit theorems 4.1 and 5.1 themselves are weak-convergence statements in the Skorohod space and are not part of this mission; the regulator map (Proposition 3.1) is the subject of a separate mission of this series.
The decomposition (2.7) is bookkeeping. The content is Proposition 2.1, which converts a sum over customers of tail differences into an integral, against , of the number of waiting customers at earlier times. The step that needs care is the change of viewpoint from "customer 's service time falls in a window of length " to "customer is waiting at time ", after which the sum over customers must be recognised, at each time , as the waiting count of the non-idling identity, with the arrivals counted up to rather than . A second point is the treatment of an atom of at : the half-open windows and the closed integration range must match, and for is used whenever a customer is still waiting.
Related platform items: WhittEfficiency.IS.* (the queue with Poisson arrivals, the infinite-server object behind ) and PalmQueueing.Palm.swiss_army_formula (a pathwise queueing identity of Palm calculus) are the nearest queueing results; neither is the object of this mission.
Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.
The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is . This mission formalizes that statement.
There are items ; item is the end item. Every item has exactly one immediate successor with , and , so the items form a tree rooted at the end item. Write for the set of all successors of , for the set of all its predecessors, and for its immediate predecessors. Item has a lead time , and its total lead time is , ; the items are indexed so that .
Time runs in periods . The demands for the end item are independent, identically distributed, nonnegative, with a density and a finite mean . In period a policy chooses the echelon inventory positions after ordering as functions of the demands already observed. The position before ordering is , and the echelon stock on hand after arrivals is ; positions referring to periods before are read off given initial data . Problem P asks for a policy satisfying
that minimizes
where is the echelon holding cost of item , the backlogging cost, the installation holding cost of the end item, the discount factor and the density of the demand over periods.
The quantity of interest is the discounted echelon holding cost of item and its predecessors,
GA(i) asks it to be positive for every item.
If for some item
then the minimal cost of Problem P is unbounded below: for every real there is a feasible policy whose cost is a real number less than .
Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is . Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.
The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.
The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of , whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.
Measure.infinitePi) of a probability measure on with , Lebesgue, integrable and .In the extended reals, : a policy whose positive and negative cost parts are both infinite gets the value . The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost would be trivially true and is ruled out. Milestone 2 is stated for , where the backlog term is unchanged.
Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.