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.
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 linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.
A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.
Fix and write a linear program in the homogeneous form (6)
where is a real matrix and is componentwise. Every linear program can be put in this form. The matrix is uncertain: it is only known to lie in an uncertainty set of matrices. Each gives an instance with feasible set and optimal value ; the family of instances is . The robust counterpart (7) is
and its optimal value is . Since does not change when is replaced by its closed convex hull, the paper assumes throughout that is convex and closed.
Let be the set of all realizations of the -th row, the projection of onto the data of the -th constraint. The uncertainty is constraint-wise if : the rows vary independently. The Boundedness Assumption asks for a convex compact set that contains the feasible set of every instance.
If the uncertainty is constraint-wise and the Boundedness Assumption holds, then
The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of in every instance's feasible set; the reduction of the semi-infinite system (8) on to a finite subsystem; the statement that the finite system (10) then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.
The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: is unchanged under passing to the closed convex hull of (§2.1) or to the product of its projections (§2.2).
Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.
The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of .
The robust counterpart has a continuum of constraints, one for each , so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in ; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in , which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and is 0 ≤ A *ᵥ x in the componentwise order. The -th row of is A i and is a ⬝ᵥ x. The projections are the images of under , not free sets, and constraint-wise uncertainty is the inclusion (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of , as on the page.
Optimal values are infima: is the greatest lower bound (IsGLB) of over , and (9) states that is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.
The goal carries the paper's standing assumption that is convex and closed, and one disclosed addition: is nonempty. The paper takes this for granted; without it part (i) fails for and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets are arbitrary sets with , or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.
A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.
Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid , and proves that no real matrix corresponds to it.
The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line , and the regular matroids by three excluded minors, , and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over .
Timeline:
Let be an matrix with columns . For a set of columns, let be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid on with rank function : the matroid of . A matroid corresponds to if it is the matroid of , with elements matched to columns.
A circuit of a matroid is a minimal dependent set. For a circuit of the matroid of , there are numbers with for every row , and exactly for ; the set of such vectors is written when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix of , determined up to nonzero factors on its rows.
A fundamental set of circuits of a matroid with nullity ( the number of elements) is a family of circuits with such that the elements can be ordered with and for ; it is strict if for every .
The matroid of §16 has elements ; its bases (maximal independent sets) are all three-element sets except
The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.
The result. The theorem separates the abstract notion of matroid from linear dependence over : some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.
Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over in Lean is known to the curators.
The obvious attempt is a direct search: suppose a real matrix has as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that in , since over a field of characteristic 2 the statement is false (milestone 8).
Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of " means: ground set everything, and the rank M.eRk N of every finite set of columns equals Matrix.rank of the column submatrix.Fin t with , and determinants are of square submatrices in the paper's row and column order.Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.
Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.
Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.
A matroid on elements is given by its independent sets; its circuits are its minimal dependent sets, its rank is the size of a base, and its nullity is . Here is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.
Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle . A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.
With , a family is a strict fundamental set of circuits with respect to if , each is a circuit, and contains but no other .
For a matrix over the integers mod 2 with columns , columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to has the column indices as elements and these independent sets.
Let satisfy (C*), with elements and base . For every matrix mod 2 (any number of rows) whose columns are independent mod 2,
Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).
The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.
Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.
Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.
Matroid (Fin (r + q)) with ground set Set.univ; Whitney's is k - 1, his is the range of Fin.castAdd q, and is Fin.natAdd r (i - 1). Writing removes natural-number subtraction; is not a free parameter, since is required to be a base.sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.Matrix (Fin m) (Fin n) (ZMod 2) with any ; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.
Many problems in imaging, signal processing and statistics are convex minimizations of the form
where is smooth, and are nonsmooth but have computable proximity operators, and is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only , the proximity operators of and , and applications of and , without ever inverting or computing the proximity operator of .
Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.
Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term , relaxation and errors (Theorem 3.1), and, for , proved weak convergence for relaxation parameters up to (Theorem 3.2), the result of this mission.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions . For , the conjugate is , the proximity operator is , and the subdifferential is .
Fix , and . The primal–dual inclusion (6) asks for with
then minimizes and solves the dual problem. The paper assumes this inclusion has a solution.
Given , relaxation parameters and error terms , , Algorithm 3.1 iterates, from any ,
Algorithm 3.2 exchanges the roles: it computes from first, then using .
Suppose and , , and
Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution of (6) with and weakly.
Remark 3.2 (the goal with affine, , instead of ) and Theorem 5.2 (the version with composite terms and condition ).
The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation and summable errors, in arbitrary real Hilbert spaces. Over-relaxation often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.
Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.
The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where , strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.
The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in are EReal-valued, with the published IsProperClosedConvex. The conjugate is an EReal supremum, so can take the value . Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product with the inner product is WithLp 2 (X × Y). Weak convergence is for all . "" means partial sums tend to , and "" means summability of a nonnegative series.
Standing assumptions are hypotheses: , and (6) has a solution. With the smoothness assumption on is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit is chosen after the run.
The condition is strict, , and relaxation is open, . A goal quantifying over no run, assuming the limit exists, or fixing before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract rank function that behaves like the rank of a set of vectors. Part II of the paper opens with the decomposition of a matroid into components. The question it answers is basic to every later use of matroids: when does a matroid split into independent pieces, and how can the pieces be recognized?
For the matroid of a graph (elements = edges, rank = number of vertices minus number of connected pieces spanned) the components are the 2-connected blocks of the graph, and Whitney's theorem recovers the classical fact that two edges lie in a common block exactly when they lie on a common cycle. Whitney had studied separability of graphs in Non-separable and planar graphs (1932), and footnote 11 of the 1935 paper points out that the theorem identifies König's "Glieder" of a graph with components. Matroid connectivity built on this notion runs through later structure theory: Tutte's higher connectivity, Seymour's decomposition of regular matroids, and the matroid minors project all start from the separation of a matroid into components.
A matroid on a finite ground set is given here by Mathlib's Matroid structure, with rank function for (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset as a matroid in its own right, a submatroid, with the rank function of restricted to subsets of . For sets he writes for the union, for the number of elements of , and
for the nullity of .
Rank is subadditive: . A submatroid is separable if it can be divided into two disjoint groups , each containing at least one element, with
and non-separable otherwise. Every single element is non-separable. A component of is a maximal non-separable part of : a nonempty non-separable set contained in no strictly larger non-separable subset of .
For two distinct elements of ,
Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.
The result. Theorem 19 makes the component decomposition computable from circuits alone and shows that "lying on a common circuit" is an equivalence relation on distinct elements, a fact that is not evident from the circuit axioms. Theorem 18 adds that the decomposition is the unique one with additive rank. Together they are the starting point of matroid connectivity: the direct-sum decomposition of a matroid, the reduction of many matroid problems (representability, duality of components, Whitney's own Theorems 24–26 on duals of components) to the connected case, and the higher-connectivity theory that followed.
Formalizing it. The results are classical and proved in the paper; nothing here is open. To our knowledge Mathlib at the pinned revision has no notion of matroid connectivity or components, so this mission produces the first machine-checked development of Whitney's §10: the rank-based definition of separability, the disjoint decomposition into components, the circuit characterization, and the ear-type construction of non-separable matroids (Theorem 17). These are reusable for any later formalization of matroid connectivity, including Whitney's results on duals of components.
The two directions of Theorem 19 rest on different machinery. That two elements on a common circuit lie in one component follows from the rank theory (Theorems 13 and 16). The converse is the substantial direction: a component is defined by the failure of rank additivity, which only says that every division of the component is crossed by some circuit (Lemma 9). It does not directly give one circuit through two prescribed elements. Combining circuits that cross different divisions into a single circuit through both and requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from to gives a connected chain of circuits, not one circuit.
Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid " are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid .ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in as the number of elements minus the rank.IsSeparable M X requires two nonempty, disjoint groups with union and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds M.E. IsComponent M K requires nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.Matroid.IsCircuit.M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside (Matroid.restrict_isCircuit_iff), and finiteness arguments for maximal non-separable sets. Proofs of the milestones, alternative proofs of the goal, and lemmas relating components to Mathlib's direct sums of matroids are all welcome.Many problems in imaging, signal processing and statistics take the form
where and are convex functions whose proximity operators can be computed cheaply, is a linear operator such as a finite-difference gradient, and is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because is generally not proximable even when is, practical methods split the problem so that each step uses only , , and , without inverting any operator.
L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming , and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with , the iterates converge under the step-size condition , equality included. Equality matters in practice: one can set and tune a single parameter, as in the Douglas–Rachford method.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions , and let , . The Fenchel conjugate is , the proximity operator is , and the subdifferential is .
The primal–dual inclusion (6) asks for with
A solution gives a minimiser of the primal problem and a solution of its dual.
Algorithm 3.1 chooses , , relaxation parameters , error terms and an initial estimate , then iterates
Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses . Section 5 extends both to (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).
Let , be finite-dimensional, , , and assume (6) has a solution. If
then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, converges to a solution of (6).
With the operator (20) and the error-free step of Algorithm 3.1:
Remark 3.2 (Theorem 3.3 with affine, i.e. in (2)) and Theorem 5.3 (the analogue for composite terms, with (i) replaced by ) are included as draft theorems.
Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size . It covers relaxation parameters up to and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.
None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.
The usual proof treats the iteration as a proximal-point or forward–backward step in the space with the inner product . That argument needs strictly positive, which is exactly what fails when : then has a nontrivial kernel, is only a seminorm, and weak convergence in the -geometry says nothing about the components of in . The proof replaces the iteration by its "shadow" on , uses that factors through , and recovers the full iterates through continuity of and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.
Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in take values in EReal and satisfy the published predicate IsProperClosedConvex (never , finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps , satisfying the published minimisation predicate IsProx for and ; such maps exist and are unique for functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. "" for a series is divergence of its partial sums, "" is summability of a nonnegative series, and convergence in the goal is norm convergence.
The standing assumptions of pp. 3–4 are hypotheses: , and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators and are plain maps on . The projector is not built: "" is stated as "", which is equivalent because is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.
The strict inequality would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps . Weak convergence in place of norm convergence, an chosen after , or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.
Useful infrastructure includes: firm nonexpansiveness of for EReal-valued functions; -ness of the conjugate and Moreau's identity; maximal monotonicity of plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Perfect graphs are the graphs for which colouring and clique problems behave as linear programs do: the stable-set polytope of a perfect graph is described by its clique inequalities, so maximum weight stable sets and minimum colourings can be computed in polynomial time (Grötschel, Lovász & Schrijver 1988). In 1961 Berge conjectured that a graph is perfect exactly when it has no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006).
The proof is a decomposition theorem: every Berge graph is basic or admits one of a few decompositions. The paper reaches it through twelve steps, 1.8.1–1.8.12 (p. 59), each handling graphs that contain a certain configuration. This mission poses step 1.8.3, Theorem 9.6. It handles Berge graphs that contain the line graph of a bipartite subdivision of , all such line graphs being degenerate.
All graphs are finite and simple. denotes the complement of . A hole is an induced cycle of length at least , an antihole is a hole of , and is Berge if all its holes and antiholes have even length. A path is always an induced path, and an antipath is a path of . The length of either is its number of edges.
Line graphs and appearances. The line graph has vertex set , two edges adjacent when they share an end. is a subdivision of if it arises from by replacing every edge by a track (a path, not necessarily induced), these tracks disjoint except for their ends. appears in if, for some bipartite subdivision of , is isomorphic to an induced subgraph of ; is then an appearance of . For the appearance is degenerate if some 4-cycle of contains the four vertices of degree three. A -enlargement is a 3-connected graph with a proper subgraph isomorphic to a subdivision of . An appearance is overshadowed if some branch of of odd length , with ends , has a vertex of nonadjacent to at most one edge at and at most one edge at .
Knots and striations. A knot is formed by two paths with ends and two antipaths with ends . They are pairwise disjoint and of length , is anticomplete to , is complete to , and the ends are joined in a prescribed twisted pattern (pp. 107–108). A degenerate appearance of is a knot. A strip is a family of paths ("rungs") from to through ; an antistrip is a strip of . A striation is made of strips and antistrips. All rungs and antirungs are odd, the strips are pairwise anticomplete, the antistrips pairwise complete, and every strip is parallel or co-parallel to every antistrip, with enough "twists" between them (p. 112). A striation is maximal if no striation has a strictly larger vertex set. The paper defines when a set of vertices is local for a knot or striation and when it resolves one.
Outcomes. A double split graph has its vertices partitioned into () and (). Each is an edge and each a nonedge, distinct pairs are anticomplete and distinct pairs complete to each other, and every and are joined by exactly two disjoint edges. A skew partition of has disconnected and disconnected. It is balanced if no odd path joins nonadjacent vertices of through and no odd antipath joins adjacent vertices of through . A proper 2-join is a partition of whose only cross edges are complete joins – and –, with the side conditions of p. 53.
Let be Berge, with every appearance of in and in degenerate and no induced subgraph of isomorphic to . Then
9.3–9.5 assume that no -enlargement appears in or and that no appearance of in or is overshadowed. An optional, non-milestone item poses 9.7 (p. 118): a Berge graph with an appearance of is a line graph or the complement of one, a double split graph, or admits a proper 2-join (in or ) or a balanced skew partition.
9.6 is the step of the proof that produces double split graphs, one of the five basic classes. In the main argument it follows step 1.8.1 (5.1, nondegenerate appearances of ) and is combined with it in 9.7. Through 9.7 it gives the first half of 13.5: every recalcitrant graph belongs to the class and so contains no appearance of in or .
The theorem has been proved since 2006. We know of no machine-checked proof of the strong perfect graph theorem or of any of its steps. Mathlib has line graphs and graph embeddings but no subdivisions, appearances or decompositions of Berge graphs. This mission produces a faithful Lean statement of step 1.8.3 and of the four lemmas its proof rests on, together with Lean definitions of knots, strips and striations.
The obvious approach would take a degenerate appearance of and study how each remaining vertex attaches to it, as §§5–6 do for nondegenerate appearances. This does not close. A degenerate appearance can be read as a line graph or as its complement, so the analysis of a vertex in and in has to be run at once. Single vertices can also be absorbed into larger structures that the line-graph analysis does not see. The proof grows the appearance to a maximal striation and classifies attachments to it, and the hard steps are 9.4 and 9.5. Their proofs need 9.3 in every case, and they use maximality to refute configurations that would let the striation grow.
Graphs are SimpleGraph V on a Fintype with decidable equality. Every object is defined as on the page, in the namespace StrongPerfectGraph.DoubleSplit.
SimpleGraph.lineGraph; "isomorphic to an induced subgraph" is an induced embedding ↪g. Subdivisions and enlargements range over graphs on Fin k.Fin m, Fin n.Dropping the bars of the complement would make the theorem false or vacuous. So would reading "path" as a non-induced path, or encoding a decomposition so that it always exists. The statements use the complement explicitly, induced paths throughout, and the full definitions of p. 53–54.
The proof of 9.6 also uses results of the same paper that are posed in other missions of this series. These are 2.1, 2.2, 4.1 and 4.2, posed in mission II (skew partitions), and 5.3, 5.8, 6.1 and 7.5, posed in mission III (line graphs). They are not posed again here. The bridge 9.2 between knots and line graphs, whose proof the paper omits as obvious, is not posed either. Proofs of 9.1, of 9.3, and reusable lemmas about knots and striations are welcome.
In 1935 Hassler Whitney asked which properties of linear dependence among the columns of a matrix can be stated without reference to the matrix at all. His answer, On the Abstract Properties of Linear Dependence (American Journal of Mathematics 57, 1935), introduced the matroid: a finite set together with a rank function obeying three short postulates. The notion now underlies combinatorial optimization (the greedy algorithm is optimal exactly on matroids, and matroid intersection and partition generalize bipartite matching and arborescence packing), graph theory (graphic and cographic matroids), coding theory and the study of linear representations over finite fields.
A defining feature of the subject is that the same structure can be axiomatized in several apparently unrelated ways: by rank, by independent sets, by bases, by circuits. Each axiom system is convenient for different arguments, and passing between them, a so-called cryptomorphism, is routine in practice. Whitney's paper is where these equivalences first appear. Part I, §§2–4 and §6 (pp. 510–514), derives the basic properties of rank from the rank postulates, deduces from them the postulates for independent sets, and shows that the two systems are equivalent. This mission formalizes that first equivalence.
Let be a finite set of elements . Following Whitney, write for , for the union and for the intersection of subsets; is the number of elements of .
A rank system is a function on the subsets of satisfying
The nullity of is , and is independent when . The increment of (3.1) is , written when .
An independence system is a predicate "independent" on the subsets of satisfying
From an independence system one recovers a rank by letting be the number of elements in a largest independent subset of . In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.
Both translations and both round trips are part of the goal: Whitney's conclusion is not only that each system implies the other but that "the definitions of the rank and the independence or dependence of any subset of agree under the two systems".
The equivalence makes the rank function and the family of independent sets two descriptions of one object. Every later result of Whitney's paper, and of matroid theory generally, moves between them without comment: the circuit postulates of §5 and §8, the base postulates of §7 and the duality of §§11–13 are all phrased through rank or independence as convenient. Theorem 3 is the submodularity of rank, the property that connects matroids to submodular function minimization and polymatroids; here it is derived from the purely local postulates (R₁)–(R₃), which constrain the rank only under the addition of one or two elements.
On the formal side, Mathlib defines Matroid through independent sets (with constructors from other axiom systems) and proves submodularity of its rank; the platform has submodularity for Mathlib matroids (FamousTheorems.matroid_rank_submodular_7a). Neither starts from Whitney's local rank postulates. What this mission adds is a machine-checked derivation of the global properties of rank from (R₁)–(R₃) and of Whitney's original equivalence, stated for his own postulates, so that the later missions of this series, which work from the same postulates, rest on a verified foundation. The result itself has been settled since 1935; the open work is the formal proof.
The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound follow by adding elements one at a time, but the submodular inequality relates arbitrary sets, and nothing in (R₃) mentions more than two new elements. The gap between the local and the global statement is the substance of Lemmas 3, 4 and Theorem 3, and the deduction of (I₂) depends on it.
In the converse direction the rank is defined as a maximum over independent subsets, while (I₂) only augments a set from an independent set with exactly one element more; (R₃) for the derived rank is a statement about three sets that are not given in that form. The round trips are where the two halves meet, and each depends on the global properties of the first half rather than on the postulates alone.
Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid is the whole type. Ranks, nullities and increments take values in ℤ, so differences never truncate; Whitney allows any number, but (R₁) and (R₂) force nonnegative integers. Postulate (I₂) is stated in Whitney's form with N'.card = N.card + 1, not the general augmentation for . Postulates (R₂), (R₃) keep their hypotheses . Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets ; Lemma 1's monotonicity for arbitrary , the form in which the paper uses it. rankOfIndep is the supremum of cardinalities over the independent members of the powerset.
The paper takes for granted that the empty set is independent in system (I). Without that hypothesis, the predicate declaring nothing independent satisfies (I₁) and (I₂) vacuously, the supremum defining the rank returns , and the round trip fails; the goal therefore assumes independent in part 2 and proves it in part 1. A formalization in terms of Mathlib's Matroid would make the goal a restatement of library facts, since Mathlib's matroids are independence systems by construction; the goal is deliberately about the postulates as predicates on functions and on families of sets.
A complete development needs only finite set combinatorics (Finset.card, induction on finite sets, Finset.sup). The derived lemmas (monotonicity, submodularity, (I₂)) are reusable for any later work from Whitney's rank postulates, including the circuit-postulate equivalence of the companion mission. A bridge from rank systems to Mathlib's Matroid (via IndepMatroid.ofFinset) would be a welcome addition but is not part of the goal. Proofs of the milestones in any order are welcome; Theorem 3 and the §4 deduction are the natural first targets.
Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.htmlMany convex optimization models combine a smooth loss, a nonsmooth penalty whose proximity operator is easy to compute, and a second penalty applied after a linear map. Imaging models, for example, often place a data-fitting term on the image and a regularizer on its transformed coefficients. The resulting objective has the form . Condat's primal–dual method evaluates the smooth gradient and two proximity operators separately, without requiring a proximity operator for the composite . Condat, 2013 establishes weak convergence with relaxation and summably weighted computational errors. This mission targets its main positive-smoothness theorem, Theorem 3.1, in the final author's version.
The theorem matters when a computed gradient or proximal point is inexact, as is common when a proximal subproblem is itself solved numerically. Its conditions account for these errors directly rather than treating the displayed algorithm as exact. It also gives one parameter regime for two orders of updating the primal and dual variables. These two algorithms share an objective and a solution inclusion, but have distinct recursions.
Let and be real Hilbert spaces and let be bounded linear, with adjoint . The smooth term is convex and differentiable. Its gradient is -Lipschitz when for all . The nonsmooth terms and are proper, lower semicontinuous, convex functions with values in . Such functions form the class . An infinite value may encode a constraint.
For a convex function , its proximity operator minimizes over , where . The Fenchel conjugate is . A subgradient obeys for every . The sought primal–dual solution satisfies
Algorithms 3.1 and 3.2 maintain sequences and . Algorithm 3.1 updates the primal proximity step before the dual one; Algorithm 3.2 reverses that order. Each uses positive step sizes , positive relaxation weights , and errors , and in the gradient and the two proximal evaluations. Their full recursions are part of the Lean setting, so a run is determined by its initial pair. The paper specifies the problem in §2 and both algorithms in §3.
The goal is Theorem 3.1 on p. 5. Suppose , the primal–dual solution set is nonempty, and . Set
For , the theorem assumes
Under these conditions, both sequences of each algorithm converge weakly to the components of a primal–dual solution. The solution may depend on the initial pair and on the run. The milestone list includes Lemmas 4.1 and 4.3–4.5, the strict positivity claim for the block operator , estimate (29), and the error-free optimality inclusions (22) and (44), ordered as preliminary results followed by the two algorithm-specific claims. These targets match the results stated in §4 of the source version.
The result supplies a convergence guarantee for a composite objective under an explicit coupling condition on , , and . It permits relaxation weights that vary with and errors that are summable only after weighting by those same relaxation values. The dual conclusion is substantive: convergence of the primal sequence alone would not give convergence of the dual certificate produced by the algorithm. The weak topology is appropriate in general Hilbert spaces; norm convergence would assert more than the paper proves.
The theorem is proved in the 2013 paper. The present formalization task is to give its statement and the selected operator lemmas machine-checked proofs in Lean. Related platform definitions for proximal maps, monotone operators, nonexpansive maps, subgradients and weak convergence already exist; the paper-specific convergence theorem and its selected milestones are new targets in this proposal. The resulting definitions and abstract Lemmas 4.1, 4.3–4.5 can be reused in later operator-splitting developments.
The displayed recursions involve three errors, two proximal evaluations, a linear map and its adjoint, and two different update orders. A direct estimate on does not by itself control the coupled dual variable, while a bound on only the combined objective value would not establish weak convergence of either iterate. The relaxation condition permits weights without a fixed positive lower bound, so a convergence argument cannot replace the stated divergent series by a simpler constant-step assumption. The abstract lemmas must also retain the endpoints and present in the source.
Lean uses complete real inner-product spaces for and , a continuous linear map for , and EReal for , and their conjugates. The conjugate supremum is taken in EReal. The paper's class and proximity maps use published definitions; the latter are parameters constrained to be the actual proximal minimizers. Positive step sizes and proper closed convex data ensure such maps exist and are unique. The subgradient predicate explicitly requires a finite value at the base point; this follows from the source's properness assumptions when a subgradient exists.
Both algorithms are represented by recursion predicates on every natural-number index, with all error terms present. The goal quantifies over every run and chooses its weak limit afterwards. Divergence to means finite partial sums tend to atTop; a finite weighted error sum means the corresponding nonnegative real sequence is summable. These choices prevent a default value of an infinite sum from satisfying the hypotheses. The nonempty solution set is an explicit standing assumption from p. 4 and implies the earlier nonempty-primal-minimizer assumption. A condition that made all runs impossible, or one that discarded either the primal or dual conclusion, would not represent Theorem 3.1.
The block operator is represented through its quadratic form ; is recorded for Algorithm 3.2. The complete development will need the abstract iteration lemmas, proximal optimality conditions, block-metric estimates, and the links from each algorithm's inclusion to the solution set. Contributions proving those results, or building reusable Hilbert-space operator infrastructure needed by them, are in scope. The several-composite-functions extension in Theorem 5.1 is reserved for separate work.
The conditional logit model assigns to an alternative in a finite choice set the probability , where is a "representative utility" built from observed attributes of the alternative and the decision maker. It is the workhorse of discrete choice econometrics, transportation demand forecasting, marketing and revenue management, where it underlies multinomial logit assortment and pricing models. Its appeal for applied work is computational; its appeal for economics is that it can be read as the aggregate behaviour of a population of utility maximizers. This mission formalizes the result that makes that reading exact: Lemmas 1 and 2 of D. McFadden, Conditional logit analysis of qualitative choice behavior (1974), which show that, under a mild regularity condition, logit choice probabilities arise from random utility maximization exactly when the idiosyncratic taste shocks follow the extreme value (Gumbel) distribution.
Timeline:
An individual faces alternatives with representative utilities . The utility of alternative is , where the taste shocks are independent and identically distributed with a common law on and distribution function . The individual chooses the alternative of highest utility, so the selection probability of is (Equation (2) of the paper)
computed under the product law of the shocks. The logit formula (Equation (12)) is . The extreme value law (Equation (13)) is .
A law is translation complete if for every function of bounded total variation on with , the condition for every real forces outside a Lebesgue-null set. Laws whose characteristic function never vanishes, the extreme value law among them, are translation complete (footnote 5 of the paper).
In Lean the law is μ : Measure ℝ with [IsProbabilityMeasure μ], is ProbabilityTheory.cdf μ, the selection probability is selProb μ V i for V : Fin J → ℝ, and the logit formula is logitProb V i.
Fix a universe of alternatives with a representative utility map onto the real line. For a translation complete law normalized by ,
The normalization only fixes the location of the shocks: without it the conclusion is the one-parameter family of Lemma 2 below.
The result separates two readings of the logit formula. Lemma 1 shows that it is consistent with utility maximization; Lemma 2 shows that, within the class of i.i.d. additive random utility models with translation complete shocks, the extreme value law is the only one consistent with it. Consequences drawn from the random utility reading, such as the log-sum formula for expected maximum utility used in welfare analysis, therefore apply to logit models without further distributional assumptions inside that class. The same reading supports the interpretation of multinomial logit demand in assortment optimization and revenue management.
Both lemmas are proved in the paper and in later textbooks; neither is open. As far as a search of the Prove2Me catalog shows, neither has a machine-checked proof. The mission provides Lean statements of the random utility model with i.i.d. shocks, of translation completeness and of the extreme value law that later discrete choice formalizations can reuse.
Lemma 1 is a computation with the extreme value density; its formal cost lies in passing from the product-measure probability (2) to the iterated integral (3) and evaluating an improper integral. Lemma 2 is harder. The natural first idea is to differentiate the logit identity in the utilities and solve a differential equation for ; this requires a density, which Lemma 2 does not assume. Without a density, the only handle on is the logit identity itself, an equality of integrals against that holds for every utility vector; turning such integral identities into pointwise information about is where the hypothesis of translation completeness enters, and it yields statements only outside a Lebesgue-null set, so one-sided continuity of distribution functions is needed to recover identities at every point. A second subtlety is that the paper's (14) is written with while the event (2) is strict, so with a general law the integrals involve left limits of .
Alternatives are indexed by Fin J; the model is indexed by the utility vector, so the individual attributes and alternative attributes enter only through . The shocks have joint law Measure.pi (fun _ => μ), which is what "independently identically distributed" means; a general joint law is not allowed. The event in (2) uses strict inequalities, and the selection probability is defined for every law, with no density. Translation completeness quantifies over BoundedVariationOn h Set.univ with limits at both ends; such are bounded and measurable, so the integrals are genuine, and "measure zero" is Lebesgue measure.
Lemma 2's hypothesis is stated on every finite subset of the paper's alternative universe, with a surjective utility map. Distinct alternatives may have the same utility. The printed proof uses equal-utility alternatives, which surjectivity alone need not supply; proving the stated theorem requires an additional continuity argument. A trivializing formalization is ruled out: the selection probability is a genuine product-measure probability, and the hypotheses of the goal are met by the extreme value law, which is translation complete with .
A complete development needs: Fubini for Measure.pi over Fin J split at one coordinate; the Gumbel density and the improper integral ; the facts that bounded-variation functions are bounded and measurable and that distribution functions are right-continuous with left limits. The integral representation (milestone 1) and the Gumbel computations are reusable in any random utility formalization. Proofs of the milestones, of the footnote-5 fact that the extreme value law is translation complete, and alternative proofs of Lemma 2 are welcome.
A perfect graph is a finite simple graph in which every induced subgraph has chromatic number equal to its largest clique size. This equality gives a structural reason that a clique lower bound on the number of colours is attainable for every induced part of the graph. Berge proposed a forbidden-subgraph description of perfect graphs: a graph should be perfect exactly when it has neither an odd hole nor an odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved that statement in The strong perfect graph theorem, Annals of Mathematics 164 (2006), Theorem 1.2. Their proof separates possible configurations in a Berge graph and shows that each either belongs to a controlled class or admits a decomposition.
This mission isolates the even-prism step, Theorem 10.6 of that paper. A prism is one of the configurations that can appear in a Berge graph even though odd holes and antiholes do not. The step matters because its conclusion leaves only a specific nine-vertex graph or one of two decompositions that the larger proof handles elsewhere. It is the result identified as step 1.8.4 in the authors’ outline (paper, pp. 59 and 124).
All graphs here are finite and simple. A path means an induced path; a single vertex is allowed as a path of length zero. A hole is an induced cycle with at least four vertices, and an antihole is a hole in the complementary graph. A graph is Berge if every hole of and of its complement has even length.
A prism has two disjoint triangles, and , joined by three pairwise vertex-disjoint induced paths from to . Between distinct paths, the only edges are those in and those in . The prism is even when all three have even length. “ contains an even prism” means that such paths exist as an induced configuration in ; may have other vertices. “ is an even prism” means the paths cover every vertex of (paper, pp. 93 and 119).
An appearance of is an induced copy in of the line graph of a bipartite subdivision of the four-vertex complete graph. It is nondegenerate if no four-cycle of contains all four branch vertices. Only appearances in are excluded in this mission; appearances in are allowed by the hypotheses (paper, pp. 72, 74–75).
A proper 2-join partitions the vertices into two sides with specified, nonempty attachment sets. The cross edges are exactly the two complete attachment pairs; every component of either side meets both of its attachment sets. If a side is itself a path between singleton attachment sets, that path has odd length at least three. A balanced skew partition divides the vertices into and so that is disconnected, is disconnected in the complement, and two path parity conditions hold: no odd path crosses between nonadjacent vertices of , and no odd antipath crosses between adjacent vertices of (paper, pp. 53–54).
The numbered milestones are Theorems 7.2–7.4 and 10.5. They assert common parity of the three prism paths, common neighbours of an anticonnected set at both end triangles, preservation of two neighbours under replacement of one even prism path, and the balanced skew partition forced by a major vertex. A vertex is major when it is adjacent to at least two vertices of each end triangle. These milestones match the paper’s statements on pp. 93 and 123 (paper).
For a Berge graph with no nondegenerate appearance of in ,
The first case describes the entire graph, not just an induced nine-vertex subgraph. The statement fixes all outcomes exactly as in Theorem 10.6, p. 124.
Theorem 10.6 removes even prisms from the unresolved part of the strong perfect graph theorem’s structural argument. If the graph is larger than the exceptional prism and has no nondegenerate appearance, the theorem supplies a proper 2-join or a balanced skew partition. Subsequent results can work with those decompositions instead of treating arbitrary attachments to a prism (paper, §10 and the outline at 1.8.4).
The mathematical result is proved in the 2006 paper. The work here is to give its graph objects and statements machine-checkable meanings, then formalize the known proof. This proposal contains open Lean theorem statements and sorry-free definitions; the proof obligations remain for solvers. The definitions of induced paths, holes, subdivisions, and decomposition predicates can also support other steps of this paper. The Roussel–Rubio lemma and the balanced-skew-partition results of §§2–4 are proved in the same paper and posed in mission II of this series. The prism-attachment result 10.4 is posed in mission VI, where it is used most directly.
An outside connected set can attach to several parts of a prism without containing a single major vertex. Its attachments need not be local to one path or one triangle, so checking vertices one at a time does not decide which decomposition exists. The paper’s §10 distinguishes several attachment patterns; the evenness of the paths and the exclusion of a nondegenerate appearance restrict them, but do not themselves give a 2-join or skew partition by a one-line parity argument. The larger proof must also account for attachments throughout the graph while preserving the full definitions of both decomposition outcomes (paper, pp. 119–127).
Lean represents a graph as SimpleGraph V with a finite vertex type. The prism is three lists of vertices, each an induced path; the lists are disjoint, and the cross-edge condition admits exactly the two end triangles. Reversing a list changes its orientation but not the underlying graph configuration. A hole uses a cyclic list with the closing edge; Berge checks holes in both and . Connectivity is reachability in an induced graph, so the empty vertex set is connected as the paper says. A subdivision uses six tracks on a finite carrier, with all its vertices and edges accounted for; the appearance uses an induced graph embedding of its line graph. The exception checks that the prism covers the whole graph and that .
These encodings require genuinely induced paths and the paper’s nondegenerate appearance condition. Dropping either would change the theorem. The proper 2-join includes component reachability and the odd-path special case; the balanced skew partition includes both path parity clauses. The nine-vertex graph formed by two triangles and three two-edge paths has a separate sorry-free Lean witness, so the exceptional outcome is nonvacuous. Useful contributions include the numbered prism lemmas, attachment analysis for 10.6, and reusable results about finite induced paths and graph subdivisions.
Linear programming, with , is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs with and for every , as the path parameter decreases to . A classical short-step method needs iterations, each solving a linear system with the matrix , for a total of roughly operations or more.
Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time (for the current values of the matrix multiplication exponent and its dual ), matching the cost of multiplying two matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.
Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to ; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached ; van den Brand (2020) derandomized the result.
Vectors are in and products, quotients and roots of vectors are coordinatewise. For and vectors , means for all ; for a scalar is defined likewise. The number of variables is and has full row rank .
The potential is , evaluated at with ; it is small exactly when every is close to .
StochasticStep (Algorithm 1) takes positive , a direction , a sampling parameter and the output of a data structure with . It rescales to , (), draws a sparse vector with independent coordinates, with probability and otherwise, and computes the step through the projection . The draw is repeated until and are at most ; the output is .
Main (Algorithm 2) sets , , , , starts at , and in each iteration sets , takes the direction
runs StochasticStep, and falls back to a deterministic ClassicalStep whenever .
For every iteration , almost surely Assumption 4.1 holds for the input of iteration (in particular and ), almost surely the resampling loop of iteration succeeds with positive probability, and
The paper writes ; its proof gives the constant .
Lemma A.1 (variance of a product), Lemma 4.12 (properties of ), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of ), and Lemma 4.13:
Lemma 4.14 is what makes the randomized method usable: the iterates stay in the -neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, , is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).
The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).
The running-time claims of the paper (Theorem 2.1's expected time , Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.
The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps at , and by an induction over iterations of under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.
Coordinates are Fin n, vectors Fin n → ℝ, a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and the natural logarithm. is written out as ; is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every , of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value ; the data structure and ClassicalStep are arbitrary measurable functions , of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. is the number of variables of the program the loop runs on.
Deviations from the page, all recorded in the items: Assumption 4.1 is used with instead of the printed , because Main sets to exactly that value; is instantiated as , the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while ; at the second term of is . No hypothesis is imposed.
A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles , cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.
Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.
The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.
Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.
Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.
A population consists of individuals, each carrying an allelic type. Its description is , where is the number of allelic types carried by exactly individuals, so that
For a real parameter , the Ewens distribution on descriptions is
where is the binomial coefficient for real . In the infinite alleles model, individuals die at rate , each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability ; then (7.6) is the equilibrium distribution with (7.5).
A random sample of size without replacement is a uniformly random -element subset of the labelled individuals, each of the subsets being equally likely; the sample has a description in the same sense.
The number of individuals carrying one given allele performs a random walk on with intensities
An allele is quasi-fixed when it is the only allele present ().
If and the population description is distributed as , then a random sample of size drawn without replacement has description with probability , the same being used for both sizes:
The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on . Kelly deduces from it the sufficiency of the number of alleles in a sample for and the heterozygosity (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).
Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.
The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between and , a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives and . Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of -subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.
Nat.Partition n, with the multiplicity of the part ; the product in (7.6) runs over . The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is times the number of -subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity ) are reusable beyond this mission.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number, and Berge if no induced subgraph is an odd cycle of length at least five (an odd hole) or the complement of one (an odd antihole). Berge conjectured in 1961 that the two classes coincide. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006), 51–229. Perfect graphs matter beyond graph theory. A graph is perfect exactly when its stable-set polytope is defined by clique inequalities (Chvátal; Lovász), so the theorem characterizes the graphs on which the stable-set and colouring integer programs are solved by their linear relaxations.
The proof is a structure theorem. Every Berge graph is basic (bipartite, the complement of a bipartite graph, the line graph of a bipartite graph or its complement, or a double split graph), or it admits a proper 2-join, a proper homogeneous pair or a balanced skew partition. The proof splits into twelve steps (1.8.1–1.8.12, p. 59), each about Berge graphs that contain a particular configuration. This mission is the first step, statement 5.1 of the paper. It covers Berge graphs that contain a large line graph, and it takes up Sections 5–8 (pp. 72–107).
All graphs are finite and simple. For a graph , is its complement. A path is an induced path, and its length is its number of edges. A track is a path in the conventional, not necessarily induced, sense. A set is connected if is connected, and anticonnected if is connected.
The line graph of a graph has vertex set , and two edges are adjacent when they share an end. is a line graph if for some graph . A subdivision of a graph replaces each edge of by a track from to , the tracks being disjoint except for their ends. A branch-vertex is a vertex of degree at least . A branch is a maximal track whose internal vertices are not branch-vertices. is 3-connected if it has more than three vertices and no set of at most two vertices disconnects it.
For a bipartite subdivision of , is degenerate if some 4-cycle of passes through its four vertices of degree three. A graph appears in if is isomorphic to an induced subgraph of for some bipartite subdivision of .
Two decompositions occur in the conclusion. A skew partition is a partition of with not connected and not anticonnected. It is balanced if no odd path joins two nonadjacent vertices of through , and no odd antipath joins two adjacent vertices of through . A proper 2-join is a partition of with nonempty disjoint such that:
The development needs further objects, each defined on its page: saturating edge sets and major vertices (pp. 77, 81), overshadowed appearances (p. 85), -enlargements (p. 75), and -strip systems with their rungs (p. 98).
Let be Berge and let be a bipartite subdivision of such that is nondegenerate and is an induced subgraph of . Then
The proposal also contains 5.2 (p. 73, step 1.8.2: Berge graphs containing ) and 5.3 (p. 74) as theorems without milestones.
5.1 is the line-graph step of the decomposition theorem. It turns "contains a substantial line graph" into "is a line graph or decomposes". The later steps of the proof start from the complementary case, where no such appearance exists (degenerate appearances in §9, prisms in §§10–13). The strip-system technique of §8 can be reused: it assembles all alternative rungs of a line-graph appearance and analyses how the rest of the graph attaches to it.
The strong perfect graph theorem is proved, but to our knowledge no proof assistant has a machine-checked proof of it. This mission formalizes one of its twelve structural steps. Several results of the same paper that the proof of 5.4 uses are posed in other missions of this series and are not posed here:
The statements 5.5, 5.6, 5.8, 8.3, 8.4 and 8.5 are also used in the proof. They are open to solvers as further lemmas.
Knowing that contains some appearance of is not enough to make a line graph or to decompose it. Vertices outside the appearance can attach to it in many ways. Each such pattern has to be shown to be impossible in a Berge graph, or to yield a larger appearance of a bigger graph , or to yield a decomposition. The first idea, analysing one outside vertex at a time, fails for two reasons. Connected sets of "minor" vertices can attach non-locally even when each vertex alone attaches locally (5.8). And anticonnected sets of "major" vertices are what produce the skew partitions (6.1). The small cases make things harder: , and degenerate subdivisions of are basic in several ways at once, so the theorem fails for them without the nondegeneracy hypothesis.
Graphs are SimpleGraph V on a Fintype. is Gᶜ. is Mathlib's H.lineGraph on H.edgeSet. " is an induced subgraph of " is an induced embedding H.lineGraph ↪g G, and "" says that this embedding is surjective. Paths and holes are vertex lists with the induced-adjacency condition. Tracks are vertex lists with consecutive vertices adjacent; their adjacency is not induced. Subdivisions carry an injection of and one track per edge of . These tracks are internally disjoint, avoid internally, and cover every vertex and every edge of . "3-connected" includes the paper's convention of more than three vertices. "", "" mean isomorphism. Existentially quantified graphs ( in an appearance, the enlargement , the graph of which is a line graph) live on Fin n.
The standing assumptions are those of each statement: is Berge and is 3-connected. In 7.1 the two edges are taken distinct, as the conclusion requires. "Up to symmetry" in 6.1 becomes an existential choice of the labelling of the 4-cycle and of the order of .
The formalization would be trivial if paths were allowed to be non-induced, if the complement bars in 5.4 and 6.1 were dropped, or if a "subdivision" could share internal track vertices or carry extra vertices or edges. The definitions rule out all three. A sorry-free check shows that is a subdivision of itself and is not bipartite.
Reusable infrastructure: tracks, branches, subdivisions, 3-connectivity, appearances and strip systems. Contributions are welcome on the graph-theoretic lemmas 5.3 and 7.1, which do not need Berge graphs, and on the Berge-specific milestones in the order listed.
Many optimization problems in statistics, signal processing and control are posed over sets of matrices with a constraint that makes them curved: matrices of fixed rank, matrices with orthonormal columns, symmetric matrices with a prescribed spectrum. Algorithms on such sets ("optimization on manifolds") compute a step in the tangent space at the current point, as in a vector space, and then need a rule that brings the point back to the set. A retraction is such a rule; the notion was introduced by Adler, Dedieu, Margulies, Martens and Shub for Newton's method on Riemannian manifolds (IMA J. Numer. Anal. 2002) and is the basic building block of the algorithms in Absil, Mahony and Sepulchre's monograph (Princeton, 2008). Any retraction preserves the local convergence of Newton's method, so the choice among retractions is about cost and convenience.
The most natural candidate is to project back onto the manifold: take the nearest point. Absil and Malick (SIAM J. Optim. 2012; preprint HAL hal-00651608) show in §3.1 that this projective retraction is always a valid retraction of maximal smoothness, and then compute it for fixed-rank, spectral and Stiefel manifolds. The underlying fact, that the nearest-point map onto a submanifold is locally single-valued and , is classical (the paper cites Lewis and Malick, Math. Oper. Res. 2008); the paper gives a short proof through the inverse function theorem on the normal bundle. This mission formalizes §3.1: that lemma and the resulting retraction.
Let be a Euclidean space, a finite-dimensional real inner product space, of dimension (in the paper's examples, with the Frobenius inner product). A set is a submanifold of class and dimension around if and there are an open neighbourhood of and a diffeomorphism from onto an open subset of with
The tangent space is the linear subspace of spanned by the tangent cone of at , and the normal space is . The tangent bundle and normal bundle are and , subsets of . denotes the orthogonal projector onto .
The projection of onto is the set of nearest points,
which may be empty (if is not closed) or contain several points (if is not convex).
A map from to is a retraction around (Definition 2.1) if on some neighbourhood of in it is of class , satisfies , and for .
The formal retraction predicate includes and a local submanifold chart at ; this ensures that its base point lies on .
For a submanifold () around , the map
is single-valued near in , and this single value is a retraction around .
The projective retraction is the reference retraction on an embedded submanifold: it exists for every submanifold, it has the maximal smoothness allowed by the tangent bundle, and it is the one practitioners compute first (truncated SVD for fixed-rank matrices, polar factor for the Stiefel manifold). Section 4 of the paper shows that it is moreover second order and generalizes it to projections along arbitrary smooth fields of transverse subspaces; Lemma 3.1 is the model of that argument. Lemma 3.1 on its own is a basic tool well beyond retractions: local single-valuedness and smoothness of the nearest-point map underlies the local convergence analysis of alternating projections on manifolds and the theory of prox-regular sets.
All statements here are proved results. No machine-checked proof of them is known to exist: Mathlib has the inverse function theorem, tangent cones and orthogonal projections onto subspaces, but no embedded submanifolds of a Euclidean space with their normal bundle and no nearest-point map onto non-convex sets. The mission produces these statements in Lean and invites proofs of them.
The obvious argument writes the nearest point as a critical point of on and applies the implicit function theorem. Two things break. First, existence: is not assumed closed, so a nearest point exists only because is locally closed near and points of far from are farther from than is. Second, uniqueness: critical points are not unique in general, and the implicit function theorem only describes critical points near a given one. Uniqueness needs a quantitative argument that every nearest point of lies in the region where on the normal bundle is injective. Finally, the normal bundle is itself only a manifold, whose tangent space at must be identified before the inverse function theorem applies; this is milestone (3.3).
The ambient space is any type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; is Module.finrank ℝ E, and are natural numbers with stated as a hypothesis (so that in ℕ is honest). The paper's standing assumption " is a submanifold of class () and dimension " enters only as the local hypothesis IsSubmanifoldAt k d M xbar, exactly as Lemma 3.1 and Proposition 3.2 state it ("around "). The chart is an OpenPartialHomeomorph onto EuclideanSpace ℝ (Fin n), in both directions, with 0-based coordinates. No closedness of is assumed, because the paper does not assume it.
The projection is the platform predicate IsMetricProjection M x z ( and for all ); single-valuedness is stated as equality of the set of such with a singleton, which asserts existence and uniqueness. A formalization that only states "some selection is ", or uses (satisfied by the empty set), would drop the main claim and is ruled out. The tangent space is the span of Mathlib's tangentConeAt; "class on a neighbourhood in " is ContDiffOn on with open; is a HasFDerivAt statement on the normed space ; is Submodule.starProjection.
A complete development needs: the tangent space of a slice submanifold equals the image of the chart's derivative, the normal bundle as a manifold, an inverse function theorem on it, and compactness of for small . These are reusable for the other missions of this series (fixed-rank, spectral and Stiefel manifolds, and the retractor construction of Section 4), and contributions of such general lemmas as intermediate theorems are welcome.
Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.
Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served -server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).
There are customer types and queues. Customers of type enter the system in a Poisson stream of rate and visit the queues in that order before leaving; two successive stages of a route are at different queues.
Queue holds its customers in positions . Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate , with for ; a proportion goes to the customer in position . An arriving customer takes position with probability . For each , and are probability vectors on .
The class of the customer in position of queue is , his type and the stage of his route. The state of queue is and the state of the network is . Its transition rates , displays (3.1)–(3.6), are the sums of the intensities of all events taking to : a departure from the system (intensity ), a move from position of queue to position of the next queue (intensity ), and an arrival into position of the first queue of a route (intensity ).
With if and otherwise, set
If every series defining converges, then
is positive, sums to over all network states, and satisfies the equilibrium equations
Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate , even though the actual arrival stream at queue is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).
The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.
The obvious first attempt, detailed balance, fails: and differ in general, because a customer's route cannot be run backwards inside the same network ( is usually when ). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of -tuples of lists, reorganized by queue length together with the identity .
Fin I, queues Fin J; the book allows countably many types with . A network state is a function assigning to each queue a list of classes with ; the state space is countable and all sums over it are tsum/HasSum.KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates ; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).tsum, which Lean sets to for a divergent series; every theorem assumes the series converges, the book's "none of is zero".Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over , and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.
In a multi-armed bandit problem a learner chooses one of actions in each of rounds and observes only the reward of the chosen action. Two models of the rewards have separate theories. In the stochastic model, each arm pays independent draws from a fixed distribution; algorithms such as UCB1 (Auer, Cesa-Bianchi & Fischer 2002) have regret of order , logarithmic in . In the adversarial model, an adversary chooses the rewards; Exp3 and its variants (Auer, Cesa-Bianchi, Freund & Schapire 2002) have regret of order , which is optimal there. An algorithm tuned for one model fails in the other: stochastic algorithms can suffer linear regret against an adversary, and adversarial algorithms pay even when the rewards are i.i.d.
Bubeck and Slivkins (arXiv:1202.4473, COLT 2012) asked whether one algorithm can be near-optimal in both models without knowing which one it faces. They answered yes with the algorithm SAO. This result started the "best of both worlds" line of work on bandits. Later contributions include EXP3++ (Seldin & Slivkins 2014) and Tsallis-INF (Zimmert & Seldin 2021).
There are arms and rounds. On round the algorithm draws an arm from a probability vector computed from the history it has observed. At the same time a reward vector is fixed, and the algorithm observes only .
The analysis uses importance-weighted estimates , the sample means , the averages , and the play counts .
SAO (Algorithm 1 of the paper) takes a parameter . It keeps a set of active arms, initially all arms, and samples them uniformly at first. On each round it applies a test, (12), that deactivates an arm whose estimate falls far below the best active one. The probability of a deactivated arm then decays as , where is the deactivation time and the arm's probability at that moment. Three further tests, (13)–(15), check that the observations stay consistent with stochastic rewards. If any of them fails on round , SAO switches permanently to the adversarial algorithm Exp3.P (Bubeck & Cesa-Bianchi 2012, Fig. 3.1) for the remaining rounds.
For every let . With probability at least , SAO with parameter satisfies, in the stochastic model (whenever some arm has ),
and, against every adaptive adversary with rewards in ,
The milestones follow the paper's proof in order:
The theorem shows that the stochastic and adversarial regret rates are not in conflict. A single algorithm, with no information about the model, gets pseudo-regret on stochastic rewards and regret against adaptive adversaries. Each rate is within polylogarithmic factors of optimal for its model. Later algorithms improved the logarithmic factors and removed the explicit switching, but they are compared against this result.
The theorem is proved in the paper. It is not known to have a machine-checked proof. Formalizing it requires a precise model of an adaptive adversary interacting with a randomized algorithm, martingale concentration with random variance (Lemma 4.4), and an exact statement of SAO including its boundary cases. The pieces are reusable: the interaction model, the estimators, Exp3.P and its high-probability guarantee all apply to other adversarial bandit results.
Neither standard analysis carries over. In the stochastic model, SAO's sampling probabilities are random and depend on the past, and a deactivated arm's probability keeps changing. Hoeffding-type bounds for a fixed sampling scheme therefore do not apply to . The variance of the importance-weighted estimate grows like , which is controlled only through the algorithm's own schedule (16). This is why Lemma 4.5 has the two-part radius with . In the adversarial model, the deterministic argument has to show that whenever the consistency tests pass, the regret accumulated before the switch is already small, for an adversary that adapts to the arms played. A union bound over all quantities, all arms and all times (§4.1) is needed before any deterministic reasoning, so every constant in the event matters.
All declarations live in the namespace BestBothWorlds.SAO.
Fin K and rounds are . An arm path is Fin n → Fin K.Real.log is the natural logarithm. All constants of Theorem 4.1 are explicit, with .A trivializing formalization is ruled out. The goal's hypotheses concern only the instance (, , , the distributions or the adversary). The algorithm's quantities (, , , the sampling probabilities) are computed by the definition of SAO and are never free variables or hypotheses. The adversarial half covers adaptive adversaries, not only oblivious reward tables.
The expectation form of Theorem 4.1 ( bounds with ), Theorem 1.1 and the two-armed warm-up of §3 are out of scope. Proofs of any milestone are welcome, as are alternative proofs of the concentration lemmas from Mathlib's martingale library.
Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.
Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.
There are periods and a known lead time : an order placed in period arrives in period . Period has a per-unit holding cost and a per-unit backlogging penalty . Ordering costs are zero (), which is the standing assumption of the paper's §4. The initial data are the net inventory and the pipeline orders .
Demands are nonnegative random variables on a probability space with a filtration ; is the information at the beginning of period , and is -measurable. A feasible policy places orders that are -measurable. Write (with for ), for the inventory position before ordering and after ordering.
The marginal holding cost of period is the holding cost that the units ordered in incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:
The cost of is ; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.
A dual-balancing policy orders nothing after period , and in each period orders the quantity that balances the two conditional expected marginal costs:
For every dual-balancing policy and every feasible policy ,
The paper writes ; quantifying over all feasible is the same statement whenever an optimum exists and needs no existence assumption.
Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals , which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when and the demands are integrable, so the goal is not about an empty class.
The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.
The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets and to be determined by the information of period , so that conditioning on commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.
ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods are read, and the pipeline is substituted for .Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded -measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.
The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.
Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.
Time is indexed by the integers . The retailer faces i.i.d. demand
where the error terms are independent and identically distributed from a symmetric distribution with mean and variance .
Single-stage policy (§2). With observations, a lead time , a safety factor and a constant , the retailer forms the moving-average estimates
raises its inventory position to the order-up-to point , and so orders . Orders may be negative: excess inventory is returned without cost.
Decentralized chain (§3). Stages form a serial chain; stage 1 is the retailer, and is the lead time between stages and . No stage sees customer demand except the retailer. Stage forecasts from the orders it receives,
uses the order-up-to point , and orders
For every stage and every period ,
The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.
For the single-stage policy with any safety factor and any constant ,
This is the i.i.d. case of the paper's Theorem 2.2. With and the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case of the goal.
The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage in the i.i.d. case equals (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio .
Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at ); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean and variance . Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.
The natural first idea is induction on the stage: treat the orders of stage as the demand of stage and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage are not i.i.d.: they are autocorrelated, and stage 's moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.
All objects live in the namespace ChenBullwhip.Decentralized.
IIDDemand P is the demand model on a probability space : a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in , with mean and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.SingleStage defines , , , and of §2; is a free real parameter, as the paper does not fix it.Chain defines the forecasts and the orders by recursion on the stage, with the convention , so that stage 1 orders . The recursion is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is , as the sequence of events on p. 440 describes.Disclosed hypotheses not on the page: (a moving average needs an observation), (the paper divides by ), and square-integrable errors (Mathlib's variance is off ). The paper's model (1) asks ; since affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period , with no stationarity hypothesis.
Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is .
A complete development needs variance and covariance calculus for finite linear combinations of independent variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.
SupplyChainTheory.*).The stochastic multi-armed bandit is the basic model of sequential decisions under uncertainty with partial feedback: a forecaster repeatedly picks one of options and observes only the reward of the option it picked. It models clinical trials, ad placement, routing and dynamic pricing, and is the building block of many reinforcement-learning algorithms. The question is how much reward is lost, compared with always playing the best option, through having to learn which option is best.
Chapter 2 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) answers this for upper confidence bound (UCB) strategies.
There are arms. Arm has an unknown reward distribution with mean . At each round the forecaster selects an arm based on the past and receives a reward drawn from , independently of the past. Write , for the gap of arm , and for the number of times arm is selected in rounds . The pseudo-regret is
Moment condition (2.2). There is a convex with and for all and every arm's reward . Its Legendre–Fenchel transform is . For rewards one may take , for which .
-UCB. With the mean of the first rewards of arm , at round select
If the rewards satisfy (2.2), then -UCB with satisfies, for every ,
This is the bound the book's proof establishes. The printed statement has in place of ; see Formalization scope.
Theorem 2.1 says that the cost of learning grows only logarithmically in the horizon, with a constant set by how well each suboptimal arm can be told apart from the best one. Theorem 2.2 shows that, up to constants, this cannot be improved: for Bernoulli rewards any strategy that is good on every instance must pay per suboptimal arm, with constant . By (2.8) this constant is at least of order , matching (2.4). Together they are the template for the analysis of most optimistic algorithms: KL-UCB, linear and contextual UCB, and UCB-style reinforcement learning.
All results of the chapter are classical and proved on paper. This mission makes them machine-checked in a common model. That model has an explicit pseudo-regret, an explicit (generalized) inverse of , an explicit initialization rule for the algorithm, and a randomized-strategy model for the lower bound. Later chapters of the series and later papers on optimistic algorithms can build on it.
The deterministic part of the upper bound is short, so the main difficulty is probabilistic. The sample mean is taken over a random number of samples that depends on the algorithm's past. A Chernoff bound for a fixed sample size does not apply to it directly. The proof needs a union bound over all possible sample sizes, together with the representation in which the -th reward of each arm is a fixed random variable. Summing the resulting tail over rounds is where enters.
The lower bound needs a change-of-measure argument between two Bernoulli instances, applied to a forecaster that may be randomized and never knows the horizon. Expressing "the forecaster cannot distinguish the instances" requires the law of the whole interaction under two environments.
Model. Arms are Fin K with , rounds are , and the natural logarithm is used. Rewards are a stack: is the reward of the -st pull of arm , all mutually independent, identically distributed per arm. For every strategy this gives the same law of arms and rewards as the book's protocol. , and are the published definitions of ImprovedLinBandits.UCBDelta.armModel. The pseudo-regret is (2.1), , not the expected regret. The arms played are measurable random variables, so that every expectation is genuine.
and its inverse. takes values in the extended reals. .
Algorithm. The index is undefined while . Unplayed arms are therefore played first, so each arm is played once in rounds . Ties are broken arbitrarily.
Corrected misprint. The book prints Theorem 2.1 with constant term . Its proof yields (bound on times ). The printed form is false for Gaussian rewards with large gaps. The goal states the proof's version. (2.4) is correct as printed because .
Constants. No O(·) appears in the chapter's statements. The constants are the book's: in Theorem 2.1 and (2.4), and the factor in (2.4) and (2.8).
Conventions made explicit.
Conventions 1–3 hold for every the book uses.
Theorem 2.2. The forecaster is a measurable rule from the history and a fresh uniform seed to an arm. It does not depend on the horizon. Consistency is required on every Bernoulli instance, every suboptimal arm and every . A term with () is , and the is taken in the extended reals. The book proves only .
Ruled out. The algorithm cannot see unplayed rewards (its index uses only the sample means of rewards already received). Non-measurable arm choices, which would make the expectations vanish in Lean, are excluded. Consistency cannot be assumed only on the instance of the conclusion.
Needed infrastructure. Cramér–Chernoff bounds for sums of i.i.d. variables, Hoeffding's lemma, the stack representation of bandit interactions, and the divergence decomposition for randomized strategies. All are reusable beyond this mission, and contributions of any of them are welcome.
The inverse Galois problem asks whether every finite group occurs as the Galois group of a finite Galois extension of . For finite simple groups, a large part of the problem was settled by the rigidity method (Shih, Fried, Belyi, Matzat, Thompson) and its refinements such as the braid-group method. Between 1984 and 1989 this machinery realized 25 of the 26 sporadic simple groups as Galois groups over , in fact as Galois groups of regular extensions of . The Mathieu group was the single exception.
Timeline.
denotes the group of permutations of the 23 points , acting on the left, so . The paper fixes three explicit permutations
and the Mathieu group is the subgroup of generated by and . A -extension of a field is a Galois extension together with an isomorphism . A finite extension of is regular if it contains no nontrivial algebraic extension of .
For a triple of conjugacy classes of , the set consists of triples with that generate , and the Nielsen class is the set of orbits of under simultaneous conjugation by . The paper works with the classes , , , represented by .
Facts about stated in §3 (order , simplicity, 4-transitivity, 17 conjugacy classes), the membership , the count , the Riemann–Hurwitz count of Lemma 3.1, the hyperbolic triangle of Lemma 3.2, and the group-theoretic step of Corollary 3.6 ( is not normal in any strictly larger subgroup of ).
Theorem 1.1 removes the last sporadic exception: combined with earlier work, every sporadic simple group is the Galois group of a regular extension of (Corollary 1.4), and hence occurs as a Galois group over every number field, in infinitely many mutually independent ways.
The paper's proof is computer-assisted: Belyi maps were computed numerically and the final claims were certified in Magma and PARI/GP. No machine-checked proof in a proof assistant is known. A formal proof of the explicit-polynomial statements (Examples 1.2 and 3.7) would give an independent, kernel-checked certificate of Theorem 1.1. The group-theoretic milestones (order, simplicity, transitivity, class counts, the Nielsen count) are reusable for any later work on or the other Mathieu groups.
The rigidity method fails for : for every -stable triple of conjugacy classes the Nielsen class has size different from , so no rational point of a Hurwitz space is forced. The smallest positive size, for , leaves seven covers, and the fact that one of them has field of moduli was found by explicit computation, with no conceptual explanation. Certifying that a particular degree-23 polynomial has Galois group exactly requires both a lower bound (the group contains , for instance via cycle types and the classification of transitive groups of degree 23) and an upper bound (the group is contained in a conjugate of , for instance via resolvents or reduction modulo primes). Neither bound is a finite check inside current Mathlib.
is Equiv.Perm (Fin 23). The paper's point corresponds to k - 1 : Fin 23, and permutations compose as functions, which matches the paper's left-action convention. is defined as Subgroup.closure {g₁, g₂}, so it is not described up to isomorphism. Galois groups are groups of field automorphisms, K ≃ₐ[ℚ] K, and a -extension is recorded as a group isomorphism with . is RatFunc ℚ. "Unramified outside " for a number field is encoded as "every prime dividing the absolute discriminant lies in ", which is equivalent by Dedekind's discriminant theorem. The Nielsen class is the set of orbits of under simultaneous conjugation. Hyperbolic angles in the Poincaré disk are defined through the hyperbolic law of cosines.
The geometric statements Lemma 3.3 and Proposition 3.5 concern the numerically computed curve and the polynomial , which the paper does not print, so they are not milestones. Lemma 3.1 enters only through its Riemann–Hurwitz count.
Contributions are welcome on decidable certificates for permutation-group facts in Lean, on Galois-group certification for explicit polynomials, and on Hilbert irreducibility.
Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?
F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on , stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.
Timeline:
A Markov chain on the states is given by a transition matrix : and for every row . Write for the probability that the chain started in first reaches (for , first returns to ) at step . The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor . A state is recurrent if and transient if ; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time is finite. The mean first-passage time from to is .
The M/G/1 matrix is built from a sequence of positive numbers summing to one ( is the probability of arrivals during one service):
that is, and, for , when and otherwise. The traffic intensity is
the mean number of arrivals per service.
The goal leaves arbitrary apart from positivity and normalization; in particular is allowed and falls in the transient case.
The result. The classification is the stability theorem for the M/G/1 queue: for the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for the queue empties infinitely often but has no steady state; for it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.
Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.
The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the -step probabilities and of hitting probabilities of state , none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic , recurrent ) need exact identities for mean first-passage times, not just bounds, and these must be handled in because the means may be infinite. And the boundary case (null recurrence) separates the two equivalences: an argument that only compares the mean drift with , such as a law of large numbers for the increments, cannot tell recurrence from transience there.
QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.i ≠ 0.mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for ).Summable or HasSum); Theorem 3's equation (6) is written as in together with finiteness of the , .Ruled out: as a real tsum (which is for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix that need not exist.
Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.
Temporal-difference (TD) learning estimates the value function of a Markov chain — the expected discounted sum of future rewards from each state — from a single stream of observed transitions, without knowing the transition probabilities. With a linear function approximator the value of state is represented as for a feature vector and a parameter . Classical TD() updates by stochastic approximation, and its behaviour depends on a step-size schedule that must be tuned.
Bradtke and Barto (Machine Learning 22, 1996) replaced the stochastic-approximation update by a least-squares solve: LS TD (Eq. (11)) recomputes at every step as the instrumental-variable least-squares solution of the empirical consistency condition. The method, later generalized as LSTD() by Boyan (Machine Learning 49, 2002), is the basis of least-squares policy iteration and of the "LSTD" methods in standard reinforcement-learning texts (Sutton and Barto, Reinforcement Learning, 2nd ed., 2018, §9.8). Its appeal is that it has no step size; the question this mission formalizes is whether it nonetheless converges, with probability one, to the true parameter.
Timeline. Sutton (1988) introduced TD(). Watkins and Dayan (1992) and Tsitsiklis (1994) proved probability-one convergence of tabular TD(0) and Q-learning. Bradtke and Barto (1996) proved probability-one convergence of LS TD on absorbing chains (Theorem 1) and on ergodic chains (Theorem 2). Tsitsiklis and Van Roy (IEEE TAC 42, 1997) proved convergence of linear TD() with general features on ergodic chains.
A finite Markov chain on a finite nonempty set is a matrix with and . A transition earns reward ; the expected reward out of is . For a discount factor the value function is
The chain is ergodic (Kemeny and Snell) if every state can be reached from every state: for all there is with . An invariant distribution is a probability vector with ; write .
Each state has a feature vector ; is the matrix with rows . The true parameter is a vector with for all .
The algorithm (Figure 3) starts at an arbitrary state , lets the chain move , and after transitions computes
the sums running over the transitions observed so far.
If is ergodic, (1) is linearly independent, (2) each has dimension , and (3) , then is finite and, from any initial law,
The goal leaves the chain, the rewards, the features and the initial law arbitrary.
The result. Theorem 2 shows that an LS TD learner running on one long trajectory recovers the exact value function whenever the features can represent every function on the states, with no step-size schedule. It is the step-size-free counterpart of the tabular TD(0) convergence theorems and the starting point for the later analysis of LSTD with fewer features than states, where the limit is the TD fixed point rather than . Lemma 5 is the general identification of that fixed point as the almost-sure limit of LSTD.
Formalizing it. The result is proved in the paper; it has not been machine-checked. A formalization adds three things the paper delegates: the strong law of large numbers for occupation times of a finite irreducible Markov chain, which the paper cites to Kemeny and Snell and which is not in Mathlib; the per-state transition frequencies used in the first sentence of the proof of Lemma 5; and the linear algebra of the limit. The first is reusable well beyond reinforcement learning.
The algebra is short once the empirical averages in (11) are known to converge. The difficulty is probabilistic: the averages are over a dependent sequence, so the ordinary strong law of large numbers does not apply. Two facts are needed: that the fraction of time in each state converges to almost surely for any starting law, including periodic chains, where itself does not converge; and that, among the visits to , the fraction followed by a move to converges to , which needs the strong Markov property at successive visit times. Neither follows from convergence of the chain's distribution, and neither holds for a chain started at a fixed state without an argument that every state is reached.
X with Fintype, DecidableEq, Nonempty, a row-stochastic matrix P : Matrix X X ℝ (structure Chain), rewards R : X → X → ℝ, features φ : X → Fin m → ℝ. Condition (2) is m = Fintype.card X; condition (1) is LinearIndependent ℝ φ.tsum is on a divergent series, so "θ* is finite" is stated as convergence of the series together with existence of with . is existential, never defined as Lemma 5's limit.Needed infrastructure: the strong law for occupation times of a finite irreducible chain under an arbitrary initial law (milestone 1), the strong Markov property at visit times, positivity of the invariant distribution of an irreducible chain, and the invertibility of for . Contributions to any of these, as standalone lemmas, are welcome.
A supplier who sells to a retailer at a per-unit wholesale price above her own production cost induces the retailer to order less than an integrated firm would. This effect, double marginalization, goes back to Spengler (1950) and is the standard benchmark against which supply chain contracts are judged: a contract coordinates the channel if it makes the decentralized decisions coincide with the integrated optimum. Revenue-sharing contracts, as used in the video-rental industry, coordinate the channel; the plain wholesale-price contract does not. Whether a supplier should bother with the administrative cost of revenue sharing depends on how much the wholesale-price contract actually loses and how much of the remaining profit the supplier keeps.
Cachon and Lariviere answer that question for a retailer whose revenue depends only on the quantity ordered, in Section 4.1.1 of their working paper Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations (June 2000; the 2005 Management Science version renumbers and revises the material). They show that the answer is governed by the curvature of the marginal revenue curve, and they compute it exactly for a one-parameter family. The source is the June 2000 working paper, whose results are unnumbered; every item cites its section, page and display.
A supplier produces at unit cost and sells to a single retailer. The retailer's expected revenue from units is , where , is strictly concave and differentiable on with derivative (the marginal revenue), is differentiable on with derivative , the product is viable (), and a finite quantity is optimal ( for some ). The supply chain profit is ; the integrated quantity maximizes over .
Under a wholesale-price contract with price , the retailer orders to maximize . Each order is induced by exactly one price, , so the supplier can be thought of as choosing . Her profit, the retailer's profit, and their sum are then
Following the paper, is assumed decreasing, which makes unimodal. The supplier's optimal quantity to induce maximizes over , and is her optimal wholesale price. The efficiency of the contract and the supplier's profit share are
In the α-family, for and , so : marginal revenue is convex for , linear for and concave for .
For and , the quantities and are the unique maximizers of and on , the profit share is , and
a quantity that does not depend on , is strictly increasing in , tends to as and to as .
The general milestones turn the paper's area argument (the triangle under the tangent to marginal revenue at ) into three comparisons: convex marginal revenue makes the wholesale-price contract worse for the chain and leaves the supplier at most two thirds of a smaller pie, concave marginal revenue the opposite. The α-family makes the trade-off exact: efficiency never falls below , while the supplier's share moves much faster than efficiency, which is the paper's argument for why revenue sharing is most attractive when marginal revenue is convex.
These results are proved on paper but, to our knowledge, not machine-checked anywhere; Mathlib has no supply chain contract theory. The formalization provides a reusable single-retailer wholesale-price model, a checked version of the convex/concave tangent comparisons, and a corrected statement of the α-family's monotonicity (see the scope section).
The general comparisons are short on paper but rest on a picture: they need the first-order condition at an interior maximizer, the tangent-line inequality for a convex or concave derivative, and the fundamental theorem of calculus for a function whose derivative is known only on a half-line and one-sided at . Strictness needs a strictly positive integrand on a nondegenerate interval.
The α-family is where the analysis is not routine. The closed forms involve real powers with exponents and , which must be combined carefully. The limit as is classical, but the monotonicity of on all of is not a one-line derivative sign check: the derivative mixes with rational terms, and its sign has to be established uniformly near and near .
Quantities and prices are real numbers. "Optimal" always means a maximizer over all admissible quantities (IsMaxOn on , or on in the α-family, as the page restricts), never a root of a first-order condition. The derivative of the general model is linked to by a one-sided derivative hypothesis on ; is required only on , since for it blows up at . In the α-family the marginal revenue is deriv of , not a separate function, and is assumed (implicit on the page: and ). Efficiency and profit share are real divisions; their denominators are positive at the optimal quantities.
Deviations from the page, all disclosed in the items:
A trivializing formalization is ruled out: the efficiency in the goal is the ratio of profits computed from at the maximizers, not a definition equal to , and the maximizers are characterized as unique argmaxes rather than assumed.
Welcome contributions: proofs of the general tangent comparisons, which are reusable for any concave revenue model; the real-analysis lemmas on ; and the α-family closed forms.
A revenue-sharing contract lets a supplier charge a retailer a wholesale price per unit and, in addition, collect the share of the retailer's revenue. The video-rental industry adopted such contracts at scale in the late 1990s, and Cachon and Lariviere showed that in a broad class of models they coordinate the supply chain: the retailer's privately optimal decisions coincide with those that maximize total channel profit, and the profit can be split arbitrarily between the firms (missions 1 and 2 of this series).
The same authors also studied where revenue sharing breaks down. The most practically relevant limitation is retailer effort: shelf space, service, store cleanliness and promotion raise demand, cost the retailer money, and cannot be written into a contract. Once the retailer gives away part of its revenue, it earns only a share of the return on its effort while still paying the whole cost. This mission formalizes Section 4.2 of the authors' working paper, which shows that revenue sharing then cannot coordinate the channel while leaving the supplier any profit, and, in an explicit linear-demand example, determines exactly when the supplier is better off with the plain wholesale-price contract.
The source is the June 2000 working paper (Cachon and Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations), whose results are displayed claims inside numbered sections rather than numbered theorems; the milestones cite section, printed page and display. The published version appeared in Management Science 51(1), 2005.
General model (Sec. 4.2.1). A supplier produces at unit cost . The retailer chooses an order quantity and an effort level after observing the contract . Expected revenue is continuous, differentiable, strictly increasing in and concave in ; effort costs the retailer , where is continuous, increasing, differentiable and convex with . The profits of the integrated channel, the retailer and the supplier are
The integrated solution maximizes over .
Linear example (Sec. 4.2.2). Inverse demand is with an effort-impact parameter , revenue is and effort costs . For a share the supplier's profit when the retailer responds optimally to is , and the supplier's optimal profit is
The share is the wholesale-price contract.
For , and every , the supremum defining is attained at the price , and
Consequently is strictly increasing on if (the wholesale-price contract is the supplier's unique best share), constant if , and strictly decreasing if , with as .
The general result (milestones 1–2) is a clean impossibility statement: with non-contractible effort, the only contract in the revenue-sharing family that coordinates the channel is the wholesale-price contract at marginal cost, which leaves the supplier zero profit. It marks the boundary of the coordination results of the earlier sections, and contrasts with the price-dependent newsvendor, where revenue sharing does coordinate price and quantity because the cost of expanding demand is captured in the revenue function and shared by both firms.
The example turns the impossibility into a design rule. Because coordination is out of reach, the supplier compares contracts by her own profit, and the threshold separates two regimes: when effort matters a lot she should leave the retailer all revenue and charge only a wholesale price ("a smaller share of a larger pie"); when it matters little she should take as much revenue as possible. The same threshold governs the counterintuitive comparative static that the integrated channel's retail price falls as production cost rises.
All results are proved on paper in the source. None has a machine-checked proof; this mission produces the first. The example is a fully explicit two-stage optimization problem, so the formal development also yields a verified computation of a Stackelberg equilibrium with moral hazard that other contract-design missions can reuse.
The individual calculations are elementary, and the work lies in getting the optimization statements right. The page solves the retailer's problem sequentially (effort first, then quantity) and writes the supplier's objective by substituting closed forms. A faithful proof must instead show that these closed forms are global optima over the constrained domains: the retailer optimizes jointly over the quadrant , the corner is optimal whenever , and the supplier's objective is a quadratic on glued to the zero function on , which is not concave on all of . The first-order-condition argument of the general model similarly needs an interior integrated optimum and a strictly positive marginal effect of effort, which "strictly increasing in " alone does not provide.
All quantities are real numbers. The general model is a structure RevShareCoord.Effort.Model carrying , its partial derivatives, , and ; derivatives are one-sided within , and joint differentiability of is replaced by its partial derivatives and joint continuity. The example lives in RevShareCoord.Effort.Linear. "Optimal" always means a maximizer over the whole admissible set ( for the retailer, for the supplier), and the supplier's value is defined as the supremum of her attainable profits, not by the printed formula.
Deviations from the page, each disclosed in the item's Formalization Note:
Plugging the printed into and comparing across would turn the dichotomy into a statement about an arbitrary price schedule; the goal instead asserts that attains the supremum over all , with the retailer best-responding jointly in .
No external library beyond Mathlib's real analysis and convexity is needed. Contributions welcome: proofs of the milestones, reusable lemmas on maximizing strictly concave quadratics over orthants, and a generalization of milestone 2 to non-interior optima.