Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Semiconductor wafer fabrication lines are reentrant: a wafer returns to the same photolithography or etching station many times along its route, so the parts competing for a machine are at different stages of completion. In such a line, a local dispatching rule decides at every machine which waiting part goes next, and the question is whether a given rule keeps the line stable whenever there is enough capacity. Lu and Kumar (IEEE TAC 36(12), 1991) showed that the answer depends on the rule. Some natural buffer priority rules make the line unstable even when every machine has spare capacity (their Example 1; see also Kumar and Seidman 1990). Two rules are proved stable for every route: first buffer first serve (FBFS) and last buffer first serve (LBFS).
LBFS serves at each machine the waiting part that is closest to completion. It is the "pull" rule of the two, and the one closer to practice: it minimizes work in progress in many settings and coincides with earliest due date when parts arrive in due-date order. This mission formalizes the paper's LBFS results, §V. The sibling mission (FBFS, §IV) treats the other policy on the same model.
Timeline:
A nonacyclic flow line has service centers; center has identical machines, each processing one part at a time. Every part follows the same route through buffers : in buffer it waits at center , then needs units of uninterrupted processing on one machine of that center. A center may serve several buffers.
Parts are released into ; part is released at time and exits at time , when its service at ends. Finitely many parts may be present at time , in any buffer, some already in service. With the number of releases in , the arrivals are bursty with rate and burst if
The work per machine that one part brings to center is , and the load is with . The capacity condition is (3). Also , and is the maximum per-machine work brought to a center by a part in , counting only buffers (6).
Scheduling is nonidling (a machine idles only if every buffer of its center is empty) and nonpreemptive, and a machine takes the part at the head of a buffer. Under LBFS, a machine takes a part from only if every buffer of its center with is empty. The number of parts in the system at time is .
Under (1) and (3), for every with ,
Here is the explicit constant of the delay estimate. The paper prints the second bound as ; its proof establishes the form above, which is the one posed.
The delay estimate behind the goal, in the order of its proof:
for a part that finds parts in the system on release.
Then the Pipeline Property , order preservation (parts exit in the order they enter), and the recursion (14) for the number in system along successive exit times. A further item states that LBFS is stable in the sense of §II: every delay is bounded.
Theorem 2 says the delay of a part under LBFS grows with the number of parts ahead at rate : the line behaves like a pipeline whose speed is set by its bottleneck center, although parts revisit centers. Theorem 3 converts this into a bound on work in progress that holds for all time, with an asymptotic bound that does not depend on the initial state. Together they give stability of LBFS for every route and every burst size, with explicit constants. This is a deterministic, sample-path result: no distributional assumption on arrivals is needed. Its constants are explicit, so they can be evaluated for a given line.
The results are proved in the paper; none is formalized. The mission produces a machine-checked model of a multi-server reentrant line with nonidling, nonpreemptive, head-of-buffer buffer-priority dispatch, together with Theorems 2 and 3 on it. The model carries over to the other policies of the paper (FBFS, least slack, earliest due date).
The obvious argument fails because under LBFS parts released later do interfere with a part : they occupy machines nonpreemptively at the low-priority buffers must still pass. So the delay of cannot be bounded by the work ahead of it alone. The paper's estimate is an induction from the end of the line backwards over the truncated systems , nested with an induction on the position of in its buffer. The constant is recomputed at every level from , so is halved at each level. A formal proof must also handle what the paper treats informally:
All declarations are in the namespace ReentrantScheduling.LBFS.
WithTop ℝ, with ⊤ meaning never, so a run need not serve every part, and the theorems assert that parts are served. A formalization with real-valued start times would assume every part is served, which is half of what stability asserts.Set.encard, never Set.ncard, which would count an infinite set as and make the capacity rule vacuous.The model is reusable for other dispatch rules on reentrant lines. Proofs of any milestone are welcome, as are lemmas on admissible runs (FIFO within buffers, finiteness of ).
Not posed here:
QueueingStability.LuKumar.theorem31;Semiconductor wafer fabs are the standard example of a reentrant manufacturing line: a wafer visits the same lithography or etching station many times along a route of hundreds of steps, so each station holds parts at many different stages of completion and must decide, every time a machine frees up, which of them to serve next. Kumar (Re-entrant lines, Queueing Systems 13, 1993) singled these lines out as a third class of manufacturing systems besides flow shops and job shops, and stability of their scheduling policies became a central question in the analysis of queueing networks.
The question is sharp because the obvious conjecture is false. Kumar and Seidman (IEEE TAC 35(3), 1990) gave a deterministic network in which a distributed policy is unstable although every machine has spare capacity, and Lu and Kumar (IEEE TAC 36(12), 1991, Example 1, p. 1409) gave a two-station reentrant line in which a buffer priority policy is unstable at load below one. Their paper then identifies policies that are always stable: first buffer first serve (FBFS, Theorem 1), last buffer first serve (Theorem 3) and the due-date policies least slack and earliest due date (Theorem 4). This mission formalizes Theorem 1.
Timeline:
A nonacyclic flow line has service centers; center has identical machines in parallel, each working on one part at a time. Every part follows the same route: it visits buffers in order, buffer sits at center , and a part in needs time units of uninterrupted processing on one machine of . The same center may appear many times along the route.
Parts enter at ; part is released at time . The releases are deterministic but may be bursty: with the number of parts released in ,
for constants . Each part brings units of work per machine to center , and the load is . The arrival rate is within capacity when (3). At time the line may hold finitely many initial parts in arbitrary buffers, some of them already in service.
A schedule is nonidling (a machine idles only if every buffer of its center is empty), nonpreemptive (a started service runs to completion) and serves the part at the head of the chosen buffer. Under FBFS a free machine at center takes a part from only if every buffer of with is empty. With the time part exits after its service at , the schedule is stable if there is with
may depend on the initial state as well as on .
For every line, every with , and every admissible FBFS run whose releases satisfy (1),
The statement fixes no constant: is chosen after the run.
An interval is an -busy period if at every instant some part waits in a buffer , , at center . With , and
Milestone 4 has an explicit bound independent of the initial state; the goal additionally covers the finitely many parts present or released during the transient.
Theorem 1 says that the simplest "push" discipline, always serving the earliest stage first, keeps every part's delay bounded on every reentrant line whose stations have spare capacity, for every initial state and every bursty but rate-limited release pattern. By Little's law it also bounds the work in process. Together with Example 1 it shows that stability is a property of the policy, not of the load condition alone, and it gave one of the first two positive results for a whole class of reentrant lines. The explicit constants make the delay guarantee quantitative after the transient.
The result is proved in the paper. As far as the platform record shows it has not been formalized: the related platform items concern the fluid models of Dai and Weiss, which have no parts, no burstiness and no nonpreemption, and a fixed instance of Example 1. This mission produces a machine-checked sample-path model of reentrant lines under buffer priority policies and a checked proof of Theorem 1 with its explicit busy-period constants. The same model serves the sibling mission on LBFS (Theorem 3 of the paper).
A first idea is a work-conservation argument per center: total work arriving at grows at rate per machine, so the center cannot fall behind. This fails because the work arriving at a center from a later buffer depends on how fast the upstream centers have pushed parts to , and an upstream center can release a burst that the downstream center absorbs only after other buffers have starved; Example 1 is exactly such a cascade under a different priority order. Any argument must therefore bound the delay of a part at a buffer in terms of delays it suffered upstream at other centers, uniformly in the initial state, while nonpreemption lets a part wait up to for a machine busy with a lower-priority buffer and the release constraint (1) controls only arrivals to , not to later buffers. On sample paths one must also show that the initial parts clear in finite time and that only finitely many parts are served in any bounded interval.
Lean represents a line by a structure with , , , the route center : Fin l → Fin S and processing times τ with . The positivity is a pinned hypothesis: the paper leaves it implicit, its proof divides by , and its only zero processing times are those of Example 1. Buffers are 0-based: the paper's is Lean index . The load is written , equal to for .
A run is a type of parts with an injective line order, a finite set of initial parts, entry buffers, release times, and for each part and buffer the start of service in WithTop ℝ, meaning never served. Admissibility imposes, at every : precedence (service begins after arrival, except that initial parts may be in service at time ), capacity , nonidling, head of buffer with ties broken by the line order, and the priority rule. All counts use Set.encard. The theorems hold for every admissible run, not for one particular tie-breaking schedule. The constants are definitions computed from the line and ; the times are existential after the run.
Two trivializing formalizations are ruled out: start times in ℝ would make every part served by construction and stability half empty, and a capacity constraint stated with Set.ncard would be vacuous for infinitely many parts. never depends on the part. A sanity file exhibits a nontrivial admissible run satisfying (1) and checks that the empty run is admissible and stable.
The page prints (p. 1410) as a product of the two brackets; the inequality it is solved from gives the quotient, which is also the printed form of , and the formalization uses the quotient.
The sample-path model (Line, Run, Admissible, Arrivals, Stable) is reusable for any buffer priority policy and for the LBFS mission. Contributions welcome: proofs of the milestones in the listed order, lemmas on finiteness of the parts served in bounded time, and interval-counting lemmas for busy periods. Not posed here: Example 1, which is already on the platform as an open problem (QueueingStability.LuKumar.theorem31), Theorems 2–3 (LBFS, sibling mission), Theorems 4–5 and Corollary 1 (due-date policies, several flow lines).
Most stochastic programs that arise in practice, such as two-stage stochastic linear programs with recourse, have far too many scenarios to be solved exactly. The standard remedy is sample-average approximation: draw independent observations of the random data, replace the expectation by the sample mean, and solve the resulting deterministic problem. A candidate solution found this way, or by any heuristic, comes with no guarantee. To judge it one needs a bound on its optimality gap , and estimating is routine; what is missing is a lower bound on the unknown optimal value .
Mak, Morton and Wood (Oper. Res. Lett. 24 (1999)) show that the optimal value of the sample-average problem supplies exactly this: its expectation never exceeds , and it can only move closer to as the sample size grows. The result requires almost no structure of the problem, and it underlies the batch-means confidence intervals on the optimality gap used throughout the stochastic programming literature, including the single- and two-replication procedures of Bayraksan and Morton (2006).
Timeline.
Let be a random vector with distribution on a measurable space , let be a deterministic feasible set, and let . The stochastic program is
Let be independent and identically distributed (i.i.d.) from the distribution of , defined on a probability space . The sample-average problem of size is
Its optimal value is a random variable. All the are built on the same sequence: uses its first terms and its first . Throughout, is assumed to exist for every .
For the proof structure the mission also uses the leave-one-out values
the sample-average optimal values of the subsamples of size of the first observations.
stated in the Introduction (p. 48) as the paper's main claim, with no assumption on or on beyond the existence of the relevant expectations and of optimal solutions.
Theorem 1 turns any sampling-based solver into a source of statistical lower bounds on : averaging independent replications of gives a confidence interval for a lower bound, and display (9) combines it with an upper-bound estimator into an estimator of the optimality gap that is nonnegative by construction. Theorem 2 justifies increasing the sample size: the bias is nonincreasing in . Both results are used, often without proof, in the analysis of sample-average approximation and of the gap-estimation procedures built on it.
The results are proved, in this paper and in textbooks (e.g. Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming). To our knowledge none of them is machine-checked. On Prove2Me, a special case of Theorem 1 under continuity, compactness and a square-integrable envelope is posed but unproved (SolutionQuality.SRP.display1_negative_bias), and the wait-and-see inequality is proved for finitely many scenarios in an extended-real model (StochasticProg.ValueOfInfo.prop1_ws_le_rp_le_eev). This mission states the general versions, for arbitrary feasible sets and integrable costs, on a measure-theoretic i.i.d. model.
Theorem 1 is short on paper; in a formal setting its difficulty is bookkeeping: minima over arbitrary sets and expectations of possibly non-integrable functions both need explicit hypotheses to mean what the paper means. Theorem 2 is harder. The natural first attempt compares and on the same sample path, but no pathwise inequality holds in either direction: one extra observation can raise or lower the sample-average optimum. The monotonicity holds only in expectation, so any argument must use the joint law of the infinite i.i.d. sequence, including the law of its subsequences, and measurability of as a function of the sample path.
The model is the published definition file SolutionQuality.SRP.Setting: decisions lie in EuclideanSpace ℝ (Fin d), is a probability measure on , the sample is an i.i.d. sequence ξ : ℕ → Ω → Ξ (the paper's is ξ (i-1)), and , , and the optimality gap are its optValue, saaValue, gapEstimate and optGap. The mission adds skipIndex, the leave-one-out value looValue and the path law pathLaw.
Committed conventions:
sInf), and expectations are Bochner integrals. Both take the value on bad inputs, so every statement carries the hypotheses that keep them genuine:
These hypotheses are disclosed in each statement and are satisfiable: a sanity instance with a singleton satisfies all of them. A formalization that dropped the integrability of , or that allowed , would make the goal false or vacuous, and one that assumed continuity and compactness would restate the special case already on the platform; neither is in scope.
A complete development needs: the expectation of a sample mean under an i.i.d. law; the identification of the law of fun j => ξ (skipIndex i j) · with Measure.infinitePi (fun _ => μ) (Mathlib's iIndepFun_iff_map_fun_eq_infinitePi_map); and the averaging identity behind the leave-one-out decomposition. The reindexing lemma for i.i.d. sequences is reusable well beyond this mission. Proofs of the milestones, and alternative arguments for Theorem 2, are welcome.
Flexible manufacturing systems are often scheduled by simple distributed rules: each machine looks only at its own buffers and decides, in real time, which part type to work on next. Switching from one part type to another costs a set-up time during which the machine produces nothing, so a natural rule is to work on a buffer until it is empty and only then switch. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989; reference [18] of the paper) showed that such clearing policies, and in particular clear-a-fraction policies, keep every buffer bounded on acyclic systems whenever each machine has spare capacity. Whether the same holds when material flows around a cycle of machines was left open.
Kumar and Seidman (IEEE TAC 35(3), 1990) answered it negatively by two examples. Example 1 is a single re-entrant part type. Example 2, the subject of this mission, has two part types, neither of which ever revisits a machine, and shows two further phenomena: instability without re-entrance, and the coexistence, for one and the same system, of a bounded periodic regime and an unbounded one, selected only by the initial state.
A manufacturing system has part types arriving at rates and machines . Parts of type follow a fixed route; at stage they wait in buffer at machine , and processing one of them takes . Switching a machine from buffer to buffer takes the set-up time . Flows are continuous: is the level of buffer , and are its cumulative input and output, and
A machine works in runs: a set-up for a buffer, then processing it at rate while it is nonempty, and at the rate of its inflow while it is empty. A clearing policy (Definition 1) keeps a machine on a buffer until the first time that is empty and another of its buffers is nonempty, and then sets it up for one of those. The system is stable if for every buffer .
Example 2 (Fig. 3) has two part types with and two machines. Part type 1 visits buffer 1 at machine 1 and then buffer 2 at machine 2; part type 2 visits buffer 3 at machine 2 and then buffer 4 at machine 1. Processing times are and setting up to buffer takes . The parameters satisfy the capacity condition (1), and , and
conditions (7)–(10). The paper's feasible instance is , with . For this system there is exactly one clearing policy.
For every parameter set satisfying (1) and (7)–(10):
The result shows that stability of a scheduling policy is a property of the initial state as well as of the system: the same parameters admit a bounded periodic orbit and an orbit along which the backlog of buffer 1 is multiplied by in every cycle. The capacity condition (1) holds throughout, so the instability does not come from overload: spare capacity is lost because one machine starves the other. The example also shows that a cycle in the machine graph suffices, without any part type revisiting a machine. Sections IV and V of the paper respond to this by giving a stronger capacity condition under which clear-a-fraction policies are stable, and a supervisory mechanism that stabilizes any policy.
The paper's argument is a stage-by-stage computation of a piecewise-linear trajectory. It has not been machine-checked. A formalization fixes what a clearing trajectory is (including the switching instants at which a buffer is empty but just starting to fill), proves that the trajectories exist and are determined by the initial state, and checks the paper's closed forms. One printed constant is wrong: the offset of the full cycle lacks a final , and the milestone states the corrected value.
The computations within each stage are linear algebra. The difficulty is the event structure. Every stage depends on the order in which the two machines' events occur: whether machine 1 clears buffer 1 before machine 2 has finished its set-ups, whether buffer 2 is still nonempty when buffer 1 empties, and so on. These orderings hold only for large, or only because (8) holds with equality and (9)–(10) hold strictly. The periodic regime depends on exact synchronization. In Case 2, a machine processing an empty buffer at the reduced rate must not be forced off it while its other buffer is empty and not yet fed. A proof must also establish existence of each trajectory, not only compute it.
Fin P, machines Fin M, buffers as pairs with Lean index for paper stage , real time, and no transport delay or assembly (as in the paper). Example 2 is an instance of this general model, with machines 1, 2 as Lean 0, 1.Contributions welcome: existence and uniqueness of clearing trajectories for the two-machine instance, the event-ordering lemmas for large , the restart (time-shift) property of trajectories, and the three milestones.
Communication networks must route many source–destination demands through shared edges. A multicommodity flow describes how much of each demand can be carried simultaneously without exceeding an edge's capacity. In an undirected network, a cut bounds the traffic that can pass between two groups of vertices, but many commodities can interfere even when no single cut is obviously restrictive. Leighton and Rao showed that the uniform concurrent flow is within a logarithmic factor of the corresponding sparsest-cut bound Leighton and Rao, 1999.
For routing, flow value alone is incomplete: a feasible flow can use long detours. Section 2.5 of the same paper establishes that a flow of the guaranteed size can be carried on paths whose number of edges is also controlled. The result supports the paper's discussion of low-congestion, low-dilation routing in communication networks, where a long route can increase latency or complicate scheduling even if every edge has sufficient capacity Leighton and Rao, 1999, §2.5.
Let be a finite set of vertices. An undirected capacitated network has a symmetric capacity for each pair, with . A pair is an edge when its capacity is positive. Parallel physical edges can be combined by adding their capacities. The network is connected: every nonempty proper subset has positive cut capacity , where .
The uniform multicommodity flow problem gives one unit of demand to each unordered pair of distinct vertices. Equivalently, it gives demand to each ordered pair with Leighton and Rao, 1999, footnote 2. A concurrent flow of value routes the fraction of every demand. Traffic in both directions of an undirected edge shares that edge's capacity. The demand crossing is , so the uniform min-cut, also called the sparsest-cut value, is
For a flow path, length means its number of edges. A separate nonnegative symmetric distance function assigns lengths to edges; its total weight is . Given a hop budget , let be the smallest -length of a walk from to using at most edges. The value is if no such walk exists. The maximum capacity incident to one vertex is . The paper uses and for the natural logarithm Leighton and Rao, 1999, footnote 3.
Theorem 18 asserts the existence of absolute constants such that every network in the setting above admits a concurrent uniform flow of value whose every route has at most edges, with
The constants precede the choice of network: they cannot depend on its size or capacities. The goal gives an actual flow and integer hop limit, not only a lower bound on a supremum Leighton and Rao, 1999, Theorem 18.
The short-path linear-programming dual uses in its distance constraint, , and minimizes . Lemma 19 partitions a network into components with both edge-radius at most and distance-radius at most , while the capacity between components is at most . Corollary 20 finds a component with at least vertices when . Lemma 21 bounds the sum of -restricted distances from any such large set to its complement by , provided . These are the mission's milestones, in source order Leighton and Rao, 1999, pp. 808–809.
Theorem 18 places simultaneous lower and upper guarantees on a routing solution: it carries a substantial fraction of every uniform demand, while each route uses a bounded number of edges. Its hop guarantee is stronger than simply knowing that the unconstrained maximum flow is large. The result is one of the paper's inputs for reasoning about routing paths with low congestion and dilation; the paper also says analogous short-path results extend to product and directed flow problems, without presenting all their details Leighton and Rao, 1999, p. 811.
The known mathematical result has a published proof; this mission asks for machine-checked statements and proofs. A complete development would establish the hop-indexed flow model, the restricted shortest-path duality, and the two-radius partition estimates in Lean. The network, proper-cut, and extended-distance interfaces can be reused in later work on sparse cuts and length-constrained routing. No machine-checked proof of this exact theorem is claimed here.
The ordinary approximate max-flow/min-cut theorem controls the amount of concurrent traffic but does not bound the number of edges on each route. Restricting routes changes the dual: a shortest path that exceeds the hop budget is unavailable, and some vertex pairs have no allowed path at all. Assigning such a pair distance zero would alter the dual constraint. The geometric estimates must control both hop count and -length on the same connecting paths, since bounds witnessed by two unrelated paths cannot be combined into one short route Leighton and Rao, 1999, §2.5.
The vertex type is finite and has at least two members. Capacities are real, symmetric and nonnegative; zero-capacity pairs are absent from the graph. Connectivity is the paper's standing cut assumption. The min-cut ranges over nonempty proper subsets, so no expression divides by a zero cardinality. Demands use the paper's ordered-pair convention. A short flow is a nonnegative commodity–hop–arc array whose equations inject, conserve and absorb traffic; the capacity constraint combines both directions and all hops. The maximum flow is a supremum over feasible values. Its use is confined to the positive-demand finite setting, where the feasible set is nonempty and bounded.
Restricted distances take values in extended nonnegative reals, so an empty family of allowed walks has value . The radius predicate requires one walk inside a component to meet both bounds. appears in Theorem 18, Lemma 19 and Corollary 20; Lemma 21's threshold uses . For expressions dividing by , the formal statements require ; this makes the printed radius meaningful. The explicit companion theorem uses the hop limit for the paper's real , which is what "at most edges" means; Lemma 21 keeps real. The polynomial-time search claim is outside this existence formalization. A definition making every restricted distance zero, or quantifying its asymptotic constants after the network, would make the goal a different theorem.
Contributions may include finite-flow and linear-programming duality, path decomposition for the hop-indexed formulation, the partition estimate, the large-component corollary, or the restricted-distance estimate. The same finite graph and extended-distance definitions may serve subsequent missions.
Nonlinear conjugate gradient methods minimize a smooth function of variables using only function values, gradients and a few vectors of storage. They are the standard choice when is too large for quasi-Newton matrices, and they remain building blocks of large-scale solvers in optimization, scientific computing and machine learning. The method of Polak and Ribière (1969) is usually the most efficient member of the family in practice, but Powell (1984, doi:10.1007/BFb0099521) showed that, even with exact line searches, it can cycle forever without approaching a stationary point. The Fletcher–Reeves method, by contrast, has a global convergence theory (Zoutendijk 1970; Al-Baali 1985, doi:10.1093/imanum/5.1.121) but is often slow.
Powell (1985, report DAMTP 1985/NA1; published in SIAM Review 1986) suggested truncating the Polak–Ribière scalar at zero. Gilbert and Nocedal, in the INRIA research report that became SIAM J. Optim. 2 (1992) 21–42, proved that this truncation, and a whole class of methods sharing a structural property with Polak–Ribière, converge globally with practical inexact line searches. This mission formalizes that result (§4 of the report).
Timeline. 1952: Hestenes and Stiefel, linear conjugate gradients. 1964: Fletcher and Reeves, nonlinear extension. 1969: Polak–Ribière and Polyak. 1970: Zoutendijk, convergence of Fletcher–Reeves with exact searches. 1984: Powell, a nonconvergent Polak–Ribière example. 1985: Al-Baali, Fletcher–Reeves with strong Wolfe searches. 1990/1992: Gilbert and Nocedal, the present results.
Let be a finite-dimensional real inner product space and continuously differentiable with gradient . From , a conjugate gradient run produces directions and iterates
with , a scalar , and a steplength chosen by a line search. Write .
Assumptions 2.1: the level set is bounded, and on an open neighbourhood of the gradient is Lipschitz: .
The line search is described only through three properties:
Property (*): whenever for all , there are and with
Finally and .
If Assumptions 2.1 hold, for all , , the line search has properties 1–3, and Property (*) holds, then
Theorem 4.3 separates what a convergence proof needs from the method (nonnegativity and Property (*) of ) from what it needs from the line search (three abstract properties). It therefore applies at once to the truncated Polak–Ribière and Hestenes–Stiefel methods, to their absolute-value variants, and to any line search, exact or inexact, that delivers the three properties. Corollary 4.4 is the guarantee behind the "PR+" rule that is the default in many nonlinear conjugate gradient codes; Powell's example shows that dropping breaks it.
The results are proved in the paper, not open. To our knowledge none of them, nor Zoutendijk's theorem in this form, has a machine-checked proof. The mission produces checked statements of the theorem, its two lemmas and its main application, and a reusable formal vocabulary for line-search methods (level sets, Wolfe steps, Zoutendijk and sufficient descent conditions).
The usual route to convergence of a descent method bounds away from zero, or shows that grows at most linearly, and combines this with the Zoutendijk condition. For Polak–Ribière-type methods neither bound is available a priori: can be as large as on many consecutive iterations, so can grow geometrically along stretches of the run. The argument must instead control the proportion of large steps over blocks of iterations and relate it to the change of direction, and reconcile both with the boundedness of . The combinatorics of blocks (floor and ceiling of , products of grouped by blocks) and the interplay between Lemma 4.1 and Lemma 4.2 carry most of the formal work. Corollary 4.4 additionally needs Zoutendijk's theorem for Wolfe line searches, which is not assumed here.
gradient f for its inner product, matching "the scalar product used to compute the gradient" (p. 2).Needed infrastructure: summability arguments for the series (4.5) and , Cauchy–Schwarz in , finite counting over index blocks, and, for Corollary 4.4, Zoutendijk's theorem (Theorem 2.1 of the report, a target of the companion mission). Contributions of general line-search lemmas are welcome and reusable well beyond this paper.
Solving a system of nonlinear equations , with continuously differentiable, is a basic task in numerical analysis and optimization: it is the inner step of interior-point and sequential quadratic programming methods, of implicit time-stepping for differential equations, and of equilibrium computations in operations research. Newton's method converges fast near a solution at which the derivative is invertible, but from a poor starting point it may fail. Trust region methods are a standard globalization: each step minimizes the norm of the local linear model over a ball , and the radius is shrunk or enlarged according to how well the model predicted the actual decrease of (Moré and Sorensen 1983; Dennis and Schnabel 1983, §6.4).
Eisenstat and Walker (1994) developed a general global convergence theory for inexact Newton methods, in which steps only reduce the linear model's norm by a factor and must also give sufficient decrease of . Their §4, Application 1, shows that this theory also covers trust region methods. This mission formalizes that application.
Let be a finite-dimensional real vector space with an arbitrary norm (the paper's ; the norm need not be Euclidean), and continuously differentiable with derivative . For a point and a step , the actual reduction and predicted reduction are
A point is a stationary point of if for every : no step decreases the norm of the linear model. A point is a limit point of if every ball around contains for infinitely many .
Algorithm TR is given , , and . At iteration it sets and picks a step
While , it replaces by for some and picks a new by (4.5). Then , and the next initial radius satisfies if , and otherwise. The algorithm does not break down if it generates an infinite sequence of iterates.
If Algorithm TR does not break down, then
and if is a limit point with invertible, then
The statement has no constants, and it holds for every choice the algorithm leaves open: the minimizer in (4.5), the factors , and the new radii.
An extra item, Corollary 3.6, states that such a sequence with divergent has , where (or if ).
Theorem 4.4 is a global convergence result that assumes neither bounded level sets, nor the existence of a solution, nor an inner-product norm. It separates two conclusions: without any regularity, the only possible accumulation points are stationary points of ; at an accumulation point where is invertible, the method finds a solution, converges to it, and eventually takes the full Newton step. The paper assumes only continuous differentiability, which does not by itself give a quadratic convergence rate. Lemmas 4.2 and 4.3 are local facts about minimizers of the linear model's norm over a ball and apply to any method that uses such steps.
The result is proved in the paper. As far as we know, none of it is formalized: Mathlib has the Fréchet derivative, the inverse function theorem and invertible continuous linear maps, but no trust region or inexact Newton convergence theory. This mission produces machine-checked versions of the paper's statements for an arbitrary norm, together with a reusable vocabulary (actual/predicted reduction, stationary points of , model minimizers, trust region runs) for later formalizations of trust region and Levenberg–Marquardt type methods.
The obvious argument shows that decreases, so it converges, and then tries to conclude that the predicted reductions tend to zero. That step fails without control on the radii: if , small predicted reductions say nothing about stationarity, and the steps could shrink while the iterates still wander. The central difficulty is to show that near a non-stationary or regular limit point the radii stay bounded away from zero, while at the same time proving that the whole sequence converges to that limit point, not just a subsequence. Under an arbitrary norm the model minimizer is not unique and the model norm is not smooth, so arguments based on gradients of do not apply.
E; is fderiv ℝ F, and "continuously differentiable" is ContDiff ℝ 1 F.IsTRRun. Iteration records the number of while-loop passes, the factors , and trial steps , each a minimizer of (4.5) for its radius. Trials fail the test , and trial passes it. "Does not break down" is the existence of such a run. Any minimizer in (4.5) may be chosen.MapClusterPt. "Sufficiently near and sufficiently large" is: there exist and such that the property holds for with . "Whenever is sufficiently large" is ∀ᶠ k in atTop.(fderiv ℝ F xstar).IsInvertible. is ContinuousLinearMap.inverse, which is the true inverse for all large .¬ Summable.IsTRRun forces neither, and it has a run with nonzero steps (for on ).Needed infrastructure: the continuity of near an invertible point (Lemma 1.1 of the paper), a uniform linearization bound near a point (Lemma 1.2), and the telescoping argument of Theorem 3.5. These are reusable well beyond this mission. Contributions are welcome on each milestone separately, and on general lemmas about minimizers of over a ball.
A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.
Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.
Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.
There are part types and machines. Part type arrives at rate and follows a route of operations; operation is done by machine and takes per part. Parts awaiting operation wait in buffer , with level . Machine serves , and switching from to costs . Flows are continuous: a machine processing a nonempty buffer drains it at rate , the output feeds instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.
The load of machine and the capacity condition are
The system is stable if for every buffer.
The supervisor picks with
and thresholds . It truncates every processing run of at ; it keeps a first-come first-served queue of the buffers that are not being processed and whose level exceeds ; when a run ends and , the head of is processed next, for exactly unless it clears earlier. When is empty the underlying policy is free. Write (26) and , the backlog of part type for machine .
Under (1), (24) and , every supervised trajectory, from every initial state, satisfies
The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.
The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With it enforces FCFS with truncated runs; with large and it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.
The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).
The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine from upstream machines whose behaviour depends on itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below ; any bound has to account for the time spent below the threshold and for repeated re-entries into , with a set-up paid at each.
Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index is Lean index . Time is real with . Set-up times satisfy : a set-up is paid only on a switch. No transport delays or assembly, as in the paper.Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).
Portfolio decisions in continuous time must respect both market uncertainty and investment restrictions. A ban on short sales, for example, restricts the vector of wealth fractions a trader may hold at every instant. The corresponding optimal consumption and investment problem is harder than its unrestricted counterpart because a candidate portfolio obtained from the usual pricing equations may violate the constraint. Cvitanić and Karatzas introduced auxiliary markets indexed by a process and used a dual optimization problem to establish existence of an optimal constrained policy in their 1992 paper. This mission formalizes the paper's existence theorem, Theorem 13.1, together with the results in Sections 12–13 that specify its dual target.
Fix a finite horizon and a complete probability space carrying a standard -dimensional Brownian motion . Information at time is the probability augmentation of the filtration generated by up to . A bond earns short rate ; stocks have appreciation vector and volatility matrix . The market assumptions require progressively measurable coefficients, a uniform lower bound on , uniform nondegeneracy of , finite expected interest-rate integral, and finite energy of the market price of risk §2.
A portfolio specifies fractions of wealth held in the stocks, while is consumption and is wealth. The feasible portfolios lie in a fixed nonempty closed convex set . Its support function is , which may equal . The process indexing an auxiliary market belongs to when it has finite expected quadratic energy and finite expected integrated support value. Its deflator combines an interest-rate discount with a Brownian exponential. The class consists of those for which the budget map is finite for every §§4, 8.
The running utility and terminal utility are strictly increasing and strictly concave for positive arguments. An admissible constrained policy has nonnegative wealth, finite expected negative utility, and for Lebesgue-time times probability almost every . The primal value is the supremum of its expected utility over all such policies with initial capital . The dual value is the infimum, over , of expected conjugate utility evaluated at §§5–6, 12.
The first conclusion of Theorem 13.1 is the paper's condition (12.9):
Thus the infimum is attained by a drift with a finite budget map. It is a conclusion of this mission, even though earlier Section 12 results assume it. The milestones include weak duality (12.8), the dual representation of Proposition 12.1, the capital-matching result of Proposition 12.2, and the analytic properties of the extended dual functional in Proposition 13.2 pp. 792–795.
The theorem's second conclusion is
Here is the constrained admissible class. Theorem 12.4 establishes this conclusion when dual attainment is assumed; Theorem 13.1 provides that assumption under the paper's stated utility and dual-finiteness conditions p. 794.
The result supplies an optimizer, rather than only a bound on the best attainable utility. It also identifies a minimizing auxiliary market for every positive dual parameter, making the dual description usable at a specified initial capital. The dual representation links the primal value to a convex function that can be studied without choosing a constrained policy first §§12–13.
The theorem is proved in the paper; the remaining work here is a machine-checked development of its definitions, hypotheses, and existence argument. The mission also produces reusable definitions of an almost-surely square-integrable Brownian integral relation, extended-real utility expectations, an extended support function, and constrained wealth classes. The Brownian state space and predictable step-sum substrate credit the published Ethier–Kurtz formalizations. The paper refers some analytic steps to earlier works instead of reproducing full proofs, including Lemma 12.3 and a final finiteness argument pp. 793–796.
Weak duality alone only bounds the constrained value from above. It does not supply a minimizer of , and an arbitrary minimizing auxiliary process need not belong to . The dual functional must retain meaningful infinite values on the full finite-energy process space ; replacing them with total-operation defaults can turn the needed coercivity and lower-semicontinuity statements into different claims. Even after dual attainment, the minimizing parameter for a prescribed capital must match the budget map §§12–13. These are the precise gaps between a numerical bound and the asserted optimal policy.
Lean uses with its Euclidean norm, a finite positive horizon, a complete probability measure, and the augmented Brownian filtration. Processes are functions of time and sample point; almost-everywhere restrictions on portfolios and auxiliary drifts are distinct from pathwise -almost-sure statements. A policy is represented by a triple whose wealth process satisfies the integral equation, matching the paper's pair together with its unique wealth solution. The integral operator is bound to the local Itô construction by predictable step approximations; it is not a free function. Integrands must be in its almost-sure square-integrable domain.
Support values, utility at zero, expected utility, and value functions use extended reals. The extension is the right limit ; an extended-real supremum defines conjugate utility where zero arguments arise. The inverse marginal is a positive-argument inverse of . The minimization in ranges over , while (12.9) asks for a minimizer in . Its witnesses remain explicit choices in statements involving ; no default-valued inverse is introduced. The functional of (13.3) is defined on , uses the paper's formula on , and is off . On it agrees almost everywhere with the original dual objective, an equality requiring a formal lemma. Assumption 6.2 and conditions (5.8), (8.25), (12.2), (12.3), and (12.11) are explicit. Their quantifiers cover both utilities and every time in where stated. The mission rules out a vacuous dual-attainment hypothesis, a zero default for an unbounded support supremum, and an unconstrained stochastic-integral operator. Contributions proving the source milestones and the analytic lemmas they need are in scope.
The Nelder–Mead simplex method (Nelder and Mead, 1965) is one of the most widely used methods for minimizing a function without derivatives. It is the default unconstrained derivative-free minimizer in several numerical libraries (fminsearch in MATLAB, method="Nelder-Mead" in SciPy) and is used routinely in chemistry, engineering and statistics, where the objective is a simulation or a measurement whose gradient is unavailable.
Its theory lags far behind its use. Until 1998 there was no convergence result for the method as stated, in any dimension. Lagarias, Reeds, Wright and Wright (SIAM J. Optim. 9 (1998) 112–147) gave the first: in dimension one, on strictly convex functions with bounded level sets, the method converges to the minimizer whenever the product of its reflection and expansion coefficients is at least one. McKinnon (SIAM J. Optim. 9 (1998) 148–158) showed in the same issue that in dimension two the method can converge to a non-stationary point even for strictly convex smooth functions, so results of this kind cannot be expected in general.
Timeline:
This mission formalizes the one-dimensional convergence theorem.
Let . In dimension one a Nelder–Mead simplex is a pair of distinct points , ordered so that : is the best and the worst vertex. Four coefficients are fixed in advance, reflection , expansion , contraction and shrink , satisfying the conditions (2.1) of the paper:
From the method forms the trial points
With , , and so on, one iteration does the following:
The worst vertex is discarded, and the accepted point becomes the new best vertex if and the new worst vertex otherwise (the paper's tie-breaking rule). The diameter of the simplex is . The function is strictly convex, and it has bounded level sets: is bounded for every . It then has a unique minimizer .
If, in addition to (2.1), , then for every nondegenerate initial simplex
The goal names no rate and no constant; it is the qualitative statement the paper proves.
A further item states the paper's remark that when the vertices stay within of , so convergence to fails when the minimizer is farther away.
Theorem 4.1, together with the remark on , identifies as the right condition for global convergence of the one-dimensional method, and it holds for all contraction coefficients and for infinitely many expansion steps. It is the base case of the low-dimensional theory: the linear-rate result for (Theorem 4.2) builds on the same bracketing and proximity lemmas, and McKinnon's example shows that nothing comparable holds in dimension two.
The result is proved in the paper; no machine-checked proof of any convergence property of the Nelder–Mead method is known to exist. A formalization gives a precise, executable definition of the algorithm with its tie-breaking rules, which the literature states in several inequivalent variants, and it checks a proof with a known gap: the bound on printed in Lemma 4.2 is false (see below), so the published argument cannot be followed line by line.
The obvious argument, that the best value decreases and so the best vertex converges, fails twice. The best vertex may stall while contractions continue, and the diameter can grow, by the factor at every expansion step, so there is no monotone potential. The proof must show that the minimizer is eventually trapped in an interval proportional to the current diameter (Lemmas 4.2, 4.3), and separately that the diameter tends to zero whatever the sequence of moves (Lemmas 4.4, 4.5); the latter needs a case analysis of infinite runs of contractions and of the two limit points of a strictly convex level set.
The Lean development lives in the namespace NelderMeadLD.Conv1D. The simplex is an ordered pair p : ℝ × ℝ with p.1 (best) and p.2 (worst); one iteration step is a function of the pair, and the run is its -fold iterate from the initial pair. Committed conventions:
StrictConvexOn ℝ Set.univ f, bounded level sets are Bornology.IsBounded {x | f x ≤ μ} for every μ, and the minimizer is a binder with ∀ y, f xmin ≤ f y;Tendsto; Lemma 4.4 asserts the existence of a common limit of both value sequences.The printed bound of Lemma 4.2 is false (, , , ) and is not stated; the existence and minimality of and the bracketing are. A formalization that drops nondegeneracy or the ordering of the initial pair, or quantifies over an arbitrary point, is not this theorem: with every iteration is a shrink to the same point and the goal is false.
Needed infrastructure: elementary facts on strictly convex functions of one real variable (three-point bracketing, monotonicity beyond the minimizer, continuity), and bookkeeping for iterates of a piecewise-defined map. Lemma 4.1 is reusable beyond this mission. Contributions are welcome on every milestone, independently: Lemmas 4.4 and 4.5 do not use .
Cryptographic keys must be uniformly random and reproducible exactly. Many secrets people actually possess are neither: a biometric reading (an iris code, a fingerprint template), a long passphrase recalled with typos, or the correlated bits two parties obtain from a quantum channel are noisy, so two readings of the same secret differ in a few positions, and they are not uniform. Fuzzy extractors, introduced by Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007; SIAM J. Comput. 38(1), 2008), turn such a secret into a nearly uniform key that can be regenerated from any sufficiently close reading, using public helper data that does not compromise the key.
The construction for the Hamming metric is the one most used in practice and in later work on biometric key derivation and physically unclonable functions. Its history is short. Juels and Wattenberg's fuzzy commitment (CCS 1999) shifted an error-correcting code onto the secret but was analysed only for uniform inputs. The syndrome of a linear code had been used for information reconciliation in quantum key agreement (Bennett, Bessette, Brassard, Salvail and Smolin, J. Cryptology 1992). Dodis et al. defined secure sketches and fuzzy extractors for arbitrary entropy distributions, introduced average min-entropy to handle side information, and proved the bound formalized here. This mission is the first of four drawn from that paper.
All logarithms are base 2. A random variable is identified with its law. For a random variable , the min-entropy is . For a pair , the average min-entropy of given is
the adversary's chance of guessing after seeing , on a log scale. The statistical distance is , and is uniform on .
The space is , where is a finite additive group with elements, , and is the Hamming distance, the number of positions where and differ. A code with codewords is an code if distinct codewords are at distance at least ; its dimension is , so .
A secure sketch is a pair of randomized procedures with whenever . It is an average-case -secure sketch if for every pair with . A fuzzy extractor has with , and whenever . It is an average-case -fuzzy extractor if
A family of functions into is universal if for all .
For every code, every , every and every natural number
there is an average-case -fuzzy extractor.
Theorem 5.2 says that the only costs of tolerating Hamming errors are the redundancy of the code, bits, and the bits that any extractor loses. Appendix C of the paper shows the redundancy term cannot be avoided for uniform inputs, so for optimal codes the construction is optimal there. The average-case form matters for composition: it remains valid when the adversary holds side information correlated with the secret, which is the situation of every protocol that uses the key afterwards or reuses the reading.
Formalizing it produces machine-checked versions of the leftover hash lemma in its average-case form, the basic calculus of average min-entropy, and the code-offset and syndrome sketches. These are the standard tools of information-theoretic cryptography, used well beyond fuzzy extraction (privacy amplification, randomness extraction, information reconciliation). All results are proved in the paper; as far as is known, none of them has a formal proof in Lean or on this platform.
The obvious route bounds the leakage of the sketch with min-entropy and then applies an extractor to conditioned on each sketch value. That fails: conditioned on a particular sketch value, may have far less min-entropy than average, so a worst-case extractor has nothing to work with on some values, and paying for those bad values costs an extra error term (Corollary 4.2). The average-case notions exist to avoid this loss, and the chain must be kept average-case at every step. In Lean the work is in the probability bookkeeping: computing laws of pairs and triples formed by independent coin flips, rearranging them, and bounding sums of maxima over possibly infinite auxiliary types, together with the leftover hash lemma itself, which Mathlib does not provide.
Random variables are their laws, Mathlib PMFs; pairs are joint laws and randomized procedures are kernels whose coins are independent of everything else. Average min-entropy is written in the equivalent joint form , which needs no conditioning on null events. The auxiliary variable ranges over every type, not only finite ones. Logarithms are Real.logb 2; is Fin ℓ → Bool; is Fin n → F with Mathlib's hammingDist.
Explicit choices:
A trivializing formalization is ruled out: the security clause quantifies over every auxiliary type and every joint law meeting the entropy bound, and are constrained exactly as in the paper, and the universal hash family is constructed inside the goal (a supporting item states that universal families exist), never assumed.
Contributions welcome: proofs of any milestone; general lemmas on PMF marginals, statistical distance and average min-entropy, which are reusable across all four missions of this paper and in other information-theoretic cryptography; and the leftover hash lemma as a standalone result.
In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?
Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.
The process starts with one ancestor. At time , each member gives birth at rate and dies at rate ; the rates are nonnegative. Let be the population size and its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.
Define the integrated net death rate and the fluctuation by
Kendall's equations (13) and (14c) identify and for the one-ancestor process. A pair is admissible here when both rates are continuous and nonnegative on . It has mean when for every . In particular, the initial value is . These definitions let the mission quantify over every admissible rate pair with the prescribed mean.
For a positive continuously differentiable mean curve, write . The minimum-fluctuation rates are and . When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.
The goal is the simultaneous variance bound
The statement also establishes that is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for and , has minimum-fluctuation death rate zero and birth rate .
The result distinguishes mean growth from population risk. Fixing fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.
The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.
The constraint imposed by a given mean fixes the difference but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.
The Lean development represents rates and the prescribed mean as functions . Every stochastic claim is restricted to ; the integrals are oriented interval integrals from zero. Both rates are continuous on all of and nonnegative on nonnegative time. The mean is , positive on all of , and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining , and continuous without changing any comparison on . These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.
Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of . The goal uses positive and negative parts of and therefore covers any positive curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of .
The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.
A retailer that sells a line of substitutable products — sizes, colours or models of one item — over a short season without replenishment must decide how to price each variate as inventory runs down. Customers substitute: when one variate is expensive or sold out, part of its demand moves to the others. Dong, Kouvelis and Tian (M&SOM 2009) model this with a multinomial logit (MNL) choice model inside a finite-horizon dynamic program and characterize the optimal prices in closed form up to one scalar equation per period.
Retailers often cannot reprice everything. A common arrangement, described in §5.1.3 of the paper, is mixed pricing: products advertised in a printed catalogue keep their catalogue prices for the season, while products sold only online are repriced dynamically. Proposition 2 of the paper gives the optimal dynamic prices in this setting. It is the third of the paper's three optimal-pricing results, after the full dynamic pricing model (Theorem 1) and unified dynamic pricing with one common price (Proposition 1); each is the subject of its own mission in this series.
There are variates and remaining periods; time counts down. In each period one customer arrives with probability . Variate has a quality index ; the no-purchase option has utility ; is the MNL scale. The inventory is , and the in-stock set is . A sold-out variate leaves the choice set.
The variates are split into a dynamic-pricing set and a fixed-pricing set , where is always sold at its fixed price . Write and . Given dynamic prices (), an arriving customer buys an in-stock variate with probability
and buys nothing with probability (numerator ). The value function is the maximum expected revenue from periods with inventory : and
The marginal value of a unit of variate is . For a fixed-price variate put and ; for the outside option , and .
In Lean the model lives in SubstitutePricing.Mixed.Model: S1, S2, P, P0, objM, piM, deltaM, v, uf, lhs15, rhs15, rstarM.
For every and inventory , the margin equation
has exactly one solution ; the dynamic prices
are allowable and attain the maximum in the optimality equation; and
In the order the paper's proof uses them: the optimality equation rewritten as a price objective plus (29); the no-purchase and fixed-price probabilities as functions of the dynamic ones (30); strict joint concavity of the objective (31) in the dynamic choice probabilities; the form (32)–(34) of an optimal price vector; the equivalence of (15) with (36) and uniqueness of its root; and the one-period recursion .
The result says that, even with part of the line frozen at catalogue prices, the optimal dynamic prices keep the structure of the full model: every repriced variate earns the same margin over its own marginal value, and one scalar equation per period determines that margin. The fixed-price variates enter (15) in exactly the role of the outside option, each weighted by its own net value ; when , (15) reduces to the margin equation (10) of Theorem 1. One difference from the full model is that the identity fails here, so the margin is not tied to the no-purchase probability alone. The structure reduces each period's -dimensional price optimization to a one-dimensional root and supports the paper's comparison of mixed, unified and full dynamic pricing in §5.
The paper gives a complete proof (Appendix A, pp. 337–338). None of it is formalized: Prove2Me and Mathlib have no MNL pricing dynamic program. The mission produces a machine-checked version of the proof, including the step the paper leaves unchecked (below).
The objective is not concave in prices, so a stationary point in price space is not automatically a maximum, and the obvious first-order argument proves nothing by itself. The fixed-price variates make the coupling worse than in the full model: their purchase probabilities move with every dynamic price, and the identity that pins the margin in Theorem 1 is lost.
The second difficulty is a gap. The price set is , and the proof never checks that the prices are nonnegative. In Theorem 1 this follows from and . Here the left side of (15) is negative for , so follows once every ; the paper bounds nowhere. Random search over small instances found no negative optimal price, so the goal is posed as printed. A complete formalization of the goal must close this gap.
Fin n; the dynamic set is a Finset; inventories are Fin n → ℕ; time counts down with defined by recursion on t : ℕ. Results are stated for .sSup over ; coordinates outside are ignored. Fixed prices are assumed nonnegative. The goal asserts feasibility of the prices, attainment of the maximum, and the value identity, so it never rests on the value of sSup at an unattained or unbounded set.A trivializing formalization — relaxing the price set to , stating the value identity without attainment, or adding a hypothesis that bounds from below — would remove the gap rather than prove the theorem, and is ruled out.
The development needs the MNL choice probabilities, the dynamic program, a strict-concavity argument on an open simplex, and a monotonicity-plus-intermediate-value root lemma. The model file is kept identical, up to the mixed-pricing data, to the files of the other two missions in this series so they can be consolidated. Proofs of any milestone, and in particular an argument closing the nonnegativity gap, are welcome.
A backward stochastic differential equation (BSDE) prescribes the value of a process at a terminal time and asks for an adapted process that reaches it while following a given drift . Adaptedness forces a second unknown , the integrand of a martingale term. Pardoux and Peng (1990) proved that Lipschitz BSDEs are well posed. BSDEs then became a standard language for stochastic control, for pricing and hedging in mathematical finance, and for probabilistic representations of semilinear parabolic PDEs.
Many such problems carry a constraint. The value of an American option must stay above its exercise payoff, and the value of an optimal stopping problem must stay above the reward for stopping now. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE: the solution is kept above a given obstacle by an increasing process that acts only when the constraint binds. This mission formalizes the paper's first main result, existence and uniqueness of the reflected BSDE, together with the estimates its proof rests on.
Let be a -dimensional standard Brownian motion on a probability space . Let be its natural filtration, augmented by the -null sets. Fix a horizon . The data are:
with the standing assumption a.s.
A solution is a triple of progressively measurable processes, valued in , and , such that
(vii), and is continuous and nondecreasing with and (viii). Condition (viii) says that increases only when touches . The integrability conditions are (v), , and (v′), and .
Under (i)–(iv) and , the reflected BSDE with (v)–(viii) has a solution, and any two solutions satisfying (v)–(viii) coincide:
Theorem 5.2 is the foundation of the theory of reflected BSDEs. With it, the solution gives the value of a mixed optimal stopping problem (Proposition 2.3). For concave it gives the value of a combined stopping and control problem, and in a Markovian setting it gives the unique viscosity solution of the obstacle problem for a semilinear parabolic PDE. The other two missions of this series formalize those consequences, and both use the existence and uniqueness proved here. The model has many later extensions (two obstacles and Dynkin games, jumps, quadratic growth), and the pricing of American options under constrained or nonlinear dynamics is formulated through it.
The result is classical and fully proved in the paper. As far as is known, no machine-checked proof of existence for a (reflected or plain) BSDE exists. The remaining work is the formalization of the known proof: the Skorohod lemma, the optimal-stopping representation, the a priori and stability estimates, and the Picard contraction. The milestones are reusable well beyond this paper, in particular the Skorohod lemma, the estimates, and the identification of the reflected solution with a Snell envelope.
The natural first idea is to treat (vi) as a forward equation and reflect it pathwise with the Skorohod map, as in forward reflected SDEs. This fails: the pathwise reflection of a backward equation produces a process that is not adapted (Proposition 2.2 gives as a supremum over the future). The adaptedness of comes only from the choice of , i.e. from a martingale representation. Any construction must produce and together, and the estimates must control the contribution of using only the minimality condition (viii). In the formal setting, Mathlib has Brownian motion, filtrations, stopping times and conditional expectations, but no stochastic integral (the platform definition Peng1990.SMP.IsItoIntegral supplies one, without any calculus), no Itô formula, no martingale representation, no Burkholder–Davis–Gundy inequality and no Snell envelope theory in continuous time.
The Lean development builds on the published definitions Peng1990.SMP.Stochastic: standard -dimensional Brownian motion, as L2F, and the Itô integral IsItoIntegral. It commits to the following conventions:
ℝ≥0, with , and only matters;Proposition 2.3 additionally assumes , which the paper's Remark 3.2 allows without loss of generality, so that every conditional expectation in it is of an integrable variable. The constants of Propositions 3.5 and 3.6 are quantified before the Brownian dimension, probability space, data and solution, and depend only on ; a per-solution constant would make both statements trivial. The condition is part of every statement, since without it no solution exists. Proposition 3.1 and Corollary 3.3 (β) are not posed.
A complete proof needs Itô's formula for , the Burkholder–Davis–Gundy inequality, Gronwall's lemma, martingale representation for the Brownian filtration, and the Snell envelope with its Doob–Meyer decomposition. Each of these is reusable on its own, and contributions of any of them are welcome, as are proofs of individual milestones.
A partially observable Markov decision process (POMDP) models an agent that acts in a stochastic world whose state it cannot see directly. The agent sees only noisy observations. POMDPs are the standard model for planning under uncertainty in robotics, dialogue systems, medical decision making and machine maintenance. The exact finite-horizon theory goes back to Smallwood and Sondik (1973), who showed that the optimal value function is piecewise linear and convex in the agent's belief, so that it can be represented by a finite set of vectors.
Kaelbling, Littman and Cassandra (1998) brought this theory to artificial intelligence. Their paper introduces policy trees as the objects behind those vectors and presents the witness algorithm, an exact value-iteration method. It is one of the most cited papers on POMDPs. The correctness of the witness algorithm rests on a single statement, Theorem A.1 of the paper's appendix, the witness theorem. This mission formalizes that theorem together with the lemmas its proof uses.
Timeline:
A POMDP is a tuple with finite sets of states, of actions and of observations. Taking action in state leads to state with probability and earns expected reward . The agent then observes with probability . Rewards are discounted by a factor with ; is the plain finite-horizon problem.
A belief state is a probability vector on ; denotes the set of all of them. After action and observation , the belief is updated by Bayes' rule to . The normalizing constant of this update is .
A -step policy tree is a single action when . For it is a root action together with one -step subtree for each observation . Its value is defined by the recursion
and at a belief state it is . The optimal -step value is over all -step trees.
A tree in a finite set is useful if some belief state gives it a strictly larger value than every tree of with a different value function. The useful trees form the parsimonious representation of . Let be the useful -step trees. The candidates are the -step trees with root and all subtrees in , and is the set of trees useful in . The Q-function is
For a set of candidates, is the current approximation. For , an observation and , the tree is with its subtree for replaced by .
For a nonempty ,
Trees with the same value function are identified, as in the paper. The statement is exact, with no constants.
The witness theorem is the stopping and growth criterion of the witness algorithm. If no single-subtree modification of the current trees beats all of them at some belief state, the current set represents the Q-function exactly. Otherwise the belief found is a witness and yields a new useful tree. Because each test is one linear program, the theorem turns an infinite search over belief space into finitely many linear programs. It is also the basis of the paper's complexity claim, polynomial time in , , , and . Incremental pruning and later exact POMDP solvers rely on the same parsimonious-set machinery.
The theorem is proved in the paper; it has not been machine-checked. A formal development would also provide reusable infrastructure: policy trees, their value recursion, belief updates, and the existence and minimality of parsimonious representations of finite sets of linear functions on the simplex. That infrastructure is needed for any formal treatment of exact POMDP value iteration.
Most steps are finite algebra. The part that needs care is the "if" direction of the goal. A belief at which a new tree beats all of shows that the true Q-function exceeds the approximation. It does not directly show that a useful tree is missing, because the maximizing tree at that belief may tie with other trees there. One needs the representation property of the parsimonious set (milestone 3): at every belief, the maximum over all candidates is attained by a useful one. Proving this means moving from a belief where several value functions tie to a nearby belief, inside the simplex, where exactly one of them is strictly largest. The proof on p. 131 also needs the Q-function to be attained on the candidate set, so that the improving subtree lies in (milestones 4 and 5).
POMDP.IsValid.PolicyTree A Ω n is the type of -step trees, so statements about -step trees with subtrees use . The type is finite, and the set of all trees of a given depth is Finset.univ.stdSimplex ℝ S. Every "there is some belief state" ranges over the simplex, not over .Finset.sup' over nonempty finite sets, or IsGreatest.The following encodings would make the theorem trivial or false, and are excluded: comparing trees by equality instead of by value function, letting range over all of , taking to be an arbitrary set, allowing , and defining the true Q-function as itself.
Contributions are welcome at every level. The parsimonious-representation lemma (milestone 3) is the reusable geometric core. The subtree-swap lemma and the Q-function identity are the algebraic core.
A backward-forward stochastic differential equation couples two equations that run in opposite time directions: a forward equation for a state , started from a given input, and a backward equation for a quantity , pinned at a terminal time by a random variable . Each equation's coefficients depend on both unknowns, so the solution at time depends on the past of and on the conditional future of . Such systems arise in stochastic control (the adjoint equation of the stochastic maximum principle runs backward while the state runs forward) and in mathematical finance (an asset's price is forward, a hedge or value process is backward).
Antonelli's 1993 paper (Ann. Appl. Probab. 3(3), 777–793) is one of the first treatments of the coupled problem. Pardoux and Peng (1990) had established existence and uniqueness for decoupled backward equations driven by Brownian motion. Antonelli proved existence and uniqueness for the coupled system under a smallness condition, and gave examples (§3) showing that without such a condition a solution may fail to exist. This mission formalizes the bounded-variation case of that result, Theorem 3.1.
Fix a horizon and a probability space with a filtration satisfying the usual hypotheses: it is right-continuous, and contains every -null set.
An integrator is an adapted process whose paths have bounded variation on , with . It is written with adapted, nondecreasing and right-continuous, and , the total variation of on . It is bounded: . The pathwise integral is the Lebesgue–Stieltjes integral over .
The system involves two integrators and the increasing process
whose pathwise Stieltjes measure is . The Doléans measure of on gives the norm
and is the space of jointly measurable processes with finite norm. The size of is .
The data are coefficients , a constant , a terminal value and a forward input . They satisfy:
In addition is -measurable and is adapted. The system is
and its right-hand side defines an operator , (3.3). A solution in the sense is a pair with and -a.e.
If and are dominated by and
then there is a progressively measurable solution of (3.1)–(3.2) in the sense, and any two progressively measurable solutions agree -a.e.:
The theorem identifies a regime in which a coupled forward-backward system is well posed. The integrability required is only , and the smallness condition ties the Lipschitz constant to the total mass of the driving integrators. With it reads , a small-horizon condition. The paper's Example 1 (mission 3 of this series) shows that at , a solution may fail to exist, so some restriction of this type is necessary. Later work on forward-backward equations, for instance the four-step scheme of Ma, Protter and Yong (1994), replaced the smallness condition by other structural assumptions. Antonelli's small-horizon result remains the base case those methods extend.
The result is proved in the paper. No machine-checked version of it, or of any backward stochastic differential equation, exists in Mathlib or on the platform. The formalization adds three things on top of the paper. It makes the solution concept precise: versions, integrability, and -a.e. equality. It repairs a gap in the printed proof (see Formalization scope). And it builds pathwise Lebesgue–Stieltjes integration against adapted bounded-variation processes, together with the optional projection identity (2.6), as reusable infrastructure.
The Banach fixed point theorem does the final step once the contraction estimate holds. The difficulty lies in reaching that estimate. The -component is a conditional expectation, defined for each only up to a null set, and these null sets accumulate when the process is integrated against , which may charge random times. The estimate has to be transported from "for each , almost surely" to "-almost everywhere". That needs càdlàg versions and the optional projection theorem, which Mathlib lacks. A second point: the naive bound treats the forward and backward differences separately and gives the constant . Obtaining requires combining both differences inside one conditional expectation, and that uses the adaptedness of the forward difference.
Time is with horizon ; integrators are frozen after . Each integrator carries its minimal Jordan decomposition as data, tied to Mathlib's eVariationOn. Pathwise measures are Mathlib's Stieltjes measures, and integrals are over . Norms are lower integrals in . Every conditional expectation is accompanied by the integrability of its argument, since Mathlib's condExp of a non-integrable function is . A version of must be jointly measurable and have càdlàg paths on . Without the càdlàg requirement, two versions can differ on the graph of a random time charged by , and the contraction estimate fails.
The formalization commits to these readings of the paper:
The solution concept rules out trivial solutions. It requires , the integrability of every argument of the conditional expectation, and a càdlàg version, and existence asserts a progressively measurable pair. A pair satisfying the equations only through Lean's junk values therefore does not count.
A complete development needs:
All four are reusable well beyond this mission. Contributions to any of them are welcome, as is a proof of any milestone in isolation.
Many nonlinear control systems behave like a chain of integrators, , with additional terms that are small either near the origin or far from it. Designs based on weighted homogeneity handle such systems by making the closed loop invariant under a dilation, which gives robustness to perturbations that are dominated by the homogeneous part (Rosier, Homogeneous Lyapunov function for homogeneous continuous vector field, Systems & Control Letters, 1992, doi:10.1016/0167-6911(92)90078-7). A single homogeneous approximation, however, describes the system only at one scale. A perturbation that is negligible near the origin may dominate at infinity, and a design tuned to the origin can then fail globally.
Andrieu, Praly and Astolfi (arXiv:0903.0298v1; SIAM J. Control Optim., 2008, doi:10.1137/060675861) introduce homogeneity in the bi-limit: a function or vector field has one homogeneous approximation near the origin and another, possibly with different weights and degree, at infinity. They develop the basic calculus of this notion, a converse Lyapunov theorem for it, a recursive observer and a recursive state feedback for the chain of integrators, and combine them into a global output feedback. This mission formalizes that output-feedback result and the chain of results it rests on.
For a weight with all and , the dilation is . A continuous function is homogeneous in the 0-limit with triple , degree , if is continuous and not identically zero and, for every compact and every , there is such that
Homogeneity in the ∞-limit with triple is the same statement for all . A vector field is homogeneous with triple , , when each is homogeneous with triple and . Bi-limit means both at once.
For the chain of integrators, and . Given degrees , the weights are
The output feedback studied is
with a gain , a state feedback and an output-injection vector field , where means . Its homogeneous approximations are the same closed loop with and with in place of .
For and there exist , homogeneous in the bi-limit with triples and , and , homogeneous in the bi-limit with triples and , such that
The pair is fixed before . No constant appears in the goal.
The theorem gives a single dynamic output feedback for the chain of integrators that is homogeneous with prescribed degrees near the origin and at infinity, and that stabilizes globally for every gain . Because the degrees at the two ends are independent, the same design can be matched to perturbations of different orders at small and large amplitudes; the paper derives from it output-feedback stabilizers for systems in feedback and feedforward form (Corollaries 5.2 and 5.3), which are outside this mission. The converse Lyapunov theorem (Theorem 2.20) and the key lemma (Lemma 2.13) are general tools for any vector field homogeneous in the bi-limit.
The results are proved in the paper; none of them, nor the notion of homogeneity in the bi-limit, has a machine-checked proof. The platform has a definition of global asymptotic stability for continuous vector fields (from the series on Chitour, Ushirobira, Efimov and Perruquetti's prescribed-time stabilization) and Mathlib has the needed analysis, but there is no converse Lyapunov theorem and no theory of weighted homogeneous vector fields. A complete formalization would supply both.
Lyapunov arguments for homogeneous systems usually compare a function with its homogeneous approximation on the unit sphere and then scale. With homogeneity in the bi-limit the comparison holds only for small or for large dilation parameters, with no control at intermediate scales, and the two approximations have different weights, so no single dilation brings the whole space to a compact set. Each statement has to hold for the system and for both approximations at once. Theorem 2.20 additionally requires a converse Lyapunov theorem for continuous, non-Lipschitz vector fields whose solutions need not be unique, so a flow map is not available. Finally, the gain in the goal is arbitrary: an argument that only works for large enough proves a weaker statement.
Points of are functions Fin n → ℝ, with the paper's coordinate at index ; the closed loop lives on Fin (n + n) → ℝ with first and second. Real powers are Real.rpow; the signed power is . Every clause of Definitions 2.1, 2.3 and 2.5 is kept: positive weights, nonnegative function degrees, continuity, approximating functions not identically zero, uniformity on compact subsets of . Dropping any of them makes the goal weaker than the paper's.
Global asymptotic stability reuses the published ChitourPrescribedTime.FixedTime.GloballyAsymptoticallyStable on the Euclidean space, applied to the time-invariant field: the origin is an equilibrium, every initial state has a solution on , and stability and uniform attractivity hold for every solution. The mission adds that no solution escapes to infinity in finite time, so that every solution is covered; for continuous autonomous fields this is the textbook notion. Positive and negative definiteness, properness ( along the cocompact filter), and partial derivatives (Fréchet derivative on a basis vector) are defined in the mission's definition files.
Corrections and readings, each disclosed in the item concerned:
A formalization in which the closed loop is replaced by its linearization, the homogeneity predicate is weakened to pointwise convergence, or the quantifier on is moved before and , proves a different statement and does not close the goal. Contributions welcome: a library of weighted dilations and homogeneous functions, the converse Lyapunov theorem, and proofs of the milestones in any order.
Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation overhead. Their 1996 paper gives an upper-bound construction as well as the lower-bound theorem targeted here. The issue matters when a storage observer can see which addresses are accessed but must learn nothing about the program's private requests.
Theorem 6.1 of the paper states that simulating steps requires at least the initial memory size and, asymptotically, a multiple of accesses. Its proof introduces a simpler ball-and-cell game that grants the player more information and freedom than the RAM simulation. The mission formalizes that game and its lower bound. This makes the combinatorial content of the published argument a precise theorem about randomized behavior and visible observations. The paper's earlier Theorem 1.2.2 on p. 437 is labeled informal and has a different explicit bound; the target here is Theorem 6.1 on pp. 469–470.
There are numbered balls and numbered cells. Cell initially contains ball , and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most balls. In one access, the player names a cell and secretly takes its ball into a nonfull hand, places one held ball into an empty cell, or leaves the cell unchanged. Taking from an empty cell and placing into an occupied cell are illegal. The observer sees the named cell at each access but not the hidden operation. A run of accesses is written , and its visible sequence is .
A request sequence names a ball for each of rounds. A run satisfies if it is legal and there are indices such that ball is in the player's hand after the first accesses. Equal indices are permitted: several rounds may finish after the same access. The player may know the entire request sequence in advance. That assumption is part of the paper's game, and the paper notes that its lower bound does not require an online player.
A randomized player assigns each request sequence a probability distribution over finite runs. It is correct if every run with positive probability satisfies its requests. It is oblivious if the distribution of is identical for every pair of request sequences of length . Thus the observer cannot infer the requested balls from the accessed cells, even statistically. These conditions quantify over all request sequences, not a selected input or a single deterministic access pattern.
For every correct oblivious player and every run in the support of its response, the mission targets
where and depend only on the fixed hand size . This is the paper's form, with representing the number of initially occupied memory words. It asserts a bound on every possible run, rather than only on average access count. No numerical constant is prescribed by the paper.
The milestones record the first-round bound, the at-most- count of legal hidden action sequences compatible with a visible sequence, and the implication from obliviousness that one visible sequence can serve every request sequence. They then state the corrected finite counting bounds
These preserve the paper's non-strict round ends. The milestone source text records the published formulas, while the formal statements and descriptions identify the corrections.
The result limits how cheaply a simulator can hide a program's memory access pattern when the observer sees addresses. In the game, a player is even allowed to remember the entire ball placement without cost, know the future requests, and randomize its actions. A lower bound under these permissive conditions applies to the more constrained access-pattern problem that motivated the game, subject to the paper's reduction from simulation to the game. The term also accounts for the initially occupied memory, independently of the asymptotic term.
The theorem is a published mathematical result, but the mission's Lean declarations are statements with proof holes until solvers supply machine-checked proofs. Formalizing the game creates reusable definitions for legal hidden operations, request satisfaction, randomized players, and visible distributions. Formalizing the corrected counting targets also makes explicit a discrepancy in the printed proof rather than silently relying on an invalid intermediate inequality.
The main difficulty is accounting for requests when several rounds end at the same access. The paper's observation that a fixed -access run serves at most request sequences is false under its own non-strict indices. A run that fetches every ball it can hold may answer many later rounds without making another access. Likewise, the alternative binomial count in footnote 29 assumes distinct completion points and fails when . The final asymptotic result still has a valid corrected counting target, but a proof cannot quote the published intermediate formulas literally. Randomized behavior adds another precise requirement: equality of visible distributions must support conclusions about runs with positive probability for each request sequence.
The Lean carrier is the paper's ball-and-cell game from §6, rather than the interactive RAM machine model of §2. The game relaxes the simulation by giving the player free memory of ball locations and advance knowledge of requests. Balls, cells, and rounds use finite types Fin m and Fin t; these are zero-based encodings of the paper's and round labels. Action steps are counted from one, with the initial state at step zero. PMF represents the player's discrete probability distributions, and equality of PMF.map visible represents observer independence. Every positive-probability run must be legal and satisfy its requests. The visible and hidden sequences have the same finite length .
The two printed estimates and are false: with and , taking both balls in two accesses satisfies all request sequences, while the printed product is . Footnote 29's also vanishes in this example. The formal milestones use Nat.multichoose q t to accommodate repeated round ends; at its value is defined directly, so no negative binomial upper index is used. The logarithm in the goal is the natural logarithm, and a threshold handles small .
Correctness and legality are part of the player type, so an unrestricted sequence of cell names cannot satisfy the mission by bypassing the hand and cell rules. Obliviousness uses equality of full distributions, and the goal quantifies over every supported run. The required development includes finite-state transition reasoning, finite combinatorial counts, PMF support and mapping, and real logarithm estimates. These components, especially the game interface and support lemmas, can be reused by later access-pattern formalizations.
In the edge-disjoint paths problem (EDP) one is given an undirected graph and a list of source–sink pairs, and asks how many pairs can be connected simultaneously by paths that share no edge. Its relaxation EDP with congestion (EDPwC) allows every edge to carry up to a fixed number of paths. Both are central problems of network routing and of approximation algorithms, and the standard algorithmic tool for them is the multicommodity flow relaxation: a linear program that may split each pair's unit of demand fractionally over many paths. Rounding this LP is how most approximation algorithms for routing work, so the ratio between its optimum and the best integral routing, the integrality gap, bounds what any LP-based algorithm can achieve.
Without congestion the gap of this relaxation can be as large as (Chekuri–Khanna–Shepherd 2006), and the question is how much a small congestion helps. Andrews, Chuzhoy, Guruswami, Khanna, Talwar and Zhang (Combinatorica 2010) proved hardness of approximation for EDPwC (their Theorems 1 and 2) and, independently and unconditionally, that the gap of the relaxation remains even when the integral solution may use congestion (their Theorem 5). In particular, for every fixed integer the gap between -integral and fractional multicommodity flow in undirected graphs is superconstant. This mission formalizes Theorem 5 for EDPwC.
Fix integers and . Write for and for the natural logarithm, and set
A random -uniform hypergraph on the vertex set has hyperedges , chosen independently, each uniformly among the -element subsets of the vertices.
From one builds a graph . For every hyperedge it has two vertices joined by a special edge; for every vertex of it has a source and a sink . If lies in the hyperedges with , the regular edges , for , and are added. The canonical path of is ; it crosses the special edge of every hyperedge containing . The EDP instance has one pair for each .
A feasible fractional solution puts flow on – paths , with routed amount for each pair and at most one unit of flow through each edge; its value is . An integral routing with congestion at most connects a set of pairs, each by one path, so that every edge lies on at most of these paths; its value is the number of connected pairs.
The analysis uses three events of : , that some set of vertices contains no hyperedge; , that more than vertices lie in more than hyperedges; and , that the graph obtained from by contracting every special edge has more than cycles of length at most .
There are absolute constants and such that for all and all integers with some hypergraph as above satisfies
so the integrality gap is at least . The paper's Theorem 5 states this as for congestion and vertices; the goal keeps the paper's own Section 2 parameters, which fix the instance and leave the constants open.
Lemma 6, Lemma 7 and Lemma 8 (); the joint good event of Section 2.4; the fractional solution of value ; and the three bounds of the gap analysis, (canonical paths), (long non-canonical paths), (short non-canonical paths), combined into .
The result shows that the multicommodity flow relaxation cannot certify a constant-factor approximation for undirected EDPwC with any constant congestion: against integral solutions of congestion its gap is at least . Any algorithm that compares its output with this LP inherits the bound. It complements the paper's hardness results, which hold only under a complexity assumption. The instance is a short explicit construction from a random hypergraph, so the theorem is also a statement in probabilistic combinatorics: random sparse uniform hypergraphs are, with constant probability, simultaneously "covering" (no large hyperedge-free set), of bounded degree, and nearly free of short cycles.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces one: a formal model of the path LP and of congestion-bounded integral routings on simple graphs, reusable for other routing gaps; a formal random-hypergraph model with first-moment and Chernoff-type estimates; and the deterministic gap analysis. Variants with better constants, or the stronger statement that at least a quarter of all hypergraphs work, are welcome as additional results.
The fractional side and the bound on canonical routings are short. The difficulty lies in two places. First, Lemma 8 bounds the expected number of short cycles of ; the adjacency of depends on all hyperedges at once (consecutiveness along each vertex's sequence), and the obvious estimate through the intersection graph of fails, because many hyperedges through a common vertex form a clique there. What keeps the count small is the order structure of each vertex's hyperedge sequence, which the intersection graph forgets. Second, the bound on short non-canonical paths requires turning two distinct routing paths of a pair into a short cycle of the contracted graph and charging it with the congestion constraint. Finally, the closing estimate holds only for large in the stated range of , and the printed chain for it is not literally correct, so the asymptotics have to be done afresh.
Vertices of are Fin n, hyperedges are indexed by Fin m with , and is an element of Fin m → {s : Finset (Fin n) // s.card = c}; probabilities are normalized counts over this finite set (uniform measure, which is independence of the hyperedges). The conventions are:
The goal cannot be met by an unrelated graph: the instance must be for a hypergraph with exactly hyperedges of size on vertices, the fractional solution must respect and capacity , and the integral bound is over all routings of congestion .
Not in scope: the ANFwC half of Theorem 5, the remark on a superconstant gap at , and the hardness results of Sections 3–5 (Theorems 1 and 2, Corollaries 3 and 4).
A complete development needs Chernoff and Markov bounds for counting measures, binomial-coefficient estimates, cycle extraction from two distinct paths in a simple graph, and the asymptotic estimates for . The routing and LP definitions and the cycle-extraction lemma are reusable beyond this mission.
A simulation run often estimates a steady-state mean without producing independent observations. A confidence interval must account for dependence in the output, and the relevant variance constant may be unknown. Standardized time series (STS) methods use the shape of an integrated output path to cancel that constant rather than estimating it separately. The resulting interval can be computed from one run, but its length can vary substantially with the chosen standardizing functional. Glynn and Iglehart introduced a common functional framework for these methods and asked how short their expected intervals can be as the run grows. Their 1990 paper identifies a universal lower bound.
The comparison is operational. A shorter confidence interval conveys a more precise estimate at the same nominal coverage. The authors also compare STS with procedures that consistently estimate the variance constant. They state that the lower bound is attained by the latter procedures and approached, but not attained, by STS intervals. The present mission isolates the bound for STS itself, Corollary 4.16. It does not make the claim that a particular STS rule attains it. This distinction follows the paper's introduction and §4.
Let be a real simulation output process for . Its integrated average path at run length is for . The unknown steady-state mean is . The paper assumes a functional central limit theorem in the space of continuous real paths:
where is standard Brownian motion. Convergence is weak convergence of random continuous paths in the uniform topology. This is Assumption (2.1), rather than a claim that every output process satisfies it. The paper lists several classes of processes for which such a theorem is available under further conditions (§2, pp. 2–3).
An STS scale functional belongs to when it is measurable, positively homogeneous, unchanged by subtracting any multiple of the identity path , positive at almost surely, and continuous at almost surely. The last two conditions ensure that the Brownian ratio is a meaningful distributional limit. The paper also describes these functionals through the bridge map : a member of can be written as for a suitable . Thus the scale is determined by a Brownian bridge while the endpoint is independent of it (Propositions 2.7–2.8).
Define . For a confidence level , choose endpoints with . The STS confidence interval from equation (2.10) has endpoints and . Its length is . Here lies strictly between zero and one; the endpoint equation is part of the construction, not an arbitrary choice.
The goal is Corollary 4.16 for every nonnegative under Assumption (2.1). Write for the standard normal distribution function and . Then
The expectation and liminf admit . The statement does not impose an integrability assumption that would remove that case. It quantifies over every admissible STS functional and every interval whose endpoints have the specified Brownian confidence mass (Corollary 4.16, p. 12).
Three substantial targets precede the corollary. Proposition 4.1(a) relates scaled expected length to . Proposition 4.3 says a symmetric choice of minimizes . Theorem 4.8 gives , where denotes the quantile of . The milestone list also includes the cited Brownian independence, mixture distribution, scale invariance, and continuous mapping statements that put these targets in context.
The corollary supplies a benchmark for the asymptotic expected length of any interval in this STS class. A proposed standardizing functional cannot beat the normal-quantile constant while retaining the stated functional limit and confidence construction. It also identifies the quantity against which the paper's other interval procedures can be compared. The bound applies uniformly to the class , not to a chosen batch size or a particular form of (Glynn–Iglehart 1990, §4).
The mathematical result has been proved in the source paper. This mission supplies formal statements and their shared definitions as proof targets; it does not claim that their Lean proofs already exist. A complete development would formalize the known arguments for the milestones and corollary, including the Brownian path representation, weak convergence, quantile properties, and expectation inequalities. Those components could be reused in other work on simulation output analysis and ratios of weakly convergent processes.
Weak convergence alone does not imply convergence of expectations. In particular, a continuous mapping limit for cannot simply be integrated as an ordinary finite real expectation when the family is not uniformly integrable. Proposition 4.1(a) asks only for a lower bound, and its statement must still account for . This is why the goal is expressed with a liminf and extended nonnegative expectations rather than a real-valued limit. A separate difficulty is that the interval width depends jointly on a distributional scale and a choice of two quantiles. Bounding either one in isolation does not state the corollary.
Paths are Mathlib's with its uniform metric and Borel sigma algebra. A standard Brownian motion is a measurable random continuous path agreeing with an -indexed real Brownian motion on . The paper's discontinuity set is the set where is not continuous. Assumption (2.1) includes joint measurability of and finite-interval pathwise integrability so that each integrated average is defined. The path is supplied together with its defining integral equation, which determines it pointwise. Its values are not free parameters.
Indices are natural numbers. At , the average uses Lean's total division and is zero; this initial value does not affect an asymptotic statement. The positive Brownian scale is finite. The parameters satisfy , and . The normal and STS quantiles appear as real parameters pinned by their distribution-function equations, avoiding an unbounded or empty real infimum. Expected nonnegative lengths and scales are integrals valued in . The class explicitly requires measurability of , the standing convention needed for its equality with .
The corollary retains the entire class and Assumption (2.1), with on all continuous paths. It cannot be replaced by a statement about a single easy functional or by assuming the bound on an auxiliary criterion. Useful contributions include the Brownian bridge independence theorem, the normal scale-mixture identity, distribution-function regularity, and the asymptotic expectation result.
Szemerédi's regularity lemma partitions the vertex set of any graph into a bounded number of parts between which edges are distributed almost randomly. It is a central tool of extremal graph theory, but the number of parts it needs is a tower of exponentials in , which makes it unusable in algorithms. In 1996 and 1999 Frieze and Kannan introduced a weaker notion, now called weak regularity: a partition is good if, for every pair of disjoint vertex sets , the number of edges between them is predicted, up to an additive error , by the densities between the parts. This weaker requirement is enough to approximate dense instances of Max-Cut and other problems, and it can be met with only parts.
The paper Frieze and Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999) derives such partitions from a matrix decomposition. Section 5.1 shows that if the adjacency matrix of a graph is approximated by a sum of a few cut matrices with small error in the cut norm, then the atoms of the sets defining those cut matrices form a pseudo-regular partition. The weak regularity of this paper later became the basis of the cut-distance theory of graph limits (Lovász, Large networks and graph limits, AMS, 2012).
Let be a simple graph with vertices and adjacency matrix . For a real matrix and write . A cut matrix has entry on and elsewhere. A cut decomposition of width is a sum of cut matrices ; its error is .
Let be a partition of with index set , write , let be the number of edges between disjoint sets and , and let be the density between parts. The deviation from regularity is
and is -pseudo-regular if for all disjoint .
For a partition , the block average of takes the value on , and is compatible with if it is constant on every block . The atom partition of is the coarsest partition of in which every and is a union of parts; it has at most parts.
If the cut decomposition has error at most , that is
then the atom partition of the sets satisfies
i.e. it is -pseudo-regular. The width is unconstrained: the statement holds for decompositions of any width, and the width only enters through the bound on the number of parts.
Claim (50) is the bridge from matrix approximation to graph partitions. Combined with Theorem 7 of the same paper (every matrix has a cut decomposition of width at most with cut-norm error for a graph), it gives the weak regularity lemma: every graph has a -pseudo-regular partition into at most parts. Pseudo-regularity in turn means that is determined up to by the numbers , which reduces Max-Cut and related problems on dense graphs to a search over a bounded-dimensional space. Lemma 7(a) is of independent use: Section 5.1.1 of the paper applies it again to pass to an equitable refinement.
The results are proved in the paper. Mathlib contains Szemerédi's regularity lemma in its equipartition form, and the platform has a published statement of it; neither the Frieze–Kannan weak regularity statement, the deviation , nor Lemma 7 has a machine-checked proof known to this mission. The mission produces a formal statement and proof of the partition half of the weak regularity lemma, reusable with any cut decomposition, including the existence result of the companion mission on cut decompositions.
The identity (47) and the compatibility of are bookkeeping, but bookkeeping over Mathlib's Finpartition, atomise and the rational-valued edgeDensity, with sums over parts that must be regrouped into sums over vertices. The substance lies in Lemma 7(a). The obvious argument bounds by , and the difficulty is the second term: is constant on the blocks of , but its block sums on arbitrary have to be controlled by block sums of , on which and need not agree. The printed argument handles only disjoint , while the lemma is stated, and needed, for all pairs; a complete proof must cover pairs that overlap.
All objects are defined in one definitions item in the namespace FriezeKannan.PseudoReg. The vertex set is a Fintype with decidable equality, the graph a SimpleGraph V with decidable adjacency, and its adjacency matrix Mathlib's adjMatrix over . A partition of is a Finpartition of Finset.univ, whose parts are the index set ; refinement is Mathlib's order . Densities are SimpleGraph.edgeDensity, cast to , for all pairs of parts. For distinct parts this is the paper's . For a part with itself it is the block average , not the value printed in the §5 preamble: with the printed value the identity (47) fails on diagonal blocks, and the proof of (50) uses (47). The atom partition is Mathlib's Finpartition.atomise of the family . The Frobenius norm is the square root of the sum of squared entries.
The paper takes the cut matrices from its Theorem 2, a randomized algorithm. The goal replaces this by the one property its proof uses: the hypothesis for all (Theorem 2 bounds the cut norm, a maximum over all pairs, by ). The paper's symmetrised error is not needed. Lemma 7 is stated for an arbitrary real matrix , and the suprema of Lemma 7(a) are written as "every bound on the right-hand family gives the bound on the left-hand family", over all pairs . No hypothesis is added to any statement.
The partition in the goal is fixed as the atom partition. A formalization that let the partition vary would be trivial: the partition into singletons has .
Needed infrastructure: regrouping sums over a Finpartition, and block sums of matrices constant on the blocks of a partition, on arbitrary and on block-compatible sets. These are reusable for any statement about cut norms of block-constant matrices. Proofs of the milestones, of the companions, and of the goal are all welcome.
A cooperative game with side payments assigns to each coalition of players the total payoff it can secure on its own and share freely among its members. The core is the set of ways of dividing the payoff of the grand coalition that no coalition can improve upon. It is the basic stability notion of cooperative game theory and of its applications in operations research: cost allocation for shared facilities, network design, inventory pooling and linear production games all ask whether a core allocation exists and what it looks like.
The core can be empty, and the question of when it is not was answered independently by Bondareva (1963) and Shapley (1967): the core is nonempty exactly when the game is balanced, a linear-programming condition on weighted families of coalitions. Scarf (1967) extended the existence half to games without side payments, and Billera (1970) recast balancedness for those games.
Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981) reads these results through fuzzy coalitions, in which each player participates at a rate between 0 and 1. In §6 every game on a family of coalitions is extended to a concave positively homogeneous function of fuzzy coalitions, and the Bondareva–Shapley theorem becomes a statement about that extension. This mission formalizes §2 and §6 of the paper: the core of a fuzzy game with side payments, its superdifferential description, and Proposition 6.1.
Let be the set of players. A coalition is identified with its characteristic vector , and . A fuzzy coalition is a vector , where is the rate at which player participates.
A fuzzy game with side payments is a worth function with that is positively homogeneous, for . Homogeneity extends from to the orthant . Its core is
the allocations that no fuzzy coalition blocks. The superdifferential of at is .
A usual game with side payments is given by a family of nonempty coalitions that contains and every singleton , and by a worth for each . Its core is the set of with and for every . For , is the set of nonnegative weights , , with for each player , and
The game is balanced if .
The first half is the Bondareva–Shapley theorem for an arbitrary family . The second identifies the core of the discrete game with the core of the fuzzy game .
Proposition 6.1 is the standard criterion for the existence of core allocations in transferable-utility games. In operations research it is the tool behind core results for linear production games, flow games, facility location and inventory games: one exhibits a family of balancing weights, or the absence of one, and reads off whether a stable cost or profit allocation exists. Aubin's version adds that a balanced game's core is the superdifferential of a concave function, so it is described by convex analysis and, when is smooth at , reduces to a single point given by the gradient.
The result is classical and proved in the literature. To our knowledge, no machine-checked proof of the Bondareva–Shapley theorem exists in Mathlib or on this platform: the platform has results on cores of convex (supermodular) games, which are a different hypothesis. The mission therefore produces a first formal proof of the theorem for a general family of coalitions, the superdifferential description of the fuzzy core, and the minimality of the concave extension . The definitions (fuzzy coalitions, balances, ) are reusable by later missions on games without side payments and on values of fuzzy games.
The inclusion and the necessity of balancedness are short computations with the balancing weights. The difficulty is sufficiency: from , a core allocation has to be produced. This is an existence statement for a system of linear inequalities, and it needs a duality or separation argument. Mathlib's finite-dimensional linear programming duality and separation theorems do not apply off the shelf, because is a supremum over a polytope of weights indexed by coalitions, and its attainment and finiteness must be established first. Proposition 2.1 similarly needs the existence of supergradients of a concave function at an interior point and their compactness, which are not packaged for functions defined only on an orthant.
Players are Fin n; multiutilities and fuzzy coalitions are Fin n → ℝ with the coordinatewise order, and the cube is Set.Icc 0 1. The commitments are:
DifferentiableAt at the interior point , and is the vector of partial derivatives.Balancedness is the equation with built from the balances of §6 (3)–(4); a formalization that defines "balanced" through the core, or takes to be an envelope already known to agree with the core, makes the goal empty and is ruled out. Contributions welcome: proofs of the milestones, a general Bondareva–Shapley lemma for finite families of coalitions, and supergradient existence for concave functions on convex sets with nonempty interior.
Interior-point methods transformed linear programming in the 1980s and 1990s. A natural question was whether the same ideas carry over to nonlinear programming, where the objective and the constraints are general smooth functions. Sequential quadratic programming (SQP) methods were then the method of choice for small and medium nonlinear problems, but each iteration solves a quadratic subproblem with all the constraints, which scales poorly. Byrd, Gilbert and Nocedal (INRIA RR-2896, 1996; journal version Math. Program. 89 (2000) 149–185) combine the two. They apply a trust-region SQP method to the barrier problem of the nonlinear program, keep the slack variables positive through the trust region and the barrier term, and prove global convergence without assuming that the constraint gradients have full rank. The algorithm became the basis of the interior-point solver KNITRO (Byrd, Hribar, Nocedal, SIAM J. Optim. 9 (1999)).
The analysis is of interest beyond this one method. It isolates the situations in which an interior-point method can fail: convergence to a stationary point of the infeasibility, or to a point where the constraint gradients of the active constraints are dependent. It shows that these are the only failure modes.
Let and be continuously differentiable. The problem is
For a barrier parameter , introduce slacks , , and the barrier problem
Write for the matrix of constraint gradients, , , and , , along a sequence of iterates. All norms are Euclidean. A second norm on is arbitrary.
Algorithm I solves (2.2) for fixed . At an iterate and a trust-region radius it computes a vertical step , which reduces the linearized constraint violation inside a smaller trust region. It then computes a horizontal step , which reduces a quadratic model of the barrier objective in the null space of the linearized constraints. Each step must give a fraction of the decrease of a scaled steepest-descent step (the Cauchy decrease conditions (2.18), (2.33)). The total step is judged by the merit function
whose penalty parameter is raised, by a factor of at least , whenever the predicted reduction would otherwise fall below times the vertical predicted reduction. A step is rejected and the radius shrunk if the merit function does not decrease by a fraction of , or if some slack component would drop below . On acceptance, and .
Algorithm II runs Algorithm I for barrier parameters (). Each inner run stops at the first point with and , where .
A sequence is asymptotically feasible if . A limit point of fails the linear independence constraint qualification (LICQ) if the columns are linearly dependent.
For a run of Algorithm II, assuming the standard regularity conditions (Assumptions 4.1) on every infinite inner run:
The milestones follow the paper's proof, in order.
together with exactly one of (i) infeasible stationarity with , (ii) an LICQ-failing limit point with , (iii) with bounded away from zero and eventually constant.
Theorem 4.3 says that the method converges to stationary points of the barrier problem unless the problem is locally infeasible or degenerate, and it says which. Theorem 5.1 turns this into first-order optimality for (2.1) at LICQ limit points of the outer iteration. The proof does not assume full-rank constraint Jacobians or bounded iterates, and it allows inexact subproblem solutions. These features distinguish this analysis from earlier ones for interior-point methods.
The results are proved in the paper; none of them is formalized. A complete development would give a machine-checked convergence theory for a practical nonlinear interior-point method, the trust-region Cauchy-decrease calculus that many trust-region analyses reuse, and a formal account of the LICQ failure modes. The formal statements also make explicit details the paper leaves to the reader: the inner rejection loop and the role of the slack reset.
The obvious argument runs as follows: the merit function decreases, it is bounded below, so the predicted reductions are summable and the iterates become stationary. This fails on two counts.
First, the penalty parameter changes, so is not monotone along the iterates. Lemma 4.4 must first bound the slacks before any summability argument applies.
Second, a small predicted reduction may come from a small trust-region radius rather than from near-stationarity. Excluding this needs a uniform statement that small steps are accepted near any non-stationary iterate. The vertical step must then be controlled by its own predicted reduction (Lemma 4.8), and that control is only available when the matrices have singular values bounded away from zero. Whether they do is exactly the dichotomy of Lemma 4.7. In Theorem 5.1(B), the multipliers of the outer iteration need not be bounded a priori; their convergence uses the LICQ at the limit point.
Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and stacked vectors in WithLp 2 products, so every norm is Euclidean. Matrix norms are operator (spectral) norms. is the adjoint of the derivative of . "Smooth" is read as on all of . The trust-region norm is a seminorm vanishing only at . The merit function is evaluated only at positive slacks, which the fraction-to-boundary test guarantees, so the paper's value is never needed.
A run of Algorithm I records, at every iteration, all rejected trials and the accepted one. Each trial is a valid pass through Steps 1–3: feasible approximate subproblem solutions, the range space and Cauchy conditions, and the penalty update with the constant . Rejected trials fail the acceptance test, and the radius is multiplied by a fixed after each rejection. The Cauchy conditions are stated as "at least times the decrease at every feasible multiple of the steepest-descent direction", which is equivalent to the paper's argmin form. The multipliers are not recorded, since they enter only through . Algorithm II is a sequence of such runs. The -th run is valid up to its first stopping index, or forever if it never stops. Outer iterations are numbered from .
Two hypotheses are added to the page. Lemma 4.7 assumes bounded below, which its proof uses. Lemma 2.3 assumes , which (2.27) guarantees. Algorithm II's stopping tolerances are taken positive. Where the paper divides by a quantity that may vanish and means ((2.21), (2.36)), the case is split off explicitly, so no bound degenerates to . A formalization in which a run may record only accepted steps, or in which the penalty may grow by arbitrarily small factors, would make the analysis unprovable or the statements weaker; the run predicate rules both out. A sorry-free check exhibits a run satisfying all hypotheses.
A complete development needs:
The Cauchy-decrease lemmas and the LICQ limit-point argument are reusable for other trust-region and constrained methods. Contributions to any milestone, and to auxiliary lemmas such as the identity (2.40), are welcome.
Many decisions are made before their objective coefficients are known. A planner may know the feasible decisions and the form of a linear optimization problem, but must predict its cost vector from available features. Squared prediction error measures how close a forecast is to the eventual coefficients; it need not measure the quality of the decision chosen with that forecast. Elmachtoub and Grigas define a loss based on the excess realized cost of the resulting decision, then introduce a convex surrogate, SPO+, for training prediction rules Elmachtoub and Grigas, 2020, §§2–3.
The central population question is whether minimizing the surrogate still selects predictions that minimize the decision loss when the full data distribution is available. Their Theorem 1 answers this under conditions on the feasible region and the conditional distribution of costs Elmachtoub and Grigas, 2020, p. 21. The result concerns the loss itself, before sample size, model capacity, or an algorithm for fitting a predictor enter the picture.
A feasible region is nonempty, compact, and convex. Given a cost vector , a decision incurs cost . The nominal value, optimal-decision set, and support function are
An optimization oracle returns one element of for each , without a tie-breaking rule. For a predicted cost and realized cost , the unambiguous SPO loss uses the worst realized decision among all decisions optimal for the prediction:
This is Definition 2 of the paper. Its SPO+ loss, Definition 3, is
The factor is fixed by the paper's surrogate. Proposition 3 states that SPO+ upper-bounds SPO, is convex in , and has the explicit subgradient Elmachtoub and Grigas, 2020, pp. 17–18.
Let denote an observed feature, its probability law, and the conditional law of given . Their joint law is . A measurable predictor maps each to a cost prediction . The population risks and are expectations over of the corresponding losses at , as in displays (11) and (12) Elmachtoub and Grigas, 2020, p. 20. There is no prescribed parametric predictor class.
Write . Under Assumption 1, the optimal-decision set is a singleton for almost every ; each conditional law is centrally symmetric about and continuous on all of ; and has nonempty interior. The goal says that every measurable minimizer of SPO+ population risk satisfies
This is the paper's Fisher-consistency statement, including its stronger identification of every SPO+ minimizer with the conditional mean Elmachtoub and Grigas, 2020, Theorem 1. The goal does not assert that a minimizer exists.
The milestone list follows the paper's numbered results: Proposition 3's pointwise upper bound, convexity, and subgradient; Proposition 6's mean minimizer and uniqueness claims for a single cost law; and both directions of Proposition 5, which relate SPO risk minimizers to decisions optimal at the mean Elmachtoub and Grigas, 2020, pp. 18, 22–23. The single-law propositions have no feature variable.
Theorem 1 identifies a condition under which a convex training objective preserves the population target of the decision loss. Its identification statement is stronger than merely saying that one selected SPO+ minimizer is SPO-optimal: all SPO+ minimizers agree almost surely with conditional mean cost. The propositions isolate what this depends on. Proposition 6 concerns the surrogate risk, while Proposition 5 connects a prediction's optimal-decision set to the true risk.
The result was proved in the cited preprint and published in Management Science in 2022; this mission asks for a Lean proof of that known result, not a new consistency theorem. A completed development would provide reusable definitions for cost-based decision losses and a checked account of the distributional assumptions needed for uniqueness. The published oracle predicate is already available on the platform; the two losses, risks, and distributional predicates are introduced here.
The SPO loss may jump when a predicted cost admits more than one optimal decision. Its definition takes the maximum realized cost over that whole decision set. Consequently, showing that a prediction selects one mean-optimal decision does not by itself control the SPO loss; Proposition 5's converse requires a singleton set. The surrogate is convex but generally not differentiable, because the support function of need not be differentiable. Establishing the unique population minimizer also depends on how the cost law covers the space: absolute continuity by itself permits a bounded-support law for which nearby predictions tie. These are substantive issues in moving from the single-cost-law statements to an almost-sure claim about measurable predictors Elmachtoub and Grigas, 2020, §4 and Appendix B.
The code represents by EuclideanSpace ℝ (Fin d) and by its standard inner product. Every theorem assumes the paper's nonempty compact convex . Real infima and suprema encode the attained minima and maxima on . An oracle is an explicit parameter satisfying the published SPOBounds.Natarajan.IsOracle predicate; it is not given an extra measurability or tie-breaking assumption. The SPO loss is the paper's unambiguous Definition 2, which differs from the oracle-dependent loss in the published module.
Expected losses are extended nonnegative integrals, so an infinite risk remains infinite. Conditional costs are represented by a Markov kernel , and the joint law by . Integrability of costs makes the conditional and joint means finite. Central symmetry means equality of the conditional law with its reflection . Assumption 1.3, “continuous on all of ,” is pinned to absolute continuity with respect to Lebesgue measure and full support, meaning every nonempty open set has positive probability. This full-support condition is needed for Proposition 6(b)'s uniqueness claim: a continuous law confined to a small ball supplies a counterexample to the weaker reading.
The risks range over all measurable predictors, as display (12) requires. A Bochner integral for an arbitrary nonintegrable loss, a restricted hypothesis class, the oracle-dependent SPO loss of Definition 1, or absolute continuity without full support would change or trivialize the target. Contributions to the support-function, measurable-risk, and conditional-law infrastructure are useful beyond this mission; the seven numbered proposition parts provide its immediate formalization targets.
A model trained to minimize its average loss can perform poorly on subpopulations that are rare under the training distribution . Distributionally robust optimization replaces the average loss by its worst case over all distributions close to in an -divergence, which upweights the tail of the loss and controls performance on every subpopulation of sufficient size. Duchi and Namkoong (arXiv:1810.08750, Ann. Statist. 49 (2021), DOI 10.1214/20-AOS2004) study this objective for the Cressie–Read family of divergences, which interpolates between the -divergence and the KL-divergence and links the robust risk to -norms of the loss.
In practice is unknown and the robust risk is computed on the empirical distribution of a sample. Whether this plug-in estimate is close to the population robust risk, and at what rate, is the question this mission formalizes. Earlier work on the same estimator (Namkoong and Duchi 2017; Duchi, Glynn and Namkoong 2021) let the radius shrink as ; here the radius is fixed, so the robust risk is a genuinely different functional of from the mean.
Let be a measurable space, a probability measure on it, a parameter set and a loss. Fix , write , and fix a radius .
The Cressie–Read function is for and for . It is convex, nonnegative and vanishes at . The Cressie–Read divergence of from is .
The robust risk at under is
the second form writing for the likelihood ratio. Let be i.i.d. with law and their empirical measure. With and , the dual objective is
The Lean development uses the same names: cressieRead, robustRisk, empiricalMeasure, dualObjective, kstar, ck, in the namespace UniformDRO.Concentration.
Assume for all , with . For a fixed and , whenever , with probability at least ,
The goal is stated exactly as printed, constants included.
The result. Theorem 2 shows that the plug-in robust risk is a consistent estimator of the population robust risk for a fixed divergence radius, at rate up to a factor; Theorem 3 of the same paper shows this rate cannot be improved in general. Through a covering argument it yields uniform bounds over a model class (Corollaries 1–2, p. 20) and hence guarantees for the plug-in minimizer : the robust risk of the learned model is close to the best achievable robust risk. The rate degrades as , quantifying the statistical price of protecting against larger distribution shifts.
Formalizing it. The result is proved on paper; no machine-checked version exists. A formal proof requires a measure-theoretic duality theorem for -divergence balls (Lemma 1), convex concentration for product measures (Lemma 6, posed on the platform and not yet proved), and a moment bias bound (Lemma 8). Formalization already exposed two slips in the printed proof, both corrected in the milestones without changing Theorem 2.
The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so concentration cannot be read off any single empirical average. The argument goes through the dual: Lemma 1 reduces the robust risk to a one-dimensional infimum of , which is a Lipschitz function of the data only for in a bounded interval (Lemma 9), and only up to a bias, because is a nonlinear (norm-like) function of an empirical mean. Neither half is routine: the duality for general requires the closed form of and an attained infimum over , and the bias bound (Lemma 8) needs a careful case split at . The naive approach — concentrating for a fixed — fails because the optimal depends on the sample.
PhiDivRobust.Counterpart.conj is reused for Lemma 3.Real.rpow; Euclidean distances on are written out as , since the default norm on Fin n → ℝ is the sup norm.sSup (the loss is bounded, so the value set is nonempty and bounded), the divergence constraint cannot be met by non-integrable ratios, and the goal mentions only , , , , and , not the proof's auxiliary objects.