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?
Multi-agent scheduling studies a machine shared by parties with their own jobs and their own objectives. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model: agents and each own a set of jobs, and the schedule must serve both. The paper frames this within multiagent systems, where agents negotiate the use of a common resource over time, and its schedules are meant to support that negotiation: either the best schedule for one agent given what the other accepts, or the whole set of nondominated (Pareto-optimal) schedules. The paper classifies the complexity of the constrained problems for the classical regular objectives.
One of its polynomial cases concerns the number of late jobs on both sides: agent accepts schedules in which at most of its jobs are late, and agent minimizes the number of its own late jobs. For a single agent, minimizing the number of late jobs is solved by Moore's algorithm (Moore 1968), and a dynamic program of the Lawler–Moore type over jobs in due-date order solves related weighted versions (Lawler & Moore 1969). §7 of the 2004 paper adapts that dynamic program to two agents by tracking the number of late jobs of each agent separately.
There are jobs , all available at time . Job has a processing time , a due date , and an owner, agent or agent . A schedule is a sequence of all jobs processed on one machine from time without idle time or preemption; the completion time of is the sum of the processing times of and the jobs before it. Job is late if and early otherwise. denotes the number of late jobs of agent .
Given an integer , the problem asks for a schedule with (a feasible schedule) minimizing . An instance may have no feasible schedule at all.
The jobs are numbered in earliest-due-date (EDD) order, . A partial schedule of is described by its set of early jobs: the jobs of run first, in EDD order, each completing by its due date, and the other jobs of count as late. The table is the minimum completion time of the last early job over partial schedules of with at most late -jobs and at most late -jobs, and if there is none. It is computed by , at a negative index, and
when belongs to (with in place of when belongs to ), where if and otherwise.
For a feasible instance with jobs in EDD order, for some , and
is the optimal value of : some feasible schedule has exactly late -jobs, and every feasible schedule has at least .
A feasible instance has an optimal schedule whose early jobs come first, in EDD order, and whose late jobs come last.
For : if is finite, it is the minimum, attained, of over partial schedules of with at most late -jobs and at most late -jobs; if , there is no such partial schedule.
The theorem places among the polynomially solvable two-agent problems (Table 1 of the paper lists it as ), in contrast with , which the same paper shows binary NP-hard. Through the binary-search argument of §3.1, solving the constrained problem for every also yields the nondominated pairs of the corresponding Pareto problem.
The result is proved in the paper; to the knowledge of this mission it has no machine-checked proof. The mission produces a checked correctness proof of the table, including the boundary convention, which the printed text leaves incomplete (see below). Further welcome work: the complexity bound in an explicit cost model, and the weighted variant.
The table is defined over partial schedules, in which the jobs outside the early set are only counted as late, while the problem is posed over complete sequences, in which lateness is measured: a job declared late may finish on time once it is appended. The correctness of must bridge the two objects in both directions, and the bridge is the structural Lemma 7.1, which the printed proofs use without detail. Lemma 7.2 is an optimal-substructure claim: it requires that the early set of minimizing total processing time is also the right one to extend by , which holds only because of the EDD numbering. Finally, the printed boundary gives only ; the natural reading for makes Theorem 7.3 false, so the boundary must be read from the definition of , not from the display.
Fin n, 0-based, numbered in EDD order, with an owner label ag : Fin n → Agent; this follows the paper's single numbered list in §7 rather than separate index sets per agent. EDD order is the hypothesis Monotone d, ties allowed. Data are natural numbers.MooreLateJobs.Shared.completionTime (sequences without idle time) and late jobs the published MooreLateJobs.NumLate.lateSet (late iff ), reused as references with the data cast to .WithTop ℕ, with ⊤ for ; no large sentinel number is used. The boundary is for all , the value forced by the "at most" definition of ; a negative index gives ; early means , as in the recursion (the proof of Lemma 7.2 prints a strict "").Nat.find of the existence clause, which the goal asserts.Balanced truncation reduces a large control system to a small one by discarding the states that are both hard to reach and hard to observe. For linear systems "hard to reach" is measured exactly by the controllability Gramian : the minimal input energy needed to steer the system from to is . For bilinear systems, in which the input also multiplies the state, no such exact formula is known, and several papers have tried to describe the nonlinear controllability energy functional through state-dependent Gramians.
Gray and Mesko ([25] in the paper, 1998) and Condon and Ivanov ([11], 2005) stated that, for with sufficiently small, the gradient of is given by a state-dependent Gramian of the linearization, , and derived from this comparison inequalities between and the algebraic Gramian. Benner and Damm (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X) observed that this formula needs an integrability condition that is not automatic, and gave an explicit two-dimensional system for which it fails (Example 3.3, pp. 697–698). This mission formalizes that counterexample.
A bilinear control system with state and input is
with real matrices and ; write for the -th column of . The system is locally controllable if the pair is controllable, that is, the Kalman matrix has rank .
Linearizing the system at a state and the input gives a linear system whose input matrix has columns . Its controllability Gramian is the solution of the Lyapunov equation
When is stable, (3.9) has exactly one solution for every , and it is symmetric. The claim under test is
A vector field on an open set is integrable (a gradient field) if for some real function .
Example 3.3 is the single-input system (, ) with
and a real parameter . In Lean these are exA, exN ν and exb (with exB the matrix ), equation (3.9) is IsLinGramian, and controllability is IsControllable.
For every , with solving (3.9) for every : the pair is controllable, and for every there is no with
The goal refutes every potential , not only , so it does not depend on how is defined; it is exactly the statement that the field is not integrable on any punctured neighbourhood of the origin, which is how (3.8) is claimed.
The result. The example shows that the state-dependent Gramian of the linearization does not, in general, describe the controllability energy of a bilinear system through (3.8), even for a locally controllable system and arbitrarily close to the origin. As a consequence, the inequalities and derived in [25, 11] from (3.8) lose their justification, and the comparison of with the algebraic Gramian requires the different argument the paper develops in its later sections. The example is a minimal one: two states, one input, one coupling parameter.
Formalizing it. The counterexample is proved in the paper by a hand computation through Kronecker products, and that computation contains a sign slip (see below); a machine-checked version settles the claim independently of it. The result is proved in the paper and, to our knowledge, has not been formalized anywhere. The general derivative formula (milestone 2) is reusable for any parametric Lyapunov equation.
The obvious route is to compute the Jacobian of at one point and observe that it is not symmetric. Two steps of this route need care. First, is defined only implicitly, through (3.9) at every point, so its differentiability in , and that of its inverse, must be derived from the invertibility of the Lyapunov operator and of near the point. Second, passing from "the Jacobian of is not symmetric" to " is not a gradient" requires the symmetry of second derivatives of a function that is only assumed differentiable with gradient on a punctured ball; the regularity of is inherited from that of , not assumed. The goal is also not a statement about a single point: it must hold for every radius , so the asymmetry must be exhibited at points arbitrarily close to the origin, where it is of order .
Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the paper's indices are Fin m. In the goal the plane is EuclideanSpace ℝ (Fin 2) and the potential is required to satisfy HasGradientAt at each point of the punctured ball , with no further regularity.Matrix.inv, which returns at singular matrices; is invertible near the origin, and milestones 2–4 assume invertibility (or ) where they use it.Contributions welcome: proofs of the four milestones, in particular the smooth dependence of the solution of a Lyapunov equation on its right-hand side (milestone 2), which is general and reusable.
Progressive hedging separates a stochastic optimization problem by scenario, solves those smaller problems, and coordinates their first-stage decisions through weighted aggregation and price updates. It is useful when the full extensive formulation is too large to solve directly. For stochastic mixed-integer programs, its iterates can provide feasible decisions, but a feasible cost alone does not reveal how far that cost is from the global optimum. A lower bound gives the missing comparison: the difference between a feasible cost and a valid lower bound is an optimality gap. Branch-and-bound methods also use lower bounds to discard regions whose best possible cost cannot improve the current solution. These are the reasons the authors seek a bound available during a progressive-hedging run, rather than only after convergence. Gade et al., author manuscript, §§1–3.
The paper establishes lower bounds for two-stage stochastic mixed-integer programs, extends them to scenario bundles, and studies their behavior computationally. The mission concerns the mathematical statement that the price vector produced at each completed iteration is eligible for a decomposed lower bound. The paper was published in Mathematical Programming in 2016; the theorem and page labels here follow the authors' SAND2013-9195J manuscript. Gade et al., author manuscript.
Let be a finite set of scenarios and let be their probabilities, with . A first-stage decision is made before the scenario is known. Its first coordinates are nonnegative integers; the others are unrestricted reals. It incurs cost and must satisfy . After scenario is observed, a second-stage decision incurs cost . Its first coordinates are nonnegative integers, and it must satisfy . The recourse matrix is common to all scenarios. The scenario feasible set contains pairs satisfying these restrictions for one . Gade et al., §2, pp. 3–5.
In the extensive scenario formulation, each scenario has a copy of the first-stage vector, and a common vector enforces implementability through . Its optimum is . Algorithm 1 starts with zero prices , solves unpenalized scenario problems, and at iteration computes and . Later scenario solves add both and to their objectives. Here is the algorithm's scalar parameter. Gade et al., Algorithm 1, p. 6.
For any scenario prices , define the decomposed dual value by
Proposition 1 states that prices with satisfy . The price invariant in §3.1 states that the update maintains this weighted zero sum. The mission's goal combines these source claims at every completed iteration of Algorithm 1:
The formal goal is the lower-bound inequality; the zero-sum statement and Proposition 1 are its two milestones. Gade et al., Proposition 1, p. 6, and §3.1, p. 7.
For a partition of the scenarios, a bundle has probability . A bundle subproblem uses one first-stage vector for its scenarios and second-stage weights . Proposition 3 gives the corresponding inequality when . The proposal also records the bundle price invariant and the resulting inequality at each completed bundled iteration as companion statements. Gade et al., §3.3, pp. 9–10.
The scenario bound turns each price vector into an independent set of optimization problems whose weighted values certify a lower bound on the original mixed-integer optimum. The bound does not require the scenario first-stage decisions to agree at that iteration. The bundle result gives the same kind of certificate when several scenarios are solved together. These are the paper's known results, not new open mathematical conjectures. Gade et al., §§3.1 and 3.3.
Formalizing them requires a reusable interface for finite-support stochastic mixed-integer models, their scenario feasible sets, implementability equations, price systems, and finite prefixes of both algorithms. It also separates the general price-feasibility inequality from the algorithmic invariant. The mission currently proposes statements with open Lean proofs; it does not claim a machine-checked proof of these paper results.
An iteration of progressive hedging solves scenario problems with a quadratic proximal term, while the lower-bound calculation uses scenario problems without that term. Their objective values cannot simply be identified. The relevant connection is the price vector: to apply Proposition 1 at an arbitrary iteration, its weighted zero-sum condition must follow from the actual aggregation and price-update rules. The bundle version adds normalization by , so every bundle must have positive mass and the bundle weights must cover the full scenario distribution. Gade et al., §§3.1 and 3.3.
Lean represents vectors as Fin n → ℝ, linear constraints componentwise, and the extensive formulation with the weighted implementability equation printed in (15). The dimensions satisfy and , as required by the paper's spaces . The finite scenario weights are positive and sum to one. The first integer coordinates are nonnegative; every remaining real coordinate is free. The paper's assumptions that the SMIP has an attained finite optimum and each is nonempty are explicit in the goal and Propositions 1 and 3. The scenario and bundle subproblem values, and , live in the extended reals: an unbounded-below subproblem retains rather than acquiring an arbitrary real infimum. Gade et al., §§2–3.
An algorithm run is a finite prefix through its last aggregation and price update, with exact minimizers recorded as conditions on its sequences; a stopping test truncates the prefix. The proximal term is the Euclidean sum of squared coordinate differences. No positivity condition on is added to the lower-bound statements, since the page does not require one for these claims. Bundles form a partition, but equal bundle sizes are not required for the inequalities. Algorithm 2's printed w^ν(i) at initialization and Σ_i P_β x^ν(β) at aggregation are read with bundle indices. A bundle recourse vector is represented as a function on all scenarios, with only its coordinates inside the bundle constrained or used.
The exact equations of the scenario model and runs prevent a trivial encoding that assumes dual feasibility or the desired bound as part of a run. Contributions to the model, the price invariants, the extended-real weak-duality arguments, and the bundle extension are all within scope. The paper's convexified limit result (Proposition 2), its cited Theorem 1, and multi-stage Algorithm 3 are outside this mission.
Benders decomposition solves an optimization problem in two groups of variables by fixing one group, solving the remaining subproblem, and turning what the subproblem's solution proves into a constraint, the Benders cut, on the fixed variables. In the classical method of Benders (1962) the subproblem is a linear program and the cut comes from its LP dual. Many problems that decompose naturally have subproblems that are not linear programs: scheduling, satisfiability, 0-1 and constraint programs. Hooker and Ottosson (Math. Program. 96, 2003) replaced the LP dual by the inference dual, the problem of inferring the strongest bound on the objective from the constraints, and obtained a Benders scheme in which any sound inference method produces cuts. This logic-based Benders decomposition has since become a standard technique for planning and scheduling problems that combine an assignment master problem with combinatorial subproblems.
The correctness of the generic scheme rests on two short theorems of the paper. Theorem 1 says that if every cut is valid, then each of the algorithm's three ways of stopping reports the right answer. Theorem 2 says that the algorithm stops when the fixed variables range over a finite set. This mission formalizes both theorems, together with the facts used in the proof of Theorem 1.
An optimization problem (1) has a domain , a feasible set and a real-valued objective ; its value is . Optimal values lie in : an infeasible minimization has value , an unbounded one , and the reverse holds for maximization. For propositions about , implies with respect to , written , if holds at every where holds. The inference dual (2) of (1) is
In Benders decomposition the variables are pairs with , , and problem (6) is over . Fixing at a trial value gives the subproblem (7), over , with inference dual (8): s.t. . A bounding function defines the cut . The cut satisfies
(B1) if every feasible of (6) satisfies , and
(B2) if , the value obtained in the subproblem dual.
The cuts generated so far form the master problem (9): s.t. for every cut , .
The generic Benders algorithm (Figure 1 of the paper) starts with and some . While the subproblem dual at has a feasible , it formulates with and adds its cut. If the master is then infeasible, it stops and reports (6) infeasible. Otherwise it takes an optimal solution of the master and repeats. When the loop exits, the optimal value of (6) is reported as .
In Lean, LogicBenders.Generic.Setting defines all of these objects: optVal, subVal, IsDualFeasible, ValidCut, masterLHS, IsMasterOptimal and MasterInfeasible, and a Run with the predicates IsRun, StopsAtWhile and StopsAtMaster.
Assume (B1) for every cut the run has added. Then three statements hold.
If (B1) and (B2) hold, is finite, and the subproblem dual is solved to optimality, then no run of the algorithm continues forever.
Lemma 3 (p. 20) gives a criterion for a 0-1 inequality to imply the branching clause (29). The §4 statement (p. 7) characterizes when a feasible linear system implies .
Theorem 1 is what allows any sound inference method to supply Benders cuts. Correctness needs only (B1), so the method that derives the cuts (resolution, constraint propagation, a branch-and-bound proof, LP duality) never has to be re-verified at the level of the decomposition. The paper's specializations to satisfiability, 0-1 programming and machine scheduling, and much of the later literature on logic-based Benders, rely on this theorem when they check validity of their cuts and nothing more. Theorem 2 is the matching termination guarantee, and the example on p. 10 shows that the finiteness of cannot be dropped.
Both theorems are proved in the paper, and to the extent known no machine-checked version exists. A formalization makes the paper's implicit conventions precise: values in , what "the subproblem dual is infeasible" means when is always a feasible bound, and exactly which cuts the master contains at each iteration. It also exposes two gaps in the printed proofs. Theorem 1's first clause uses the attainment of the subproblem optimum without stating it. Theorem 2's printed proof claims the subproblem value increases at every iteration, which is false, although the theorem itself is true. The definitions form a small reusable layer for later formalizations of specific logic-based Benders schemes.
The mathematics is elementary, and the difficulty lies in stating it faithfully. Several readings of the statements are wrong. A "run" whose are not master optima for exactly the cuts generated so far makes Theorem 1 false. Optimal values taken as real infima turn the infeasible case into junk. Defining "dual infeasible" over the extended reals makes clause 3 vacuous. For Theorem 2, the obvious argument is the printed one, that (or ) increases strictly. It fails: with three values of and cuts equal to away from their own , the subproblem value can decrease between iterations while stays fixed. The printed argument therefore cannot be transcribed, and the theorem needs a proof the page does not give.
X stands for , Y for and D for . The feasible set is S : Set (X × Y) and the objective is f : X → Y → ℝ. Optimal values are EReal infima and suprema, with for infeasible and for unbounded problems.EReal, so is always feasible. "The subproblem dual is infeasible" is therefore stated as "no real is feasible". A master optimum means and is at most that maximum at every ; the value means the master is unbounded.ybar k, has bound zbar k, and adds cut k. The structure IsRun encodes Figure 1 exactly: zbar 0 = ⊥, every iteration finds a dual-feasible beta k > zbar k with cut k (ybar k) = beta k, and the next is a master optimum for exactly the cuts 0, …, k. An unconstrained "run", or a dual infeasibility that satisfies vacuously, would trivialize the goal, and both are ruled out by these definitions.Retailers decide which product variants to stock, and most assortment-planning tools model consumer choice with the multinomial logit (MNL) model: a consumer who does not find an acceptable variant simply leaves without buying. Cachon, Terwiesch and Xu (Retail Assortment Planning in the Presence of Consumer Search, working paper of December 2002; published in MSOM 7(4), 2005, doi:10.1287/msom.1050.0088) point out that consumers also search: a consumer who likes what the store offers may still walk out to look elsewhere, and that is more likely when the assortment is narrow.
In practice a retailer does not know consumer preferences; it estimates them from sales data and re-plans. This mission formalizes §5.1 of the paper, which asks what happens when a retailer runs this estimate-and-replan loop with the traditional no-search MNL model while consumers actually search. The loop can settle at a heuristic equilibrium in the sense of Cachon and Kok (2002), and the question is how that equilibrium compares with the truly optimal assortment.
There are product variants, labelled from most to least popular, with preferences , and a no-purchase option ("variant 0") with preference . An assortment of depth is the set . Variant has margin , with whenever (monotone margins, p. 6), and carrying it at demand incurs an operational cost , where is concave and increasing on (demand is normalised to one consumer).
True demand: the independent assortment model. With a constant (Theorem 1 of the paper: ) and , the probability that a consumer searches is , and variant has demand
The no-purchase demand is , and the true profit is .
Estimates. Observing for , the retailer fits the MNL model, normalised by : for , and for variants not carried it reuses the estimates from an initial depth test with the full assortment. The no-search model fed with preferences predicts the shares and the profit .
Heuristic equilibrium. A depth is a heuristic equilibrium when maximises over : the assortment is optimal for the estimated preferences, and the estimates are those observed under the assortment. An optimal depth maximises the true profit over .
If is a heuristic equilibrium and is an optimal depth such that every deeper depth is strictly worse ( for ), then
Theorem 8 says that a retailer who ignores consumer search and plans iteratively from its own sales data can only err on the side of a too-narrow assortment, never a too-deep one. The bias is structural: Theorem 7 shows that the estimates get every product variant's relative preference right but misjudge the no-purchase option in a direction fixed by the depth. The result thus separates the part of the MNL model that survives consumer search (IIA among products) from the part that does not (IIA with respect to the no-purchase option).
The results are proved in the paper, by short arguments, but some steps are only asserted: the non-negativity of variant profits at the equilibrium is attributed to "the previous section", and the overlapping assortment model is dismissed with "the similar process". No machine-checked proof of these results is known. A formalization makes explicit the hypotheses the paper leaves implicit (, and a strict-deeper condition on in place of the presumed uniqueness of the optimum), and delivers a reusable formal model of MNL estimation under search.
Each step is elementary, and the difficulty lies in keeping two profit functions apart and carrying the right inequalities between them. The tempting shortcut, "the estimates are correct, so the no-search optimum is the true optimum", fails: the estimates are correct only up to the no-purchase preference , which depends on , and that single number shifts every predicted share. The proof of Theorem 7 must reduce the comparison of and to the monotonicity of the function . The step from no-purchase demand to profit needs every predicted variant profit to be non-negative, which requires the monotone labelling of preferences and margins together with concavity of and ; the paper asserts it without proof.
Fin n, 0-based: the paper's variant is index . Depths are natural numbers, and depth is the published RetailVariety.Structure.popularSet n x; the MNL share is the published RetailVariety.Structure.share.Fin n; its preference and estimate are separate reals.Trivializing formalizations are ruled out: the estimates are not the true preferences (in particular , which would force ); is not an arbitrary maximiser but one with all deeper depths strictly worse; , where nothing is observed, is excluded rather than given junk estimates; and nothing is claimed for the overlapping model.
Contributions welcome: proofs of the milestones, in particular Theorem 7 and the positivity step, and a formal treatment of the overlapping model with its additional hypotheses.
A retailer choosing which variants of a product to stock (colours, sizes, models) faces a trade-off that operations management has studied since van Ryzin and Mahajan (1999): a deeper assortment attracts more purchases, but each added variant takes demand away from the variants already on the shelf. This loss is called cannibalization. In the standard model of consumer choice, the multinomial logit (MNL), cannibalization holds exactly: every variant's purchase probability falls when a variant is added.
The MNL assumes that a consumer who walks into a store buys either from that store or nothing. Real consumers can also leave to search elsewhere, and a deeper assortment makes them less likely to leave. Cachon, Terwiesch and Xu (working paper, 2002; published in Manufacturing & Service Operations Management, 2005, doi:10.1287/msom.1050.0088) add search to the MNL and ask whether cannibalization survives. Two forces now act on a variant's demand when the assortment expands: the share of buyers who choose it falls, and the share of consumers who stay in the store rises. This mission formalizes their answer for the first of their two search models, the independent assortment model, in which the outside option does not depend on what the retailer stocks.
There are possible variants ; the retailer stocks an assortment . A faux variant represents not buying.
Gumbel shocks. Fix a scale and let be Euler's constant. The zero-mean Gumbel law with scale has distribution function and density
Utilities. Variant has expected net utility (utility minus price), and the no-purchase option has (its price is ). A consumer's realised utilities are and , with independent and Gumbel. The preference of variant is , and .
No search. The consumer buys the variant of with the highest utility, or nothing if is higher. The probability that she buys is .
Search. A consumer may instead search at a cost and receive , where is another independent Gumbel shock that she has not yet observed. Having seen , the best utility in the store, she searches when the expected gain minus the expected loss is at least :
The independent-assortment demand is the probability that variant has the highest utility in , beats the no-purchase option, and the consumer does not search. Write (the search threshold), and .
For all and with ,
The goal leaves the utilities , , , the search cost , the scale and the number of variants arbitrary.
Theorem 1 says that under independent-assortment search the demand for every stocked variant is its MNL demand scaled by one common factor, the probability that the best option in the store clears the threshold . The threshold itself does not depend on the assortment. Theorem 2 then shows that the MNL's cannibalization effect dominates the retention effect of a deeper assortment, so each variant's demand still falls strictly when variants are added. The paper's later results on the shape of the profit function and on the structure of optimal assortments under search build on this closed form.
The paper's proofs are short but rely on steps it states without proof: the MNL formula is cited from Anderson, de Palma and Thisse (1992), the search rule is obtained "after rearranging terms", and the closed form follows from a change of variables. No machine-checked version of these steps is known. The mission produces a checked derivation of a logit-type closed form from an explicit random-utility model with an outside option and an endogenous stopping decision, at the paper's scale and with its centring constant .
Theorem 2 is not monotonicity of a single fraction. Adding a variant enlarges the denominator of and simultaneously raises the factor , so the sign of the change is a competition between the two, and a bound on either factor alone does not settle it. The comparison becomes one-dimensional only after Theorem 1 is available, and Theorem 1 itself requires computing a probability of an event defined by finitely many strict inequalities among independent Gumbel variables together with the consumer's search decision. That calculation is an iterated integral over the product law, with the decision rule, the mean of the Gumbel law and the change of variables each needing their own justification.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is the extra index none of Option (Fin n). Assortments are Finset (Fin n), and is S ⊂ Splus.IsZeroMeanGumbel μ G says the probability measure G on ℝ has distribution function above; and is Real.eulerMascheroniConstant. Such a law exists for every (checked sorry-free locally).Option (Fin n) → ℝ with the product measure Measure.pi (fun _ => G). The search shock does not appear in it: the consumer decides before observing , so only its law enters, as integration against G in the search rule.noSearchProb) and (searchProb) are the real values of the probabilities of the choice events, with strict inequalities. The search event uses the paper's decision rule (the displayed integral), not the threshold ; the equivalence is a milestone. The closed form is the published RetailVariety.Structure.share.Ruled out. Demand defined by the closed form (3), which would make Theorem 1 true by definition and Theorem 2 a calculus fact; Theorem 2 with and ; a standard Gumbel law (scale , mean ) in place of the paper's zero-mean scale- law; and a model without the no-purchase option.
Infrastructure. A complete development needs the distribution theory of the Gumbel law (density, mean), choice probabilities of products of i.i.d. continuous variables as iterated integrals, and calculus for . The Gumbel and MNL lemmas are reusable for any logit-based choice model, including the other missions of this series. Contributions of proofs of any milestone, or of general MNL infrastructure that the milestones can import, are welcome.
A retailer deciding which variants of a product to stock trades off two effects. A deeper assortment captures consumers whose favourite variant would otherwise be missing, but it splits demand among more variants, each of which then carries its operational costs (shelf space, handling, inventory) at a smaller, less efficient scale. Van Ryzin and Mahajan (Management Science 1999) showed that under multinomial-logit (MNL) demand the optimal assortment consists of the most popular variants, which reduces the search over assortments to candidates.
Cachon, Terwiesch and Xu (working paper, 2002; published in MSOM 2005) add consumer search: a consumer who finds nothing good enough in the store may leave to look elsewhere, and a deeper assortment makes that less likely. In their independent-assortment model the search threshold does not depend on the store's assortment, but the fraction of consumers who stay does. This mission formalizes their Theorem 5: even with this extra dependence, the profit change from adding a variant is quasi-convex in that variant's preference.
There are variants. Variant has a preference and the no-purchase option has preference (in the paper , with the net utility and the Gumbel scale). For an assortment the MNL purchase probability without search is
A consumer searches when her best alternative in the store, including no purchase, falls below a threshold . With Euler's constant and , this happens with probability , and by the paper's Theorem 1 the independent-assortment demand is
Each variant sold earns a margin , and stocking a variant with demand costs , where the cost function is concave and increasing on (economies of scale). Variant 's profit is . Write .
Fix and a variant , and treat 's preference as a variable. Let be variant 's profit in ; its demand carries the factor , not . The cannibalization loss and the profit change are
Quasi-convexity of says that a variant is worth adding, if at all, at an extreme of its popularity. The paper uses it to conclude that, as without search, the optimal assortment under independent-assortment search lies among the popular assortments, the sets of the most preferred variants. This reduces assortment optimization to candidates. The paper also shows that the conclusion fails in its overlapping-assortment model, so the independent-assortment case marks where this structural result survives the addition of search.
The result is proved in the paper; none of it has a machine-checked proof. The paper's proof contains gaps that a formalization must close: several sign and monotonicity facts are asserted without proof ("It can be shown", "by a similar argument as in Theorem 4"), display (8) is printed without a factor , and the step from (10) to (11) rests on an inequality asserted without the full expression. A complete formal proof of Theorem 5 therefore also fixes the argument.
The no-search analogue (Theorem 4) is easy: the numerator of is increasing, so changes sign at most once. Here the search factor depends on , and the derivative splits as with , , nondecreasing and nonincreasing, but neither nor is monotone. So the argument used for Theorem 4 no longer applies, and when and the derivative cannot be written as a positive factor times a monotone one. The proof needs a separate second-order argument at critical points in that case. Showing only that has at most one zero is also not enough: it must change sign from negative to positive.
Fin n (0-based); the no-purchase option is a separate real v0 > 0, not an element of Fin n. All preferences are positive. The MNL probability is the published RetailVariety.Structure.share, referenced, not redefined.deriv c. The value is unconstrained; .Function.update v j x on insert j S, with . Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0).A retailer that sells a product in many variants (colours, sizes, flavours) has to decide which variants to stock. This is the assortment planning problem. Each variant added to the shelf brings new demand. It also cannibalizes demand from the variants already stocked, and it lowers their cost efficiency, because operational costs (shelf space, handling, holding) usually show economies of scale. Cachon, Terwiesch and Xu, in Retail Assortment Planning in the Presence of Consumer Search (Wharton working paper, December 2002), study this trade-off under the multinomial logit (MNL) model of consumer choice. They compare a model without consumer search with two models in which consumers may leave to search elsewhere.
There are nonempty assortments of variants, so full enumeration is impractical. The retailer wants to know whether attention can be restricted to the popular assortments , the assortments made of the most preferred variants.
Timeline. Van Ryzin and Mahajan (Management Science 45(11), 1999, doi:10.1287/mnsc.45.11.1496) showed that, without search and with a cost derived from the newsvendor model, the profit change from adding a variant is quasi-convex in that variant's preference. As a consequence, the optimal assortment is a popular one. Cachon, Terwiesch and Xu (working paper 2002; Manufacturing & Service Operations Management 7(4), 2005, doi:10.1287/msom.1050.0088) extended the quasi-convexity to any concave increasing cost (Theorem 4 of the working paper), and then to search with independent assortments (Theorem 5). This mission formalizes Theorem 4.
Let be the possible variants. Variant has a preference ; in the paper , where is the variant's expected net utility and is the Gumbel scale. The no-purchase option has preference . With assortment , the MNL demand of variant is
Variant has margin (price minus purchase cost). Stocking it incurs an operational cost , where the cost function is concave and increasing on (the consumer population is normalised to , so demands lie in ). The profit of variant is , and the retailer's profit is .
Fix and a variant , and let . Treat 's preference as a variable. Write for variant 's demand with assortment , and for its profit. The loss on the variants already stocked is
and the net profit change from adding is . Adding is profitable exactly when . Write .
that is, every sublevel set is an interval. The goal holds for every concave increasing and every choice of margins, and assumes no differentiability.
The result. A quasi-convex function on an interval attains its maximum at an endpoint. So if adding a less preferred variant to is profitable, adding a more preferred variant (with ) is at least as profitable. With monotone margins, this exchange argument shows that an optimal assortment with variants consists of the most popular variants. The search for the optimal assortment then reduces from candidates to . The paper uses this structure again for the search model with independent assortments (Theorem 5) and in its analysis of a heuristic equilibrium (Theorem 8).
Formalizing it. The theorem is proved in the paper, and is not known to have been formalized anywhere. The mission produces a machine-checked proof for an arbitrary concave increasing cost, with per-variant margins. The paper's proof differentiates and writes a single common margin. A formal proof settles that neither assumption is needed. Van Ryzin and Mahajan's newsvendor-specific Lemma 1 is posed separately on Prove2Me (RetailVariety.Structure.lemma_1). It concerns a different function, a ratio on , and is not a special case of the statement here.
Adding changes every demand at once: 's own demand rises while all of 's demands fall, each through the shared denominator . The obvious approach is to show that is convex, and it fails: is in general not convex in , for example, when is linear and every margin equals some , is a positive multiple of the concave demand plus a constant. The paper's own argument goes through the derivative (6). It needs a derivative of , and its last step ("at most one with ") is literally false when the numerator of (6) vanishes on an interval, for instance when is linear with slope equal to a common margin, so that is constant. A rigorous proof must handle a non-differentiable concave , the endpoint where 's demand is , and a numerator that may be constant on stretches.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is not a variant: is a separate real, with and for all .RetailVariety.Structure.share (from RetailVariety.Structure.Model), with assortments as Finset (Fin n). is share applied to the preference vector with 's entry replaced by the variable, on insert j S, and is assumed.ConcaveOn ℝ (Set.Icc 0 1) c, MonotoneOn c (Set.Icc 0 1)). Nothing is assumed about , so .m : Fin n → ℝ are arbitrary reals. The monotone-margin assumption of §3 is not needed and not imposed.QuasiconvexOn ℝ (Set.Ici 0). The domain is the closed half-line, including .deriv c. The goal does not.The following formalizations would trivialize the problem and are ruled out: a specific cost (newsvendor, power, linear); convexity instead of quasi-convexity; only on ; or a common margin imposed without need.
Contributions welcome: proofs of the milestones, a proof of the goal that avoids derivatives, and general lemmas on quasi-convex functions of one variable and on the algebra of MNL shares, which the companion missions of this series (I and III–V) can reuse.
Treewidth measures how closely a graph resembles a tree. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) study an algorithm for producing tree decompositions. Its headline result is algorithmic; this mission formalizes one combinatorial lemma used in its analysis.
In §4.3.2, p. 349, the authors isolate a purely combinatorial fact, Lemma 4.3, which bounds the number of nodes of a rooted tree in terms of a measure placed on its nodes. They use it for the partial tree decomposition built by FindPartialTD, with a measure of the form . This mission formalizes Lemma 4.3 and the steps of its proof. The lemma is self-contained and does not mention graphs or treewidth.
A rooted tree consists of a finite vertex set , a root , and a parent map defined on such that every vertex reaches by iterating . If , then is a child of and is the parent of . A vertex without children is a leaf. The descendants of are the vertices with for some (including itself), and the subtree rooted at is the tree they span; is its number of vertices, and .
A measure is any function . Lemma 4.3 considers measures with three properties, for a constant :
Throughout, .
Under properties (i)–(iii),
Each step is stated for an arbitrary vertex of , with the subtree in the role of the paper's tree.
The result. Lemma 4.3 converts two local conditions, superadditivity of the measure over the children of each node and geometric decay by a factor along each parent–child edge, into a global linear bound on the size of the tree. Superadditivity alone does not bound the size: a long path with constant measure satisfies (i) and (ii). Decay alone does not either: a star with many leaves satisfies (iii). The counting principle can also be used when a recursive construction splits a resource among child nodes while reducing that resource along every edge.
Formalizing it. The lemma is proved in the paper. The mission produces formal statements of the lemma and the main bounds in its proof, over a published, reusable encoding of finite rooted trees by parent maps. A complete development would also establish structural facts about descendants and children that can be reused for other results about finite rooted trees.
The summed bound for the children's subtrees contains the term . When , superadditivity alone does not give the target's final : a path with constant measure is a counterexample if geometric decay is omitted. Formalization also has to account for the fact that the reusable tree representation is a parent map on a finite type, rather than an inductively constructed tree.
The rooted tree is the published definition HarelTarjan.Compressed.RootedTree: a finite vertex type V with a root and a total parent map in which every vertex reaches the root, with the convention . is Fintype.card V, and is the published subtree size size T v (the number of descendants of , including ). The local definition file adds IsChild T v c ( and ) and children T v; the condition removes the pseudo-edge , so the root is never its own child.
Conventions: is real valued, as on the page; property (ii) is a sum over a possibly empty set of children; the constant of property (iii) is a parameter with the two hypotheses and , because the conclusion is stated with that same . The fraction is real division, and the hypothesis keeps it away from Lean's convention . The bound keeps the page's "".
A trivializing formalization is ruled out explicitly: the parent–child relation is directed by the root, so property (iii) constrains each edge in one direction only. A symmetric reading (" for all adjacent ") would be unsatisfiable for and make every statement vacuous; the hypotheses here are satisfied, for example, by the two-vertex tree with and .
A complete development needs the decomposition of size T v as and an induction principle for parent-map trees. Both are reusable for statements about rooted trees given by parent maps, and contributions of them as separate lemmas are welcome. The paper's subsequent application is outside this mission's scope.
Classical mean field theory describes exchangeable diffusions, each interacting with the empirical average of all the others. As the particles become independent copies of a McKean–Vlasov process (propagation of chaos). Many systems of interest are not exchangeable. Particles sit at the vertices of a network and interact only with their neighbours, as in models of opinion dynamics, epidemics on contact networks, synchronisation of oscillators and systemic risk in financial networks. When the network is dense and its adjacency structure converges, the natural limit object is a graphon, a symmetric measurable function that encodes the limiting edge density between "positions" (Lovász, Large Networks and Graph Limits, 2012).
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) develop a law of large numbers for such systems. This mission formalizes their second main result, Theorem 3.1. Under cut-metric convergence of the interaction kernels, the empirical measure of the -particle system converges in probability to the averaged law of a continuum graphon particle system. Related work includes Bhamidi, Budhiraja and Wu (Stochastic Process. Appl., 2019) on weakly interacting particles on inhomogeneous random graphs, Coppini, Dietert and Giacomin (Stoch. Dyn., 2020) on Erdős–Rényi graphs, and Bet, Coppini and Nardi (arXiv:2006.07670) on oscillators on dense random graphs.
Write with Lebesgue measure and fix a horizon . Let with the uniform norm . On one probability space take independent initial states with laws and independent -dimensional Brownian motions , for all . The graphon particle system (2.1) for a graphon and Lipschitz coefficients is the continuum of nonlinear diffusions
where is the law of . Write for the path law of and for the averaged law.
The -particle system (3.1) places particle at label , starts it at , drives it by , and weights its interaction with particle by :
The weights come from a step graphon , constant on the squares of the -grid. Either , or are independent Bernoulli variables for , independent of the noise (Condition 3.1). The kernels converge in the cut norm . Two further norms appear: the operator norm , and the Wasserstein-2 distance on .
Assume the initial laws are measurable in with a uniform -moment and are Lipschitz (Condition 2.1). Assume is -continuous on each interval of a finite cover of (Condition 2.2(a)), and that Condition 3.1 holds with in the cut metric. Then
If, in addition, is continuous at for a.e. at each interior point of the cover (Condition 2.2(b)), then
In order: Remark 2.1, where cut-norm convergence implies operator-norm convergence; Theorem 2.1(a), continuity of in ; the weak-LLN bound (6.4); the discretization bound (6.11); Lemma 6.1,
Lemma 6.2, a law of large numbers for the continuum particles ; the approximation of by continuous graphons; the continuity (6.12) of in the graphon, in a corrected qualitative form; the empirical coupling bound for ; and (6.14).
Theorem 3.1 shows that the averaged graphon law is the correct macroscopic description of a dense heterogeneous particle system. This holds for deterministic weights and for Erdős–Rényi-type random weights, and the graphon may be discontinuous. It is the foundation for graphon mean field games and for control of large networked systems, where replaces the intractable -particle law. Under the regularity Condition 2.2(b) the convergence holds in , particle by particle, along the natural coupling.
The result is proved in the paper (§6.1–§6.2). Nothing in it is formalized. A formal proof would produce reusable infrastructure: graphons, the cut and operator norms, Lusin approximation of graphons, Wasserstein distances between empirical measures, and laws of large numbers for random probability measures on path space. It also needs pathwise stability estimates for SDE systems built on Itô integrals, which goes well beyond what Mathlib has today.
The particles are neither exchangeable nor identically distributed. The classical propagation-of-chaos argument compares each particle with an i.i.d. copy of one McKean–Vlasov process, and it does not apply here. Each must be compared with its own limit , and the error has two sources: the random or discretized weights , and the replacement of by . Cut-metric convergence controls only through integrals against bounded test functions. The interaction term, however, integrates the unbounded function against varying laws . When is merely measurable, the map need not be continuous, and the error of replacing by the average over the labels need not vanish. The direct estimate therefore fails for (3.3) without Condition 2.2(b), and this is the case the goal must cover.
The setting file GraphonMF.DenseLLN.Setting fixes these conventions:
Fin d → ℝ with the sup norm. All statements are invariant under this choice: constants are existential and the other conclusions are limits.Peng1990.SMP.IsItoProcess. The filtrations are the uncompleted natural filtrations and .WassersteinDRO.Duality.wassersteinDistance with values in .Two encodings would trivialize the targets, and both are ruled out. A pointwise or almost-sure reading of (3.3), or convergence of for a single test function, is not the claim. Choosing the constants of Lemma 6.1 and (6.11) after the sequence would make them nearly empty, so they are chosen before it. A sorry-free check confirms that the solution predicates are satisfiable: with the constant paths solve both systems.
Solvers will need several pieces of library work: the inequality , BDG-type moment bounds for the Itô integrals of Peng's library, Gronwall estimates, Lusin's theorem on , and the metrization of weak convergence on (Lévy–Prokhorov). Contributions to any of these are welcome independently of the goal. The paper's proofs are in its §5 (Theorem 2.1) and §6.1–§6.2 (Lemmas 6.1, 6.2 and Theorem 3.1).
Policy gradient methods optimize a parameterized policy for a Markov decision process by local search on its expected cost. The objective is nonconvex, so local search can in principle stall at a poor stationary point. Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods show that for a broad family of control problems this does not happen, and, in quantitative form, that the objective is gradient dominated: its suboptimality is bounded by a multiple of the size of its gradient. The multiple involves a single problem-dependent quantity, the effective concentrability coefficient , which measures how well the initial state distribution covers the states that matter for optimal behaviour. Theorem 2 and the convergence rates of Theorem 5 of the paper are only informative when is finite, so sufficient conditions for a finite are what make those results usable. This mission formalizes the paper's three such conditions (Theorem 4).
Distribution-mismatch coefficients of this kind go back to Kakade and Langford (2002), and appear in the analyses of approximate dynamic programming by Scherrer and Geist (2014) and of policy gradient methods in finite MDPs by Agarwal et al. (2021).
A discounted Markov decision process consists of a measurable state space , nonempty feasible action sets , a bounded measurable per-period cost , a transition kernel , a discount factor and an initial probability distribution on . A feasible measurable stationary policy () picks an action in every state. Its cost-to-go is the expected discounted cost from , its discounted state-occupancy measure is
and its average cost is . The Bellman operator acts on bounded measurable functions by
An optimal policy minimizes at every state; . A policy class is indexed by a convex set , and .
The effective concentrability coefficient (Definition 3) is the smallest scalar such that
with , and if no scalar works. It converts a -weighted Bellman error into a -weighted optimality gap.
If for every measurable set , then satisfies (13); equivalently
(a) If is finite and for all , then . (c) If is a contraction with modulus in a norm with , then .
The element-wise inequalities , (5); the performance difference identity (29); the sup-norm bound (26); the occupancy-weighted inequality from the proof of part (b); and the contraction step from the proof of part (c).
Theorem 4 is what turns the paper's gradient-dominance theorem into a usable statement: with part (b), the constant in Theorem 2 is bounded by the worst-case likelihood ratio between the optimal policy's state distribution and the initial distribution, a quantity that can be checked without knowing the policy class. Part (a) shows that in finite problems any fully supported initial distribution suffices, and part (c) gives a route through weighted norms, used in the paper for optimal stopping (Lemma 13).
The results are proved in the paper. None of them is machine-checked. The mission produces a general-state-space formalization of the discounted cost MDP (kernels, occupancy measures, Bellman operators, measurable selection) together with the performance difference identity on measurable state spaces; existing formal developments of policy gradient theory on the platform are for finite MDPs only. The occupancy-measure and Bellman-operator layer is shared with the other missions of this series.
The argument for part (b) is short on paper, but each step is a measure-theoretic statement about infinite-horizon objects. The performance difference identity (29) exchanges an infinite discounted sum with integration against the chain's laws and needs the occupancy measure to be built from the -step kernels of the controlled chain. The change of measure from to needs the Bellman error to be nonnegative and integrable; its measurability is not automatic, because is a pointwise minimum over uncountably many actions, and is supplied by the measurable selection assumption. Part (c) needs the fixed-point property of the optimal cost-to-go, which again rests on measurable selection.
All statements use one Lean layer: MDP S A with measurable spaces S, A (a generalization of the paper's Borel subsets of Euclidean spaces), the cost and kernel given on all of , measurable stationary policies MPolicy S A, and costToGo, occupancy, loss, bellmanPi, bellmanOpt. The paper prints the Bellman operators (3)–(4) without the discount factor; every later use includes it, and so does the formalization. The optimal policy is a binder πstar with IsOptimal M πstar. Assumptions 1 and 2 of the paper are standing hypotheses of every main statement.
The coefficient is never formed as a number: "" is the predicate IsConcBound M Θ πθ πstar X, which says that satisfies (13); because the right-hand side of (13) is nondecreasing in the scalar, the two are equivalent. Part (b) quantifies over every with setwise, which is equivalent to ; a real-valued essential supremum is avoided because it reads exactly when the paper's bound is infinite. Part (a) assumes for every state, since otherwise is on paper and in Lean. Part (c) requires the norm comparison (21) on all bounded measurable functions, as its proof uses it on and , and encodes "a norm" by subadditivity, the one property used.
A formalization in which (13) or the occupancy-weighted inequality is assumed, or in which is a junk value of an empty infimum, would make the goal trivial; neither is used.
Contributions are welcome on every milestone, in particular on the performance difference identity and the measurability of the cost-to-go and of , which are reusable for any discounted MDP on a measurable state space.
Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.
Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.
A Markov decision process consists of a state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial distribution . A policy is a measurable map with ; is the set of all of them. The cost-to-go is , the loss is , and the discounted state-occupancy measure is . An optimal policy has pointwise for all ; . With the Bellman operator , the weighted policy-iteration objective is
A parameterized policy class is for a convex , and . A point is stationary for if is differentiable at and for all .
The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages ; from a state in , , every feasible action leads to ; and is a costless absorbing state. The parameter is a concatenation , the parameter set is a product , and on the action depends only on . The stage objectives are .
Condition 4 asks that for every , the problem has no suboptimal stationary points. Assumption 3 asks that for every . Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.
Under Conditions 0, 3 and 4 and Assumption 3, if is an optimal policy for some , then every stationary point of on satisfies
Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go , which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.
The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.
The obvious approach reasons stage by stage directly on , but couples the stages: changing changes the distribution of states visited after stage . The paper's argument instead passes through the policy gradient theorem, which turns stationarity of into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve , while Condition 4 speaks about ; relating them requires a backward induction over stages in which almost-sure equality on stage is transported to stage through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than , to be equivalent to , which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).
The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. is never defined as an infimum: an optimal policy is a hypothesis, with . Stages and sub-vectors are numbered from by a measurable stage index and a block index on coordinates; the product structure of is encoded as closure under exchanging one block.
Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of on , the premise of Definition 1. The Bellman operators carry the factor omitted in the printed (3)–(4). The stage-wise balance equation is stated for ; the printed range fails at the absorbing state.
A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within . Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.
Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.
Taxi fleets, ride-hailing services and dial-a-ride systems assign incoming customer requests to vehicles under time constraints. Bertsimas, Jaillet and Martin (Online Vehicle Routing: The Edge of Optimization in Large-Scale Applications, Operations Research 67(1), 2019) model the online taxi routing problem, a special case of the online dial-a-ride problem with time windows in which a vehicle serves one customer at a time. They show that mixed-integer optimization over a sparsified graph can dispatch thousands of New York City taxis in real time. The offline problem, in which all requests are known in advance, is the building block of their online algorithms, and its structure determines which offline methods are fast.
The structural fact this mission formalizes is the paper's Theorem 1. When every customer has a fixed pick-up time, the mixed-integer formulation of the offline problem is integral: its linear relaxation has only binary extreme points. So the problem is a linear program in disguise, which the paper uses for its maxflow heuristic.
The source is the authors' accepted manuscript (March 2018, 46 pages); every page and display number below refers to that manuscript, not to the typeset article.
Let be a finite set of customers and a finite set of taxis. Customer has a pick-up time window , and taxi becomes available at time . For customers , the number is the travel time from serving to picking up , and is the profit earned when is served right after . The numbers and are the travel time and profit when is the first customer of taxi .
The graph has the customers and taxis as nodes. Between customers there is an arc exactly when
Taxi nodes have outgoing arcs only. Throughout the paper is assumed acyclic (§2.1, p. 7).
The mixed-integer formulation (5)–(14) (pp. 11–12) has binary variables (customer is picked up right after ), ( is the first customer of taxi ) and ( is served), and continuous pick-up times . It maximizes subject to the flow constraints
the binary constraints (9)–(11), and the time constraints
Constraints (13) and (14) are strengthened Big-M constraints: with , (13) reads .
The LP relaxation replaces (9)–(11) by . A formulation is integral when every extreme point of its LP relaxation has .
If for every customer (and is acyclic, the standing assumption), then
Three further statements from the same pages are included as plain theorems. The first is the paragraph after Theorem 1: a solution with fixed times is feasible for the formulation with windows. The other two are the conditions (3) and (4) of §2.1, which exclude 2-cycles and all cycles of .
Theorem 1 turns a mixed-integer program into a linear program when the time windows shrink to points. The fixed-time problem can then be solved by the simplex method or by a max-flow algorithm. By the paragraph after the theorem, any choice of times inside the windows then gives a feasible solution of the original problem. This is the maxflow heuristic, and the paper reports it to be near-optimal when windows are small. The theorem also locates the source of the integrality gap: the time constraints (12)–(14), not the flow structure.
The result is proved on the page, briefly. No machine-checked version exists. Formalizing it means making the page's "equivalent to a formulation in which variable is removed" precise. The extreme points of the relaxation in -space must correspond to those of a flow polytope in -space. The integrality of that flow polytope must then be proved, which the page settles by appeal to max-flow.
The reduction to the flow system is elementary linear arithmetic. The substance is milestone 3. The system (6)–(8) is not literally in the standard form of a network-flow problem: it mixes an equation defining with inequalities, has unit upper bounds, and allows arbitrary arc sets, including cycles and loops . Neither the integrality theorem for standard-form network flows nor total unimodularity can be applied without first exhibiting a network and checking that the polytope corresponds to its flow polytope. Mathlib has the definition of total unimodularity but not the Hoffman–Kruskal theorem.
The page's phrase "the formulations are equivalent" also hides a step: the goal speaks of extreme points in -space, while the flow system lives in -space, and the two notions of extreme point have to be related explicitly.
Set.extremePoints ℝ.Two trivializing readings are ruled out. "Integral" is the extreme-point property of the relaxation, not the existence of an integral optimum for a given objective, and not the integrality of the mixed-integer feasible set, which holds by definition. Integrality is never demanded of the continuous times .
A complete development needs an integrality theorem for flow polytopes with integer bounds, which Mathlib does not have. Such a result is reusable well beyond this mission. Contributions of general network-flow integrality lemmas are welcome.
Policy gradient methods search for a policy by changing a finite vector of parameters. The method can reach a stationary point of its objective without finding an optimal policy: a small change in the available parameters might not represent the policy improvement that the underlying control problem calls for. Bhandari and Russo identify a condition on the policy class that limits this obstruction. Their exact-closure result rules out suboptimal stationary points; their approximate-closure result measures the residual cost when the class can represent policy improvements only approximately. This mission formalizes the latter statement, Theorem 5 of Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods, using the arXiv v3 text and numbering.
The result concerns the optimization landscape rather than a particular gradient algorithm or convergence rate. It applies to structured policy classes in discounted control problems, including settings with general state spaces. The paper also discusses state aggregation as a source of small approximation error in Lemma 15; that example motivates the error condition, while the target here is the general guarantee of Theorem 5. The error is measured in the states visited by each current policy, so the condition describes what the restricted class can do where improvement affects that policy's performance.
A Markov decision process has a measurable state space , a measurable action space , and a nonempty feasible action set at each state . Choosing incurs a bounded cost and changes the state according to a probability kernel . A discount factor reduces future costs, and an initial probability measure specifies where evaluation begins. A stationary policy is a measurable choice .
The cost-to-go is the expected sum of discounted costs when starting at and following . The discounted occupancy measure is the normalized, discounted distribution of visited states when the initial state has law . The policy's objective is . The factor puts on the scale of a per-period cost. An optimal policy minimizes cost-to-go at every state. Section 2, pp. 5–8 supplies these objects and Assumptions 1 and 2: absolute continuity of with respect to , and measurable selection of a Bellman-minimizing action for bounded measurable value functions.
A parameter belongs to a convex set and determines a feasible policy . The policy gradient objective is . A stationary point is a feasible parameter with for every . The Bellman optimality operator selects the smallest one-step cost plus discounted future value among feasible actions. The weighted policy improvement objective evaluates the one-step Bellman update from a candidate policy , averaged under the current policy's occupancy measure. Section 5.1, pp. 12–14 introduces its smoothness and stationary-point conditions.
The target is Theorem 5, p. 26. Condition 5 says the restricted class has inherent Bellman error : for each current policy in the class, a class member gets within of the best one-step weighted Bellman objective over all feasible policies. Condition 2.A says stationary points of that weighted one-step objective are global minima over . Condition 0 supplies differentiability. For a nonnegative coefficient satisfying the effective concentrability inequality (13), the goal is continuous differentiability of and, at every stationary point,
The paper defines as the least coefficient satisfying (13). The Lean statement quantifies over an admissible ; its conclusion therefore includes the bound at when that coefficient is finite. The milestone list follows the paper's supporting statements: occupancy domination after (2), Bellman inequalities (5), the performance difference identity (29), the policy gradient formula in Lemma 6, the stationary policy-improvement identity in Lemma 7, and the Bellman-error bound displayed in the proof of Theorem 5.
The bound turns a property of the policy class into a quantitative guarantee about every stationary parameter. If and a finite concentrability bound applies, the stated cost gap is zero. For positive error, it separates the approximation error from the factor that reflects evaluation under the exploratory start distribution and the effective planning horizon. Thus a small gradient alone is not the claim; the structural conditions on the one-step objective and the policy class determine what stationarity means for long-run cost. Theorem 5 and its discussion, §8 make this interpretation explicit.
The paper proves Theorem 5. The declarations in this mission currently compile as open theorem statements; they are not machine-checked proofs. A complete development would formalize the links among discounted kernels, occupancy integrals, Bellman operators, and gradients on the parameter space. The general measurable-state MDP definitions would be reusable for other discounted control results, while the stationary-point and approximate-closure predicates provide a vocabulary for further policy-gradient theorems.
A stationary point of need not be a minimum of the one-step Bellman objective by definition. Condition 0 and Lemma 6 connect their gradients, and Condition 2.A then links stationary points to minima of the restricted one-step objective. Approximate closure only compares that restricted minimum with the unrestricted one up to . The final result also requires moving an error measured under to one under and relating Bellman residual to the optimality gap. Each comparison has a distinct measure or operator, and losing a discount factor changes the constant in the theorem.
The Lean model uses arbitrary measurable spaces for and and measurable stationary policies, extending the paper's Borel-subset setting. The cost and kernel are defined on all and are uniformly bounded there; feasibility still restricts every policy and Bellman minimization to . These extensions let Condition 0 evaluate nearby parameter values even when their policies need not be feasible. The representation uses Mathlib kernels, measures, Bochner integrals, and Euclidean parameter vectors. It fixes , a probability initial distribution, nonempty feasible action sets, an optimal policy, and the paper's Assumptions 1 and 2. The goal carries a nonnegative concentrability coefficient and Conditions 0, 2.A, and 5; it does not assume exact closure or the Bellman-error conclusion it is meant to establish.
Two corrections to the printed assumptions are explicit. The Bellman operators contain , consistently with equations (6) and (7), although displays (3) and (4) omit it. Condition 0 asks for joint continuous differentiability near the current parameter pair, the form used by the proof of Lemma 6; the printed condition lists two partial maps. The theorem's is constrained to be nonnegative to represent the paper's effective concentrability coefficient. Definitions use pointwise optimality rather than a real-valued infimum over policies, and Bellman minimization uses the nonempty feasible-action subtype. These choices prevent default values of ill-bounded infima or non-integrable functions from turning the target into an empty claim. The needed contributions are proofs of the six milestones and the final bound, plus supporting measurable-kernel and gradient facts.
Classical Markov decision theory minimizes expected cost. A decision maker who dislikes variability, such as an insurer, a portfolio manager or an operator of a service system, may instead evaluate a random cost by its certainty equivalent for an increasing utility (disutility) function . Bäuerle and Rieder (More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014; authors' manuscript at KIT 1000039663) develop dynamic programming for this criterion with general . Classical risk-sensitive MDPs, studied since Howard and Matheson (1972), use the exponential utility, and for it the average cost problem differs considerably from the risk-neutral one (Cavazos-Cadena and Fernández-Gaucherand 2000; Di Masi and Stettner 1999). Their §5 asks what happens in the long run. The average cost per stage is evaluated through a power utility . Does risk sensitivity change which stationary policy is optimal?
This mission formalizes their answer, Theorem 5.2, and the results its proof uses (manuscript p. 17).
A controlled Markov process in discrete time has a standard Borel state space and action space . A measurable set lists the admissible state–action pairs, and every is nonempty. A transition law gives the distribution of the next state, and a measurable cost satisfies on .
A history-dependent policy chooses the action measurably from the past. The set of all such policies is . Each and initial state determine a probability measure on trajectories, with and . The accumulated cost is .
A stationary policy uses a measurable decision rule with at every stage. Under it, is the Markov chain with kernel .
Fix and . The risk-sensitive average cost (5.1) and its optimal value are
The risk-neutral average cost is , the case .
A Markov chain is Harris recurrent if, for some nonzero -finite measure , every set with is visited infinitely often almost surely from every starting point. It is positive Harris recurrent if it also has an invariant probability measure (Meyn and Tweedie 2009, §§9–10). The MDP is called positive Harris recurrent if the state chain of every stationary policy is.
Let and let the MDP be positive Harris recurrent. If satisfies for all and , then
The optimal policy does not depend on .
The result. Theorem 5.2 reduces a risk-sensitive long-run problem to a classical one. Under positive Harris recurrence, any stationary policy that is optimal for the expected average cost, for instance one obtained from the average-cost optimality equation, is also optimal for every convex power criterion , simultaneously. Theorem 5.1 explains why: along a positive Harris recurrent chain the empirical average cost converges almost surely to a constant, so in the limit the power utility sees no randomness at all. The contrast is with exponential utility, where the risk-sensitive average cost generally differs from the risk-neutral one and leads to a multiplicative Poisson equation. Positive homogeneity of the utility is what removes the risk effect.
Formalizing it. The results are proved in the paper. As far as is known they have no machine-checked proof, and the platform has no strong law of large numbers for Harris chains on general state spaces. The mission produces a Borel MDP with history-dependent policies and Ionescu-Tulcea path measures, a reusable definition of (positive) Harris recurrence for an arbitrary Markov kernel, and a formal comparison of risk-neutral and risk-sensitive average costs. Each milestone is a self-contained target.
Milestones 1 and 3 are elementary once the expectations are handled correctly: holds only almost surely, and Jensen's inequality has to be applied with real powers. The central difficulty is Theorem 5.1. It needs the ergodic theorem for positive Harris recurrent chains, almost surely from every initial state (Meyn and Tweedie, Theorem 17.0.1). It also needs an identification of the state process under with the canonical chain of . The natural first idea, to quote a convergence theorem in total variation, fails: positive Harris recurrence allows periodic chains, for which need not converge. Pathwise averages converge, marginal laws need not, and the argument has to work with the former.
Kernel.trajMeasure on . Stationary policies act through .Real.rpow. For all terms of the sequences lie in , so real limits superior are meaningful. The term (Lean's ) is irrelevant.Contributions are welcome at every level. Reusable pieces, such as the identification of the state process with the chain of , the strong law for positive Harris chains, or bounded-convergence lemmas for path measures, are valuable beyond this mission.
When a controller acts on a system whose state is hidden, measurements may help it choose later actions, but the value of those measurements depends on the transition law, the observation mechanism, and the available controls. Åström's 1965 paper gave a finite-state formulation of this problem and compared the best expected loss under incomplete measurements with two limiting cases: exact state observations and no useful observations. The comparison, stated in (5.12), quantifies the value of the information available to the controller without requiring a particular numerical example. Åström, 1965.
The bounds are useful when an exact partially observed policy is difficult to calculate. The complete-information problem provides an optimistic benchmark, because a controller that sees the hidden state can condition its decision on more information. The open-loop problem provides a conservative benchmark, because it commits to a control schedule without responding to later measurements. Both auxiliary problems have simpler backward equations than the partially observed problem, as Åström notes in §V of the paper. Åström, 1965, pp. 190–193.
The hidden state belongs to a finite nonempty set , and the measured output belongs to a finite nonempty set . There are decision stages. At stage , a control is chosen from a nonempty compact set . Given state and control , the next state is with probability . At state , the observed output is with probability ; observations are conditionally independent given the state path. The stage loss is , with no fixed sign, terminal loss, or discount. The transition probabilities and loss are continuous in the control. Åström, 1965, §II.
An admissible control law may use the whole output history when choosing . Write for its expected total loss, computed from the joint law of the state and output paths, and write for the infimum of over every such admissible law. The distribution of is . After the first output , the belief is the conditional distribution of . More generally, is the conditional distribution of given outputs through time , when that history has positive probability.
Three backward values describe the information regimes. The partial-observation value obeys the Bayesian recursion (3.28). The complete-information value is the linear extension of the statewise recursion (5.4). The open-loop value obeys (5.7), in which the belief moves by prediction through without using an output. Each recursion has terminal value zero at . Åström, 1965, pp. 184, 190–191.
Theorem 2 identifies the partial-observation value with the original control problem: a selector attaining the minimum in (3.28) exists, and every such selector yields an admissible feedback law attaining . Theorem 4 gives the complete-information lower bound , and Theorem 5 gives the open-loop upper bound for every probability belief and every stage . Both inequalities apply to a general observation matrix. Åström, 1965, Theorems 2, 4 and 5.
The goal is the paper's expected-cost comparison (5.12), with its middle term explicitly identified as the minimum of the original problem:
Here the expectation is over the first measured output under and . An output with probability zero contributes zero. The left and right members represent, respectively, the costs with perfect state information and with no useful measurements. Åström, 1965, (5.12), p. 193.
For any model satisfying the stated finite-state assumptions, the two easier dynamic programs bracket the best achievable expected loss with partial information. The differences between these values are the paper's measures of the value of perfect state information and the value of incomplete state information, described immediately after (5.12). Because the loss may have either sign, these are order comparisons of minimal costs rather than bounds that depend on a nonnegativity convention. Åström, 1965, (5.13)–(5.14).
The mathematical result was established in the paper. This mission asks for machine-checked proofs of its finite-path model, the three value recursions, the identification of P.1's minimum, and the information bounds. The value functions are linked by shared definitions, so later finite-state partially observed control developments can reuse the pathwise cost and Bayes update instead of rebuilding them for each theorem.
The tempting comparison between the three Bellman equations cannot simply replace the posterior belief by its average: the controller may choose different actions after different observations, and the continuation value is generally nonlinear in the belief. The exact-information case must also be read at beliefs concentrated at a single state. Its value formula is linear in an arbitrary input belief by definition, but the partial-observation value need not equal that linear function away from those state vertices. A second issue is connecting a feedback solution of (3.28) to the original expected loss over all output-history laws; using a belief-defined objective at the outset would assume the identification that Theorem 2 establishes.
The Lean model uses finite state, output, and horizon types, a nonempty compact control set in , stochastic transition and observation rows, and continuous dependence on controls where the paper requires it. All probabilities and expectations are finite sums and products. A Fin N index of zero represents paper time one. The model starts from the law of , since §II introduces the law of but specifies neither a control at time zero nor the transition to . The transition controlled at time is therefore written with the paper's transition index . These conventions make the first-output expectation and (3.22) use the same timing.
The norm of is its norm, the sum of absolute coordinates. At an impossible output, Lean's totalized posterior is zero; the associated continuation term has weight zero. Conditional-probability claims apply only to positive-probability histories. Each minimum over controls is represented by a real infimum over . The compact control set is nonempty and the continuous costs are bounded on it, so this has the intended finite attained meaning on probability beliefs. The terminal values , and are zero.
The original objective is a separate pathwise expected cost, minimized over all admissible output-history laws. The target includes its equality with ; stating only an inequality between three unrelated Bellman solutions would omit the subject of (5.12). Reusable contributions include finite-path probability identities, the Bayes recursion, attainment for continuous control minima, and the three value comparisons. No special observation matrix is assumed in Theorems 4, 5, or the goal.
Approximate message passing (AMP) is an iterative method for large systems with random matrices. At each step, every coordinate receives a weighted combination of nonlinear messages from all other coordinates, together with a correction for dependence created by earlier steps. For symmetric random matrices, the correction makes a simple description of the high-dimensional iterates possible: a finite collection of covariance matrices predicts their limiting distributions. Bayati, Lelarge and Montanari prove this state evolution statement for polynomial AMP on a broad class of independent sub-Gaussian matrix entries, rather than only Gaussian entries (paper, §§1.2–1.3). It gives a precise distributional account of an algorithm whose coordinates are coupled at every iteration.
The paper has three distinct headline results. Its Theorem 3 compares AMP moments under two matrix laws with equal entry variances, and its Theorem 2 concerns projected cross-polytopes. This mission targets Theorem 4, which identifies the limit of empirical averages of AMP iterates with a Gaussian expectation. The companion missions address the other results; the statements here use their own copy of the paper's AMP model because draft definitions cannot yet be imported across proposals (paper, pp. 5, 8–9).
For each size , let be a random symmetric matrix with zero diagonal. Its entries above the diagonal are independent, centered, and sub-Gaussian at scale . Each coordinate carries a polynomial map at iteration and an initial vector . Their coefficients have degree at most and a uniform bound . The AMP orbit is
The second sum is the Onsager memory term; it is absent at . Here is the Jacobian, so its product with the preceding -vector is another -vector. The initial vectors obey an exponential bound on their squared Euclidean norms. These assumptions form the paper's -regularity condition (Definitions 2–4, pp. 6–7).
A converging sequence has a fixed finite set of classes . Coordinate belongs to for one class , whose proportion approaches . A symmetric nonnegative matrix specifies entry variances: if and , then . Independent labels have class-dependent laws , each a finite mixture of Gaussian laws that may be degenerate. The polynomial maps have the common form for (Definition 5, pp. 8–9).
The empirical second moments of converge in probability to a prescribed positive semidefinite matrix . For , state evolution defines
where is independent of . The index in the first formula and in the second are essential (equations (1.9)–(1.11), p. 9).
For a nonnegative multi-index and a coordinate sequence eventually in class , Proposition 4 identifies the Gaussian limit of each moment. Proposition 5 says the variance of the class-average monomial tends to zero:
The diagonal two-time identity (4.4) is another milestone: has four blocks, each equal to . These are the paper's stated intermediate targets (pp. 15, 30, 32).
For , class , and every locally Lipschitz function with for some , prove convergence in probability:
The target covers polynomial-growth test functions, including functions beyond monomials. The expectation on the right is under the product law of the Gaussian state and the independent class label (Theorem 4, p. 9).
The theorem assigns a computable asymptotic distribution to each class of AMP coordinates at every fixed positive iteration time. It can be used to evaluate empirical observables without tracking the full coupled -dimensional random trajectory. The class weights and variance profile permit heterogeneous coordinates, while the sub-Gaussian assumption covers more matrix laws than a Gaussian-only statement (paper, Introduction and Theorem 4).
The paper proves this result. The mission's Lean statements are compilation-checked targets, with proofs still to be formalized. A completed development would establish the measure-theoretic meaning of the covariance recursion and its Gaussian expectations, as well as the moment and concentration claims needed for the empirical limit. The polynomial representation, random-matrix regularity predicate, and Gaussian transport are reusable for other AMP results from the same paper.
The matrix is reused at every AMP iteration, so a new coordinate is correlated with earlier coordinates and with the matrix entries that produced them. A direct independent-summand argument for its Gaussian limit is unavailable. The memory term is tuned to this dependence, and any formal proof must account for its exact Jacobian and squared-entry form. Passing from individual moments to empirical averages also requires control of correlations between different coordinates. The target allows locally Lipschitz functions with polynomial growth, so convergence for a fixed monomial alone does not finish the job (paper, §4.7).
Vectors in are functions Fin q → ℝ; squared Euclidean norms are explicit sums of coordinate squares. Polynomials use bounded real coefficient arrays as in (4.10), with an explicit Jacobian. Fin N uses zero-based indices. The orbit stores the current and preceding iterates and omits the memory term at . A single probability space carries all sizes; matrix entries, labels, coefficients, and initial vectors have explicit measurability and independence conditions.
The paper's displayed sub-Gaussian formula conflicts with its stated scale, so the model uses the scale required by its moment estimates and imposes the moment-generating bound for all real arguments. Its initial exponential bound is read almost surely at every size, which ensures the expectations used by the paper are well-defined. Label-dependent polynomial coefficients are measurable. The full label vector is independent of the matrix and initial vectors; this makes explicit the independence needed for Theorem 4's Gaussian-label product law. Independence of the induced polynomial coefficients alone would not imply it when ignores part of a label. The initial covariance limit is entrywise convergence in probability; finite-dimensional equivalence makes this the same matrix convergence. Class averages divide by the class cardinality, even though that expression has Lean's default value at an empty class for a small . Positive limiting class fractions make those finite exceptions irrelevant.
Gaussian laws live on Mathlib's Euclidean space and are transported to coordinate vectors. Theorems explicitly assert positive semidefiniteness or integrability where a non-PSD covariance, non-integrable expectation, or non-square-integrable variance could otherwise give a default value. The source's in (1.12) is read as , its summation index, and its final covariance as . The Gaussian covariance is computed by the recursion above; it is not defined from the proposed limit. Contributions establishing moment bounds, covariance positivity, Gaussian integrability, the three milestones, or the full Theorem 4 are within scope.
Policy gradient methods optimize a parameterized policy for a Markov decision process by running gradient descent on its expected cost. They underlie most large-scale reinforcement learning, from robotics to game playing, and are also natural in operations research, where structured policy classes (linear feedback, base-stock levels, thresholds) are standard. The objective, however, is almost never convex in the parameters, and classical theory only promises convergence to stationary points. Whether such methods find optimal policies therefore depends on the landscape: whether stationary points can be suboptimal.
J. Bhandari and D. Russo (arXiv:1906.01786v3, published in Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which the answer is no, connecting policy gradient to classical policy iteration. Fazel et al. (2018) established a landscape result for linear-quadratic control; Kakade and Langford (2002) developed a performance-difference identity for conservative policy iteration on finite MDPs. Bhandari and Russo's Theorem 1 gives a general sufficient condition on a general state space; Agarwal et al. (2021) developed the tabular case in detail.
A Markov decision process is a tuple : a measurable state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial probability distribution . A policy is a measurable map ; it is feasible, , if for every .
For a policy , the cost-to-go is the expected discounted sum of costs started from . The discounted average cost is , and the discounted state-occupancy measure is . The Bellman operators are
An optimal policy satisfies pointwise for every . Two standing assumptions hold throughout: Assumption 1, (the initial distribution is exploratory), and Assumption 2, measurable selection of a minimizing action in .
A parameterized policy class is with convex, and is the policy gradient objective. A point is stationary if for all . The weighted policy-iteration objective is
the cost of following for one period and then incurring , averaged over .
The three conditions of the main theorem are:
Under Conditions 0, 1 and 2.A, is continuously differentiable, and for every
The right side compares with the optimum over all feasible policies, not only the class.
Theorem 1 converts a question about a nonconvex, multi-period objective into checks on single-period problems. Any algorithm that provably reaches stationary points (projected gradient descent, for instance) then reaches globally optimal policies whenever the policy class is closed under improvement and the one-step problems are benign. The paper verifies the conditions for LQ control, finite MDPs with softmax policies, optimal stopping with threshold policies and inventory control with base-stock policies; the quantitative refinements (gradient dominance, approximate closure, finite horizons) are the subject of the later missions of this series.
The result is proved in the paper; nothing in it has been machine-checked. A formalization would produce a measure-theoretic library for discounted MDPs on general spaces (cost-to-go via kernels, occupancy measures, Bellman operators, the performance difference identity) that is reusable well beyond this paper, and would pin down the exact differentiability hypothesis the argument needs.
The obvious route, differentiating directly, requires differentiating an infinite discounted sum of -step kernels in the parameter, and on a general state space that derivative is not available without regularity of the transition law. The performance difference identity demands an exchange of an infinite series with integrals against composed kernels, and measurability of every object involved, including , which is measurable only through the selection assumption. The stationary-implies-optimal direction must pass from an inequality weighted by to one weighted by , and then to , where Assumption 1 enters.
and are arbitrary measurable spaces; the paper takes Borel subsets of Euclidean spaces, a structure no argument uses. The cost is bounded and, with the kernel , defined on all of : Condition 0 differentiates at parameters near , where need not be feasible. Policies are deterministic, stationary and measurable; randomized policies are covered by taking actions to be probability vectors. is the Euclidean space, gradients are Euclidean, and is convex (not assumed closed).
Conventions committed to in Lean:
The goal does not assume that contains , the equation of Lemma 7 or the conclusion of Lemma 8; a formalization that takes any of these as a hypothesis trivializes the theorem.
A complete development needs the composition of kernels, interchange of series and integrals for bounded functions, the fixed-point identity , the performance difference identity, the first-order optimality condition on a convex set, and the chain rule for a jointly function along the diagonal. The MDP layer, the identity (29) and the element-wise inequalities are reused by the other missions of the series. Proofs of the milestones, and proofs of the identity (29) in isolation, are welcome.
Large interacting diffusion systems often have different interaction strengths between different pairs of agents. A graphon gives a continuum description of such weighted networks: each agent carries a label in , and a kernel assigns the strength of interaction between two labels. The question in this mission is whether the law of the resulting continuum stochastic system changes continuously when its graphon changes. This matters when a large finite network is represented by an approximate graphon, since an approximation of the network should lead to an approximation of the dynamics. Bayraktar, Chakraborty and Wu establish this stability as Theorem 2.1(c) of Graphon mean field systems.
The paper also studies dense and less dense finite-particle systems. Their convergence results use a limiting graphon particle system even when the limiting kernel is only measurable, with no continuity in the labels. Theorem 2.1(c) is the continuity result that makes approximation by simpler graphons useful in those later sections Bayraktar–Chakraborty–Wu, §§3–4.
Let , fix a time horizon , and let be the space of continuous paths with the uniform norm . A graphon is measurable and symmetric. Its cut norm is the largest absolute integral of over a measurable rectangle . For two graphons, their cut distance is the cut norm of their difference.
For each label , an initial state and a -dimensional Brownian motion live on one probability space. Initial states are mutually independent, Brownian motions are mutually independent, and the two families are independent of each other. The initial state has law . The process evolves with a drift obtained by averaging first against the time- law of and then over . Its diffusion coefficient averages the matrix-valued in the same way and drives . This is the graphon particle system (2.1) Bayraktar–Chakraborty–Wu, p. 3591.
Condition 2.1 requires measurable initial laws, a uniform moment for some , and a common global Lipschitz bound for and . The path-law family belongs to when it is measurable as a family of probability measures on and has uniformly bounded second moments. The distance between path laws uses the supremum norm through time ; is the supremum of these distances over labels Bayraktar–Chakraborty–Wu, pp. 3591–3592.
For graphons converging to in cut metric, let and be the laws of the associated solutions, with the same initial laws and coefficients. The target is
The conclusion is an integrated law convergence statement. It does not assert that the laws converge uniformly in or that paths converge almost surely. This is precisely Theorem 2.1(c) Bayraktar–Chakraborty–Wu, p. 3593.
The mission also states the paper's cut-to-operator convergence (Remark 2.1), existence of frozen-flow solutions (5.2), the squared estimate established in the proof of (5.3), well-posedness and moments for the nonlinear system (Proposition 2.1), and the quantitative stability display on p. 3604. These are the source's claims used to reach the target, with their provenance attached to each milestone Bayraktar–Chakraborty–Wu, §§2 and 5.
Stability shows that the continuum model is robust to graphon approximation in a metric natural for dense networks. Together with Proposition 2.1, it gives a well-defined solution-law family whose dependence on the network kernel can be controlled. The paper uses this framework in its later laws of large numbers for finite interacting systems Bayraktar–Chakraborty–Wu, §§3–4.
The theorem is proved in the paper; this mission asks for a machine-checked proof of the faithful statements. A complete development would also supply reusable Lean interfaces for graphons, cut and operator norms, measurable families of path laws, and stochastic systems whose coefficients depend on those families. The Itô-process and general Wasserstein definitions already available as published modules are reused. The remaining graphon-specific definitions and the estimates in §5 are open proof targets.
A direct stability argument for stochastic differential equations would compare the two coefficients point by point. Cut convergence does not provide pointwise convergence of to , nor a uniform bound on their difference that tends to zero. The drift and diffusion also contain laws generated by the processes being compared, so a change in the graphon feeds back into the law family. The central challenge is to control these coupled differences using only a weak kernel metric while retaining the measurable structure needed to integrate over labels Bayraktar–Chakraborty–Wu, §5.2.
The result also depends on a well-posedness theory for a continuum of stochastic equations. The laws need to vary measurably with even though the paper does not assume the sample paths themselves vary measurably with Bayraktar–Chakraborty–Wu, Remark 2.3(b).
Lean uses unitInterval for , nonnegative real time, and continuous maps from to Fin d → ℝ for . The norm on is the sup norm; the paper's Euclidean norm is equivalent in finite dimension, so existential Lipschitz and stability constants may change while the qualitative claim remains the same. The diffusion coefficient is a matrix, measured through its entries. Wasserstein quantities and nonnegative expectations are valued in , avoiding defaults for infinite moments. The path-law family uses the measurable space of measures, with the Borel space on paths. A zero-time or zero-dimensional state space is admitted where the formulas still have their stated meaning; and are explicit.
For each graphon, a solution is a continuous-path process driven by the same given initial variables and Brownian motions, adapted to the natural filtration of those variables for each label. Its path map is almost everywhere measurable, its law family belongs to , and the nested interaction integrals are required to be integrable. These clauses prevent a zero measure from arising through a nonmeasurable pushforward and prevent a nonintegrable Bochner integral from silently evaluating to zero. The graphons are explicitly measurable, symmetric, and -valued, so the real cut and operator norms are used only on bounded kernels. The theorem also asserts measurability of each Wasserstein integrand, reflecting the paper's treatment of the displayed integral.
The paper's proofs are in §§5–7; this mission concerns §5. Contributions to any stated milestone and to the reusable measure and Itô lemmas needed for them are welcome. A formalization that assumes the stability limit, that treats arbitrary unbounded kernels as graphons, or that uses an empty solution class would not establish this target.
An online decision maker repeatedly chooses an action, observes an outcome, and receives a reward. In a Bayesian model, an unknown parameter controls the outcomes, and the decision maker begins with a prior distribution for that parameter. Thompson sampling acts by drawing a parameter from its current posterior distribution and choosing an action that would be best if that draw were correct. This makes it applicable when an agent can simulate a plausible model and optimize an action for that model. Russo, Van Roy, Kazerouni, Osband, and Wen explain this rule for general online decision problems in Section 4 of their tutorial.
The tutorial's Section 8.1.2 asks how to analyze the rule's expected regret. An upper confidence bound method chooses an action using an optimistic score and can analyze regret through the score's optimism and its uncertainty width. Thompson sampling does not choose its actions by maximizing such a score. Yet the tutorial shows that any score computed from the observed past can be used to split Thompson sampling's expected regret into the same two types of terms. The result is stated on pp. 72–73, equation (8.4) and the display that follows.
Let be a finite, nonempty set of actions, a finite set of outcomes, and a measurable parameter space. A prior probability measure is placed on the unknown parameter . If action is selected, the outcome is sampled from a probability kernel on . A known function turns an outcome into a reward. The mean reward of action under parameter is
For each , choose an action maximizing . This choice uses a fixed tie-break and is measurable. The same selector is used throughout the mission. A length- history records the first action–outcome pairs. A policy assigns an action distribution to every such history. The prior, the policy, and the outcome kernel together determine the law of all histories: first draw from , then choose each action from using the past history, and finally generate its outcome using .
After history , the posterior law of is obtained by reweighting the prior by the likelihood of the observed outcomes. Thompson sampling draws a parameter from this posterior and plays the selected optimum for that parameter. Thus the law of its next action, given , is the posterior law of given . The policy remains defined even for a history with zero likelihood; choices there do not affect expectations.
For a period , let be any real score that uses the action and the observed history . The score is fixed before the period's outcome or the unknown parameter can be inspected. The period regret is , with expectation taken over the prior, the policy's randomization, and the outcome process.
The first target makes posterior sampling precise. For every feasible history and action , the probability that Thompson sampling next plays , together with observing , equals the joint probability that the selected optimum is and the history is . Consequently, for every history-determined ,
This is equation (8.4) on p. 72. It asserts equality of unconditional expectations while preserving the fact that may depend on the past. It does not assert that and have the same joint law with .
The goal is the full chain of equalities displayed on p. 73:
The theorem holds for every score determined by the past history. In particular, need not be a confidence bound for the identity to hold. Being a useful upper confidence bound matters when one later estimates the two terms.
The equality permits analyses built around optimistic scores to be transferred to Thompson sampling. It separates expected regret into a term measuring whether the score falls below the true optimal mean and another measuring the gap between the score and the true mean at the sampled action. The tutorial cites Russo and Van Roy for the surrounding regret bounds; the identity here is the precise bridge used in that discussion.
The result is already proved in the tutorial. This mission seeks a machine-checked proof of its finite-action, finite-outcome form, including the posterior-sampling law, the policy-dependent history distribution, and the conditioning behind equation (8.4). The goal and milestones are open Lean statements, not completed machine-checked proofs. Their definitions can be reused in later finite Bayesian decision models with a general measurable parameter.
The central issue is that and are not interchangeable inside an expression that depends on . The sampled action and the selected optimum have the same distribution after conditioning on the observed past, but generally have different dependence on the true parameter. For example, replacing by would make the claimed equality false. A formal proof therefore has to respect the boundary between history-derived scores and parameter-dependent quantities, and it must use the same history law to interpret every expectation. Histories of zero probability also require a consistent posterior convention.
The Lean model uses finite action and outcome types and a general measurable parameter type. This is a disclosed specialization of the tutorial, which also allows infinite actions and more general outcome spaces. The kernel is nonnegative, sums to one over outcomes, and is measurable in . The prior is a probability measure. The reward function is real valued and bounded because its domain is finite. The optimal-action selector has measurable fibers and maximizes the mean reward for every parameter. These conditions make the integrands measurable and bounded, avoiding default values of nonintegrable Lean integrals.
Histories are functions from a finite period index to action–outcome pairs. Policies are normalized, nonnegative behavioural action probabilities. The likelihood of a history multiplies both its policy action factors and its kernel outcome factors. The posterior uses only outcome likelihood factors, which give the Bayes update on every positive-evidence history. The Thompson-sampling predicate enforces the posterior action probabilities on those histories and permits any normalized policy on impossible ones. Lean period denotes the tutorial's period .
The shared tie-break is essential: Thompson sampling and use the same selected maximizer. The score has type , so it cannot inspect or the current outcome. No definition is allowed to supply regret or the decomposition as a predetermined constant; the expectation is built from the prior, policy and outcome kernel. The development needs reusable definitions for the Bayesian model, finite histories, behavioural policies, likelihoods, posterior masses, and the two regret terms. Contributions proving probability matching, equation (8.4), and the final identity are welcome.
Policy gradient methods for Markov decision processes are frequently run on a regularized objective rather than on the cost of interest: a convex penalty on the action distribution is added to every single-period cost. Regularization smooths the problem, makes optimal policies strictly stochastic, and keeps iterates away from the boundary of the probability simplex, where gradients of common parameterizations vanish. Entropy and relative-entropy penalties are standard in this role; a unified treatment of regularized MDPs is given by Geist, Scherrer and Pietquin (2019), and Agarwal, Kakade, Lee and Mahajan (2021) analyse policy gradient with a log-barrier penalty added to the softmax objective.
Regularization changes the problem being solved. Anyone who uses it needs a quantitative answer to one question: how suboptimal, for the original costs, is a policy that is exactly optimal for the regularized costs? Bhandari and Russo (arXiv:1906.01786v3), whose main results establish that policy gradient objectives have no suboptimal stationary points under a closure condition, answer this question for a relative-entropy regularizer in finite MDPs (their Lemma 10). Bounds of this type for the negative-entropy regularizer are in Geist et al.; as Bhandari and Russo note (p. 20), those bounds do not apply to the unbounded log-barrier regularizer used here.
The state space is finite. There are deterministic actions , and an action is a probability vector . A policy chooses at each state; is the set of all such policies. Transitions are linear in the action,
where each is a probability vector. Each state has a nonnegative cost vector . For , the regularized cost is
where is the uniform distribution. The divergence is unless every , so takes values in .
Given a discount factor and an initial distribution , the discounted average cost of a policy is
is the unregularized cost. The discounted occupancy of is . and denote the optimal cost-to-go and state-action cost-to-go of the unregularized problem. The constant of the result is
If with , then
The result. Lemma 10 says that the price of regularization is of order as , with an explicit constant depending only on the cost scale and the effective horizon . Together with the paper's landscape results (Example 4 shows the regularized policy-iteration objective is strongly convex and the policy class is closed under policy improvement, so the regularized objective is gradient dominated), it turns convergence of first-order methods on the regularized problem into near-optimality for the original problem, and it gives a principled rule for choosing as a function of the target accuracy. The bound holds for the log-barrier (relative entropy from the uniform distribution) regularizer, which is unbounded on the simplex, a case the negative-entropy analyses do not cover.
Formalizing it. The result and its proof are published (arXiv:1906.01786v3; Operations Research, 2024). No machine-checked proof of Lemma 10 or of its steps is known. The mission produces Lean statements of the lemma and of the four steps of its proof, built on a published finite-MDP layer, and invites proofs. Step 2 relies on the duality-gap bound for log-barrier problems from interior-point theory, which the paper cites from Boyd and Vandenberghe; a formal proof of that bound (in the simplex case) is reusable for any log-barrier analysis.
The first idea, comparing with an unregularized optimal policy , fails: is typically deterministic, so and , giving no information. The comparison policy has to be built by hand: it must be strictly stochastic, nearly optimal for the unregularized problem, and have bounded divergence from the uniform distribution at every state. Each of these three properties is a separate argument: a duality-gap bound for a barrier problem on the simplex, a propagation of a one-step Bellman inequality to the whole horizon, and a quantitative lower bound on the smallest action probability of the barrier minimizer.
A second pitfall is the printed form of the lemma, whose right-hand side is ; since gives , that inequality is trivially true. The proof establishes, and the text on p. 20 announces, the bound against , which is the goal here.
States and deterministic actions are finite types S and I (nonempty, as on the page, so that is defined); . Policies, transition kernels, the occupation distributions, the cost-to-go and come from the published FoundationsML.ReinforcementLearning layer (IsPolicy, IsTransitionKernel, OccupationDist, PolicyValue, QFunction), with the cost vector passed in the reward slot: PolicyValue is a plain discounted sum, so this is the cost-to-go. Optimality is the cost-minimizing notion, defined locally.
, and take values in , with off the open simplex; real-valued junk such as never stands in for , and is never coerced to (that would make boundary policies look optimal). At the convention gives , and Lean's makes the goal's bound , the limit of the page's bound. is written as " for every policy ". The minimizer is a hypothesis (any minimizer); the barrier-greedy policy of (36) appears only in the milestones, never in the goal. A statement of the goal with the printed right-hand side , or one that assumes (35) or the divergence bound, would be a trivializing formalization and is ruled out.
Welcome contributions: proofs of the four milestones and the goal; a general Lean lemma that the discounted cost of a stationary policy in a finite MDP equals the occupancy-weighted single-period cost (milestone 1), which is reusable across policy gradient formalizations; and the log-barrier duality-gap bound on the simplex.
A failed buyer can leave a supplier with goods it can no longer sell through an existing order. A failed supplier can leave a buyer without inputs for future production. In a network, either loss can weaken another firm and start a sequence of defaults. Birge, Capponi and Chen model these effects together with two responses: suppliers reroute unsold goods to other buyers, and buyers seek replacement suppliers. Their accepted manuscript asks whether the resulting market decisions and the default cascade determine a single outcome. The issue matters when a network's resilience or fragility is measured from that outcome: a measure based on an unspecified equilibrium would not be well defined.
A supply chain order network has finitely many firms and goods . An order is the nonnegative quantity of good that firm promises to deliver to firm . The network also records each good's original price , each firm's initial equity , its safety stock and holding cost , and a realized net production cost . The realization is fixed throughout this mission; the source treats it as random when comparing network performance later in the paper. Rerouting one unit costs firm an amount ; an unfilled unit of demand incurs back-order cost . These costs and the orders and stocks are nonnegative. The basic model is on pp. 8–17 of the manuscript.
If firm defaults, a promised delivery to it is not made. Write for this undelivered order, and for firm 's total amount of good available to reroute. If a supplier defaults, write for the buyer 's lost input. After using safety stock, that buyer's unserved demand is , where . These are the quantities in equations (1)–(5).
The rerouted market for good contains firms with . At price , firm can sell up to . Aggregate demand at price is , with inverse demand . The sourcing market contains firms with . At switching cost , firm can replace up to units. Aggregate supply is , with inverse supply . In either market, an efficient allocation maximizes the stated integral objective over the capacity box, and allocates proportionally to capacity among firms quoting the same price or cost. A partial equilibrium additionally makes every active firm's quoted price or cost a best response to all nonnegative unilateral deviations. These are Definitions 2.1–2.2 and 3.1–3.2.
A firm's ex-post net worth combines original-order revenue, production and stock costs, rerouting revenue and cost, and back-order and replacement-supplier costs exactly as in equation (10). A firm defaults when its net worth is strictly negative. Starting with no undelivered orders or unserved demand, the update maps and mark all orders affected by firms that default after each market has reached its partial equilibrium. A market stable state is both the limit of that sequence and a fixed point of the update. A general equilibrium combines such a state with a partial equilibrium in every market (Definitions 3.3–3.4 and equation (18)).
The goal is Proposition 4.3, stated on p. 24:
The quadruple consists of rerouting prices , switching costs , undelivered orders , and unserved demand . The claim includes existence and uniqueness of the full outcome, not merely of its default set. The milestone list follows the paper's dependency path: Propositions A.3 and A.6 identify the unique efficient allocations in the two markets; Propositions 4.1 and 4.2 identify their partial equilibria; Lemma A.7 states that greater disruption cannot increase any firm's partial-equilibrium net worth; and Lemma A.8 states that the default updates are bounded and increasing. The numbered results and their equations are in the E-Companion, EC pp. 4–12, and the main text, p. 22.
Proposition 4.3 makes the network's outcome a function of its order commitments, stocks, prices, market functions, and realized production costs. Later comparisons of network structures can therefore refer to the equilibrium without choosing among several price or default profiles. The result also separates local market choice from the way losses spread through the network: a firm can reroute or switch optimally and still fail once the effects of other failures are accounted for.
The paper proves the result in its E-Companion, EC pp. 12–13. This mission concerns a Lean statement of that known result and the reusable definitions needed to check a proof. The draft propositions are open proof obligations; this proposal does not claim machine-checked proofs of them. The two market allocation predicates, the default update, and the cascade limit can also support later formal work on the paper's resilience results.
The market and network conditions interact. An arbitrary fixed point of the default update need not be the state reached from zero; using only the fixed-point equation loses the uniqueness asserted by the paper. Conversely, knowing a cascade limit does not by itself show that the limit is fixed, because the update changes discontinuously when a firm's net worth crosses zero. At the market level, the price and switching-cost equilibria must be established from optimization and best-response conditions. Writing the formulas for the claimed equilibrium prices into those definitions would leave the central market claims unproved.
Firms are Fin N and goods are Fin M, with ; the source numbers both from one, while Lean numbers them from zero. Orders and all default matrices are real valued and coordinatewise ordered. Active markets may be empty, as at the start of the cascade. Market objectives are ordinary real interval integrals over finite capacity boxes. The standing conditions include the paper's smoothness, concavity, and monotonicity assumptions on demand wherever it is positive and on the supply function, plus inverse identities and continuity on the quantity ranges used by the model. The inverse functions remain general data tied to and ; no linear demand or supply curve is imposed.
Several domain conventions make the displayed formulas meaningful. Assumption 2.1's minimum order is read over positive-order suppliers of a good; over all firms it would force zero safety stock whenever a nonsupplier exists. The inverse supply is nonnegative on feasible quantities, with , so the claimed switching cost belongs to the nonnegative strategy space. Demand inverse at zero is fixed to the reservation price. Assumptions 4.1–4.2 apply at each positive active-market total; for the general-equilibrium goal they are required for every binary profile the cascade can visit. Differentiability at those totals is explicit. Initial equity and the order, stock, holding, rerouting, and back-order data are nonnegative; the realized net production cost can have either sign. The model uses the p. 23 convention for prices and costs outside active markets.
An efficient allocation remains an optimizer of equations (7) or (9), with proportional tie handling; a partial equilibrium remains a best response to every admissible deviation. The general equilibrium includes both the limit from zero and the fixed-point condition. These clauses exclude an equilibrium that is true by definition or a fixed point unrelated to the default cascade. The source's informal statement that every firm “supplies, consumes, or purchases” a good has no separate activity flag in this model; a firm with no internal order can still have outside production or consumption represented in . Milestone statements involving arbitrary disruption profiles restrict them to the feasible order box , where the market inverses are defined.
Approximate message passing (AMP) is a family of iterative algorithms driven by a large random matrix. It was introduced for compressed sensing by Donoho, Maleki and Montanari (PNAS 2009), and it is also used for low-rank matrix estimation, regression and spin-glass optimization. Its main appeal is that, for Gaussian random matrices, the empirical distribution of its iterates is tracked exactly in the large-dimensional limit by a scalar or low-dimensional recursion called state evolution. Bolthausen (CMP 2014) and Bayati and Montanari (IEEE Trans. Inf. Theory 2011) proved this for Gaussian matrices. Those proofs condition on the matrix through linear observations, and that conditioning argument works only for Gaussian entries.
In practice, and in the compressed-sensing phase transition that motivates the paper, the matrices are not Gaussian: Bernoulli, Rademacher and other sub-Gaussian ensembles are used. Bayati, Lelarge and Montanari (arXiv:1207.7321, Ann. Appl. Probab. 25(2), 2015) prove that the asymptotic behaviour of AMP with polynomial nonlinearities is universal: it depends on the law of the matrix entries only through their variances. This mission formalizes that universality theorem, Theorem 3 of the paper, together with the main steps of its proof.
Fix a dimension and a degree bound . For each , an AMP instance consists of three objects:
The AMP orbit is
where is the Jacobian. The second term, the memory or Onsager term, is absent at . A sequence of random instances indexed by is -regular if it satisfies the following conditions:
The proof also uses an auxiliary message-passing iteration. It consists of messages with and
Monomials are written for .
Let and be two -regular sequences. They share the polynomials and the initial condition, and for all . Then for every and every family of polynomials of degree at most with coefficients bounded by ,
In each milestone depends only on , as Note 2 of the paper specifies.
Theorem 3 lets results proved for Gaussian matrices be transferred to every sub-Gaussian ensemble with the same variance profile. In the paper, it is the first link of a chain:
The universality of the weak-neighborliness threshold for non-Gaussian matrices, observed numerically by Donoho and Tanner (Phil. Trans. R. Soc. A 2009), is a consequence of this chain.
The result has been proved since 2012. No machine-checked proof of it, or of any AMP state-evolution statement, is known to exist. The mission asks for a formalization of the published proof, or of any other argument. Two pieces of the proof are useful elsewhere: the absolute-moment bound for sub-Gaussian variables and the moment comparison of the message-passing iteration.
The first idea is a Lindeberg-type swap: replace the entries of by those of one at a time and bound each change. This does not work directly. Every iterate depends on all entries through nested polynomial layers. The memory term also couples consecutive iterates through the squares . A single swap therefore changes every coordinate of every later iterate, and the per-swap errors have to be summed over swaps with a total error of .
Two features of the statement make it delicate. Only second moments of the entries are matched, so every contribution of higher moments of the entries must be shown to vanish in the limit. In addition, the AMP orbit is not itself a message-passing iteration: its moments match those of (Proposition 3) only because of the memory term, and without that term they do not. A formal proof also has to establish finiteness of all the moments involved, which the paper takes for granted.
Vectors in are Fin q → ℝ, and indices are 0-based. A polynomial is given by its coefficient vector over the exponent vectors of total degree at most , as in (4.10) of the paper. This keeps random polynomials in a measurable space. The Jacobian is the explicit sum of formal partial derivatives. A sorry-free sanity file checks it against the analytic derivative on an example and checks the memory term on a small instance.
The orbit is computed by recursion on , with no memory term at . The memory term uses itself, not its expectation . All random objects live on one probability space. The two sequences of Theorem 3 share one coefficient process and one initial condition.
Three readings of the printed Definition 4 are disclosed:
HasSubgaussianMGF), not only for ;Every expectation appearing in a target is also asserted to be finite. Without that, a bound or a limit could hold only because Lean assigns the value to the integral of a non-integrable function. Squared Euclidean norms are written as sums of squares, never as the sup norm that Mathlib puts on Fin q → ℝ. The deterministic identities of the tree expansion (Lemma 1, Lemma 3) and the first claim of Lemma 2 are not posed, because they need the labelled-tree families of Definition 6. Contributions of that tree machinery are welcome. Moment bounds for sub-Gaussian variables and polynomial moment estimates for sums of independent variables are reusable well beyond this mission.
A firm can lose a planned input when one of its suppliers defaults. Safety stock can absorb some of that loss, while the rest becomes demand for replacement supply. A network with more buyer and supplier links spreads orders across more firms, but the resulting benefit depends on which firms default, how much each link carries, and the price of replacement supply. Birge, Capponi, and Chen study this interaction in a supply chain model with firm defaults, switched demand, and market prices. Their Theorem 5.1 asserts that a particular order-preserving form of diversification improves the network's resilience. This mission formalizes that comparison in the notation and conventions of the accepted manuscript, including its E-Companion proof.
The question is relevant to supply chain design because adding a link alone does not specify how much business moves to it. The theorem compares two networks that retain each firm's total incoming and outgoing order quantities. It therefore isolates the effect of redistributing those orders among more partners. The result concerns a precise resilience metric: the fraction of a network's baseline out-of-stock cost reduced by holding safety stock. It does not claim that diversification prevents all defaults or reduces every component of systemic loss.
There are firms and goods. The order quantity is the amount of good that firm promises to deliver to firm . Good has price . Firm has initial equity and a unit holding cost for safety stock of good . Its realized net production cost is . Two networks and share prices, equity, holding costs, firms, and goods; their order quantities may differ. The source calls this five-part data a supply chain network, with a stock profile that is specialized here to a common scalar for the resilience comparison (§2, pp. 8–9; §5.1, p. 25).
A tiered network places each firm in a tier . A positive order of good runs from tier to tier . Tier 1 firms supply good 1, tier firms buy good , and every intermediate firm both buys and supplies its designated goods. The undirected graph underlying positive orders is connected. The model's supplier set contains firms delivering good to , and its buyer set contains firms receiving good from (§5.2–5.3, pp. 26–27).
For a common realization and safety stock , the fundamental-default set contains firms whose initial net worth is strictly negative:
The switched demand of firm for good is . The inverse supply function prices the aggregate replacement demand for good . Firm 's cost sums holding cost and switched-demand cost over every good. The network's resilience ratio is its aggregate reduction in this cost divided by aggregate cost at zero safety stock (§5.1, p. 25).
For each firm, is more diversified than when total incoming and outgoing orders are unchanged, and , and an expanded neighbor set divides orders into quantities no larger than the old quantities. Where a neighbor set is unchanged, its individual order quantities are unchanged. This is the complete condition of Definition 5.3, with the supplier good indexed as as required by §5.2.
The goal is Theorem 5.1: for two tiered networks sharing their non-order data and tier assignment,
for every admissible common safety stock and common realized production-cost vector . The three milestones are the tier-grouped expression for total cost, its order comparison between and , and equality of their zero-stock baseline costs. They are the steps of the displayed chain in the E-Companion, EC p. 18, rather than separate numbered lemmas.
The theorem gives an order-sensitive comparison of the paper's out-of-stock metric. It says that, under the stated redistribution constraints, the same amount of uniform safety stock offsets at least as large a fraction of baseline cost in the more diversified network. It supports comparisons of network designs with equal firm-level order totals. It does not rank networks with different equity, prices, or holding costs, and it does not address the paper's distinct contagion-based fragility metric (§5.1–5.3).
The result is proved in the paper; the open work here is its machine-checked formalization. The definitions of tiered order networks, fundamental defaults, switched demand, and the resilience ratio give reusable interfaces for later results about the same model. The draft Lean theorems state the full result and the three intermediate targets, with proofs left for solvers. The comparison also makes the paper's indexing and cost conventions explicit so those interfaces can be audited independently.
The default set depends on the order network, even though the two networks use the same realized costs. Thus a cost comparison cannot begin by treating defaulted firms as an unrelated common parameter. Moreover, switched demand takes a positive part after subtracting safety stock, and the inverse supply curve is evaluated at an aggregate across firms. Merely comparing individual orders or counting more links does not determine the resulting total cost. The final resilience ratio has a baseline-cost denominator that can be zero. The formalization has to cover that boundary case as well as positive baseline cost.
Firms use Fin N; goods and tiers use the paper's one-based natural-number indices. Both and are positive. Orders and holding costs are nonnegative, prices are nonnegative, and initial equity is nonnegative (the source assumes every firm is initially solvent, p. 9). A tiered network has only consecutive-tier positive orders, has activity appropriate to every firm's tier, and has a connected underlying undirected graph. The two networks share , , , the inverse supply curves, and the tier map. The source's tier-constant rerouting cost does not occur in the resilience metric and is not represented in these statements.
The paper prints Assumption 2.1 as a minimum over all firms. Since non-suppliers have zero orders, that literal reading would force and empty the theorem of its intended positive-stock content. The formalization reads the bound over actual suppliers, with . It uses monotone inverse supply curves, as implied by Assumption 2.3, and explicitly requires their values to be nonnegative for nonnegative demand; the latter is an additional convention corresponding to nonnegative inverse supply prices. These choices appear in the definitions and in the statement audit notes.
The printed supplier-order superscript in Definition 5.3 uses , while §5.2 says firm buys good ; the Lean definition uses the latter. The E-Companion's cost chain drops holding costs for goods a firm does not buy, although §5.1 sums them for all goods. The formalized cost and tier-grouped milestone retain the full sum. The paper states an almost-sure comparison under a random cost vector; its proof is pointwise, and the goal quantifies over every common realization. Each network computes its own default set. Lean sets , so a zero baseline cost requires no extra positive-denominator assumption. These conventions rule out a vacuous zero-stock reading or a cost formula weakened by omitting terms.
Competitive equilibrium is a way to divide goods when each participant has a budget reflecting her entitlement. With divisible goods, proportional value is a natural fairness target. Indivisible goods make that target unavailable in some markets: a single item cannot give two agents positive fractions of its value. The question becomes what fairness a market outcome can guarantee without dividing an item or assuming that agents value items additively. Babaioff, Nisan and Talgam-Cohen, §2.3 and §3 place this question in a discrete Fisher market, where budgets determine purchasing power but leftover money has no value to agents.
The paper introduces an -out-of- maximin share to express the entitlement of an agent whose budget is at least . Its Proposition 3.2 says that every competitive equilibrium provides this share. The result applies to any number of agents and to arbitrary cardinal preferences; it does not require the additive assumptions used for the paper's equilibrium existence results. The same paper compares the conclusion with the earlier one-out-of- guarantee for nearly equal budgets and explains that other rational shares can give a stronger benchmark in a given market. Babaioff, Nisan and Talgam-Cohen, §3.3
Let be a finite set of indivisible items and a finite set of agents. Agent has a valuation for each bundle and a positive budget . The budgets are normalized by . An allocation partitions all items: each item belongs to exactly one agent's bundle. A price vector gives each item a nonnegative real price , and the price of a bundle is . Babaioff, Nisan and Talgam-Cohen, §2.1–2.2
An allocated bundle is demanded when it costs at most and every bundle that strictly prefers costs more than . A competitive equilibrium (CE) is an allocation and price vector for which each agent demands her allocated bundle. Demand compares with every subset of , including bundles assigned to other agents and unions of several such bundles. Money is an allocation device in this model; an agent's valuation concerns her bundle alone. Babaioff, Nisan and Talgam-Cohen, Definition 2.1
For and , consider every partition of into labeled parts. Empty parts are permitted. For each partition, an adversary can leave the agent any parts, so the smallest value of a union of exactly parts is her guarantee for that partition. The agent chooses the partition that maximizes this worst-case value. This is her -out-of- maximin share. The allocation guarantees the share when is at least the resulting maximin value. Babaioff, Nisan and Talgam-Cohen, Theorem 1.2 and Definition 3.1
For every agent , every competitive equilibrium, and every pair of natural numbers with and , the goal is Proposition 3.2:
The three milestones record the paper's intermediate claims in order: the total price of all items is at most the total budget; among parts, some have price at most of the total; and a bundle an agent can afford is no better for her than the bundle she demands. The goal quantifies over every eligible rational share rather than selecting a single fixed denominator. Babaioff, Nisan and Talgam-Cohen, proof of Proposition 3.2
Two companions record the first welfare theorem, which makes a CE allocation Pareto optimal under strict preferences, and the appendix's coalition form of justified envy. The latter excludes the single case in which the comparing agent's bundle and the coalition's union are both empty, because the printed strict comparison is false there. These companions provide context for the equilibrium notion; neither changes the valuation generality of Proposition 3.2. Babaioff, Nisan and Talgam-Cohen, Theorem 2.4 and Claim A.8
The proposition gives a fairness conclusion conditional on equilibrium existence. It covers agents with different entitlements and nonadditive valuations, using a share that the agent herself evaluates through a partition of the items. The result does not assert that an equilibrium exists for every market. It says that any equilibrium already present meets all the stated rational-share benchmarks simultaneously. The paper uses this to relate competitive outcomes to maximin guarantees previously studied for nearly equal budgets. Babaioff, Nisan and Talgam-Cohen, §3
A machine-checked development would add a reusable account of finite allocations, bundle prices, demand, and maximin shares, plus a certified bridge between equilibrium and fairness. The draft Lean items in this mission are open statements with sorry; the local build checks their types and imports, not their mathematical proofs. The equivalence of the chosen maximin encoding with the finite max–min formula is checked separately in a sorry-free sanity file. Formal proofs of the goal and its milestones remain solver work.
The main formal issue is to keep the quantifiers and boundary cases aligned with the fairness definition. The guarantee concerns every partition into parts, including empty parts, and the worst choice among subsets of exactly parts. A benchmark formed from one convenient partition, from at most parts, or from a restricted family of affordable bundles would have a different meaning. The total price comparison also depends on every item being allocated exactly once. The appendix companion has a separate edge case: strict envy cannot follow from demand when the two compared bundles coincide as the empty set.
Items are Fin m, agents are Fin n, and valuations are real-valued functions on finite item sets. An allocation is a function from items to agents, so feasibility and market clearing are part of its type. A partition into parts is a function from items to Fin d; it allows empty parts. Prices and budgets are real. The goal assumes positive budgets with sum one, nonnegative prices through the CE predicate, and . The case is allowed; the budget condition implies . The Lean maximin guarantee is written as a quantified comparison rather than using a real supremum or infimum, avoiding default values on empty extrema. A sanity theorem relates it to the finite max–min expression under its proper domain conditions.
The paper's normalization and arbitrary-preference scope are retained in the goal. Strict preferences are used only for the first-welfare and appendix companions. There, injective valuations exclude the paper's exception for identical items, and the appendix claim additionally excludes the case in which the comparing agent's bundle and the coalition's union are both empty. The mission's setting is repeated locally because no published platform definition has the same bundle market and budget conventions; the related housing, divisible-goods, and convex-economy models use different objects.
Contributions should preserve full market clearing, demand over every item bundle, nonnegative prices, all -part partitions, and exactly selected parts. The definitions and finite averaging milestone can be reused in other fair-division developments. Proving the three source milestones and the goal, or improving the formal treatment of the appendix edge case, are within scope.