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 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?
Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.
Timeline.
There are cities, numbered . Every two of them are linked by a direct road, and city is the destination. The travel time from to is a real number ; the matrix need not be symmetric. Throughout, for .
A route from to is a sequence of cities in which consecutive cities differ. Its stops are , and its time is . The minimal time (3.1) is the least time of a route from to , and .
The routing equation (3.2) is the system
Approximation in policy space (§5) starts from the direct-route policy (5.2), , and iterates (5.1):
The second scheme (§7, (7.1)) starts instead from and uses the same step.
For every the following hold. Each is the minimal time from to , attained by a route. The vector solves (3.2). Every real solution of (3.2) equals :
This is the claim of the Summary ("converges after at most iterations") and of the last sentence of §5. The paper's bound is kept, although also suffices.
The result. The note turns an enumeration over exponentially many paths into rounds of minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.
Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.
The minimum in (3.2) may be attained at a whose own optimal route passes back through . The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use to exclude zero-time cycles: with , the system (3.2) has infinitely many solutions. The bound depends on the at-most--stops reading of and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in .
Cities are Fin (n + 1), so , with standing hypothesis . City is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with for . Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at . Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all , the destination included.
The paper's loose phrases are made explicit as follows.
Two printed slips are corrected. (5.2) is printed for , which would set , and with statements (5.4), (5.5) and the goal would be false. The formalization uses , the value the paper's own justification needs. (7.1) prints "" for . Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.
The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.
The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound .
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.
This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.
Let be a finite set of elements. For subsets we write for and for .
Rank system. A function assigning an integer to each satisfies the rank postulates if
With the number of elements of , the nullity is . An element is dependent on if . A circuit of is a minimal dependent set: a subset with such that for every proper subset of . In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.
Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if
(C₁) No proper subset of a circuit is a circuit.
(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.
In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.
Rank from circuits. Whitney defines (p. 516):
Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.
In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset .
For every finite set :
where is the family of circuits of and is the rank defined from . This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."
The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.
On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of , with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.
The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in , obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, for circuits of a rank function requires turning the local postulate into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.
α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set .ℤ), so that is a true difference.N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under – or invariance of rankSeq under prefix-preserving changes.
Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4Whitney'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.
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.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.htmlSequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.
The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.
A state is an element of a nonempty standard Borel space , and an action is an element of a nonempty standard Borel space . The transition kernel gives a probability distribution for the next state after action in state . The reward may depend on that next state ; it is bounded and Borel measurable. Future rewards are discounted by with . These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.
A plan assigns a probability distribution of actions to each possible history before a decision. At stage , that history contains completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function at each stage; a stationary plan uses the same function at every stage and is denoted . Starting from state , the plan has discounted expected return
Here and are the state and action at stage . The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.
Two actions are equivalent at state when they have the same reward for every next state and the same transition measure . An action set is essentially countable by a Markov plan if, for every , one of the actions is equivalent to at . It is essentially finite by that plan if has a countable Borel partition such that, for , one of is equivalent to every action at . A finite action set is a special case. Blackwell 1965, pp. 233–234.
For a probability distribution on and , -optimality asks for a stationary with
Theorem 6(b) asserts that such an always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform -optimality statement: for every there is a stationary with for all . Its other targets identify the optimal return with the fixed point of the operator and with the unique bounded solution of the optimality equation . Blackwell 1965, pp. 232–234.
The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary with exact optimality:
The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.
The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.
Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.
On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an -optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.
The Lean model uses nonempty StandardBorelSpace types for and . “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on , and ; is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by in Lean, corresponding to the paper’s index . The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.
For the operator results, means bounded and measurable real functions. The suprema defining and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece corresponds to the paper’s , with rules .
An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.
In network design games, selfish users build a shared network and split the cost of every edge among the users of that edge. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008), DOI 10.1137/070680096) studied the fair connection game, in which the cost of an edge is shared equally (the Shapley value) among its users. In this game the worst equilibrium can cost times the optimum, so the relevant measure is the price of stability: the ratio between the cheapest pure Nash equilibrium and the optimal centralized design. Their Theorem 2.1 bounds it by the harmonic number in every directed graph, and that bound is tight for directed graphs.
For undirected graphs the paper notes that is not tight and calls the correct bound "an interesting open problem". Its Section 4 settles the smallest case: two players with a common terminal. The general theorem gives there; Claim 4.1 improves this to , and a three-node example shows that is the right value.
Timeline. Rosenthal (1973) showed that congestion games have pure Nash equilibria through a potential function. Anshelevich et al. (FOCS 2004; journal version 2008) introduced the price of stability for the fair connection game, proved the bound and the two-player undirected bound treated here. Subsequent work studied the undirected multi-player case, which remains without a matching upper and lower bound in general.
Let be a finite undirected simple graph, with a cost on every edge . There are two players, a common terminal and personal terminals . A strategy of player is a set of edges that connects with : in the graph , and lie in the same connected component. A profile is a pair of strategies.
Under fair cost sharing each edge is paid for equally by the players using it. With the number of players whose strategy contains , player pays
A pure Nash equilibrium is a profile in which no player can lower its payment by switching to another strategy while the other player's strategy stays fixed. The total cost of a profile is the cost of the network it builds,
For a set of edges write . For a profile , the quantities , and split the total cost into the private and the shared parts.
The game is an instance of a congestion game, with per-user latency on edge ; the mission builds on the published congestion-game layer CongestionPoA.AsymSum.Model.
If the game has a profile, then some pure Nash equilibrium satisfies
Moreover, in the three-node example (nodes , edges of cost , edge of cost , with ) the cheapest pure Nash equilibrium costs exactly and the optimum costs exactly , so the ratio approaches .
The result shows that the price of stability of fair cost sharing depends on the network: the bound, tight for directed graphs, is not tight for undirected ones even with two players. It is the first undirected bound below and the starting point for the later study of undirected fair network design, where the question for many players is still open.
The theorem is proved in the paper; this mission formalizes it. A search of the Prove2Me library found no formalization of the price of stability of fair connection games. Beyond the theorem itself, the mission produces a reusable undirected layer over the congestion-game library: connectivity strategies stated with Mathlib's graph reachability, fair cost sharing as a congestion game, and the total-cost functional. A checked proof of the potential inequality (4.1) is the two-player case of the potential argument behind Theorem 2.1.
The obvious argument starts from an optimal solution, follows improving moves to an equilibrium and compares potentials. For two players this only yields the factor : the potential counts shared edges with weight , so a potential inequality alone cannot rule out an equilibrium in which both players share expensive edges. The improvement to needs a second inequality, (4.2), obtained from a specific deviation of each player in the equilibrium, and that deviation is valid only because of the undirected structure: the private parts of the two optimal paths together connect with , and the deviating player can then follow the other player's equilibrium route to . Making this connectivity claim precise for edge sets rather than drawn paths is where the formal work lies. It holds when the optimal strategies are inclusion-minimal, which is why the deviation milestones carry that hypothesis.
Fintype with decidable equality; edges are unordered pairs Sym2 V; the graph is a SimpleGraph V. Edge costs are a real function c with 0 ≤ c e for every e.i : Fin 2 (the paper's players 1 and 2 are 0 and 1) is a Finset of edges contained in G.edgeSet such that t i and s are Reachable in SimpleGraph.fromEdgeSet. Strategies are not restricted to paths.CongestionGame from CongestionPoA.AsymSum.Model with latency ; profiles, player costs and pure Nash equilibria are that library's IsProfile, cost and IsPureNash.Contributions welcome: a proof of the potential inequality (finite improvement paths in the two-player fair game), the graph-theoretic lemma that the symmetric difference of two simple paths with a common endpoint connects their other endpoints, and a computation of the three-node example.
Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.
Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the -stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.
Let (states) and (controls) be sets, and for each let be a nonempty control constraint set. Write and let be the set of all functions , ordered pointwise. A mapping is given, subject to the Monotonicity Assumption: implies for all , .
A selector is a function with for all . A policy is a sequence of selectors. Define
and let be the -fold composition of . A terminal function with for all is fixed. The -stage cost of and the -stage optimal cost are
A policy is uniformly -stage optimal if each tail is -stage optimal, and -stage -optimal if where and where .
The three conditions on used in the chapter are F.1 (continuity of along nonincreasing sequences with ), F.2 (there is with for all ), and F.3 (a quantitative selection property with a constant ).
Under F.1, if for all and ; or under F.2, if for all and :
and under F.2, for every there is with .
The identity says that an infimum over an infinite-dimensional policy space equals nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in . Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.
These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.
The obvious argument interchanges the infimum over policies with the composition of operators: . The inequality follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside (F.1) or bounding how errors at later stages propagate through (F.2, F.3). Both steps break at infinite values. With there may be no -optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is , which is why F.3 and the definition of -optimality have two cases.
The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. is m.T^[N], and is a recursion that applies first. All values lie in EReal. The book's convention never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns when the positive part diverges). Every theorem assumes and . Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants and .
is defined as an infimum over policies of the composed operators, never through , so the goal is not true by definition. A formalization in which already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.
Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.
Many large convex programs have the form "minimize a strictly convex function subject to linear equations ". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of .
L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets , in which each step replaces the current point by its -projection onto one set: the minimizer of a distance-like function over that set. §2 chooses from the objective itself, with the gradient of ; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.
Work in the Euclidean space with inner product . Let be a convex set with closure and interior . Let be strictly convex and continuously differentiable over , with gradient at , and continuous over . Let be an matrix with nonzero rows and . The problem (2.1)–(2.3) is
with feasible set , assumed nonempty. A point of minimizing over is a solution.
The function (1.4) is
and also denotes the hyperplane . The paper assumes that satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every , a -projection minimizing over . It also assumes condition (2): if and , then .
A relaxation sequence with control starts at and sets . The control is any sequence of row indices. Finally,
is the set of points of at which the gradient lies in the row space of .
Assume that the -projection of every point of onto every lies in . For every control and every relaxation sequence with that converges to a point ,
Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.
An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.
Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for .
The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.
The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of , so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on , the limit may lie on the boundary of (or outside , in ), and need not extend continuously there, so the multipliers need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at . Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that preserves ; on the boundary of a minimizer over need not satisfy (2.7).
The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and is the real inner product. The gradient is explicit data tied to by HasGradientWithinAt f (g x) S x for and continuous on ; is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:
lam.The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open , or to a limit assumed to lie in : any of these would trivialize the passage to the limit that the theorem is about.
A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality for , , and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.
A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function that represents evaluation at is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.
Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.
Let be an arbitrary set and subsets with union . For each let be a complex Hilbert space of functions on , with norm , in which point evaluations are continuous; , for , is its reproducing kernel, characterized by and
with the scalar product linear in . For and , denotes the restriction of to . The standing assumptions of §9 A (p. 362) are:
together with the existence of every kernel . For two kernels on a set , means that is a positive matrix: for all finite families , . is the restriction of to .
The limit class is the set of functions on such that (1°) every restriction belongs to and (2°) .
Under the standing assumptions there is such that, whenever ,
and is the reproducing kernel of with the norm
The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With for all (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of in every .
Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over , with kernels on varying domains.
The kernels live on different sets , so convergence is not convergence of a sequence of functions on one set: a pair enters the sequence only from the first containing both. The identification of the limit class needs three separate facts: that with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that , and that reproduces. The natural first idea, to embed all in one space and take an intersection, fails: the are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.
H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set is a type X with no topology, measure or nonemptiness assumption.kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's is ⟪g, f⟫_ℂ.IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on . Indexing starts at .KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).ComplexOrder, which also asserts that these values are real.Tendsto).RKHS.OfKernel K₀ and then asserts that its kernel is would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.
Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.
Let be an arbitrary set and let be a class of complex-valued functions on that forms a complex Hilbert space with scalar product , linear in and conjugate-linear in . A reproducing kernel of is a function such that, for every , the function belongs to and
Such a kernel exists exactly when every point evaluation is continuous.
For a bounded linear operator on , with adjoint defined by , the kernel of is
the value at of the element of . By the reproducing property, for every and , so is determined by .
A function is a positive matrix if for every finite family of points and complex numbers . For two arbitrary functions on , one writes if is a positive matrix. A bounded operator is symmetric if , and positive if for every . A symmetric has lower bound and upper bound if
A kernel is hermitian symmetric if .
For an arbitrary hermitian symmetric function and real numbers :
The function is not assumed to have ; that membership is part of what the condition yields.
Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities ) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.
All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.
The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: is an arbitrary function, and the hypothesis is only about finite families of points. One has to produce an operator on all of . The obvious attempt, defining on the dense span of the functions by the kernel and extending by continuity, needs the bound on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of and does not by itself give the membership , which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of , while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.
RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function is the element RKHS.kerFun H y 1.L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point with , and , the kernel is .Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume and neither does the statement: for both sides hold exactly when and .H, and that the kernel of L₁ ∘L L₂ is their scalar product.⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by this contains the paper's over ; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in correspond to operators of finite norm) needs the direct product and is not stated.RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function with is the kernel of an operator , and the inclusion theorem , both reusable beyond this mission.Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012
The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2
Let be a finite ground set, and let assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value among all . Write for that value when no confusion arises, and for a set attaining it. Submodularity means
There is no monotonicity or normalization assumption: and may both be positive. A value oracle returns for a requested subset . The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2
Algorithm 2 visits the elements once in an arbitrary order . It keeps two sets, starting at and . At step , it measures the gain from adding to and the gain from removing from . It clips each gain at zero, giving and . It adds to with probability and otherwise removes it from . When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2
The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:
The milestone statements retain the paper's key local quantities. For a comparison optimum , set . Lemma II.1 asserts . The endpoint statement identifies and . Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of with the expected combined change of and . The telescoped display keeps the initial endpoint values and before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2
A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities , let . The maximum of is exactly the optimal welfare of a two-player partition. Algorithm 2 on is asked to satisfy
This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)
The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4
This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.
The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of alone does not control the movement of . The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of . Buchbinder et al., proof of Lemma III.1
The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.
The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.
The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints for in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in , a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.
In a network design game each player must connect its terminals in a graph whose edges carry fixed costs, and the cost of an edge is split among the players that use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008)) studied the fair (Shapley) split, in which the users of an edge pay equal shares. That game is a congestion game in the sense of Rosenthal (Int. J. Game Theory 2 (1973)), so it has an exact potential and pure Nash equilibria always exist.
Section 6 of the same paper turns to weighted players: player has a weight (a traffic volume, a bandwidth demand, a share of ownership) and pays for each edge it uses a share proportional to its weight. The equal-split potential is then lost, and the paper notes that weighted games with three or more players need not have a pure Nash equilibrium at all (Chen and Roughgarden, Network design with weighted players, SPAA 2006). Theorem 6.3 identifies a natural class in which equilibria survive: all players share one source and one sink. For that class it shows more than existence. The simplest decentralized procedure, letting players in turn switch to a cheapest route, always stops, and where it stops is an equilibrium.
A finite directed multigraph has a finite set of arcs; each arc has a tail and a head vertex, and parallel arcs between the same two vertices are allowed. Fix a source and a sink . A simple – path is a sequence of arcs (), each starting where the previous one ends, beginning at , ending at , and visiting no vertex twice; it is identified with its arc set . Write for the finite set of these paths.
The weighted single-commodity game has a finite set of players; player has a weight , arc has a fixed cost , and every player's strategy set is . In a profile let
be the total weight on arc . Player pays
A profile is a (pure) Nash equilibrium if no player can lower its payment by switching alone to another path.
A best-response move of player replaces by a path that minimises 's payment given the other players' paths, provided this strictly lowers 's payment. Best-response dynamics is any sequence of profiles in which each profile arises from the previous one by a best-response move of some player.
For every such game with and :
The goal asserts only termination and existence; it fixes no bound on the length of a run.
For a profile define the marginal cost of a path, , and the tuple of all values , , sorted increasingly. With strictly positive arc costs:
The theorem gives a guarantee about dynamics, not only about existence: in single-commodity weighted network design, any order in which players take turns playing best responses reaches a stable outcome in finitely many steps. This places the single-commodity case on the positive side of the boundary drawn by the nonexistence examples for general weighted games. The tuple of sorted path costs is a potential that is not a single number, a device that applies to other games without an exact potential.
The result is proved in the paper; it has no machine-checked proof that this mission is aware of. A formal development contributes a reusable layer for weighted cost-sharing games (payments, best responses, Nash equilibria on arbitrary strategy families), a treatment of simple directed paths in multigraphs as strategy sets, and a lexicographic termination argument over sorted lists of extended reals. The goal is stated for nonnegative costs, as in the paper's model, while the printed proof uses positive costs; closing that gap is part of the work.
The obvious route, finding a real-valued function that every improving move decreases, is unavailable: the paper notes that Rosenthal's potential is not a potential once weights are added, and that improving moves can increase it. Termination must instead come from an ordinal quantity, a whole sorted list compared lexicographically, and the move of one player changes the marginal costs of every path that shares an arc with the old or the new route, in both directions.
The argument also depends on the shape of the strategy sets. Two distinct simple – paths are never nested as arc sets; with walks that repeat vertices, or with arbitrary strategy families, the comparison between a path's marginal cost before and after a deviation can fail. Arcs of cost zero create a further gap: is on an unused free arc, and the strict inequalities of the proof degenerate, so the nonnegative-cost goal needs more than the printed argument.
Finset of arcs; the strategy family of every player is the finite set of arc sets of simple – paths (a list of consecutive arcs with distinct visited vertices). There are no paths when .IsStandard); the milestones (6.1) and the lexicographic decrease assume .ℝ≥0∞): an unused arc of positive cost contributes . Computing it in the reals, where , would make unused paths free and the milestones false.Contributions welcome: lemmas on simple paths in multigraphs (non-nestedness), the multiset-to-sorted-list lexicographic comparison, and the treatment of zero-cost arcs.
We establish the polynomial simulation needed for WordRAM-based NP proofs. It reuses the same machines and Cook–Levin definitions, with uniform programs, logarithmic word widths, and standard bit input/output.
The targets cover function outputs and verifier verdicts, including loading and serialization costs.
This adapts Cook–Reckhow’s Theorem 2(a), pp. 361–363, to Hagerup’s bounded-word operations, including multiplication; no particular simulation exponent is prescribed.
Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.
Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting procedure is the standard algorithm for the problem written in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.
A finite, nonempty set of jobs is processed on a single machine, one job at a time and without interruption. Each job has a processing time and a cost function that is monotone nondecreasing. The value is the cost incurred when is completed at time .
The precedence constraints are an arbitrary relation on jobs: means that job is required to precede job . A sequence lists every job of once. It observes the precedence constraints if never holds for positions . The machine starts at time with no idle time, so the completion time of is . The maximum incurred cost of is
and a feasible is minmax optimal if for every feasible .
For a set of jobs, is the set of jobs of that are not required to precede any other job of , and . Lawler's rule builds a sequence from the last position to the first. With the jobs not yet placed, it chooses with , places in the latest open position and removes it from . Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible (), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.
Every sequence that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies
This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.
The result shows that is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the partial sums along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.
The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets and times to be the correct ones at each stage, which the definitions fix.
The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set and the time must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.
A first attempt often proves only the Theorem, that some optimal sequence has last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of with last need not restrict to an optimal sequence of . Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.
ι with decidable equality, and the job set is J : Finset ι.a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in (the "others" of the page exclude the job itself).The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing for , and nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative (), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.
The rule is the property IsLawlerSequence of a finished sequence. At each position , the job there lies in of the jobs in positions and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.
The operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.
In a network design game each of players must connect its own terminals in a shared graph, and the cost of every edge that is bought is split among the players who use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008) studied the fair (Shapley) split, in which the users of an edge each pay . That game is a congestion game in the sense of Rosenthal (Networks 1973), so it has an exact potential function and pure Nash equilibria always exist.
When players carry different amounts of traffic, the natural rule is to split an edge's cost in proportion to weight: a player of weight on an edge whose users have total weight pays . The paper notes that this rule is analogous to weighted generalizations of the Shapley value (Monderer and Samet, Variations of the Shapley Value, Handbook of Game Theory III, 2002). The weighted model leaves Rosenthal's framework: the share depends on which players use an edge, not only on how many, and Chen and Roughgarden (SPAA 2006) showed that weighted games with three or more players need not have a pure Nash equilibrium at all. Section 6 of the paper identifies structural conditions under which equilibria do exist. This mission covers the first of them.
Timeline. Rosenthal (1973): every congestion game has a pure Nash equilibrium, via an exact potential. Monderer and Shapley (GEB 1996): potential and weighted potential games, and the equivalence of exact potential games with congestion games. Anshelevich et al. (FOCS 2004, journal 2008): Theorem 6.1, existence when every resource is shared by at most two players, and Theorem 6.3, existence when all players share a source and a sink. Chen and Roughgarden (2006): weighted network design games with three or more players may have no pure equilibrium.
A weighted cost-sharing game consists of a finite set of players, a finite ground set of edges (resources), and for each player :
together with a fixed edge cost for every . A profile picks for every player. For an edge , is the total weight of the players with , and player 's payment is
A profile is a pure Nash equilibrium when no player has a with , where is the profile in which plays and everyone else keeps their strategy.
The strategy space of player is the set of edges that occur in at least one strategy of . The hypothesis of Theorem 6.1 is that every edge lies in the strategy spaces of at most two players: no edge can ever be shared by three players, whatever they choose.
The network design game is the instance in which is the edge set of a graph and is the set of edge sets of paths connecting player 's source to its sink .
The paper's proof uses an explicit function with when is unused, when alone uses , and when and both use it, where . It is part of the definitions of this mission.
If every edge lies in the strategy spaces of at most two players, there is a weighted potential: a real function on profiles with
and, if every is nonempty, a pure Nash equilibrium exists. The goal asserts the existence of such a rather than fixing the paper's formula, so it remains valid for any other weighted potential.
An extra item states Corollary 6.2: every two-player weighted game with nonempty strategy sets has a pure Nash equilibrium.
The result. Theorem 6.1 is one of the two existence results the paper proves for weighted cost sharing, a game that in general has no pure equilibrium. It shows that the obstruction found by Chen and Roughgarden needs resources shared by three or more players: whenever sharing is limited to pairs, the game is a weighted potential game, so improving moves cannot cycle and equilibria exist. Corollary 6.2 makes the two-player case unconditional, and the paper notes that the same potential gives a (weak) bound on the price of stability.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a reusable Lean model of weight-proportional cost sharing (shared in form with the companion mission on single-source single-sink weighted games), an explicit weighted potential, and the general step from a weighted potential to a pure equilibrium, which applies to any finite game with positive weights.
The obvious approach, reusing Rosenthal's potential from the unweighted game, fails: the paper observes that in a weighted game improving moves can increase it. A player's share of an edge depends on the weights of the specific co-users, so no function of the edge loads alone can track all players' costs. The identity must therefore hold for every unilateral move, including moves that leave some edges and join others at the same time, and for every pair of possible co-users of an edge. The statement fails without the at-most-two hypothesis, so any argument has to use it in an essential way. The existence step needs the identity on all profiles reachable by feasible deviations, not only along a single path of moves.
Lean namespace PriceOfStability.WeightedPotential. Players form a Fintype ι and edges a Fintype E; a game is a structure with strategies : ι → Finset (Finset E), weight : ι → ℝ and edgeCost : E → ℝ. Standing assumptions wᵢ ≥ 1 and c_e ≥ 0 are the predicate IsStandard. Profiles are functions ι → Finset E with the feasibility predicate IsProfile; every deviation is to a feasible strategy, via Function.update. Nash equilibria are pure and in cost form. The strategy-space hypothesis is a bound on the number of players whose strategy space (the union of their strategies) contains each edge — not a bound on the users in one profile, which would be a different statement. Φ_e is computed from the current users of e; its value with three or more users is a placeholder that never arises under the hypothesis. Strategies are arbitrary subsets of the ground set, as the paper's remark after the proof allows, so the network game is a special case.
The goal is not satisfiable trivially: the function Φ must satisfy the weighted identity for every feasible unilateral deviation from every profile, and an exact (unweighted) potential is not what is asserted. Nonempty strategy sets are added explicitly for the existence part, since without a profile there is no equilibrium.
Needed infrastructure: finite sums over filtered Finsets, the improvement-path argument over the finite set of profiles. The improvement-path lemma (milestone 3) is reusable for any weighted potential game. Contributions of proofs for any milestone are welcome.
Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.
Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).
Timeline:
A network has single-server stations and job classes. Class is served at station , and is the set of classes served at station . Class- jobs arrive from outside as a Poisson stream of rate , service times are exponential with rate , and after service a class- job becomes a class- job with probability or leaves with probability . The traffic equations
have a unique solution (the network is open), and at every station.
The state counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write for the event that station serves class , and for the event that station is idle. Under such a policy is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution and that for all . Let , which equals with the mean response time of class (Little's law), and define
For a set of classes, f-parameters are reals for such that is nonnegative and the same for all ; that common value is , and when (restriction (17)). The sums over include the exit .
For every policy satisfying Assumption A, every and every f-parameters satisfying (17),
where
The formal goal is the product form .
Theorem 4.1 gives, for each choice of and , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables implies all of these inequalities at once, so the parametric search over is unnecessary.
The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.
Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions (, ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending to quadratic needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify with . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because on , and at most one class per station is in service.
Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs of the paper are not built: the paper notes that its expectations at are expectations under the invariant distribution of .
Conventions fixed in Lean:
A quotient-form statement of (18) would be trivially true when , and defining as would make the utilization identity hold by definition; both are excluded.
Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.
The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.
The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.
There are trials. Trial offers alternatives, indexed by and . Alternative has an attribute vector , and counts how many times it was selected in that trial. Each trial has at least two alternatives and observations. The vector is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative a probability proportional to , with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).
For the test, define the weighted difference
It is indexed by every trial and every ordered pair of alternatives, including and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.
Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank . Equivalently, the vectors span ; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction satisfies for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.
Let be the set of feasible vectors
The mission's goal is the equivalence in Lemma 4:
The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).
Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.
The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.
The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints in equation (22). Both conditions must appear in their proper places.
The full-rank condition alone does not ensure that the vectors span the attribute space if a trial has no observed choices. The section describes repetitions of each trial, and the formal data require . This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.
Lean represents a nonempty set of trials by Fin N, alternatives in trial by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count is the sum of observed choice counts. The model requires and for each trial. There is no extra assumption that : the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.
Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.
The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.
The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).
The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.
There are agents , each with a nonnegative value , and goods indexed in decreasing order of nonnegative weight:
An assignment gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by with . Its value is . Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order , chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.
The offline optimum, , assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If , the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.
The reservation algorithm draws a sample size , observes the first agents without allocation, and retains the best sampled agents. Positive values are grouped into value classes for integer . A sampled agent in class reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first agents, then selects the first later arrival better than every predecessor; its winner receives good .
The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm , which runs the reservation algorithm with probability and the classical rule with probability :
Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.
Four source results form the milestones. The classical secretary rule selects the maximum with probability at least . Lemma 3.2 compares the starting indices and of class- blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class , the reservation rule assigns at least agents from that class in expectation. Lemma 3.3 converts this to expected value at least . The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).
Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with or . It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).
The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.
A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).
Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time corresponds to Lean index . An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by for permutations and by for sample sizes. No measurability or integration convention is needed. For the goal, makes the heaviest good available; is allowed.
Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class holds the values “between” and (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval , so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.
The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.
A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor tends to the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats as a limit of : it expands the discounted return of a stationary policy in powers of and reads off which policies remain good as . The two leading coefficients of that expansion, the gain and the bias , became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).
Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all near (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through and . Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders (-discount optimality).
There are finitely many states and a finite nonempty set of actions. Action in state pays an income and moves the system to with probability . is the finite set of decision rules . A policy is a sequence of decision rules; uses every day, and uses first and then . For , is the vector and the Markov matrix . The discounted return of is the vector
and abbreviates . Vectors are compared coordinatewise; means and . A policy is β-optimal if its return dominates that of every policy, and is the return of a β-optimal policy. It is optimal if it is β-optimal for all sufficiently near , and nearly optimal if as .
For any Markov matrix , the limit matrix is the limit of , and the deviation matrix is . For a rule , and are those of , and
With , the set consists of the actions with , or with and ; consists of those with equality in both.
For any with for all :
Milestones: Lemma 1(b) (), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).
The mission also states, as intermediate results:
Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income , then of the bias . It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.
The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.
Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through .
States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's . is a real tsum. is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; is a matrix tsum, whose summability for is part of Lemma 1(d); uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). and are defined by the closed forms and from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along . "Nearly optimal" is encoded without : for every , for all β in some interval , every policy's return is at most in every coordinate; this is equivalent to because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set .
A formalization in which optimality or near optimality is tested only against stationary policies, or in which is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.
Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.
Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).
The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio , where is the number of elements and the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).
This mission formalizes the core of the weighted result: the algorithm that is given a value at least the optimal cost, and its guarantee (Theorem 3.4).
The ground set has elements and the family has sets; every set has a cost . Both are known to the algorithm in advance. For an element , denotes the sets containing . Elements of an unknown subset of arrive one at a time in a sequence ; on arrival each must be covered by a chosen set. The chosen family can only grow. is any family covering every arriving element, and .
The algorithm is given . It discards sets costing more than , buys sets costing at most outright, and rescales costs; on the resulting normalized instance and for every set (p. 365).
The algorithm keeps a weight for every set, initially ; the weight of an element is . With the set of covered elements and the indicator of , the potential is
with natural logarithms throughout. When arrives with nothing happens; otherwise the algorithm performs weight augmentation steps while . In a step, for each : (a) ; (b) if , add to when does not exceed its value before (a); (c) if has increased, return FAIL.
In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.
On the normalized instance, with covering , , and , every reachable configuration is a running state (never FAIL) in which (i) every with is covered, and (ii)
The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant assumed) is included as a supporting reference.
Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic -competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.
The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis . Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the terms replaced by explicit expressions.
The cost bound in the last step is short once two facts about the run are available: that stays below , and that the fractional cost stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add or not) does not increase ; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most . The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers , where the initial bound is a genuine size condition on and .
The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by .
Conventions: costs, weights and are real; and are the cardinalities of the finite types cast to ; is Real.log; and are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:
The goal is a statement about the configurations the algorithm actually reaches from and the empty cover. Taking the invariant or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown is not part of this mission.
A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.
In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.
The paper gives a deterministic online algorithm whose cost is within a factor of the offline optimum, where is the number of elements and the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of and , every deterministic online algorithm has competitive ratio . The lower bound is the reason the product, rather than the of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.
This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.
A ground set and a family of distinct subsets of are fixed and known to the algorithm; . An adversary presents elements of one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm , on the arrival of , sees the earlier arrivals and , and adds a finite family of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of , that element lies in a chosen set. After an arrival sequence the chosen collection is , and since every set has unit cost, the cost is . The offline optimum is the least number of members of covering the elements of . The competitive ratio of is at least when some arrival sequence has and .
Two families are used.
and the family consists of all ; it has members.
For all positive integers and all with
there is a family of exactly distinct subsets of an -element set such that for every valid deterministic online algorithm there is a nonempty arrival sequence , covered by a single member of , with
The goal leaves the instance existential, as the paper does, and keeps both bounds on and the bound on exactly as printed.
A supporting item (not a milestone) records the count of the block family.
The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing of order and of order turns it into the asymptotic bound , which shows that the paper's algorithm is optimal among deterministic algorithms up to a factor. Without it, the gap between the achievable offline and the achieved online would be unexplained. Proposition 4.1 alone gives the matching bound when .
Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.
The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only sets. To force sets with , the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most blocks after steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly elements and exactly distinct sets without creating sets that help cover the adversary's elements.
The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit (1-based) of is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).
The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set (), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies as .
The statements contain no : every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of and , is excluded, as are the remarks on the trivial ratio- and algorithms.
Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.
Set cover asks for the fewest sets from a family of subsets of a ground set of elements whose union contains . It is NP-hard, and the best ratio achievable in polynomial time is (Feige 1998, doi:10.1145/285055.285059).
Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.
The question is how much an algorithm loses against an offline adversary who knows and covers it with a family . This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor of . Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.
An instance consists of a finite ground set with elements and a finite family of sets. For an element , is the collection of sets containing . Every set has cost , so the cost of a family is its number of members.
The adversary gives a sequence of elements (the given elements form ). A family covers if each element of lies in some member of it.
The algorithm keeps a weight for every set, initially , and a cover , initially empty. The weight of an element is , and is the set of elements covered by members of . The potential is
When the adversary gives an element :
Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.
For , every arrival sequence , and every family covering : a run of the algorithm on exists, and every run ends with a cover that covers every element of and satisfies
The paper states ; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.
Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most
Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family with such that
where is the potential before the iteration and the potential after it, computed with the augmented weights and the cover .
The theorem shows that online set cover over a known instance admits a deterministic -competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.
The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.
The central step is Lemma 2.2: a family of at most sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of can exceed the cardinality bound, since may contain up to sets. Adding nothing, or a single set, can increase : every uncovered element sharing a set with has its weight raised, and its term grows by a factor up to . The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of .
The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs and a careful treatment of the initial potential, which is at most and equals when every element lies in every set.
The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight () and coveredBy (). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. and . Weights are real numbers; is the real power.
The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.
Explicit forms of the paper's asymptotic and unspecified quantities:
The goal adds the hypothesis , which the paper's assumes tacitly: for no set may be added and the element is never covered.
Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.
A complete development needs elementary real analysis (Real.rpow, Real.log, ), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.
The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form . Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.
That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" shared by all alternative sets.
Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes , the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.
Let be the universe of objects of choice and the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set ; a designated family of finite sets is the family of possible alternative sets. The selection probability is the probability that an individual drawn at random from the population, with attributes and facing , chooses . For every and possible , is a probability vector on . Whenever belong to a possible set, the pair is possible too, so binary choices are defined.
In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.
Under Axioms 1 and 2 and a universal benchmark , with , for every , every possible (containing or not) and every :
The function is the same for all alternative sets; this is what distinguishes the goal from Equation (10).
The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.
Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.
The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick as benchmark" produces a function that depends on the set through the choice of . The goal requires a single for all sets, including sets that do not contain , where neither Equation (10) nor the axioms on alone say anything about . A second subtlety is the diagonal: , so is set to by definition rather than read off a singleton choice.
Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.
The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit , never as "for each there is a ", which would only restate (10).
Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).