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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A finite two-person zero-sum game is given by a real pay-off matrix, and its value can be computed by linear programming. In 1949 George W. Brown proposed a much simpler procedure, now called fictitious play: each player in turn plays a best pure reply to the accumulated play of the opponent so far, and the running averages are read off as estimates of the value (Brown, RAND P-78, 1949). Brown conjectured that both estimates converge to the value. Julia Robinson proved the conjecture in An Iterative Method of Solving a Game, Annals of Mathematics 54 (1951).
The result is the starting point of the theory of learning in games. Fictitious play is the basic model of boundedly rational players who best-respond to empirical frequencies, and the question "for which classes of games does it converge?" has driven a long line of work.
Timeline.
Let be a real matrix, . The first player chooses a row , the second a column , and the second pays the first . A mixed strategy is a probability vector for the first player, or for the second. For all mixed strategies,
A pair for which equality holds is a solution, and the common number is the value of the game. The minimax theorem says that a solution exists.
Write for the -th row, for the -th column, and , for the largest and smallest component of a vector . A vector system for is a pair of sequences of -vectors and of -vectors with and
where and . In the alternate vector system the column satisfies instead. A row is eligible in the interval if for some , and similarly a column if for some .
With , is the payoff vector of the first player's empirical mixed strategy against each column, and that of the second player's against each row. In the Lean development these objects are vmax, vmin, IsVectorSystem, IsAltVectorSystem, RowEligible, ColEligible and IsSolution, in the namespace RobinsonFP.Convergence.
For every vector system for , and the value of the game,
The statement holds for arbitrary initial vectors with and for every way of breaking ties.
Two further items are not milestones: the Theorem for the alternate vector system, which the paper says follows by the same proofs, and the bracketing when (p. 297).
The Theorem shows that a payoff-based procedure with no linear algebra finds the value of every zero-sum matrix game. It was one of the first iterative methods for linear programs with a convergence proof, and it is the base case for every later convergence result about fictitious play: potential games, games with identical interests, games, and continuous-time best-response dynamics.
The result is proved, and its proof is short. To our knowledge it has no machine-checked proof. The mission produces a Lean proof of the Theorem and its four lemmas, together with reusable definitions of vector systems and eligibility. A statement with an explicit rate, such as Shapiro's, or a proof for the alternate system, is a natural extension.
Lemmas 1–3 are elementary estimates. The difficulty is Lemma 4. The obvious approach follows a single run of the iteration and tries to show that the gap grows sublinearly. This fails because a run can spend arbitrarily long windows in which some row or column is never a best reply, and nothing about one fixed run controls the gap over such a window. What is needed is a bound that is uniform over all vector systems, whatever their initial vectors and tie-breaking, which is why in Lemma 4 comes before the vector system, and why display (3) quantifies over every vector system of the smaller matrices. In Lean, this uniformity has to range over matrices of every smaller size, so the statements must be general in the index types.
ι, κ (the paper's ); Fin m, Fin n is a special case. The matrix is Matrix ι κ ℝ.Finset.sup' and Finset.inf' over all indices, hence attained.Tendsto … atTop (𝓝 ·); lim inf and lim sup of real sequences are stated in -form (for every , eventually), with no boundedness side conditions.IsSolution A x y v, i.e. probability vectors , with . Such a solution exists by the minimax theorem, which is proved on the platform as MatousekLP.ZeroSum.minimax_equality in a different encoding. A statement with free, or with "there exists ", would be false or would lose the identification with the value; neither is used.A general "restriction of a vector system to a submatrix" lemma would be reusable for later work on fictitious play. Proofs of any milestone are welcome, as are proofs of the two extra items.
Section 4 of Herbert Robbins's 1952 address Some aspects of the sequential design of experiments (Bull. Amer. Math. Soc. 58, 527–535, doi:10.1090/S0002-9904-1952-09620-8) isolates a problem that every user of significance tests meets: if the sample size is not fixed in advance, an experimenter can keep sampling until the test rejects. Robbins shows that a fixed-sample test then loses all control of its error probability, and he proposes the compromise of allowing the sample size to range over a window , with an explicit bound on the resulting error.
The question is still current. "Optional stopping" and "peeking" at accumulating data are a standard concern in clinical trials and online A/B testing, and the modern theory of always-valid inference and confidence sequences (for example Howard, Ramdas, McAuliffe and Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), arXiv:1810.08240) answers exactly the question Robbins raises: how large is the probability that a running statistic crosses a boundary at some time in a range. The earlier treatment Robbins cites is Feller's 1940 discussion of the statistics of ESP experiments.
Let be independent real random variables on a probability space , each normal with mean and variance . This is the null hypothesis for observations that are normal with unknown mean and unit variance; the alternative is . Write
The fixed-sample test of size rejects if and only if
for a real constant . (In this mission always denotes this test constant; in Section 2 of the paper the same letter is the mean of a coin.) The standard normal distribution function is
For integers the window probability is
and . In Lean these are Phi, S X n ω = ∑ i ∈ Finset.range n, X i ω and g P X n₁ n₂ α, in the namespace RobbinsSeqDesign.OptionalStopping.
For integers and every real , with ,
The inequality is strict, as printed, and holds for every real , not only the large values of practical interest.
For every and real ,
For every real , with probability the inequality holds for infinitely many .
The results. (22) says that the fixed-sample test has error probability whatever is. The infinitely-often statement says that this guarantee is void under unrestricted optional stopping: sampling until (21) holds rejects a true with probability one, however large is. The goal (25) quantifies the compromise: if the stopping time is confined to , the error probability is at most the fixed-sample error divided by , where depends only on the window's ratio. For large and moderate this keeps the error of the same order as the fixed-sample error; Robbins notes that it is useful when is not too large and that sharper inequalities can be devised.
Formalizing it. The three statements are classical and their proofs are short on paper, but none is machine-checked for Gaussian partial sums. The goal needs stopping-time machinery for discrete-time Gaussian random walks; the infinitely-often statement is a consequence of the lower half of the law of the iterated logarithm, which Mathlib does not contain. On the platform, DurrettProbability.brownian_limsup_sqrt (proved) gives for Brownian motion, a different process, and AzumaWeightedSums.IteratedLog.theorem2_limsup_le_one gives an upper iterated-logarithm bound for weighted sums, the opposite direction; neither states any of the targets here, but both are related infrastructure.
The goal is a maximal inequality over a window of times. The obvious argument, a union bound over , gives , which grows with the window length instead of depending on alone, and exceeds for long windows. The events for different are strongly dependent, and the boundary is curved, so the bound has to account for when, inside the window, the boundary is first crossed; this requires stopping-time arguments for a discrete-time walk that are not yet available for Gaussian random walks in Mathlib. The strictness of the inequality also has to be tracked through the argument. The infinitely-often statement cannot be obtained from the central limit theorem alone, which gives only ; upgrading this to probability one needs a zero–one law or the law of the iterated logarithm.
The observations are X : ℕ → Ω → ℝ on a probability space (Ω, P) with [IsProbabilityMeasure P], iIndepFun X P and ∀ i, HasLaw (X i) (gaussianReal 0 1) P; the paper's is X (i - 1). The explicit readings committed to are:
cdf (gaussianReal 0 1)).P.real of the event; (22) is stated for .∀ᵐ ω ∂P, ∃ᶠ n in atTop, α * √n < S X n ω, for every real .A trivializing formalization is ruled out: is the probability of the union over the whole window (not the event at alone), is the fixed standard normal distribution function (not an arbitrary monotone function), and the parameter range excludes , where Lean's convention would replace the right side by .
A complete development needs the law of a sum of independent Gaussians, the strong Markov property of a Gaussian random walk at a stopping time (or an equivalent first-passage decomposition), and, for the infinitely-often milestone, either the lower law of the iterated logarithm for Gaussian walks or the Hewitt–Savage/Kolmogorov zero–one law combined with the central limit theorem. These pieces are reusable well beyond this mission; contributions of any of them, as separate lemmas, are welcome.
A linear program subject to , assumes that the constraint matrix is known exactly. In practice the columns of — the activity vectors, describing how much of each resource one unit of activity consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.
The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.
Fix integers . Vectors in are compared componentwise. For a set and a scalar , , and the sum of sets is Minkowski addition, .
Let be nonempty convex activity sets and a nonempty convex resource set. Problem (I) is
and denotes its set of feasible . Problem (Ib) is the special case for a right-hand side .
The support functional of a set is , a value in . With the -th unit vector, the auxiliary matrix is the matrix with entries
defined when all of these are finite, and LP is the linear program subject to , . Finally is the set of matrices whose -th column lies in .
In the application, the activity sets are Euclidean balls around nominal columns of a matrix , with radii .
Assume every is nonempty and convex and for all . Then
and for every objective , the optimal solutions of (Ib) and of LP coincide.
The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in , of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column is inflated by the full radius , which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.
The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.
The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every " to uses that the supremum of a sum of independent terms is the sum of suprema, which needs every nonempty and the scalars nonnegative; with an empty activity set the Minkowski sum is empty and every becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.
Fin m → ℝ and Fin n → ℝ, with indices in place of ; the order on vectors is componentwise.(∑ j, x j • K j) ⊆ R (pointwise set operations) together with . It is not defined as "for every choice ", which would make milestones 1 and 5 trivial, and is constructed from the , not an arbitrary matrix dominating , which would make the goal trivial.EReal. The entries of are its real conversions, so every statement mentioning assumes and , the paper's standing assumptions (pp. 1154–1156). Convexity of the is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of ).EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii .FenchelRobust.Counterpart.supportFun with the same body.EReal statement equating the optimal values, are welcome.An inventory controller must decide how much to order while demand changes with an observed external condition. A single demand rate misses that dependence: the same inventory position can justify different orders when the condition changes. Song and Zipkin's 1993 study asks whether a simple policy remains optimal when the condition follows a continuous-time Markov chain and orders arrive after a random lead time. The answer for linear ordering costs is a world-dependent basestock policy: each world state has one target inventory position, and an order raises the current position to that target when it lies below it.
The policy claim concerns an infinite horizon. It is stronger than showing that a particular collection of target levels performs well or that such a policy minimizes a one-step cost. Theorem 2 of Song and Zipkin identifies the targets through a limiting value function and establishes optimality for the full discounted problem. This mission formalizes that theorem and the finite-stage results the authors use to state its limit precisely.
The world state belongs to a nonempty countable set . The world evolves according to a conservative continuous-time Markov generator , with exit rate . When the world is in state , customers demand individual units at rate . The exit rates and demand rates are bounded above. Inventory is fully backlogged: a negative inventory level records unmet demand. The controller observes the world state and the inventory position , which includes outstanding orders, and chooses an order-up-to position .
An order has actual unit cost and may have fixed cost . This mission takes the linear-cost case, so the discounted fixed cost is . The lead time is a finite nonnegative random time, independent of the world and demand process. Its Laplace transform discounts the ordering costs to , where is the discount rate. Holding one unit costs per unit time; backlogging one unit costs .
Write for the number of demands during the lead time conditional on initial world state . The cost rate of an inventory level is for and otherwise. The lead-time cost and myopic cost are
where is a uniformization rate at least , , and . The paper's Assumption 1, , applies to the later results. It ensures the myopic cost has finite nonnegative minimizers. The smallest such minimizer in world state is , and .
With zero fixed cost and zero terminal cost, the -stage transformed cost minimizes the auxiliary cost over . Each combines the myopic cost with the expected discounted continuation after a demand, a world-state jump, or a self-loop. Let and denote their pointwise limits. A basestock policy orders to in state ; it never cancels an outstanding order.
The main target is the finite, smallest global minimizer of for each world state, with the inequalities of Theorem 2(c):
Here is the limit of the smallest finite-stage minimizers . Theorem 2(e) then asserts that has minimum infinite-horizon expected discounted cost from every state among all feasible policies. The milestone list states Lemmas 1, 2 and 4, Corollaries 1 and 2, all parts of Theorem 1 as identified by the paper's internal references, and the limit and optimality-equation clauses of Theorem 2. Together they fix the finite-stage and limiting objects used by the goal.
The theorem reduces a decision at every integer inventory position to one integer target for each observed world state. It gives an exact policy structure for a model with a changing demand rate and random lead time, rather than an approximation derived from a constant-demand model. The limiting inequalities also locate an optimal target relative to the myopic target and the finite-stage targets, giving a mathematically specified range for policy computation. These claims are the linear-cost part of Song and Zipkin's analysis; the paper proves the result but supplies no Lean proof.
Formalization will leave reusable definitions for countable-state uniformization with a demand counter, integer convexity of inventory cost functions, and discounted costs of history-dependent policies. The mission's theorem statements compile as open goals. The remaining work is to verify the analytic properties of the lead-time demand law, the finite-stage inequalities, convergence, and the infinite-horizon policy comparison. The fixed-order-cost and monotone-world-state results of the paper are separate missions.
The world can have countably many states, so a continuation value includes a series over possible world jumps. The stage cost grows with inventory position, so a bounded-cost finite-state dynamic-programming theorem does not directly cover the model. The minimization is over an unbounded set of integers, and the minimizers themselves change with the stage number. Convexity of a one-stage cost alone does not establish that the limiting policy beats policies that use the entire observation history. These are the specific gaps the paper's bound, ordered-difference, and limit results address.
World states are a nonempty countable Lean type, inventory positions and order-up-to levels are integers, and costs are real until policy evaluation. The lead-time law is a probability measure on finite nonnegative real times, independent of world and demand. The demand-count law is defined by exact Poisson uniformization at rate , with demand, world-jump, and self-loop branches. The infinite-horizon policy cost uses extended nonnegative reals and a supremum of finite-horizon costs, so it can express an infinite expected cost without a default real value. Policies may depend on all past observed states; the goal compares its basestock policy against every feasible deterministic policy in this class. Randomized policies are omitted because they cannot improve expected nonnegative costs on this countable state space.
Assumption 1 is attached only to the results that use it. The linear-cost recursion has and . Integer convexity means nondecreasing forward differences. Smallest minimizers and the minimum across world states are asserted to exist; neither is encoded by an integer infimum that returns a default on an empty or unbounded set. The goal requires an actual optimal policy cost comparison from every state, so solving the limiting optimality equation only within basestock policies cannot close it. Contributions to the lead-time mixture, integer convexity, boundedness of the real series and infima, and unrestricted policy comparison all fit this scope.
A fault-tolerant system often replicates a computation on several processors and needs the nonfaulty ones to act on the same data, even though some processors may fail in arbitrary ways: send wrong values, send different values to different recipients, or lie about what they were told. Pease, Shostak and Lamport posed the question in 1980, motivated by the SIFT fault-tolerant aircraft-control computer under development at SRI (Wensley et al. 1978), where it arises in clock synchronization among other places: processors, at most of them faulty, communicate by two-party messages whose sender is always identifiable, and each holds a private value. Can the nonfaulty processors all compute the same vector of values, one entry per processor, whose entry for every nonfaulty processor is that processor's true value? The paper (J. ACM 27 (1980) 228–234) calls this interactive consistency and settles it: possible if and only if when messages can be forged in relay, and possible for every when they cannot. The same problem, under the name Byzantine generals, became the standard model of arbitrary ("Byzantine") failures in distributed computing (Lamport, Shostak & Pease 1982); the bound underlies the quorum sizes of later replication protocols.
This mission covers the positive half of the paper's characterization: Section 3's recursive procedure, which achieves interactive consistency with processors in rounds of message exchange.
Let be a finite set of processors and a set of values. A string over a set is a finite sequence of elements of , repetitions allowed. For a -level scenario is a map from the nonempty strings over of length at most to . The value is 's private value ; for , is the value tells that told … that told is 's private value. A -level scenario records the outcome of rounds of message exchange.
Faults are modeled by a set of nonfaulty processors, unknown to the processors. Nonfaulty processors relay truthfully, so is consistent with when
Faulty processors are otherwise unconstrained. A processor sees only its view , the restriction of to strings beginning with .
The procedure (p. 230). Processor computes the entry for processor as follows, with and the current processor count and fault bound:
In Lean this is InteractiveConsistency.OralAlgorithm.record m P τ q with τ = fun w => σ (p :: w), values in Option V with none for NIL.
For , for every with and every -level scenario consistent with ,
This is procedure_assures_ic. It is the paper's claim about this procedure, not an existence statement.
The theorem is the upper bound in the tight characterization of when interactive consistency is achievable with unauthenticated messages; the matching impossibility (the paper's Section 4 THEOREM) shows that no procedure, with any number of rounds, does better. The procedure is the ancestor of the "oral messages" algorithm of the Byzantine generals paper, and its quorum arithmetic (, intersections of two quorums containing a nonfaulty member) recurs throughout Byzantine fault-tolerant replication.
The result is proved in the paper, in a half-page induction. What this mission adds is a machine-checked proof against an explicit model of scenarios, views and consistency with a bounded number of rounds. Machine-checked proofs exist for the related algorithm of the later Byzantine generals paper in other proof systems; this procedure, with its quorum-based step (1), has to our knowledge not been formalized in Lean, and nothing on message-passing agreement exists on this platform.
Each step of the paper's proof is short, but the bookkeeping is where an argument breaks. The recursion changes three things at once: the processor set loses , the fault bound drops by one, and the scenario becomes of one level less. The induction hypothesis must therefore be stated for every finite processor set and every scenario, and applied to a subscenario whose consistency is inherited only for strings of the right length. The mixed case, where one nonfaulty processor exits at step (1) and another recurses, is the delicate one: the two processors' computations take different branches, and since is faulty nothing forces either value to be 's private value. The thresholds are exact: in step (1) and agreeing entries in step (2), both in the current and ; off-by-one changes in either break the case analysis. Finally, step (2)'s majority value must be shown unique, so that two processors with the same vector record the same value.
Processors form a Finset α with decidable equality; strings are List α, read left to right (the receiver first, the originator last), so is σ (p :: (w ++ [q])). A scenario is a total function List α → V; consistency with (ConsistentUpTo P N (m + 1) σ) constrains it only on strings over of length at most , the domain of an -level scenario and all the procedure reads. The procedure receives only the view fun w => σ (p :: w), never or . The fault hypothesis is P.card ≤ N.card + m; is included.
Explicit readings of the paper's prose: "size " is P.card + m < 2 * Q.card; is natural-number division; "strings over of length " includes the empty string and allows repetitions; the step-(2) vector is indexed by P.erase q and includes 's own entry; the recorded value in step (1) is (the empty string forces it); when several values reach the step-(2) threshold one is chosen deterministically from the vector (under the goal's hypotheses at most one does); for a failing step (1) records NIL (never reached under the hypotheses). Two printed slips are corrected in the Lean: "records and " (for "for ") and "" (for ).
Trivializing formalizations are ruled out: the procedure never sees itself (with it, recording would be trivial), consistency constrains only relays by nonfaulty processors, and ranges over every subset of size at least .
The development needs only finite sets and lists; no library beyond Mathlib is required. The quorum-intersection lemmas and the subscenario construction are reusable for other oral-message protocols. Contributions welcome: proofs of the four milestones, the goal by induction on , and a computable version of the procedure for concrete instances. This is mission 1 of a series of three on this paper; mission 2 formalizes the impossibility THEOREM for (Section 4), and mission 3 the authenticated-message procedure for every (Section 5).
Many stochastic systems accumulate a real-valued quantity while repeatedly returning to a state at which a new cycle begins. A queue may accumulate work or cost, a component may accumulate wear, and a recurrent system may accumulate time in a state. The observations at a fixed clock time usually cut through a cycle. This makes the moments of the observed process different from the moments of a sum stopped exactly at a regeneration epoch. W. L. Smith introduced cumulative processes to state mean, variance, ergodic, and central limit results for this setting in a common language (Smith 1955, §5).
The mean growth rate describes the long-run reward per unit time. The variance growth rate also records the dependence between a cycle's length and its reward. That dependence matters in systems where unusually long cycles tend to accumulate unusually large rewards; assuming the two are independent would erase a term in Smith's formula (Smith 1955, Theorem 8). This mission targets the exact first-order mean and variance asymptotics, along with the source results Smith uses to pass from completed cycles to observations at ordinary times.
Work on one probability space . The cycle lengths are nonnegative, independent, identically distributed random variables whose common law is not concentrated at zero. Set and for . Thus is the th renewal epoch after the initial renewal at time zero. For , counts the epochs , including . The corresponding renewal function is , where is Smith's zero-delay law. These conventions come from §2·1 and §5·2 of the paper (Smith 1955, pp. 9 and 23).
A cumulative process is real valued, starts at , and has almost surely bounded variation on each finite nonnegative time interval. The cycle reward is . Write for the total variation of the path on and for its variation on . For the moment results, the cycle vectors are independent and identically distributed across . Their coordinates within one cycle may be dependent. This joint-cycle interpretation is required by Smith's common joint distribution for in the proof of Lemma 5 (Smith 1955, pp. 23–24).
Let , , and when the moments exist. Put , , and . Smith writes , with the cycle length–reward correlation. The covariance remains defined when either variance is zero. The auxiliary sum includes a reward beyond the cycles completed by time , exactly as in (5·2·1) (Smith 1955, p. 23).
The first target is the mean part of Theorem 8. If and are finite, then
The goal includes the variance part under the additional assumptions and :
Both limits are along real time, and neither assumes that a cycle's length and reward are independent. The milestone list contains the mean and variance limits for , the cycle-moment estimate used for the incomplete cycle, and Theorem 8(i) as the explicit mean target (Smith 1955, Lemmas 4, 5, 9 and Theorem 8).
The theorem gives a linear approximation to the process's expected value and variance, with errors smaller than the observation horizon. The leading variance coefficient separates reward variability, cycle-length variability, and their covariance. It can therefore be used without a false independence assumption when the duration of a cycle affects the amount accumulated during it. The formulas are first-order statements; they do not claim a bounded error or a limiting distribution (Smith 1955, (5·3·6)–(5·3·7)).
Formalizing these statements requires reusable definitions of renewal counts, path variation, random-cycle rewards, and the moment conditions that make expectations and variances genuine. The statement is a draft target, not a claim that Smith's proof already has a machine-checked reconstruction. A completed development would also give formal tools for other regenerative reward models whose observations occur between renewal epochs.
The auxiliary sum is sampled at a random index, while is observed at a deterministic clock time. They differ by part of a cycle that crosses . Ordinary laws for sums of a fixed number of independent rewards do not directly control either this random index or the crossing-cycle contribution. At second order, a bound on the mean difference alone does not determine the variance difference. The length–reward covariance must also survive the passage from completed cycles to the continuous-time process (Smith 1955, pp. 24–28).
Lean uses real time and real-valued paths. Cycle laws are represented by random variables on one probability space; the renewal at zero is explicit. The renewal count takes the value zero on a path with infinitely many renewals before a finite time, a null event under the nondegenerate i.i.d. length law. Variation is represented by Mathlib's extended nonnegative eVariationOn and converted to a real number only under the almost-sure bounded-variation condition. The theorem states integrability of and its square as consequences of the cycle-moment assumptions, avoiding default values for divergent real integrals or variance. A finite th moment is an integrability condition, not a comparison between a real number and infinity.
The paper's exact identity (5·2·2) is off by one under its own definitions of and ; the mission targets its valid asymptotic consequence (5·2·3). The last variance in the printed Lemma 5 coefficient is , while Theorem 8 and the calculation require . Milestone provenance retains the printed text; the Lean statements use the corrected coefficient. Lemma 9 is formalized for the absolute th moment of the cycle increment, which is the printed statement for a nonnegative cycle quantity such as the variation to which Theorem 8 applies it. Solvers may contribute the renewal and random-index estimates needed for the listed targets. A definition that makes rewards independent of cycle lengths would remove the covariance term and would not represent this mission's model.
The classical implicit-function theorem solves an equation for as a function of a parameter near a known solution , provided is (strongly) Fréchet differentiable in with an invertible partial derivative. Much of optimization does not meet that hypothesis. Optimality conditions of constrained problems, complementarity problems and variational inequalities are routinely rewritten as equations involving the projection onto a convex set, the componentwise , or the normal map of a polyhedron. These maps are Lipschitzian and piecewise smooth, but not differentiable. Sensitivity analysis asks whether the solution of such a system moves Lipschitz-continuously with the problem data, and the classical theorem cannot answer it.
Stephen M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, pp. 292–309, gives a theorem with the same shape as the classical one, in which differentiability is replaced by strong approximation by a function whose inverse is Lipschitzian. The paper's §4 applies it to parametric variational inequalities over polyhedral sets through the normal map.
Timeline. Robinson's Strongly regular generalized equations (Math. Oper. Res. 5, 1980) proved an implicit-function theorem for generalized equations under a linearization hypothesis called strong regularity. The 1991 paper reformulates that idea for single-valued nonsmooth equations: the approximating function need not be linear. Lemma 3.1 extends the Banach perturbation lemma for linear operators (Kantorovich–Akilov, Functional Analysis, Th. 4(2.V)) to Lipschitzian functions; after acceptance, A. Ioffe pointed the author to closely related results of Dmitruk, Milyutin and Osmolovskii (Lyusternik's theorem and the theory of extrema, Russian Math. Surveys, 1980, Theorems 1.2, 1.3), credited in the paper's footnote.
Let , , be real normed linear spaces, with complete. Fix , , a neighborhood of and a neighborhood of . Let map to , with , and let map to , with . denotes the closed ball of radius about .
Expansion modulus. For a map between metric spaces and a set ,
If , then is one-to-one on and its inverse is Lipschitzian with modulus . In Lean the mission works with lower bounds: ExpansionAtLeast f S d says on , i.e. .
Strong approximation (Definition 2.4). strongly approximates in at , written (Lean: StronglyApproxInX f F x₀ y₀), if for each there are neighborhoods of and of with
When is the partial derivative map this is strong partial Fréchet differentiability; in general may be piecewise linear or any map with a Lipschitzian inverse.
Assume (a) at ; (b) for each , is Lipschitzian on with modulus ; (c) is a neighborhood of in ; (d) . Then for each there are neighborhoods of , of and a function with
Every strictly above is claimed; is not.
where .
The result. Theorem 3.2 yields existence, local uniqueness and Lipschitz dependence of solutions of parametrized nonsmooth equations, with an explicit Lipschitz modulus arbitrarily close to . In the paper it underlies Theorem 3.3 and Corollary 3.4 (approximation and B-differentiation of the implicit function) and the sensitivity results of §4 for parametric variational inequalities over polyhedral convex sets. The same template, an equation approximated by a map with Lipschitzian inverse, is the basis of later strong-regularity and semismooth-Newton analyses in nonlinear programming and complementarity.
Formalizing it. The theorem is proved in the paper; it has not been machine-checked. The platform has the smooth implicit-function theorem (FamousTheorems.implicit_function_theorem, Rudin.ch09_implicit_function) and Mathlib has the contraction mapping principle, but there is no Lipschitz-inverse perturbation result and no notion of strong approximation. The mission produces both, together with the formal Theorem 3.2 that a follow-on mission (Theorem 3.3, Corollary 3.4, §4) would reference.
The obvious approach, differentiate and invert, is unavailable: need not have a derivative anywhere near , so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of onto a ball uniformly in from information about alone. Injectivity transfers directly from through the small Lipschitz modulus of ; surjectivity does not, because carries no information about beyond the small Lipschitz modulus of the difference, and the domain ball, the image ball and the parameter neighborhood must be chosen once for all . Completeness of is essential (the paper stresses this on p. 306) and is not available for and .
All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:
[CompleteSpace X]); , are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.ExpansionAtLeast f S d in place of "", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be on sets with fewer than two points.F : X → Y → Z and ; hypotheses constrain them on only, and the conclusions keep the implicit function inside the domain: , , . This makes explicit what the paper leaves implicit (its is only defined on ). Likewise , used implicitly in the paper's proof, is a conclusion of milestone 2.Metric.closedBall), radii written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at ), in which may shrink to , is existential, or uniqueness is asserted outside , would be a different and trivial or false statement; the statements here rule these out.
Needed infrastructure: the contraction mapping principle on a closed subset of a complete space (Mathlib's ContractingWith), Lipschitz estimates on sets, and the two definitions of this mission. Lemma 3.1 is reusable for any Lipschitz-perturbation argument. Proofs of either milestone, or a direct proof of the goal, are welcome.
Classical cooperative game theory assumes that any coalition of players can form and coordinate. In many settings cooperation is mediated by pairwise relationships: communication lines, contracts, alliances, or trade links. Roger Myerson's discussion paper Graphs and Cooperation in Games (Northwestern University, 1976; published in Mathematics of Operations Research 2(3), 1977, doi:10.1287/moor.2.3.225) models such a cooperation structure as a graph on the set of players and asks how the players should share the worth of the game when only linked players can coordinate directly.
The answer, now called the Myerson value, is the starting point of the literature on communication situations and network games. It underlies later work on network formation (Jackson and Wolinsky, A strategic model of social and economic networks, JET 1996) and on allocation rules for networks, and it is a standard textbook example of an axiomatic solution concept.
Timeline:
Let be a nonempty finite set of players and the set of nonempty coalitions . A game in characteristic function form is a vector ; is the transferable wealth coalition can divide.
A link is an unordered pair of distinct players and a graph is a set of links; is the set of all graphs, the complete graph, the graph with one link removed, and the number of links. Players are connected in by if or a path of links of joins them through players of only; the classes form the partition of , and is the set of connected components of . The graph-restricted game is
An allocation rule is a function , with the payoff of player under cooperation structure . It is a fair allocation rule for if
is totally stable if for every and every link , and is superadditive if for disjoint .
A game in graph function form assigns to every pair with a closed, comprehensive (closed under decreasing coordinates), proper () set of feasible payoffs; its fair allocation rule replaces (7) by (14), .
If is superadditive, then the fair allocation rule for is totally stable:
Every has a unique fair allocation rule; every game in graph function form has a unique satisfying (14) and (10).
The fair allocation rule is
The milestones follow the paper's Section 7: the steps of the proof of Theorem 4 (displays (15)–(17)), Theorem 4, Theorem 1, the decomposition of and the efficiency and equity of (proof of Theorem 2), Theorem 2, and the monotonicity of and in a link (proof of Theorem 3). Theorem 3 is the goal because its proof uses the formula of Theorem 2, whose proof uses the uniqueness of Theorem 1, which is the transferable-utility case of Theorem 4: all four numbered results lie on one path.
The theorems give an axiomatic foundation for allocation in networks: two natural requirements, component-wise efficiency and equal gains from each link, single out one rule, and that rule is an explicit formula built from the Shapley value. At the complete graph it recovers the Shapley value itself, so the result is also a new characterization of the Shapley value. Total stability says that, for superadditive games, no player has an incentive to break a link, which connects the allocation rule to the question of which networks form.
The results are proved in the paper. A search of the platform found no formalization of cooperation graphs, the graph-restricted game, the Myerson value or total stability; the Shapley value is available as a platform definition and is reused. This mission produces machine-checked statements of all four theorems and of the intermediate steps of their proofs, together with a reusable definition layer for communication situations.
The equity condition (10) relates the payoff at a graph to the payoff at a graph with one fewer link, and it constrains only pairs of linked players; it is not evident that these conditions, together with efficiency on components, determine the rule at every graph, nor that they are consistent. Uniqueness and existence must hold simultaneously for all graphs, and the constraints couple each graph to all of its subgraphs and each player to every other player of its component. In the graph function form, efficiency becomes a boundary condition on a closed comprehensive set, and the existence and uniqueness of the relevant extremal point depend on all three properties of .
Identifying the rule with requires the efficiency of the Shapley value on each component of , which is not the efficiency of on , and equity requires tracking how the partitions change when a link is removed. Total stability is false for general games: without superadditivity a player can gain by cutting a link, so the hypothesis cannot be dropped.
Players are Fin n, with in every theorem as the paper assumes nonempty; the paper's player is index . The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): is ⊤, the empty graph ⊥, is h ≤ g and is h < g. A game is a function Finset (Fin n) → ℝ; its value at is a junk coordinate that no definition reads, and no theorem assumes . Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at to . is ↥S → ℝ with the product topology, and is the topological frontier.
Explicit readings of the typescript:
The equity and stability conditions quantify over links of only. Quantifying over all pairs of players would make Theorem 1 false and the goal vacuous, so that reading is ruled out. Likewise (14) is boundary membership, not membership in .
Contributions welcome: general lemmas on the partitions (refinement under link deletion, restriction to components), Möbius inversion over the subgraph lattice of a finite simple graph, the carrier and null-player properties of the Shapley value, and the extremal-point lemma for closed comprehensive sets. These are reusable beyond this mission.
In a finite stopping problem, a decision maker observes rewards one at a time and must accept one without seeing the future. A fully informed observer takes the maximum. This comparison is often called a prophet inequality. The abstract bound that an optimal stopping rule can secure at least half the expected maximum does not say how to choose a simple rule. Samuel-Cahn showed that a threshold chosen from a median of the maximum already gives this guarantee, even when the rewards are independent but differently distributed. The rule requires one number fixed before observations begin. Samuel-Cahn, 1984
The paper builds on earlier comparisons between the maximum and the best stopping value, then narrows attention to rules that accept an observation when it crosses a fixed threshold. This mission isolates its first main result, Theorem 1, and the two cases that determine whether the crossing test is strict or weak. The paper's second main result, concerning the sharpness of the constant for identically distributed rewards, belongs to the next mission in this series. Samuel-Cahn, 1984, pp. 1213–1215
Let , and let be independent, nonnegative real random variables. Write . For a threshold , the weak threshold rule takes the first with and ; the strict threshold rule uses . If no earlier observation qualifies, either rule takes , even when is below the threshold. Hence every rule returns exactly one observed reward.
The paper distinguishes the full stopped reward from its positive threshold reward. In its notation,
The last forced observation may contribute to or while contributing zero to or . This difference is essential to the theorem's middle bounds. A median of means both and . Define the excess sum , where . The two median inequalities allow an atom at , and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)
For every median , the goal retains both of the paper's conditional conclusions:
At equality , both conclusions apply. The attack path follows the expected maximum bound (1.3), the displayed identities and probability bound in (1.4), and the companion weak threshold display. Each milestone points to an actual line of the paper. The NOTE and ASSERTION give a further interval of working thresholds: if and , then every satisfies the same chain with . Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215
Theorem 1 replaces the unspecified best stopping policy with a specific threshold chosen from the distribution of the maximum. It also shows that the thresholded part of the stopped reward alone meets the factor two bound. That stronger middle statement distinguishes the theorem from an outer comparison . For a reward distribution with atoms, the theorem says exactly when to use and when to use . Its companion ASSERTION shows that a median is not the only useful threshold choice. Samuel-Cahn, 1984, p. 1214
The result is proved in the paper; the work here is to express its assumptions, boundary behavior, and all displayed inequalities as Lean statements that solvers can prove. The milestones expose reusable facts about positive parts, forced stopping, and independence of a current observation from the event that the rule has survived earlier ones. No machine checked proof of these drafted statements is claimed. The second mission can use the completed theorem to formalize why the factor two cannot be improved uniformly over threshold rules, even for identically distributed observations.
The event that a rule reaches index depends on the observations before . Establishing its independence from the excess of requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at also makes the positive threshold reward smaller than the full stopped reward whenever the last observation misses the threshold. Ignoring that last case would erase one of the theorem's conclusions. Finally, atoms at the median prevent the strict and weak crossing events from being interchanged. Samuel-Cahn, 1984, (1.1)–(1.4)
Lean indexes the observations by Fin with . Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop . The rules are the least qualifying index or that final index. The paper's and therefore become and . Observations are measurable, nonnegative almost surely, and mutually independent under a probability measure.
Expectations use the extended nonnegative integral of the positive part, taking values in . This keeps infinite expected rewards visible without imposing an integrability assumption absent from Theorem 1. The median has both strict tail inequalities from (1.1). The identities for positive stopped rewards state directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds and are parameters satisfying the paper's defining equations, with no extra uniqueness hypothesis in statements that do not use it.
The goal cannot be satisfied by replacing with , by permitting a rule to return no observation, or by making the median predicate empty. Useful contributions include the measurable threshold rule interface, the pathwise excess decomposition, the factorization under mutual independence, and the remaining extended nonnegative arithmetic. Those pieces can also support other finite prophet inequality developments.
Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6
Fix a dimension , an integer with , and a vector . Draw a random -dimensional subspace from the distribution invariant under orthogonal transformations. Let be the Euclidean orthogonal projection of onto , and put , its projection onto . The matrix turns the vector into the coordinatewise product .
For a coordinate vector , let and . Thus records the magnitude of the largest negative coordinate of . An unsubscripted vector norm is always the Euclidean norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2
The formal model samples an matrix with independent standard normal entries and sets . The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension . The construction covers the endpoint cases and as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6
For arbitrary choices and at each dimension, the central target is
The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of and may change with ; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13
The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6
The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7
The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.
A direct norm bound on and loses the coordinate information needed for the factor . The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.
Vectors are EuclideanSpace ℝ (Fin n), so is the norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated -dimensional law almost surely.
Lemma 6 concerns and , where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains , , and . Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition . All limits are probabilities tending to one, never probability one at every finite .
Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.
A production process deteriorates over time, and the state it is in cannot be observed directly. Each period the operator chooses among three actions: produce without looking, produce and inspect the item (which reveals the current state at a cost), or revise the process back to its good state. This is one of the earliest partially observed Markov decision problems with a costly observation action, and it is the prototype of the inspection and machine-replacement models that followed in operations research and maintenance theory. Ross (Management Science 17(9), 1971) set it up for a countable state space, reduced it to a fully observed problem on beliefs, and determined the structure of an optimal policy for two states.
Intuition suggests a three-region policy for two states: produce while the probability of the bad state is small, inspect at intermediate probabilities, revise when it is large. Ross showed that the true structure has up to four regions: produce, inspect, produce again, revise. This mission formalizes that structure theorem and the general results it rests on.
The underlying process has a countable set of states , with transition probabilities from state at the end of a period to state at the beginning of the next. In state , producing without inspection costs , producing with inspection costs , and revising costs ; costs are bounded, and future costs are discounted by . A revision puts the process in state .
The decision maker tracks a belief , a probability vector on the states, ranging over
Producing without inspection moves the belief to , with . Inspecting reveals the state; if it is , the next belief is the row . Revising leads to .
The -discounted optimal cost is the limit of value iteration: and
The three terms with replaced by form the right side of the optimality equation (1). The -optimal produce, inspect and revise regions are the sets of beliefs at which the corresponding term equals , and a stationary rule is -optimal when it always selects an action attaining the minimum.
In the two-state process of §3, state is good and state is bad: , , , , , , with . The belief is a number , the probability of the bad state, , and the optimality equation becomes
There are thresholds with such that the rule
is -optimal, and whenever revising is -optimal at some belief. Degenerate thresholds (empty intervals) are allowed, so the statement fixes only the order of the regions, not their number.
Theorem 3.3 reduces the search for an optimal policy in the two-state problem to the choice of three numbers, and it fixes the order of the regions: there is never a revise region below an inspect region, and inspection never occurs below the deterioration probability . Together with Theorems 3.4 and 3.7 of the same paper (separate missions in this series), it is the basis for computing optimal inspection policies by searching over thresholds. Theorem 2.2 holds for any countable state space and is the general form of the observation that, in partially observed problems with linear-in-belief action costs, the regions of the "information" and "reset" actions are convex while the region of the passive action need not be.
The results are proved in the paper. As far as a search of the Prove2Me library shows (October 2026), none of them is formalized. Related formal work treats other models: belief-state reductions of finite POMDPs, and abstract contraction models for discounted dynamic programming. The mission produces machine-checked versions of the general model's optimality equation, the concavity of its value function, the convexity of two of its regions, and the two-state structure theorem.
The paper's proofs are short and lean on facts quoted from the literature. Theorem 3.3's proof is two sentences long. Filling it in requires several facts that the paper leaves implicit. The revise region of the two-state model is a closed right-hand interval. The inspect region meets in an interval, through the affine embedding of into . The half-open endpoints of the rule select optimal actions. That last point needs continuity of inside , a consequence of concavity, and Lemma 3.2 at the left end. The naive reading of the printed theorem, with all three thresholds in , is false in general (see below), so the threshold bookkeeping cannot be skipped.
On the general side, the optimality equation (1) is quoted from Blackwell. Here it must be proved for value iteration on the belief simplex of a countable state space, where the inspect term is an infinite series of values at the rows . Its convergence and the contraction estimates use the boundedness of the costs.
The general model is a structure over a type ι with [Countable ι], a distinguished state i₀, a transition matrix Pm, costs C I R : ι → ℝ and β. A separate predicate Model.Valid requires nonnegative entries, rows with HasSum (Pm i) 1, bounded costs and 0 < β < 1. The simplex uses HasSum P 1, never tsum, so it consists of genuine probability vectors. is defined as limUnder atTop of value iteration from , which is the paper's own characterization in the proof of Lemma 2.1. It is not an arbitrary function assumed to satisfy (1). The paper's definition as an infimum over measurable policies is not formalized; the policy class would be a separate mission. Regions are subsets of .
The two-state model is the instance ι = Fin 2 with , , , , and its value at the scalar belief is the general at . The general Lemma 2.1 and Theorem 2.2 therefore apply to it without restatement. Standing hypotheses of §3 are , and . is implicit in the paper, where the good state costs and the bad state . "-optimal rule" means a rule selecting a minimizer of the right side of (3) at every , the criterion the paper quotes on p. 588. "Every -optimal policy produces" (Lemma 3.2) means that producing is the unique minimizer.
Threshold repair. The paper prints . This is false when revising is never optimal, for instance when : then always producing is optimal and revising at is strictly worse, so no rule revising on a nonempty is optimal. The goal keeps exactly when the -optimal revise region is nonempty and otherwise allows ; the rest of the printed chain, , is kept. Adding the hypothesis instead would drop a case the paper covers.
The statement admits no trivializing reading. The thresholds are quantified existentially, but the rule must be optimal at every belief in , is pinned down by its definition, and the paper's numbers (, , , , ) satisfy all hypotheses.
Infrastructure needed: tsum manipulations on the belief simplex (linearity of , summability of for bounded ), a sup-norm contraction argument for value iteration, and closure of concavity under minima and pointwise limits. The value-iteration and contraction lemmas are reusable for any discounted model with bounded costs. Contributions of intermediate lemmas, such as continuity of the two-state on or the bridge identities , are welcome.
A prophet inequality compares two observers of a sequence of nonnegative random variables . The prophet knows all values in advance and collects . The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of , and the factor is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.
Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least , is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor : with a median of , Theorem 1 of the paper gives or . Mission I of this series formalizes that theorem.
Timeline (as recounted on p. 1213 of the paper).
Fix and a probability law on . Let be independent with common law , and . For a constant the threshold rules are
The stopped value is or . The truncated expectations are and : they discard the forced stop at time below the threshold. The class is the set of all and with .
The lower half of the theorem uses an explicit family. For , , and , the variables take the values , , with probabilities , , . Two constants enter:
This is unrelated to the of the NOTE in §1 of the paper.
In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are and ; Emax, EstopT, EstopS, EplusT, EplusS are , , and the terms; supE and supEplus are the two suprema over ; threePoint n a b c is the law of ; aStarIID and Q are the constants above.
over i.i.d. nonnegative . It is stated as three facts: for every and law; ; and for every some and law with .
Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.
The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.
The limits are "easily seen" on the page, but each requires controlling uniformly with the exact law of a stopped index on a product space, including the forced stop at whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every and with must be shown to coincide almost surely with one of , , or stopping at , and the first and last must be shown dominated by for every finite , not only asymptotically. The final step is a joint limit in , in which while the correction term vanishes like ; an iterated limit is not the statement.
The i.i.d. variables are the coordinates of under the product measure ; all quantities depend only on the joint law, so the supremum over is a supremum over laws with . Indices are 0-based in Fin n with [NeZero n], the paper's index being ⊤. Expectations are lintegrals of ENNReal.ofReal in : no integrability is assumed and is allowed. The sup over ranges over and over both families and . Limits along the triangular array are indexed by and taken in after toReal; the early terms with , where the clipped weights of threePoint do not form a probability measure, do not affect any limit.
The page's ratios are not written literally: in the quotients and take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on , which rules out the Dirac mass at and sub-probability witnesses.
A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.
Menger's theorem is the oldest of the min–max theorems of combinatorial optimization. It says that the largest number of disjoint paths joining two sets of vertices of a finite graph equals the smallest number of vertices whose removal disconnects them. The max-flow/min-cut theorem of Ford and Fulkerson (1956), the Kőnig–Egerváry theorem on bipartite matchings (1931), Whitney's characterization of -connected graphs (1932) and the integrality of network-flow polytopes all belong to its family. In operations research it underlies network reliability (how many vertex failures a network survives) and disjoint routing.
Karl Menger proved it in 1927, in a paper on curves. In Zur allgemeinen Kurventheorie (Fund. Math. 10, pp. 96–115) the graph statement is a lemma, Satz δ (p. 101), on the way to characterizing the order of a point of a regular curve by the number of arcs ending there (the subject of mission II of this series).
Timeline.
Let be a finite simple graph on a vertex set , and let be disjoint sets of vertices.
A set separates and if every walk of from a vertex of to a vertex of passes through a vertex of . The set may contain vertices of and of ; in particular always separates.
is -point connected between and ("n-punktig zusammenhängend", p. 100) if no set of fewer than vertices separates and :
A family of disjoint – paths consists of paths of , each from a vertex of to a vertex of , whose vertex sets are pairwise disjoint, end vertices included.
The degree (Grad) of is its number of edges. A part of is a spanning subgraph ; it is proper if it lacks an edge of . is irreducibly -point connected between and if it is -point connected and no proper part is. For a separating set , the side of towards is formed by the components of that meet , together with their edges to ; the side towards is defined symmetrically.
In Lean these are Menger27.Graphs.Separates, NPointConnected, HasDisjointPaths, IrreduciblyNPointConnected and sidePart.
This is the direction Menger states; the converse (disjoint paths force every separator to be large) is immediate and is not part of the mission.
The result. Satz δ is the vertex form of Menger's theorem for two sets, from which the other standard forms follow: the two-vertex form, Whitney's theorem, the edge form (through line graphs), Kőnig's theorem (for bipartite with , the two sides) and, through a standard reduction, integral max-flow/min-cut for unit capacities. Menger used it as the finite step of his theorem on -legs at points of regular curves.
Formalizing it. The theorem is proved, with many published proofs. Mathlib at the pinned revision has edge connectivity of simple graphs but no vertex separators between sets and no form of Menger's theorem; nothing on Prove2Me states it in set form. The mission produces a statement of Satz δ about Mathlib's SimpleGraph, together with the intermediate claims of Menger's own induction, so that the original argument, including the step Kőnig completed, can be checked. Related posed items on the platform are the two-vertex Whitney theorem Balinski61.Whitney.whitney_theorem (internally disjoint paths between two vertices) and Kőnig's theorem MatousekLP.Integrality.konig; neither is the set form stated here, and neither is proved yet.
The obvious argument, choosing disjoint paths one at a time, fails: a first path chosen badly can block every completion, so the paths must be chosen together. Menger's induction avoids this by passing to an irreducible part and cutting it at an -vertex separator, but it needs a vertex outside to cut at (milestone 4). When every vertex of the irreducible part lies in the part is bipartite between and , and the claim is then Kőnig's matching theorem rather than an observation; this is the gap of 1927. The gluing step (milestone 7) is also more delicate than on the page: the paths of the two sides must meet the separator only at their ends, which depends on how the sides are cut out.
Representation. Menger's gewöhnlich eindimensionaler Raum, a finite union of arcs meeting at most in end points, is read as a finite simple graph G : SimpleGraph V with [Fintype V]; and are Finset V. Vertices are the points of and the end and branch points (Menger's punktförmige Stücke); edges are the arcs between them, subdivided so that there are no loops or parallel edges. Subdivision changes neither separation nor the number of disjoint paths, and a separating point inside an arc can be moved to an end of the arc. Menger's degree (the number of arcs between consecutive punktförmige Stücke) becomes the number of edges, which a subdivision only increases; every milestone stays true.
Conventions and explicit readings of the paper's phrases.
H ≤ G; "echter Teil" is H < G.sidePart G P S), not quantified over; it has no edges at the vertices of , matching Menger's considered between and .Trivializations ruled out. Forcing separators to avoid , counting internally disjoint or edge-disjoint paths, or allowing two paths to share an end vertex would each change the theorem; none is done. No hypothesis restricts , and is the trivial case, not an excluded one.
Needed infrastructure. Walk surgery (prefixes up to the first visit of a set, concatenation, conversion of walks to paths), transfer of walks along SimpleGraph inclusions, and well-founded induction on the number of edges. Separators and disjoint path families between sets are reusable beyond this mission, for Whitney's theorem, Kőnig's theorem and flow integrality. Proofs by any method are welcome, including a proof of the goal through max-flow/min-cut or an independent argument (Göring's) bypassing the milestones.
An arc can end at a point of a curve in several distinct directions. Menger's 1927 paper asks whether the number of arcs that can meet only at that point is determined by a local measurement: the smallest boundary size available around the point. This gives a concrete meaning to the order of a point in a regular curve. The question belongs to the early study of curves as compact metric spaces rather than as drawn or parametrized lines. A curve can wind near a point in ways that make the count of visible branches misleading; the local boundary definition is meant to survive such behavior. Menger, Zur allgemeinen Kurventheorie (1927), pp. 96–99.
The paper also states a topological version of the disjoint-path principle: if a small point set cannot separate two finite sets in a suitable compact space, the space contains a corresponding number of disjoint arcs between them. This principle connects the local order question to Menger's finite-graph result, treated separately in the first mission of this series. Here the central object remains a regular curve and one of its points. Menger (1927), Satz β and Satz δ, pp. 100–102.
A curve is a compact connected metric space in which each point has arbitrarily small open neighbourhoods with totally disconnected boundaries. A point is regular if arbitrarily small open neighbourhoods have finite boundaries. A regular curve is a curve all of whose points are regular. Because every finite set is totally disconnected, the Lean representation takes a compact connected metric space and requires every point to be regular; this already satisfies the paper's curve condition. Menger (1927), pp. 96–97.
For a point , write for the boundary of an open neighbourhood . The point has order at most if every open neighbourhood of contains one with at most boundary points. It has order exactly if it has order at most and no smaller finite order. Thus an upper bound on order is not the same as exact order. An arc is a continuous injective map . A topological -leg at is a family of arcs with and with images intersecting exactly in for distinct indices. Injectivity makes each leg a real arc, including when the space has isolated or degenerate cases.
To express the intermediate results, a set separates and in a space if is the union of two disjoint relatively closed parts, one containing and the other containing . The space is -point connected between and if no subset with fewer than points separates them. In the theorems using this notion, and are disjoint and closed in , as stipulated before Menger's definition. A separator may itself meet either set. Menger (1927), pp. 99–100.
The main target is the first and final assertions of Menger's Theorem on p. 98. For every point of exact finite order in a regular curve ,
This states that is the greatest possible number of legs. The second assertion is the observation begun on p. 97 and completed on p. 98; it is included because the Theorem's concluding characterization depends on it. The paper's separate assertion for points of growing order is outside this finite-order target. Menger (1927), pp. 97–98.
The principal supporting target is Satz β. In a compact metric space whose points are all regular, let be finite disjoint sets. If is -point connected between them, there are pairwise disjoint arcs, each with one endpoint in and the other in . Satz δ is the finite union-of-arcs case, while Satz γ concerns decreasing intersections of closed separators. The milestone list also records the neighbourhood sequence, its annulus connectivity statement, and Satz α, which gives disjoint arcs crossing each annulus. Menger (1927), pp. 99–105.
The result turns a definition made from arbitrarily small neighbourhood boundaries into a geometric count of arcs. It permits local point order to be recognized through an embedded finite star, without choosing a drawing or a parametrization of the whole curve. Satz β supplies a reusable disjoint-arcs statement for compact regular spaces; Satz γ isolates the compactness and local-connectedness condition needed when separators are obtained as a limit. These are independent point-set topology statements as well as parts of the order theorem. Menger (1927), pp. 98–105.
The theorem is proved in the paper; the work here is to state its objects and assertions precisely in Lean and then supply checked proofs. Mathlib supplies boundaries, compactness, extended cardinality, unit intervals and connected components, but these Menger-specific definitions and topological disjoint-arcs theorems are not already represented by a matching published platform item in the local prior-art catalog. The first mission of this series treats the finite-graph form of Satz δ; its draft statement is distinct from the topological version here and cannot be imported as a published theorem.
A direct attempt to add one new arc to a chosen collection can fail. Menger gives a curve made from a line segment and a spiral winding toward its midpoint: the point has two available directions, but choosing the spiral as the first leg leaves no second leg disjoint from it away from the midpoint. The count of already selected arcs therefore does not by itself control whether another can be added. The paper also notes that an inverse-limit argument does not immediately apply, because the order of a point in a decreasing family of regular curves can drop in the intersection. These examples explain why the statement needs conditions on boundary sizes and separators rather than only a local picture of branches. Menger (1927), p. 99.
The Lean development uses a metric space with CompactSpace and ConnectedSpace for the main regular curve. An open set containing is a neighbourhood. “Arbitrarily small” means that every such open set contains a smaller open set with the stated boundary property. Boundary size is measured by Set.encard, so infinite boundaries do not receive the spurious value zero. Exact order includes a minimality clause for every , including . Arc maps use the closed unit interval and are continuous and injective; the parameter value zero is the endpoint at . Pairwise disjoint legs have image intersection exactly , while arcs joining to have disjoint images altogether.
For the neighbourhood milestone, “shrinking to ” is made quantitative by diameters tending to zero, with each neighbourhood bounded; compactness gives the latter. The paper's sequence starts at , while Lean starts at . The annulus is constructed as from nested open neighbourhoods, and its endpoints are the two frontiers. Relative closedness in the definition of separation is imposed inside . Satz β is stated for a compact space of regular points without adding connectedness or an independent finite-components assumption. A compact subset can be represented by its subtype when this theorem is applied. The ordinary one-dimensional spaces of Satz δ are finite unions of injective arcs, with distinct arcs meeting only at common endpoints.
The development needs reusable lemmas on finite-boundary neighbourhoods, regularity of the relevant subspaces, closed separators, and the relation between point connectivity and disjoint arcs. Contributions to these foundations and to the seven stated milestones are in scope. Constant maps cannot count as legs, and order at most alone cannot be used to demand an -leg; both would erase the theorem's content.
The traveling salesman problem asks for a shortest closed route through a set of cities. Writing it as an integer program requires linear constraints whose integer solutions are exactly the routes. The assignment constraints (each city entered once and left once) are not enough: their integer solutions include collections of disjoint cycles, called subtours, that never pass through the starting city. Some extra family of constraints must rule these out.
In 1960 C. E. Miller, A. W. Tucker and R. A. Zemlin gave such a family using one auxiliary real variable per city (J. ACM 7(4), 326–329). Their MTZ constraints have polynomially many rows, for cities, whereas the subtour elimination constraints of Dantzig, Fulkerson and Johnson (1954) (Oper. Res. 2(4)) have one row per subset of cities. They also handle a generalization: a salesman who returns to base several times, visiting at most cities per trip. This is the basic form of a capacitated vehicle routing problem. MTZ-type constraints remain standard in vehicle routing models and in textbook formulations of the TSP. Their linear relaxations are known to be weaker than those of the subtour elimination formulation (Padberg and Sung, 1991).
The paper attributes the model to Tucker and reports five machine experiments with Gomory's all-integer algorithm. The computational part is outside this mission.
There are cities and a base city . A tour is a succession of visits to cities without stopping at city . In problem (1) the salesman leaves , visits each of the cities exactly once and returns to , possibly several times, with at most cities per tour. Formally, an itinerary is a list of tours. Each tour is a nonempty list of cities other than of length at most , and each city occurs exactly once in the concatenation of the tours. The number of tours is the number of returns to . Tour travels the arcs . denotes the number of times travels the arc . For real distances , the length of is the sum of over the arcs it travels.
Problem (2) has non-negative integer variables () and real variables :
When the number of tours is fixed, the relation is added. With and , (1) is the standard traveling salesman problem.
For every and every :
with equal to the number of tours , and with the in the converse taken to be non-negative integers. In addition, equals the length of for all real . The paper says that (2) "will be shown to be equivalent to (1)". Its "burden of proof" is that the two feasible sets correspond and the two objectives agree, and the goal states exactly that.
The result. The theorem justifies using (2) in place of (1). Because the feasible sets match and the objectives agree, an optimal solution of (2) is an optimal itinerary of (1), and the same holds with the number of tours fixed. It also shows that a compact, polynomial-size family of linear inequalities in auxiliary potentials excludes every subtour. The same idea, with the read as loads or arrival times, underlies the standard capacity and time-window constraints of vehicle routing.
Formalizing it. The result is classical and its proof is short, but the paper argues informally. It follows successor chains, treats "a tour" without defining an itinerary, and leaves several steps implicit, including the hypothesis and the distinctness of and . No machine-checked statement of the MTZ equivalence is recorded on the platform. The remaining work is the whole formal proof: the combinatorics that turns a 0/1 matrix with unit row and column sums and no subtours into a list of tours, the converse labelling, and the bookkeeping identity between the two objectives.
The inequalities themselves are elementary. Each milestone about (2) is a short computation with the potentials . The work is in the passage from a feasible matrix to an itinerary. The successor walk from city must be shown to terminate at and to cover every arc of . The resulting tours must be listed so that their arc counts reproduce exactly, including the number of arcs leaving . That number is not constrained directly in (2). It equals only through a counting argument on the row and column sums. A proof that only shows some itinerary exists does not establish the correspondence the paper claims.
Cities are Fin (n + 1) with 0 the base city, which is the paper's indexing. The commitments, each also stated in the items' Formalization Notes, are:
List of tours, each tour a List of cities. The paper's "legitimate itinerary" is read as: every tour nonempty, free of 0, of length at most ; the concatenation duplicate-free; every city present.Not formalized: the constraint and variable counts and the elimination of "to produce an equivalent problem with inequalities and variables" (p. 328), which the paper does not make precise, and the machine experiments (pp. 328–329).
Trivializing readings are ruled out. The goal identifies with the arc counts of an itinerary, not merely the existence of some itinerary. The hypotheses are satisfiable: for , , the itinerary with is feasible for (2), while the subtour is not, for any . Contributions welcome: proofs of the milestones, a reusable library of "functional digraph with unit in- and out-degree" decompositions, and the optimization corollary (equal optimal values of (1) and (2)).
A two-stage stochastic program with recourse models a decision taken in two steps: a first-stage decision is fixed before a random outcome is observed, and a second-stage (recourse) decision is chosen after the outcome is known, both subject to constraints and both incurring costs. The model is the standard framework for planning under uncertainty in operations research: capacity planning, production and inventory, energy dispatch, finance.
For linear recourse problems, duality was developed in the 1960s and early 1970s by Wets and others, partly under integrability restrictions on the random data. R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality (Pacific J. Math. 62 (1976), doi:10.2140/pjm.1976.62.173), treat the convex case, where every cost and constraint function is convex, by embedding the problem in a family of perturbed problems and applying the perturbational theory of convex duality (Rockafellar, Conjugate Duality and Optimization, SIAM 1974) together with the theory of convex integral functionals. The paper's dual variables are integrable price systems, interpreted as equilibrium prices for perturbations of the constraints; it is the starting point of a series of papers by the same authors on stochastic convex programming (relatively complete recourse, Kuhn–Tucker conditions, singular multipliers).
Let be a probability space. A vector is chosen subject to and (), at cost . Then is observed and is chosen subject to and (), at cost . The aim is to minimize the expected cost
The standing assumptions are: , convex, closed and nonempty; and convex and finite everywhere; measurable, summable for and bounded for .
Decisions live in and perturbations in . The perturbation functional is the expected cost if satisfies the constraints with right-hand sides and, almost surely, , and otherwise. The problem minimizes .
The space is paired with by , and with in the same way. The Lagrangian is , the dual maximizes over , and the perturbation function is . Conjugates , are taken with respect to the pairing of with .
If and are bounded, then
and in fact is a proper convex function on , lower semicontinuous for the weak topology , the infimum defining is attained for every , and . The goal is the theorem exactly as printed, all conclusions included.
The mission also poses the explicit form (1.8) of the Lagrangian and Corollary 1 (dual solutions are the negatives of subgradients of at ; saddle-point characterization of primal solutions when ).
Theorem 3 gives, for bounded constraint sets, the absence of a duality gap between a convex recourse problem with essentially bounded decisions and its Lagrangian dual over integrable multipliers, together with existence of an optimal decision. Through Corollary 1 it reduces the necessity of the Kuhn–Tucker (saddle-point) optimality conditions to the single question whether is nonempty, and through the paper's later results it describes the directional derivatives of the optimal value with respect to perturbations of the constraints.
The result has been proved since 1976; it has not been machine-checked. A formal development produces the problem model on and spaces, the weak topologies of the pairings, and conjugate duality for extended-real-valued functions on such paired spaces, none of which is currently available as a ready-made Lean statement on this platform.
The obvious argument fails at two points. First, is , and the biconjugate equals only for a lower semicontinuous proper convex function in a topology compatible with the pairing. Lower semicontinuity of in the norm topology of is not enough: the pairing is with , not with the norm dual of , so the relevant topology is the weak topology , and an infimum of lower semicontinuous functions is in general not lower semicontinuous. Second, the lower semicontinuity of itself, in the weak topology, is a statement about convex integral functionals on that rests on measurability of the integrands in jointly with continuity in the decision variables. Boundedness of , is what supplies the compactness that is otherwise missing.
Fin n → ℝ and the products , are dot products. Constraint indices are Fin m.Lp (Fin n → ℝ) ⊤ σ and Lp (Fin n → ℝ) 1 σ, spaces of almost-everywhere classes; all second-stage conditions are stated almost surely. is a probability measure (IsProbabilityMeasure).EReal; infima and suprema are lattice operations in EReal, so there are no junk values for empty or unbounded sets. Every sum has a real first summand, so no convention enters.A complete development needs the identification of with the dual of on a probability space (for weak-* compactness), lower semicontinuity of convex integral functionals, and conjugate duality on paired locally convex spaces. These are reusable well beyond this mission. Proofs of milestones, and of auxiliary lemmas of this kind as separate theorems, are welcome. The mission Stochastic Convex Programming: Basic Duality 2 formalizes the paper's other main result, on the first-stage problem and attainment of the recourse.
The Graph Minors series of Robertson and Seymour proves that finite graphs are well-quasi-ordered under the minor relation. A central tool of the series is the duality between two ways of measuring how "tree-like" a graph is: decompositions along a tree, which certify that a graph is thin, and tangles, which certify that it contains a highly connected region that no small separation can split. Graph Minors X (Robertson and Seymour, 1991) introduces tangles and proves the exact minimax relation between the tangle number and branch-width, an invariant within a constant factor of tree-width. Tangles became a standard object of structural graph theory and were later abstracted to connectivity systems, matroids and data clustering; branch-width is the parameter behind dynamic-programming algorithms on graphs and matroids of bounded width.
A hypergraph consists of a finite vertex set , a finite edge set and an incidence relation; an edge may be incident with any number of vertices, its ends, and the size of an edge is its number of ends. Write for the maximum size of an edge ( if ).
A subhypergraph is given by a set of vertices and a set of edges containing all ends of its edges. A separation of is a pair of subhypergraphs with and no common edge; its order is .
For an integer , a tangle of order is a set of separations of order such that (i) for every separation of order , one of lies in ; (ii) for any three members of ; (iii) for every . The tangle number is the largest order of a tangle in , or if there is none.
A ternary tree is a tree whose vertices have valency or . A branch-decomposition of is a ternary tree with a bijection from its leaves onto . Deleting an edge of splits the leaves, hence , into two parts; the order of is the number of vertices of incident with edges on both sides. The width is the largest order of an edge of , and the branch-width is the minimum width over all branch-decompositions, with when .
The proof goes through an abstract setting. On a finite set , a connectivity function is a symmetric submodular map . A set is efficient if . A bias is a set of efficient sets containing one of for each efficient and no three members covering . Its dual object is a tree-labelling: a ternary tree whose incidences carry efficient sets, complementary across each edge, covering at each internal vertex, and absorbed by a given family at each leaf.
The exception is genuine: a hypergraph with a vertex and only edges without ends has and .
A companion statement, (4.4), computes and, for , .
The minimax theorem makes tangles the exact obstruction to small branch-width: either a branch-decomposition of width at most exists, or a tangle of order witnesses that none does. Every later use of tangles as certificates of high connectivity in the Graph Minors series, including the tree-decomposition of a graph into regions indexed by its maximal tangles and the grid theorem, rests on this duality. The abstract lemma (3.5) applies to any connectivity function, so it also gives the duality for matroid branch-width and for other symmetric submodular functions.
The results are proved in the published paper; none has a machine-checked proof that this mission is aware of. The platform has branch-width objects for set functions on subcubic trees, from the Oum–Seymour approximation of clique-width (ApproxCliqueWidth.Certificate.bw_ge_of_wellLinked, bw_le_of_no_wellLinked), which bound branch-width by well-linked sets, a different obstruction. This mission adds a hypergraph tangle library and the exact minimax.
The inequality and the direction "a tangle of order excludes width " are short. The converse, building a branch-decomposition of width when no tangle of order exists, is the hard direction. A natural first attempt is to merge small separations greedily into a tree, but the submodular uncrossing step can destroy the leaf conditions already established, and an induction on the edge set does not preserve the tangle hypothesis. A second difficulty is bookkeeping: the trees are ternary, so every construction that cuts, joins or contracts trees must restore valencies and , and the passage between leaf labels and edges of needs the labels at the leaves to partition .
The objects live in the namespace RobertsonSeymour1991.GM10.Minimax.
V, E; every theorem assumes [Finite V] [Finite E], as the paper assumes all hypergraphs finite.IsTangle G θ 𝒯 with built in, and the three members in the second axiom need not be distinct. The tangle number is a supremum in of a set bounded by , so it is a maximum.Fin n. A branch-decomposition stores as an injection of the edges onto the leaves.Set E, and is the complement. The incidence with is the adjacent pair , and every condition on labels is required on adjacent pairs only.Junk values would make the goal trivial: a tangle number of from an unbounded set of orders, or a branch-width of from an empty set of decompositions. Neither occurs: every tangle has order at most , and a branch-decomposition exists whenever . The goal also keeps the exact exception , neither dropped nor strengthened.
A complete development needs finite trees with leaf counting, path and component reasoning in SimpleGraph, and submodular uncrossing arguments. The tangle library of §2 and the abstract minimax of §3 can be reused beyond this mission. Contributions of tree lemmas (ternary trees on Fin n, grafting two trees at a leaf, contracting a valency-2 vertex) are welcome.
The other main results of the paper are separate missions of this series: Graph Minors. X. … II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1), III: In the θ-Grid, the Separations of Order < θ With Small E(A) Form a Tangle of Order θ, IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions, and V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}.
The proximal point algorithm is a basic iterative scheme of convex optimization and monotone operator theory. To solve a problem governed by a monotone operator, it replaces the problem by a sequence of better-conditioned problems, each regularized by a quadratic term centred at the previous iterate. Augmented Lagrangian methods, the Douglas–Rachford and ADMM splitting schemes, and many bundle methods can all be read as instances of it.
The scheme first appeared in a five-page note by Bernard Martinet in the Revue française d'informatique et de recherche opérationnelle (1970), under the name régularisation par approximations successives. Martinet stated it for a monotone variational inequality on a bounded closed convex subset of a Hilbert space and proved that the weak cluster points of the iterates are solutions. This mission formalizes that first convergence theorem as it was originally stated.
Timeline.
Let be a real Hilbert space with inner product and norm . Let be its dual, and write for the value of a functional at . Let be convex, closed and bounded, and let be
The variational inequality (1) asks for such that
Its solution set is denoted (solSet T C in Lean).
Martinet's regularization algorithm starts from . Given , it determines such that
In words, solves the variational inequality for the operator , which is strongly monotone. A point is a weak cluster point of if every neighbourhood of in the weak topology contains for infinitely many .
Every weak cluster point of the regularized iterates solves (1). The paper's Lemme 2 states the same thing. The goal assumes neither that (1) has a solution nor that is bounded on .
The result. Théorème 1 is the first convergence theorem for the proximal point method. The method only needs to solve strongly monotone subproblems, and those are well posed even when the original problem is not. Together with the existence result, the theorem says the iterates accumulate weakly only at solutions. When the solution is unique, the whole sequence converges weakly (the Corollaire). The later theory of Rockafellar, Brézis–Lions and the splitting literature refines this statement.
Formalizing it. The result has been proved since 1970. What this mission adds is a machine-checked version that follows the original hypotheses: an operator into the dual, hemicontinuity rather than continuity, and no maximality assumption. The cited ingredients, the Lions–Stampacchia existence theorem in an infinite-dimensional Hilbert space and Minty's lemma, are not in Mathlib as far as this mission is aware. Formalizing them is part of the work and is reusable well beyond this paper. The milestone items on the platform are statements awaiting proof. None of them has a machine-checked proof yet.
Lemme 1 and inequality (7) follow from the defining inequality (2) and the algebra of the inner product. The difficulty is at two other points.
First, the iterates satisfy the variational inequality only approximately, and only with evaluated at the iterate. A weak cluster point gives no control over , because is merely hemicontinuous and is not assumed weakly continuous or bounded. The obvious idea, to pass to the limit in , fails for this reason. Passing to the limit requires the reformulation in which is evaluated at a fixed point of . That reformulation is Minty's characterization (5), and proving it uses hemicontinuity along segments.
Second, the proof of Lemme 1 needs a solution of (1) to exist. In infinite dimensions that is the Lions–Stampacchia theorem. Its standard proof goes through Brouwer's fixed point theorem on finite-dimensional sections together with weak compactness of , and this is the heaviest item of the mission.
NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H. The paper says only "espace de Hilbert". Its ordered inequalities force real scalars.StrongDual ℝ H, and is φ y. is not replaced by a map through the Riesz isomorphism.IsRegSeq): any sequence with that satisfies (2) at every step. Existence and uniqueness of the step are milestone 2, not built into a definition.MapClusterPt in WeakSpace ℝ H, a cluster point in the weak topology. It is not a cluster point in the norm topology, which would make the goal weaker.Filter.liminf on returns a junk value on sequences that are unbounded below.A trivializing formalization is ruled out. The goal does not assume , boundedness of , or strong cluster points. Its hypotheses are satisfiable: , , , is an instance, checked locally.
Not formalized: Remarques 1 and 2 of §II (a variable-weight variant of (2), whose printed form is apparently misprinted, and the removal of boundedness of under a coercivity condition), because the paper gives neither a proof. Théorème 2 (§III) and the convex-minimization §IV are not formalized either. §IV is the subject of the companion mission.
Contributions are welcome on each milestone, and especially on the general infrastructure: Minty's lemma, Hartman–Stampacchia/Lions–Stampacchia existence for monotone hemicontinuous operators, and the fact that bounded sequences in a Hilbert space have weak cluster points. A proved Brouwer fixed point theorem (AGT.brouwer_fixed_point) and a Banach–Alaoglu theorem (FamousTheorems.banach_alaoglu) are available on the platform as tools.
Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation
where is the normal-cone operator of a closed convex set . S. M. Robinson introduced strong regularity of such an inclusion at a solution in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).
Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set the paper's appendix does this by a reduction: locally around the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.
Work in with the standard inner product, which identifies with its dual. For the normal cone at is
A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex , an real matrix and , and consider
It is strongly regular at a solution with constant if there are neighbourhoods of and of such that for each the perturbed inclusion
has exactly one solution in , and on .
The reduction uses the following objects, all built from the data:
The reduced form of (A.1) at is the inclusion for ; in an orthonormal basis adapted to , and it is with an matrix . It is vacuous when .
If solves (A.1), then (A.1) is strongly regular at if and only if
No Lipschitz constant is fixed: the left side is "strongly regular for some ".
Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where itself is neither positive definite nor a P-matrix.
The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.
The definition of strong regularity is local, while condition (ii) is global on . The obvious argument, "linearise and read off the inverse", does not apply, because is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of may move the solution off the face , and only polyhedrality, through the finitely many values of on and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near to uniqueness on all of . The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.
EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is . A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause , so off ; without it every inclusion would be satisfiable at points outside and the statements would change meaning.Submodule.starProjection.A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.
The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.
Let be positive integers and give its Euclidean norm. Write , with and . Let be nonempty, closed, and convex, and put . For , the normal cone is
For , is empty. Thus the inclusion itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.
Partition the real square matrix into blocks , , , and , where is . When is nonsingular, its Schur complement in is
A real matrix is positive definite in the theorem's sense when for every nonzero . Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.
For , the first target is the sufficient condition
Here “is Lipschitz” includes that exactly one inverse value exists at every . The assertion holds for every nonempty closed convex ; it is not restricted to polyhedral sets.
When , the second target is an equivalence:
The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.
The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.
A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.
Nonsingularity of the full matrix alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as reaches different faces of . A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of . For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.
Lean represents as a Euclidean space indexed by the disjoint union of and . This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.
The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex , matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.
Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.
The job-shop scheduling problem asks how to time a set of tasks on shared machines so that every product is finished as early as possible. Around 1959 several authors proposed to solve it with Gomory's then new integer programming (Gomory 1958). The obstacle is the noninterference condition: two tasks on the same machine must not overlap, so one of them must finish before the other starts. That is an "either-or" condition. It describes a nonconvex set, and classical linear programming cannot express it.
A. S. Manne's note On the Job-Shop Scheduling Problem (Operations Research 8 (1960) 219–223) writes the either-or condition as two linear inequalities in integers. It adds one 0–1 variable per pair of tasks that compete for a machine, and it uses a large constant derived from a bound on the start days. This is the origin of the big-M disjunctive formulation, which remains the standard textbook integer program for job shops and, more broadly, the standard way to linearize a disjunction of two linear inequalities.
Timeline. Johnson (1954) introduced the make-span criterion for two- and three-stage production schedules. Bowman (1959) and Wagner (1959) proposed integer programs for machine scheduling. Manne (1960), stimulated by Bowman's paper, gave the formulation stated here. He counted its unknowns as 275 for 5 machines with 10 tasks each, against 600 for Wagner's formulation on the same example (p. 222).
There are tasks and machines. Task requires the single machine for consecutive days, where is an integer. An integer horizon bounds the start days: the integer unknown is the day on which task begins. A pair with and is a conflicting pair. For each such pair the tasks must not overlap:
The instance may also impose precedence for given pairs (5a), exact delays for given pairs (5c), and delivery dates for given tasks (6). A schedule is an satisfying (1), (5a), (5c) and (6). Its make-span is
the calendar time needed for all jobs when the shop starts on day .
Manne's integer program has integer unknowns with , one integer for each conflicting pair, and the minimand , subject to (5a), (5c), (6),
and for every (7). The value means that precedes ; means that precedes .
For every instance and every integer ,
Both minima are required to exist. In particular the program has an optimum exactly when a schedule exists. The paper claims this when it says that "the problem now consists of the minimization of " subject to (2)–(7) (p. 221).
The result. The goal certifies that a single integer program, with one binary variable per conflicting pair, computes the optimal make-span of a job shop with precedence, exact delays and delivery dates. The same pattern is used whenever a disjunction or of bounded linear forms has to be put into a mixed-integer program: a binary variable selects the active branch, and a constant at least as large as the range of the inactive form switches the other branch off. Milestone 1 is that pattern in its simplest form, and milestone 4 shows why the binary variable cannot be relaxed.
Formalizing it. The paper's argument is informal. It rests on a summary table of admissible values of that holds only when the gap is large enough. A machine-checked version fixes the exact hypotheses: integrality of , the bound , and nonemptiness of the task set. To the best of the curators' knowledge, no machine-checked proof of the correctness of the big-M job-shop formulation exists; the definitions here can serve later scheduling missions that need a disjunctive integer program.
The mathematics is elementary, and the difficulty lies in stating it exactly. The obvious reading, "(3)–(4) are equivalent to (1)", is false without the bound . For instance, with condition (4) reads , which cuts off valid orders if start days may lie beyond the horizon. It is also false for real . Equally, "minimize subject to (7)" equals the maximum of only after the optimum over and over are interchanged and the empty task set is excluded. A naive formalization that states the schedule side as "the least with (7)" proves nothing about the make-span.
Tasks are Fin n (the paper's task is index ), machines Fin M. Start days, durations, horizon, delays, delivery dates, and are integers (ℤ), so that and are not truncated. Durations are not assumed positive except in milestones 2 and 4, where positivity is necessary. One definitions file, ManneJobShop.Formulation.Model, holds the instance, the conflicting pairs, schedules, the make-span (Finset.sup', so is required via [NeZero n]) and the integer program.
Explicit readings of loose phrases:
IsLeast of the feasible values of , matched against IsLeast of the set of make-spans of schedules.Trivializing formalizations are ruled out: the make-span is a maximum, not a restatement of (7); is an integer; the horizon appears on both sides; the goal is stated for every instance with , including infeasible ones. The (5b) example is (5a) for two pairs. Wagner's comparison, the remarks on Gomory's algorithm, Dantzig's secondary constraints and Monte Carlo methods, and the economic discussion of the make-span are not formalized. Proofs of every milestone and of the goal are welcome.
Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point has to satisfy . In applications the data depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.
S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.
This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.
Let be a real normed linear space and its topological dual, the continuous linear functionals on . Let be closed and convex. The normal-cone operator of is
A generalized equation is the inclusion , for a function from an open set to . For it is the equation . For the nonnegative orthant of it is the nonlinear complementarity problem. For a general closed convex it is the variational inequality over .
Let solve the generalized equation, and let be Fréchet differentiable at . Linearising gives the multifunction
The generalized equation is strongly regular at with associated Lipschitz constant if there are neighbourhoods of in and of with the following property: for every the inclusion has exactly one solution in , and on . The condition depends only on , and .
In the parametric problem the function is , with in a topological space and base point . Its partial derivative in is .
Assume that exists on , that and are continuous at , and that solves , strongly regularly with constant . Then for every there are neighbourhoods of and of , and a function , with two properties. First, is the unique solution in of . Second,
Write for the linearisation at , for the residual, and . The milestones are four claims of the proof:
Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at , the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.
The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of .
The obvious approach is to apply the classical implicit-function theorem. It fails because is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: from , then and , then the ball radius , then the parameter neighbourhood. The estimate (2.4) has to come out with the constant and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of , for example through the completeness of .
StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off , and an inclusion is written .HasFDerivAt at every point of , for every . Continuity of at is joint and in operator norm.A complete development needs the following:
The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.
Prediction with expert advice asks a learner to predict a binary label in each of a sequence of trials, having seen the predictions of a pool of prediction algorithms (the experts), and to make not many more mistakes than the best of them, with no probabilistic assumption on how the instances and labels are generated. Littlestone and Warmuth's Weighted Majority Algorithm (Littlestone, Warmuth 1994) maintains a weight for each pool member, predicts by a weighted vote, and shrinks the weights of members that err. Its mistake bounds are the origin of the multiplicative-weights method used throughout online learning, game theory and optimization (Arora, Hazan, Kale 2012).
A deterministic master with binary predictions can be forced to err in every trial in which the weight is split evenly, which costs it a factor of about two against the best expert. Section 6 of the paper introduces a randomized master, WMR, which predicts with probability equal to the weighted average prediction of the pool. Theorem 6.1 bounds its expected number of mistakes under a precisely stated condition on how its randomization interacts with the choice of instances and labels.
Timeline:
A pool of algorithms is run for trials on a probability space . In trial the pool member predicts , the label is , and the master predicts . All of these are random variables; deterministic sequences are a special case. Write .
Each member carries a weight. The initial weights are positive, and the update step (5.1) multiplies the weight of member in trial by a factor that depends on , and :
where and . WMR updates in every trial. Let , so and , and let
be the weighted average prediction. WMR predicts with probability . Its number of mistakes is .
The weak independence condition (p. 238) requires, for ,
The conditioning includes the current predictions of the pool and the current label. It allows instances and labels to depend on the master's past predictions, and it holds, for instance, when WMR draws one uniform number and predicts whenever , provided the instances and labels are generated independently of .
Under the weak independence condition, and with almost surely,
The statement fixes neither the pool, nor the update factors within (5.1), nor the distribution of instances and labels.
The step of the proof on p. 240: under the weak independence condition, almost surely, and hence
Theorem 6.1 gives the randomized master the same bound that Theorem 5.2 gives the deterministic master WMC, whose predictions are allowed to lie in . With equal initial weights, for every pool member with total loss , and the bound yields Corollary 6.1 (p. 241): . For close to this is better by nearly a factor of two than the bound for the deterministic binary master WMG. The weak independence condition is also what makes the bound valid against labels that adapt to the master's past predictions, which is the setting of later regret analyses.
The result is proved in the paper; this mission produces a machine-checked version. The platform has proofs of the randomized weighted majority bound in the form of Hazan's Lemma 1.4 and of Mohri et al.'s Theorem 8.4, but both state an expectation over the algorithm's internal distribution with deterministic data, unit weights and one fixed update rule. Neither covers random instances and labels, the conditional-expectation condition, or the whole class of updates (5.1).
The pathwise part of the argument is the loss bound for the weighted average (Lemma 5.3, posed in the companion mission on WMC). The new difficulty is probabilistic. The predictions, labels and weights are random and may depend on each other across trials, so the mistake indicator cannot be replaced by pointwise. The replacement holds only after conditioning on the -algebra , and requires that is -measurable and binary, so that the indicator is affine in . A reading that conditions on less (dropping the current label) or uses unconditional expectations does not support this step when the label depends on earlier randomness.
A second difficulty is that may be infinite: the weights can become arbitrarily small with positive probability.
The pool is Fin n; trials are indexed from to , so totalWeight … 0 is and totalWeight … t is . The probability space is a measure P with IsProbabilityMeasure P. Predictions, labels and master predictions are real-valued measurable random variables; pool predictions lie in and labels and master predictions in on every sample path. Initial weights are deterministic and positive. The update factor of member in trial is a measurable function of the member's prediction and the label, satisfying (5.1) on every sample path; the weights are computed from it, so they are random variables determined by the predictions and labels. is the supremum of the -algebras generated by the pairs , , and the weak independence condition is stated with Mathlib's conditional expectation P[λ j | 𝓕 j].
Expectations in the goal are lower Lebesgue integrals in , so the right-hand side may be and no integrability of the logarithm is assumed. The hypothesis almost surely excludes the case where the paper's bound is infinite and Lean's would make the literal statement false. A formalization that replaces the conditional expectation by the unconditional one, takes the logarithm's Bochner integral (which is when the logarithm is not integrable), or restricts to deterministic instances and labels does not state Theorem 6.1.
A complete development needs the pathwise loss bound of Lemma 5.3 for this weight model, the pull-out property of conditional expectations for bounded measurable factors, and the exchange of expectation and finite sums. The weight model and the filtration are reusable for Theorem 6.3 and for the lazy variant of the Appendix. Proofs of the milestone and of the goal are welcome, as are formalizations of Corollary 6.1.
In prediction with expert advice, a master algorithm predicts a binary label in each of a sequence of trials, after seeing the predictions of a pool of other algorithms (the "experts"), and is charged one mistake whenever its prediction differs from the label. No probabilistic assumption is made on the sequence: the goal is a bound on the master's mistakes, valid for every sequence, in terms of the mistakes of the best pool member. The Weighted Majority Algorithm of Littlestone and Warmuth (Inform. and Comput. 108, 1994) achieves this for a finite pool of members with mistakes, where is the number of mistakes of member .
Many natural pools are infinite: all programs in an enumeration, all hypotheses of a countable class, all values of a discretised parameter. Section 4 of the paper asks whether a master can compete with every member of a countably infinite pool , making at most mistakes for every , while keeping only finitely many weights at any time. Running the Weighted Majority Algorithm on infinitely many weights would give such a bound, but cannot be implemented.
Timeline. Barzdin and Freivalds (1972, 1974) studied prediction of a sequence by an enumerable family of functions and gave an essentially optimal bound for the case of a pool containing a member consistent with the whole sequence ( below). Littlestone and Warmuth's earlier versions of the paper (1989) introduced an algorithm WMI for infinite pools; the journal version (1994) replaced it by , which matches the Barzdin–Freivalds bound when and a consistent member exists, and extends it to pools in which every member may err.
Fix a parameter with and put . Fix two real functions and on the positive integers with
is the initial weight of the pool member , and bounds the weight of the tail .
A sequence of trials gives, for each trial , the prediction of every pool member and a label . Member makes at most mistakes: for at most trials .
The master keeps an active pool and a weight for each active member. With the number of its own mistakes so far, let
Initially, and after each trial in which it errs, raises (starting from ) to the least value with ; a newly activated gets weight . In a trial it computes the active weight predicting and predicting ; it predicts if , predicts if , and may predict either otherwise. After a mistake, every active member that disagreed with the label has its weight multiplied by . The weights of the analysis are the current weight of an active member and for an inactive one.
The goal is Theorem 4.1, part 3 (p. 227). Let be the total number of mistakes of on the sequence.
If , then
and if and for some , then .
At the beginning of any trial, is the minimum with , where counts the mistakes made in prior trials.
After any initial sequence of trials in which mistakes have been made,
The result. The bound holds simultaneously for every pool member, so the master competes with the best member of an infinite pool, paying for the position of that member in the enumeration. With and (the paper's Corollary 4.1) this is mistakes, with an active pool that grows exponentially in the number of mistakes but is finite at every time. Different choices of trade the mistake bound against the growth of the active pool. The same analysis shows how the predictions can be computed from finite-precision approximations of the weights, which is the reason for the slack band in the prediction rule. Its case recovers the Barzdin–Freivalds bound.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist, and there is no formalization of the Weighted Majority Algorithm on infinite pools on Prove2Me. The work is to formalize the paper's proof: the size statement for the active pool, the inductive invariant for the total weight, and the final logarithmic bound. The definition of a run of , with free predictions in the slack band and lazily activated weights, is reusable for other lazy-activation algorithms on countable pools, and the paper's Corollaries 4.1–4.3 are direct instances once the goal is proved.
The ordinary Weighted Majority analysis tracks the total weight of the whole pool, which shrinks by the factor after each mistake. For that argument does not apply as is: the master only sees the active weights, and the inactive tail, whose weight is unknown to the algorithm and charged at its initial value, may vote with the label. The obvious bound on the tail is too weak if applied with a fixed slack; it must shrink with the number of mistakes at the right rate so that the accumulated overhead stays below a constant factor. The slack band in the prediction rule interacts with this: when the master errs inside the band, the active majority may not have been wrong by much, and the shrinkage factor must be recovered from the band's width. The factor is where these effects are balanced.
The pool is indexed by ℕ+ and trials by Fin T; false encodes the prediction , true the prediction . IsWMI2Run is a relation between the input sequence and the master's predictions, the weights and the active-pool sizes at every trial boundary ; a prediction inside the slack band is unconstrained, so the theorems hold for every run. Only active weights are constrained; the analysis uses omega, which counts inactive members at . The bound is any upper bound on the mistakes of . The tail hypothesis is stated with a tsum together with Summable W, and the milestone on the total weight asserts summability of in its conclusion, so it cannot hold through the value that Lean assigns to a divergent series. The infimum in the goal is stated as a bound for every , which is equivalent. Logarithms in the ratio are natural logarithms (the base cancels); the bound uses Real.logb 2. The paper requires and to be computable; this only makes the algorithm implementable, and the formal statements hold for arbitrary real functions with the stated analytic properties.
A statement for an algorithm whose runs do not exist would be vacuous; runs of exist for every sequence under the hypotheses (this has been checked locally in Lean), because and keep the active pool finite.
Needed infrastructure: finite sums over the active pool, tsum manipulations for sequences that agree with outside a finite set, and real logarithm inequalities. Contributions welcome: proofs of the two milestones and the goal, and the Corollaries 4.1–4.3 as follow-up statements.
This mission formalizes A. Erschler and T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155 (doi:10.1007/s00222-019-00922-0). Page and result numbers are those of arXiv:1802.09077v2.
The growth function of a group generated by a finite set counts the elements of word length at most . A group has polynomial growth, exponential growth, or intermediate growth, strictly between the two. Grigorchuk's groups were the first groups of intermediate growth, and for forty years the precise asymptotics of their growth was open, even for the most studied of them, the first Grigorchuk group . Erschler and Zheng determine its growth exponent:
where and is the positive root of . The upper bound was known; the new lower bound comes from random walks.
Timeline.
is the rooted binary tree, its vertices the finite words over and its boundary the infinite rays; automorphisms act on the right, . For a string , the Grigorchuk group is generated by certain automorphisms of , . The automorphism changes the first letter of a word, swapping the two subtrees of the root, while are defined as follows. They fix , and on a word each of them either changes the first letter of or does nothing, depending on the letter of the string: if , then and change it and does nothing; if , then and change it and does nothing; if , then and change it and does nothing. The string gives the first Grigorchuk group.
Assumption asks that every block contain or ; it implies that is periodic. is the sum of the entries of for three explicit matrices: the lengths of the words the substitutions of §2 produce.
A measure on a group is a function of total mass 1. A function is -harmonic if , the entropy is , and the Poisson boundary of is non-trivial when some bounded -harmonic function is not constant.
For every there is such that for every satisfying there is a non-degenerate symmetric probability on of finite entropy and non-trivial Poisson boundary with, writing for the word length,
and hence, for some depending on ,
The printed theorem has in place of ; that version is weaker and does not give the exponent.
The abstract's headline, that the volume exponent of the first Grigorchuk group is , is the last milestone, ErschlerZheng.hasVolumeExponent_firstString_alpha0: Theorem A combined with Bartholdi's upper bound.
The result. It answers the growth question for : the exponent is . It gives near-optimal lower bounds for every with satisfying , and its measures are the first examples on these groups of random walks with non-trivial Poisson boundary and power-law tails. The method, building a measure with non-trivial boundary and controlled tail and reading off a volume bound from entropy, applies beyond Grigorchuk groups.
Formalizing it. No machine-checked proof of these results exists; Mathlib has neither Grigorchuk groups nor Poisson boundaries. On this platform the mission builds on the published bundle of the first Grigorchuk group, Garrido_Grigorchuk, from the Garrido Amenable Groups III mission, and on Chou's word balls, Chou_Growth. The general Markov-chain inputs (Cheeger, Faber–Krahn and Nash inequalities, and off-diagonal heat-kernel bounds) are separate standalone theorems.
Lower bounds by anti-contraction of word lengths (Grigorchuk, Leonov, Bartholdi, Brieussel) stall well below . The entropy route needs a measure with non-trivial Poisson boundary, but on a group of subexponential growth every finitely supported symmetric measure has trivial boundary. The measure must therefore have heavy tails, and the lower bound it gives is only as good as its tail decay. The difficulty is to make the tails as light as allows while keeping the boundary non-trivial. That needs a non-homogeneous random walk on the Schreier graph of to be transient enough to fix the germ at , and heat-kernel bounds for jump processes that are not translation invariant.
Tree automorphisms are permutations of finite words (Garrido.BinaryTreeAut), acting on rays on the right by , so that . A measure is a function summed with tsum; it is symmetric when , and non-degenerate when its support generates as a semigroup. The Poisson boundary is non-trivial (HasNontrivialPoissonBoundary) when some bounded harmonic function is not constant on the submonoid generated by the support of ; for the non-degenerate measures of the goal this is the criterion of p. 2 (ErschlerZheng.hasNontrivialPoissonBoundary_iff_exists_bounded_isHarmonic_ne_of_isNondegenerate). Growth is evaluated at real radii. The definitions are in the bundles ErschlerZheng_Walks, ErschlerZheng_Germs, ErschlerZheng_Grigorchuk and ErschlerZheng_Construction.
Where a statement departs from the print, its milestone description says so: under Correction when the printed claim is false or undefined ((2.3), the substitutions on p. 15, Fact 3.5, the Gray code on p. 34, Fact 7.3, on p. 59, Lemmas 7.9, 7.17 and 7.21, Propositions 7.12 and 7.18, and the uniform digits on p. 55), and under Formalization note when it reads the print or strengthens it (Lemma 2.1, Proposition 7.19, Corollary 8.2, and the constants and ). The goal is Theorem 8.3 with the its proof gives, as above.
The goal is not trivial: its measure must be a non-degenerate symmetric probability on , and the growth bound is about the generating set itself.
Reusable beyond this mission: Grigorchuk groups for every with their substitutions, germ groupoids of group actions, entropy and the Poisson boundary of random walks.
What is left out. Theorems B and C, Corollary 8.4 and the other applications in §8 to general , which need the upper bounds of Bartholdi and Erschler (doi:10.5802/aif.2902); the side results of §§4–6 on the first Grigorchuk group (Theorem 5.7 and the critical constant of recurrence); the illustrative Examples 2.4 and 7.10; and the remarks and questions of §9. They are planned for a sequel mission.