Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).
The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).
A road's traffic stream is divided into subsidiary streams, indexed by . Stream has flow , the number of vehicles passing a point per unit time, and speed . Its concentration is , the number of vehicles occupying a unit road length. Total flow and concentration are and . The time frequency weights each stream by how often its vehicles pass a point. The space frequency weights it by the fraction of vehicles present along the road.
The time-mean speed is . The space-mean speed is . Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as , and the corresponding coefficient of variation as (equations (1)–(3), (7), pp. 328–331).
These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.
The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):
The subsidiary targets follow the paper's order. Equation (4) says for each stream, giving equation (5), . Appendix II then uses the centered identity and rewrites the time mean as . These three claims are the mission milestones. Equation (8) is included as a companion formulation:
The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).
The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.
The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes . The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).
Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.
The relation looks like a routine identity for weighted means, but the two weight systems are coupled through . One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.
The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.
Lean uses Fin C for the streams and real numbers for , , , both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require , , and for every . These requirements make , , and positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering .
The variance is defined from equation (7), . Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since and are explicit finite weights.
A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.
Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.
Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.
Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.
A committee of individuals chooses from a finite set of alternatives. A strong order on is a complete, transitive relation with no indifference between distinct alternatives; denotes strict preference. Let be the set of strong orders and the set of strict ballot sets .
Arrow's conditions on : CS—for all some gives ; IIA—if for all then ; NNR—raising an alternative in individual ballots, with the order of the other alternatives unchanged, never lowers against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for over yields .
For and there is a bijection
with for every and every .
The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.
On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.
The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation does this, but proving that is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.
A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.
A, ι with decidable equality; , throughout.ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.Set.range v = Set.univ.Equiv together with " underlies " for every . A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.Reusable beyond this mission: the strict-preference vocabulary (strong orders, , Arrow's conditions in the paper's form) and Gibbard's construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.
A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.
Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.
Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.
Timeline.
A committee of individuals ranks a finite set of alternatives. A weak order on is a complete, transitive relation, and reads " is preferred or indifferent to ". Its strict part is : and not . The weak orders form . A strong order is a weak order with no indifference between distinct alternatives, and the strong orders form . A ballot set is .
A social welfare function assigns to every ballot set a social ordering . A strict social welfare function is defined only on strong ballot sets and takes values in . For , is the set of -best elements of , and is the restriction of to .
A tie-breaking function maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order .
For , and any social welfare function on weak ballot sets,
The converse is false with indifference, so the goal is one-directional.
Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').
All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.
Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.
A and ι with decidable equality. = Fintype.card ι, = Fintype.card A, and , are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.
The method of multipliers (augmented Lagrangian method), proposed independently by Hestenes and Powell in 1969, solves a constrained optimization problem by a sequence of unconstrained minimizations of a penalized Lagrangian, updating a multiplier estimate between them. It became one of the standard algorithms of nonlinear programming and is the ancestor of ADMM and of the proximal-point view of dual methods. Rockafellar's 1973 paper (Math. Programming 5, 354–373) extended the method to inequality constraints with the penalty Lagrangian and reinterpreted it as unconstrained maximization of a smooth concave dual function . Its §4 shows that primal points recovered from any maximizing dual sequence are asymptotically minimizing; its §5, the subject of this mission, asks how fast they converge.
Timeline. 1969: Hestenes and Powell introduce multiplier methods for equality constraints. 1973: Rockafellar treats inequality constraints in the convex case through and its dual (this paper), and in the same year applies the multiplier method of Hestenes and Powell to convex programming (J. Optim. Theory Appl. 12). 1976: Rockafellar's "Augmented Lagrangians and applications of the proximal point algorithm in convex programming" (Math. Oper. Res. 1) gives the general convergence theory.
Let be convex and convex. The problem is
With and a parameter , the penalty Lagrangian is
and the dual problem maximizes over all ; is its supremum. A maximizing sequence is a sequence with . The dual method of Theorem 4.1 takes a bounded maximizing sequence and, for each , a point that minimizes to within a tolerance :
The standing assumptions of §5 concern a point that is an optimal solution of (P), near which are twice continuously differentiable, and a multiplier vector satisfying with the Kuhn–Tucker conditions (, , , and minimizes over ). With the active set and , they are: (i) for ; (ii) the , , are linearly independent; (iii) for every nonzero with for all .
Under the standing assumptions, with as in (4.7), if for some
then there is a constant with
No rate for is fixed: the statement compares the primal error with the dual error, whatever method produces the dual sequence.
Corollary 5.3 is the paper's answer to the practical question of how accurately each inner minimization must be done. A tolerance proportional to the current dual gap costs nothing in the order of convergence: the primal iterates then converge at least as fast as the dual ones. Since is with a negative definite Hessian near (Theorem 5.1 (v)), any locally linearly or superlinearly convergent unconstrained method applied to yields a primal sequence with the same rate. The estimates (5.15)–(5.17) are the quantitative bridge between inner accuracy, dual error and primal error, and reappear in later analyses of inexact augmented Lagrangian methods.
The results are proved in the paper (1973) and in textbook treatments; none of them has a machine-checked proof on this platform or in Mathlib. The mission produces a formal statement of the second-order theory of the penalty Lagrangian: the local smooth structure of and , the implicit minimizer map , and the rate comparison. Complete formal proofs of each milestone are the remaining work.
The obvious argument linearizes everything at , but is only globally: has a kink in its second derivative, so smoothness of must first be established on a neighborhood of , using complementary slackness and strict complementarity (i) to fix which branch of (2.4) each constraint follows. The sequence is not assumed to converge; localizing it into that neighborhood requires the uniform statement of Theorem 5.1 (i) (with chosen after ) and the uniqueness of and . The minimizer map then comes from the implicit function theorem applied to , and the formula for needs the derivative of the envelope .
EuclideanSpace ℝ (Fin n), multipliers in EuclideanSpace ℝ (Fin m); constraint indices are Fin m (0-based), and is a separate argument.ConvexOn ℝ X, an explicit hypothesis of every theorem, the paper's standing assumption of p. 358), and twice continuous differentiability only on a neighborhood of . Smoothness of and is always a conclusion, never a hypothesis.EReal, so (4.7), (5.2), (5.3) and (5.18) are differences in ; is explicit for the penalty Lagrangian, while is defined separately.Analysis/Calculus/Implicit), second derivatives of compositions, envelope differentiation, and the quadratic-growth estimates of a function with definite Hessian. Results on Hessian forms and on strict complementarity are reusable beyond this mission. Proofs of individual milestones are welcome independently.Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility than the close alone. Rogers and Satchell (1991) propose an estimator, , that is unbiased for whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.
Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at times. The sampled maximum falls short of the true maximum by an amount , and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,
enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.
Fix a volatility and a sampling mesh (in the paper ). For a level define
The factor is the probability that a Brownian bridge of duration and volatility climbs above level . The factor is a probability density on . Since and decreases continuously to , it is the survival function of a law on . This law is the paper's display (9).
A real random variable has distribution (9) if it is measurable and for every . In the paper, is the overshoot of the continuous maximum over the sampled maximum in the sampling interval to the left of the time at which is attained, and is the overshoot in the interval to the right. The paper then assumes (p. 508) that and are independent, each with distribution (9), and approximates by . Write .
In Lean, overshootSurvival σ h α is , HasOvershootLaw P σ h Z is " has distribution (9) under ", and constA, constB are and .
For and independent with distribution (9), the variables and are integrable, and
The goal combines milestones 2–5 through , which the paper uses in (11).
The result. The two identities are the coefficients of the corrected estimator (5): replacing and by and turns the high–low estimator into an equation whose positive root largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for and the correction has no concrete form.
Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes ). To our knowledge none of these identities has been formalized before.
The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights on an unbounded domain. The minimum of and couples two such integrals, and the resulting kernels and have to be integrated in closed form over the unit square. Matching and exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is .
(Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels : the formula is even in , and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. and are max and min.Integrable, or MemLp … 2 for second moments). The conditioning "" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "" in (13) is read as , as its first line shows. The integrals in (9) run over and .survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.Concentration of measure on the symmetric group concerns random permutations. A uniformly random permutation of objects appears in random assignment problems, in sampling without replacement, in the longest increasing subsequence and in the analysis of randomized algorithms. A tail bound for a function of a random permutation is useful when it does not require computing the function's distribution. The symmetric group is not a product space, so the inequalities proved for product spaces do not apply to it directly.
Timeline. B. Maurey [Maurey 1979] gave the first concentration inequality on , for distances that count the coordinates in which two permutations differ. Every permutation can be written uniquely as with , where is the transposition of and . Through this decomposition the Hamming bound (2.1.3) for product spaces carries over to . Milman and Schechtman present the result in their monograph [Milman–Schechtman 1986]. In Chapter 5 of his 1995 memoir Talagrand 1995, M. Talagrand proves the analogue on of his convex hull inequality (Theorem 4.1.1 of the memoir). In the author's words, it improves Maurey's result in the way that Theorem 4.1.1 improves Proposition 2.1.1.
is the group of permutations of and is the uniform probability on it. Fix and . A 0–1 vector is admissible if some agrees with at every coordinate where is zero:
is the convex hull of , and
is the squared convex distance from to . Unlike of Chapter 4, here is already squared. If , then and . A permutation that agrees with some element of outside coordinates has .
The proof uses three variants. counts coordinate twice, . , for , restricts that infimum to the face (Eq. (5.5)). drops coordinates and (Eq. (5.6)). In , and , with uniform probabilities and . is the transposition of and . The maps and send and , respectively, onto the permutations fixing , that is, onto .
For every and every ,
The constant is the paper's.
For every and every ,
Since , this pair implies Theorem 5.1.
The milestones are the numbered results of the induction step from to , in the order of the paper:
The result. Theorem 5.1 has the same form as Theorem 4.1.1. By Markov's inequality, . Any function on that is controlled by the convex distance therefore concentrates around its median with Gaussian tails whose scale does not depend on . Because the convex distance weighs coordinates by an arbitrary unit vector, this includes functions that are Lipschitz only in a weighted, configuration-dependent sense, which a Hamming-distance bound does not reach. This is the setting of random permutation problems such as the longest increasing subsequence and the assignment problem.
Formalizing it. The result has been proved since 1995. To the best of current knowledge none of Chapter 5 has a machine-checked proof, and the platform has no concentration statement on . This mission formalizes the statements and the induction of the chapter. Its reusable output is the convex distance on and the embedding of into through the blocks , .
sits inside through . If were the whole product, (5.2) would follow from Theorem 4.1.1. But is a very small subset of that product, and the uniform measure on is not a product measure. The decomposition into transpositions does give a product structure, but it is highly non-commutative. Coordinate distances in the decomposition do not match coordinate distances of the permutations, so it transfers only the weaker Hamming-type bound. The paper notes that a direct induction on for (5.2) itself apparently fails. The strengthened pair , is needed, and its two halves cross: is proved from , and from .
Equiv.Perm (Fin N), with indices from . In the point is Fin.last N, and composition is the group product, so is ρ * t N i.convexHull ℝ. The functionals , , and are infima of explicit sums of squares, so the sup norm on Fin N → ℝ plays no role. They take values in , so an empty infimum is and . The integrand is computed in EReal, so .ℝ≥0∞, so gives on both sides.Restricts ρ τ ( for ). and are the corresponding image sets.Contributions are welcome at every level: proofs of the deterministic lemmas, the bijections and their measure-transport facts, and the final Hölder–Lemma 4.1.3 step.
Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.
M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from to a set is measured by the number of coordinates in which differs from the best single point . The method of this chapter is the template for every later chapter of the memoir.
Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent , which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on .
Let be a probability space and an integer. Points of the product are written , and denotes the product probability. For a set and a point , the Hamming distance to is
the least number of coordinates that must be changed to move into ; it is when is empty. Given positive weights , the weighted Hamming distance replaces the count by .
Two families of constants appear. The first is
and the second, for and ,
extended by its limit ; one checks .
For every measurable , every and every ,
and, when , for every ,
The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.
The result. Inequality (2.2.7) shows that if is bounded below, the set of points at Hamming distance at least from has probability at most , with no assumption on or . Applied to for a function that changes by at most one when a coordinate changes, it gives concentration of around its median at scale . The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter is what makes the constant in (2.2.7) attainable rather than as in (2.1.3).
Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its -version) and the induction over as reusable components: every later chapter of the memoir (two-point space, penalties, points, convex hull distance) follows the same induction with a different one-coordinate lemma.
The bound does not follow from a union bound or from independence of coordinates, because depends on all coordinates jointly through an arbitrary set : changing one coordinate of changes by at most one, but which point of is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on or a constant factor in the exponent, and the constant in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its -version) are extremal problems over all measurable functions rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in and need not be measurable in general.
Fin N → Ω (0-based coordinates) and is Measure.pi (fun _ => μ). is never restricted to a finite or countable set.MeasurableSet A and the map carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.ℝ≥0∞), so ; integrals are lower Lebesgue integrals ∫⁻ in ; is EReal.exp; and are computed in , so makes the right-hand sides .Needed infrastructure: Fubini/Tonelli for Measure.pi split as , Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.
A recurring phenomenon in probability is concentration of measure: on a product of many probability spaces, a set of non-negligible measure has a neighbourhood that carries almost all of the mass. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces developed a systematic method — induction over the number of coordinates — that yields such statements for several different ways of measuring "how far" a point is from a set. These inequalities underlie sharp tail bounds for combinatorial optimization problems (bin packing, travelling salesman, longest increasing subsequence), for empirical processes, and for spin glasses, and Part II of the memoir develops several of these applications.
This mission formalizes Section 3 of the memoir, Control by q points. In Section 2 the distance from a point to a set counts the coordinates of that a single point of fails to reproduce (the Hamming distance). Section 3 lets several points cooperate: a coordinate of is captured if any one of chosen points agrees with there. The memoir's introduction (p. 79) presents Theorem 3.1.1 as a much simpler substitute for the isoperimetric inequality of Talagrand's earlier work on sums of independent Banach-space valued random variables (Talagrand, Ann. Probab. 17 (1989), 1546–1570), whose phenomenon "had a major impact in Probability in Banach spaces"; Chapter 13 of the memoir applies it to tails of such sums.
Let be a probability space, an integer, and the product probability on . Fix an integer ; this is a standing assumption throughout the section. For and points , coordinate of is captured if . For subsets the -point control is
the least number of coordinates of that remain uncaptured when one point is chosen in each . It is a whole number between and , or when some is empty.
For the sharpening of Section 3.2, given , the number is the unique with
For all subsets of ,
and in particular, for and ,
The constant is exact: the base of the exponential moment is itself, and the dimension does not appear.
Theorem 3.1.1 gives an exponential tail for whose rate is independent of the dimension and of the space . Applied with a set of probability at least , it says that outside an event of probability a random point agrees, on all but coordinates, with one of points of . This is the form in which the memoir (Chapter 13) bounds the tail of for independent Banach-space valued : taking , on most of the space the sum is controlled by points of up to the largest terms. Proposition 3.2.1 shows the base can be improved from to order for large , and the memoir's example on shows that this is sharp up to a universal constant in the base.
None of these results has a machine-checked proof. A formalization produces reusable Lean infrastructure for the induction method on product measures (sections and projections of subsets of , Fubini on Measure.pi, one-coordinate functional inequalities) that the other chapters of the memoir — the Hamming distance of Section 2, penalties of Section 3.3, the convex hull distance of Section 4 — share.
The inequality cannot be obtained by a union bound over choices of points or by a coordinate-wise martingale argument with bounded differences: both lose a factor depending on , while (3.1.2) has none. The induction on needs a functional inequality on one coordinate that holds uniformly over functions at once, with the exact constant , and the induction step has to pass through the projections of the sets — which, for measurable , need not be measurable. The exact constant in Proposition 3.2.1 additionally requires quantitative control of the root of (3.2.2) as .
Fin N → Ω (coordinates ), is Measure.pi (fun _ => μ) with [IsProbabilityMeasure μ], and is Fin.snoc x ω.ℕ∞, so an empty gives , not ; ; integrals are ∫⁻ and probabilities are in ℝ≥0∞, where . Hence the degenerate case makes the right sides infinite and cannot trivialize any statement.A complete development needs the induction step over Measure.pi on Fin (N+1) (splitting off the last coordinate), measurability of sections, and the one-coordinate inequalities. Proofs of any milestone are welcome, as are alternative proofs of the goal.
Concentration of measure in a product space asks how much of the space lies close to a set of non-negligible probability. In the simplest setting closeness is the Hamming distance: the number of coordinates of that cannot be matched by a point of . Talagrand's 1995 memoir in Publications Mathématiques de l'IHÉS develops a family of such inequalities with one method, induction over the number of coordinates, and applies them to combinatorial optimization, random graphs, spin glasses and sums of Banach-space-valued random vectors.
Counting a missed coordinate as ignores how far apart the two coordinate values are. Sections 2.4 and 2.5 of the memoir replace the unit cost by a penalty that depends on the values being matched. The resulting bounds have the shape of Bernstein's inequality: a Gaussian tail for moderate deviations, governed by the size of the penalty, and an exponential tail for large ones, governed by its sup norm. Theorem 2.4.1 is used again in Chapter 11 of the memoir, Corollary 2.4.4 in the study of the Sherrington–Kirkpatrick model in Chapter 12, and Theorem 2.5.1 in Section 11.5.
Let be a probability space, an integer, and the product probability on . A penalty is a measurable function with for every (the paper's standing assumption (2.4.2)). For and the penalized distance is
with . For off the diagonal this is the Hamming distance. Theorem 2.4.1 also uses the symmetrized penalty .
Section 2.5 measures the penalty against sets: for ,
the infimum being over the second variable, as in . The one-coordinate steps of the two inductions use the transforms (2.4.5) and with (2.5.7), for a function on .
For each measurable and each with ,
It is the most general exponential-moment bound of the section; every tail bound of Section 2.4 is derived from it.
The results. Theorem 2.4.1 turns a single integrability condition on the penalty into a bound on the exponential moment of the distance to any set, uniform over all sets of a given probability and factorized over coordinates. Chebyshev's inequality then gives the Bernstein-type tails of Corollaries 2.4.4 and 2.4.5, which hold for every set , not only for half-spaces or for sums of independent variables. Theorem 2.5.1 replaces exponential integrability of by condition (2.5.2) on the set functional , which is much weaker: when is itself a product of spaces, times the Hamming distance on satisfies (2.5.2) but not (2.4.12). Applied to blocks of coordinates, it shows that the coordinates a typical point misses in are concentrated in few blocks.
Formalizing them. All six results are proved in the memoir with short arguments. None of them has a machine-checked proof. A complete development would give a general-alphabet version of Talagrand's induction on product measures, written once for a cost function, that later chapters (the -point control, the convex-hull distance) also rely on.
The induction over requires a one-coordinate inequality whose right-hand side does not depend on the set. The difficulty is that the natural one-coordinate quantity, a section measure , can vanish on part of , so the function takes the value , and a statement proved for finite must be extended by truncation. The other subtle point is measure theoretic: need not be measurable even when is, and the paper's convention of ignoring measurability has to be matched by explicit hypotheses. In Section 2.5 the integrand in condition (2.5.2) may be non-measurable for the sets the proof uses, and Fubini's theorem is applied to the function .
Points of are functions Fin N → Ω (coordinates indexed from ), is Measure.pi (fun _ => μ) for a probability measure μ, and double integrals are over μ.prod μ. The penalty is a real function h : Ω → Ω → ℝ with explicit hypotheses , and joint measurability, in every statement. The distance is defined by (2.4.1) with the indicator and takes values in , so ; likewise and the transform (2.5.7). All integrals are Lebesgue integrals of -valued functions, , and when .
Measurability follows the paper's convention (pp. 81–82) as explicit hypotheses: is measurable and is measurable; in the propositions, and are measurable. Condition (2.5.2) is stated for every subset with the upper integral , which the paper prescribes when measurability fails. In Corollary 2.4.5, the quotients are computed in , so a quotient by , or is when its numerator is positive. The bound is when , as the printed factor intends. No statement is restricted to a finite or countable : restricting it would turn the general theorems into their finite-alphabet special cases. Dropping or defining the distance by a real infimum (whose value on the empty set is ) would change the theorems and is ruled out.
A complete development needs product measures on Fin (N+1) → Ω split as , sections of measurable sets, Tonelli's theorem, and the elementary convexity inequalities used in the proofs; the induction scaffold is reusable for the other distance functionals of the memoir. Proofs of any milestone are welcome, as are proofs of the extension of Proposition 2.4.2 to with values in , which the paper states without number on p. 92.
Processors in a distributed system may hold separate readings of a sensor, clock, or diagnostic result while some processors give misleading reports. The aim of interactive consistency is for every functioning processor to compute the same vector of reported values and to put each functioning processor's actual private value in its corresponding position. A shared vector can then be used for a common decision. Pease, Shostak, and Lamport formulated this problem for isolated processors communicating by two-party messages; their paper discusses clock synchronization, input stabilization, and diagnostic tests as concrete applications Pease–Shostak–Lamport 1980.
In the paper's oral-message model, faulty processors can invent reports about values they received from others. The other two missions in this series formalize the recursive majority procedure for and the matching impossibility result below that bound. Section 5 changes the communication assumption: a faulty processor may refuse to pass on a received value but cannot pass on an altered value as if it came from its original sender. Under that assumption, the authors give a procedure for every , including configurations outside the oral-message threshold Pease–Shostak–Lamport 1980, §§3–5.
Let be a finite set of processors and a type of private values. Each processor has a value . A scenario records the values reported along chains of processors. A string is read from receiver to originator: receives a report ultimately attributed to . A recorded value may be NIL, meaning that no authenticated value is available. The view available to receiver is its -scenario, the restriction ; it contains no report that begins with a different receiver.
Choose a set of nonfaulty processors. At most processors may be faulty, expressed as . An authenticated scenario consistent with obeys two conditions whenever the displayed strings are in the -level scenario. If and , the report made by nonfaulty relay is truthful: . For any prefix , a chain passing through nonfaulty carries either the value at or NIL: . The second condition allows omission by later relays while excluding a changed value falsely attributed to Pease–Shostak–Lamport 1980, p. 233.
For each receiver and originator , the procedure forms , the set of all non-NIL values in 's view on strings . The intermediate string has at most distinct letters, all in . Receiver records the sole value in when this set is a singleton; otherwise it records NIL. The resulting entries, one for each , form 's proposed consistency vector Pease–Shostak–Lamport 1980, p. 233.
The first milestone covers a nonfaulty originator : every nonfaulty receiver sees exactly its true value. The second covers a faulty originator: the set of non-NIL values seen by one nonfaulty receiver is contained in the set seen by another. The same statement with the receivers exchanged gives equality of their sets.
The goal is the procedure's full interactive-consistency guarantee, for every choice of and every authenticated scenario satisfying the conditions above:
Here is the optional value recorded by processor for processor . Both clauses matter: agreement alone could be achieved by always recording NIL, while correct nonfaulty entries alone would leave faulty entries inconsistent.
The result identifies an exact communication assumption under which the paper's oral-message bound no longer governs the procedure. Even if a faulty originator gives conflicting values, nonfaulty receivers finish with identical entries for that originator; if an originator is nonfaulty, they retain its actual value. The paper describes authenticators as a practical approximation to the assumption, but the guarantee here is a mathematical statement about scenarios satisfying its two conditions, not a probability claim about a cryptographic implementation Pease–Shostak–Lamport 1980, §5.
Formalizing this result supplies precise interfaces for authenticated scenario consistency, local views, the set , and the recording rule. The paper proves the result on pp. 233–234; this mission asks for a machine-checked proof of those statements in Lean. The scenario and local-view definitions can support later formalizations of message-passing protocols with truthful or omissible relays. Contributions that establish the two source milestones and the final guarantee, or develop reusable list and finite-set facts needed by them, are within scope.
The case of a faulty originator is the central difficulty. Its private value has no required relationship to what different nonfaulty receivers hear, so simply asserting that every receiver obtains the same direct report is unjustified. A faulty relay may also omit a report, which makes equality of raw scenario entries too strong. The target must compare sets of non-NIL values obtained along admissible relay chains. At the longest allowed chain, the length bound prevents adding another relay, and the number of faulty processors is needed to establish that an admissible nonfaulty relay occurs in the chain Pease–Shostak–Lamport 1980, p. 234.
Lean represents processors by a finite set P : Finset α, values by a type V, strings by List α, and NIL by none : Option V. A scenario is a total function from strings to optional values. Only strings over of length at most are constrained by authenticated consistency, matching the -level scenario that the procedure reads. A single-letter string has a non-NIL private value for every processor in . Conditions (i) and (ii) constrain nonfaulty relays only; condition (ii) allows either the original value or NIL for every prefix over , including an empty prefix.
The procedure is applied only to 's view , so it has no access to the full scenario or to . Its intermediate strings are repetition-free, exclude both and , and have length at most . The set contains values in , not NIL; an empty set and a set with multiple values both cause a NIL record. The formal theorem retains the printed condition, although it is not needed in the proof of the stated set relationships. It also covers , , and empty or singleton processor sets when their quantified conditions apply. These conventions rule out an always-NIL decision rule and the trivial rule that reads from outside the receiver's view.
The cryptographic maps , their message encodings, and the paper's assertion that practical authenticators can meet the assumption with arbitrarily high probability are outside scope. The formal result assumes the two exact authenticated-scenario conditions. A complete development needs finite-set cardinality and list facts, especially about distinct relay strings and bounded concatenation; these facts can be reused for other authenticated relay models.
A fault-tolerant system built from several processors must let its working processors act on the same data, even though some processors may have failed in ways nobody can predict: a failed processor may stop relaying information, relay something it invented, or tell different processors different things. Pease, Shostak and Lamport (J. ACM 27 (1980) 228–234) isolated the core question in the setting of the SIFT aircraft-control computer: each of processors holds a private value, at most processors are faulty, and processors communicate only by two-party messages. Can the nonfaulty processors each compute a vector of values, one entry per processor, such that all nonfaulty processors compute the same vector and the entry of each nonfaulty processor is its true private value? This requirement is called interactive consistency.
The paper answers with a sharp threshold. Interactive consistency can be achieved when (Section 3), and it cannot be achieved when , however many rounds of message exchange are allowed (Section 4). With unforgeable signatures it can be achieved for every (Section 5). The impossibility half is the origin of the "" bound that appears throughout Byzantine fault tolerance, popularised two years later as the Byzantine Generals Problem (Lamport, Shostak, Pease, ACM TOPLAS 4 (1982)). This mission is the impossibility theorem.
Timeline:
Let be a finite set of processors and a set of values. Write for the set of strings over (the empty string included) and for the nonempty strings. A string is read as a chain of reports: was told by that was told by that 's private value is the recorded value.
A scenario is a map . The value is processor 's private value, and is the value received for the chain . For , the -scenario is the restriction of to the strings beginning with : everything ever learns.
For a set of nonfaulty processors, is consistent with if
that is, every nonfaulty processor reports truthfully what it knows or hears. Faulty processors are unconstrained.
A decision family assigns to each a map that takes a -scenario and a processor and returns a value : the entry computes for . The family assures interactive consistency for faults if for every with and every scenario consistent with ,
In the Lean development these are InteractiveConsistency.Impossibility.ConsistentWith P N σ and AssuresIC P m F, with restrict σ p the -scenario.
If and
then no family assures interactive consistency for faults. Since scenarios are defined on strings of every length, no bound on the number of rounds is assumed.
The theorem shows that the algorithm of Section 3 is optimal in its fault tolerance: with oral messages, processors are not only sufficient but necessary. Every later lower bound for Byzantine agreement, Byzantine broadcast and approximate agreement with unauthenticated messages rests on this bound or a variant of its argument, and it is the reason replicated state machines tolerating Byzantine faults use replicas. It also explains why Section 5 needs authentication: the argument depends on faulty processors being able to relay fabricated values.
The result has been proved since 1980; what is open here is its formalization. Nothing on Prove2Me models message-passing agreement, and this mission states the theorem in the paper's own model: scenarios on unbounded strings and decision functions of a single -scenario. The mission produces a reusable vocabulary (scenarios, consistency, interactive consistency) and the explicit three-scenario construction.
The obvious attempt is to argue round by round about what a processor can know after rounds; with unboundedly many rounds this never terminates in a contradiction. The paper's argument instead needs three entire scenarios, each a legitimate behaviour for a different set of faulty processors, that two processors cannot tell apart from their own views. Writing these scenarios down so that consistency holds on every string while the indistinguishability survives on every string is the delicate part: the faulty set of each scenario must relay exactly the values that keep the other scenario's view intact, and one of the defining equations () looks like a misprint but is what the argument requires. The counting step is elementary but carries the hypothesis that the printed theorem leaves implicit.
Processors are a Finset P in a type with decidable equality; strings are lists read left to right ( is the head of the list); a scenario is a total function List α → V whose values on the empty list and on lists with a letter outside carry no meaning: every condition quantifies only over strings whose letters lie in . Decision functions have type α → (List α → V) → α → V and are applied only to the -scenario fun w => σ (p :: w), never to ; giving the whole scenario would make the problem trivial (output ). Consistency with constrains only relays by members of , and includes the empty . The quorum is written , which avoids truncated subtraction on . is the existence of two distinct values.
Explicit readings of the page:
A complete development needs only finite sets and lists from Mathlib. The vocabulary of p. 232 is shared with the other two missions of this series, Reaching Agreement in the Presence of Faults 1 (the algorithm for ) and 3 (authenticated messages, ), each of which defines it in its own namespace. Proofs of the milestones and of the goal are welcome, as is a proof of the goal by a different route.
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.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 studied in operations research "start afresh" at certain random instants: a single-server queue each time a customer arrives to find the server idle, an inventory system each time stock is replenished to its order level, a reliability system each time a failed unit is replaced. Between such instants the system may evolve in a complicated way, but its future after one of them does not depend on its past. W. L. Smith's 1955 paper Regenerative stochastic processes made this idea into a general theory. Its first main result, Theorem 2, says that the state probabilities of such a process converge as time grows, and gives the limit explicitly in terms of the behaviour of the process within one cycle and the law of the cycle length.
This limit theorem is the standard way of proving that a queue, an inventory or a reliability model has a limiting distribution and of computing it: one exhibits regeneration points and evaluates one cycle.
Timeline.
A general renewal process is a sequence of independent non-negative random variables in which have a common law , not concentrated at , with mean , and the delay has a law . The regeneration epochs are , and is the number of epochs in . The renewal measure is
so that . The law is periodic with period if all its mass sits on ; otherwise and is aperiodic. belongs to the class if some convolution power , , has a non-zero absolutely continuous component.
An equilibrium process consists of a process on a measurable state space , a class of measurable sets of states, a family of probability measures indexed by boundary conditions , and under each of them a general renewal process whose cycle law does not depend on and whose delay has law . For each there is a measurable function , depending on only, such that
where is the epoch of the last regeneration at or before . In words: once a regeneration has occurred, the chance of being in at time depends only on the time elapsed since the last one.
If the process is aperiodic () and the regeneration event is certain (), then for every and every satisfying one of the regularity conditions (iv) ( integrable and monotonic), (iv) ( and of locally bounded variation) or (iv) ( and ),
the limit being when .
The result. Theorem 2 reduces the long-run behaviour of a regenerative system to a one-cycle computation: the limiting probability of is the expected time spent in during a cycle divided by the expected cycle length. It underlies the existence of limiting distributions for the waiting time in the GI/G/1 queue, the number in system in many queueing networks, inventory levels under policies and the availability of repairable systems, and it is the continuous-time counterpart of the ergodic theorem for positive recurrent Markov chains. The paper's later sections apply it to semi-Markov processes.
Formalizing it. The results here are classical and proved; none is machine-checked. Mathlib has measure convolution and the strong law of large numbers but no renewal measure, no Blackwell or key renewal theorem, and no regenerative process. On Prove2Me only the discrete Erdős–Feller–Pollard renewal theorem for renewal sequences is proved. A completed mission supplies the continuous-time key renewal theorem in two forms, a reusable renewal-measure interface, and a general limit theorem for regenerative processes on which queueing and inventory results can be built.
The decomposition (3·4·3) is a direct consequence of independence and the renewal structure. The difficulty is the key renewal theorem. Blackwell's theorem controls on intervals of fixed length; passing from intervals to a general kernel requires the kernel to be directly Riemann integrable, which is why Theorem A asks for monotonicity and Theorem 2 lists three alternative regularity conditions. A merely integrable kernel tending to zero is not enough for a general aperiodic : may concentrate on a set where the kernel has tall narrow spikes. Theorem 1 removes monotonicity only for , through a Laplace-transform argument that needs Lemma A, the uniqueness theorem for Laplace transforms and the fact that the singular part of contributes nothing in the limit. Blackwell's theorem itself, for a non-lattice law with possibly infinite mean, is not in any library and is a substantial development of its own.
Laws are measures on carried by ; the distribution function is and . The mean is an extended non-negative real, so is a value; every statement with a treats and as separate cases rather than relying on a default value of division. Stieltjes integrals are integrals against the renewal measure over the closed interval . Aperiodicity is the lattice condition on , not a density condition. The delay law in Theorem A and Theorem 1 may have mass below one.
In the equilibrium process the conditional-probability representation is stated as the defining identity of conditional probability for every Borel set of last-regeneration epochs, every , every and every . The paper writes for the last regeneration epoch, although under its own indexing that symbol is the first epoch after ; the formalization uses the last epoch at or before . The delay is real-valued, so the regeneration event is certain (hypothesis (iii)); improper delays and cycles, which §3 of the paper also allows, are outside this mission.
A trivializing formalization would condition only on rather than on the epoch of the last regeneration, or fix globally; both are ruled out, and hypothesis (iv) is imposed separately for the one set of the conclusion.
Infrastructure needed: Blackwell's renewal theorem (non-lattice, finite or infinite mean), direct Riemann integrability, Laplace–Stieltjes transforms of functions of bounded variation and their uniqueness. All of these are reusable well beyond this paper; contributions of any of them are welcome. The convolution power and the Laplace–Stieltjes transform are taken from the published definition QueueingFundamentals.MG1.transforms.
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.
A random walk on the integers in which the probability of stepping right depends on the current site is the simplest model of motion through a disordered medium: a particle diffusing in a crystal with impurities, a molecule moving along a heterogeneous polymer, or a gene frequency drifting under fluctuating selection. When the site-dependent probabilities are themselves drawn at random, the result is a random walk in a random environment (RWRE). Fred Solomon's 1975 paper [Solomon 1975] gave the first rigorous analysis of this model on with independent, identically distributed site probabilities, and its recurrence criterion opened the subject now surveyed in [Zeitouni 2004].
Timeline. Chung [Chung 1960, pp. 65–71] gave the hitting probabilities and the recurrence/transience criterion for a nearest-neighbour chain on with fixed, site-dependent transition probabilities. Fluctuation theory, as presented in Chung's A Course in Probability Theory [Chung 1968, Ch. 8], characterises when a sum of i.i.d. random variables drifts to , to , or oscillates, through the series and . Solomon (1975) combined the two to classify the RWRE on , and also computed its speed and exhibited sub-ballistic and non-Gaussian behaviour. Kesten, Kozlov and Spitzer (1975) [KKS 1975] identified stable limit laws in the transient sub-ballistic regime, and Sinai (1982) [Sinai 1982] found the scaling of the recurrent case.
Let be independent, identically distributed random variables with values in . Given a fixed sequence in (an environment), the chain on jumps from to with probability and to with probability . The random walk in a random environment is the process obtained by first drawing and then running from ; jointly,
The walk is a Markov chain given the environment, but not after averaging over it. Define
and, for a fixed environment, the hitting probability . The quantity is defined when the expectation of the positive or of the negative part of is finite.
Assume is not almost surely constant and either for all or for all . Then
and if both series diverge, , all almost surely. When is defined, the three cases are exactly , , .
Theorem (0.1): almost-sure properties of the walk in almost every fixed environment transfer to the RWRE. Lemma (1.1)(i)–(ii): the hitting probabilities in a fixed environment with , as ratios of series in . Lemma (1.5): in a fixed environment, and decide transience to , to , or recurrence. Lemma (1.6): fluctuation theory for i.i.d. sums, including the summability of . Two claims from the proof of (1.7) (p. 5): the boundary cases where equals or with positive probability, and the equivalence for . A companion item asserts that the RWRE exists for every law of on .
The theorem classifies the long-run behaviour of the RWRE on by a condition on the law of a single site variable, with no moment assumption. It shows that the averaged drift is not the right quantity: a walk can be recurrent or transient to the left while its average step is positive, because the criterion involves , a geometric rather than arithmetic mean. The criterion is the starting point for the speed law (Theorem (1.16) of the same paper), for the limit laws of Kesten–Kozlov–Spitzer and Sinai, and for the large-deviation theory of RWRE.
Solomon's results are proved; none of them, nor the fixed-environment criterion of Chung, is formalized in Lean. This mission produces machine-checked statements of the full trichotomy including the boundary cases , of the classical hitting-probability formulas for birth–death chains on , and of the fluctuation-theory criterion with infinite-valued expectations allowed.
The naive approach applies the law of large numbers to ; it fails because the increments are neither independent nor stationary once the environment is averaged out. The argument must instead pass through a fixed environment, where the criterion of Lemma (1.5) involves the full random series and , and then decide when these series converge almost surely. That step requires fluctuation theory for , a random walk whose steps may be infinite and may have no mean. In Lean, the main missing infrastructure is the fluctuation-theory criterion , which Mathlib does not have, and the transfer from quenched to annealed statements for a process defined only through its cylinder laws.
Everything lives in the namespace SolomonRWRE.Recurrence. The fixed-environment chain is IsChainInEnv P a i X, specified by its cylinder probabilities. The RWRE is IsRWRE P α X on an arbitrary probability space: measurable with values in at every outcome, iIndepFun α P, identically distributed, and the joint cylinder law above. , , and all series are in (ℝ≥0∞), so "" and "" are literal; series over are indexed by in Lean. and are extended reals, is the difference of two lower Lebesgue integrals, and "defined" means one of them is finite. Recurrence is always stated in the paper's "in fact" form: and . "Correspond respectively" is formalized as three equivalences between the series conditions and the sign conditions.
Two trivializing formalizations are ruled out. Without nondegeneracy () both series vanish and (i), (ii) would contradict each other; the hypothesis is part of every statement that needs it. A cylinder law that cannot be met would make every theorem vacuous; a sorry-free check confirms that the environment with satisfies IsRWRE, and the companion item asserts existence for every law of . The page's alternative " for all or for all " is kept, since a single range would let change .
Needed infrastructure: hitting probabilities of birth–death chains (reusable for any nearest-neighbour chain), the fluctuation-theory criterion for i.i.d. sums with extended values (reusable throughout applied probability), and a quenched-to-annealed transfer lemma. Contributions to any of these 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.
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.
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.
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)).
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.