Algorithmic Game Theory V: Stable Matching and Trading without Money

Motivation

When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.

Setting

Marriage market (§10.4): finite sets $M$ of men and $W$ of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; $P\,i\,a\,b$ reads "$i$ strictly prefers $a$ to $b$"). Following the book's dummy-partner convention, $|M| = |W|$ and a matching is a bijection $\mu : M \simeq W$. A pair $(m, w)$ blocks $\mu$ if each prefers the other to their assigned partner; $\mu$ is stable if no pair blocks it. A stable $\mu$ is male-optimal if every man weakly prefers it to every stable alternative. A coalition dominates $\mu$ if it can rematch within itself with every member strictly better off; the core is the set of undominated matchings.

Housing market (§10.3): a finite set $N$ of agents, agent $i$ owning house $i$, each with a strict preference over all houses; an allocation is a permutation of $N$. A coalition blocks an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.

Formalization targets

Goal (capstone) — Theorem 10.13

Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.

Theorem 10.10 — existence

Every marriage market has a stable matching.

Theorem 10.11 / Gale–Shapley 1962 — male-optimality

Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.

Theorem 10.12 — the core

A matching is stable iff it is in the core of the matching game.

Theorems 10.6 and 10.7 — housing

The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.

Significance

These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.

Difficulty

Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.

Formalization scope

Preferences are strict total orders as in Mission III (IsPrefProfile), oriented "first argument preferred". Matchings are Equivs; the book's $|M| = |W|$ convention enters the existence statements as the hypothesis Nonempty (M ≃ W) and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching Equiv together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no Fintype.

Selected references

• D. Gale, L. S. Shapley, College admissions and the stability of marriage, Amer. Math. Monthly 69 (1962), 9–15. DOI
• L. Shapley, H. Scarf, On cores and indivisibility, J. Math. Econ. 1 (1974), 23–37. DOI
• L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley algorithm, Amer. Math. Monthly 88 (1981), 485–494. DOI
• A. E. Roth, The economics of matching: stability and incentives, Math. Oper. Res. 7 (1982), 617–628. DOI
• A. E. Roth, Incentive compatibility in a market with indivisible goods, Econ. Letters 9 (1982), 127–132. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 10. DOI

Motivation

Hassler Whitney introduced matroids in On the Abstract Properties of Linear Dependence (Amer. J. Math. 57, 1935, doi:10.2307/2371182) to capture what linear dependence among the columns of a matrix and the circuit structure of a graph have in common. One of the central constructions of the paper is duality. For graphs, duality exists only for planar graphs (Whitney, Non-separable and planar graphs, Trans. AMS 34, 1932); for matroids Whitney showed that every matroid has a dual, and that duality has a direct linear-algebra model: the matroid of a subspace of $\mathbb R^n$ and the matroid of its orthogonal complement are duals.

Matroid duality underlies much of combinatorial optimization: the duality between cycles and cuts in graphs, the relation between a linear code and its dual code, the exchange of rank and corank in matroid intersection and partition, and the treatment of network flows as duals of potential problems. Whitney's §§11–13 are where this structure is first defined and where its linear-algebra meaning (Theorem 28) is established.

Setting

A matroid $M$ is a finite set of elements $e_1,\dots,e_n$ with a rank function $r$ on its subsets; equivalently, a family of independent sets, or of bases (maximal independent sets). For a subset $N$ write $\rho(N)$ for its number of elements and

$$n(N) = \rho(N) - r(N)$$

for its nullity; $r(M)$ and $n(M)$ are the rank and nullity of the whole set of elements.

Duality (§11). Let $M$ and $M'$ be matroids and $\sigma$ a one-to-one correspondence between their elements. $M'$ is a dual of $M$ (via $\sigma$) if, for every subset $N$ of $M$, with $N'$ the complement in $M'$ of $\sigma(N)$,

$$r(N') = r(M') - n(N). \tag{11.1}$$

The matroid of a subspace (§12). Let $E_n$ be $n$-dimensional Euclidean space with coordinates $x_1,\dots,x_n$, and let $H$ be a hyperplane through the origin, which in Whitney's usage is a linear subspace of any dimension. For a set $S$ of coordinates, project $H$ onto the coordinate subspace $E'_S$ spanned by the axes $x_i$, $i\in S$. The matroid associated with $H$ has elements $e_1,\dots,e_n$, one per coordinate, and gives the set $\{e_i: i\in S\}$ the rank

$$r_H(S) = \dim \pi_S(H).$$

If $H$ is the row space of a matrix $\mathbf M$, then $r_H(S)$ is the rank of the columns of $\mathbf M$ indexed by $S$, so the associated matroid is the column matroid of $\mathbf M$.

In the Lean development these objects are WhitneyMatroid.Components.nullity (shared), IsDualVia M M' σ, IsDual M M', subspaceRank H S and IsAssociated M H.

Formalization targets

Goal: Theorem 28

Let $H$ be a subspace of $E_n$ and $H' = H^\perp$ its orthogonal complement. If $M$ and $M'$ are the matroids associated with $H$ and $H'$, then $M$ and $M'$ are duals under the correspondence of equal coordinates:

$$\forall N\subseteq\{e_1,\dots,e_n\}:\qquad r_{M'}(\overline N) = r(M') - n_M(N).$$

Milestones

1. Theorem 27. For every subspace $H$ there is exactly one matroid associated with $H$.
2. Theorem 6 (already proved on the platform). All bases have the same number of elements.
3. Theorem 7. $B$ is a base iff $r(B)=r(M)$ and $n(B)=0$.
4. Theorem 8. If $B$ is a base and $N$ is independent, then $N\cup N'$ is a base for some $N'\subseteq B$.
5. Theorem 20. If $M'$ is a dual of $M$, then $r(M') = n(M)$ and $n(M') = r(M)$.
6. Theorem 23. $M'$ is a dual of $M$ via $\sigma$ iff, for every $B$, $B$ is a base of $M$ exactly when the complement of $\sigma(B)$ is a base of $M'$.
7. Theorem 21. Duality is symmetric.
8. Theorem 22. Every matroid has a dual.

Significance

The result. Theorem 28 identifies abstract duality with orthogonal complementation. With Theorem 23 it says that the column matroid of a real matrix whose rows span $H$ and the column matroid of a matrix whose rows span $H^\perp$ have complementary bases. This is the basis of the standard representation of the dual of a represented matroid ($[I_r\mid A]$ and $[-A^{\mathsf T}\mid I_{n-r}]$), of the cycle/cocycle duality of graphs viewed through incidence matrices, and of the fact that a matroid representable over a field has a dual representable over the same field. Theorems 20–23 are the basic facts every later treatment of matroid duality starts from: duality exchanges rank and nullity, is symmetric, always exists, and is characterized by base complements.

Formalizing it. All of these results are classical and proved in Whitney's paper; what this mission adds is a machine-checked development of Whitney's own definition of duality, the rank identity (11.1), rather than the base-complement definition used in modern libraries. Mathlib defines the dual matroid $M^*$ by base complements and proves that it is a matroid; it does not, at the pinned revision, contain the rank formula (11.1) for $M^*$, the matroid of a real subspace, or Theorem 28. Theorem 6 is already proved on the platform and enters as a reference. Theorems 7 and 8 are close to Mathlib lemmas and are footholds rather than new content.

Difficulty

The difficulty of the goal is not in the combinatorics but in the passage between the two descriptions of a subspace. The natural first idea is to compare the ranks $r_H(S)$ and $r_{H^\perp}(\overline S)$ directly by counting dimensions of $H$ and $H^\perp$. This does not close: $r_H(S)$ is the dimension of a projection of $H$ onto coordinates, while $\dim H^\perp = n - \dim H$ only controls $H^\perp$ as a whole, and the rank of a complementary coordinate set in $M'$ is not determined by the dimensions of $H$ and $H^\perp$ alone. Some relation between coordinate projections of $H$ and the structure of $H^\perp$ on the complementary coordinates has to be established. Theorem 27 is itself nontrivial in Lean: the rank function $r_H$ has to be shown to satisfy the matroid axioms, which needs a careful treatment of coordinate projections and of submodularity of dimension. On the abstract side, Theorem 23 needs both directions of the passage between the rank identity and base complements, including the counting step $r(M) + r(M') = \rho(M)$.

Formalization scope

• Matroids are Mathlib Matroid α on a finite type α whose ground set is all of α (Whitney's matroid is its finite set of elements). This finiteness and the ground set convention are part of the definitions; all theorems are stated under them.
• Ranks and nullities. Ranks are Mathlib's eRk, finite on a finite type and converted to integers; the nullity $n(N)=\rho(N)-r(N)$ and the identity (11.1) are computed in $\mathbb Z$. No truncated subtraction appears.
• Duality is Whitney's rank identity (11.1) for every subset, for a fixed bijection σ : α ≃ β (IsDualVia) or some bijection (IsDual). It is deliberately not defined as Mathlib's M✶: with that definition Theorem 23 would be nearly definitional and Theorem 28 would lose the rank identity. A formalization that replaces (11.1) by the base-complement condition, or states Theorem 28 only for bases, is not this mission's goal.
• Euclidean space is EuclideanSpace ℝ (Fin n) with its standard inner product; the orthogonal hyperplane is Hᗮ. The field is $\mathbb R$, as in the paper; the analogous statement over other fields with the dot-product annihilator is a generalization and not part of this mission.
• The associated matroid is a predicate (IsAssociated M H): ground set Fin n, and the rank of every set $S$ of coordinates equals the finrank of the image of $H$ under the coordinate projection onto $S$ (not of $H\cap E'_S$, a different set function). Existence and uniqueness is Theorem 27.
• Implicit hypotheses made explicit: the ground sets are finite and equal to the whole element type; Whitney's "dimension $r$" and "dimension $n-r$" in Theorem 28 are consequences of $H'=H^\perp$ and are not hypotheses. The goal covers $n=0$, $H=\{0\}$ and $H=E_n$.
• Infrastructure needed and reusable: the matroid of a real subspace (equivalently the column matroid of a real matrix), with its rank function in terms of coordinate projections; the rank formula of the dual matroid; the dimension identity relating projections of $H$ and sections of $H^\perp$. All are reusable for the other missions of this series (the Fano matroid and binary matroids) and for any later work on represented matroids. Proofs of the milestones, alternative proofs of Theorem 28 through Mathlib's M✶, and supporting lemmas on coordinate projections are welcome.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011, Chapter 2 (duality). https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• Mathlib, Mathlib.Combinatorics.Matroid (Dual, Rank). https://github.com/leanprover-community/mathlib4

Motivation

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.

Setting

Let $M$ be a finite set of elements. For subsets we write $N + e$ for $N \cup \{e\}$ and $P_1 + P_2$ for $P_1 \cup P_2$.

Rank system. A function $r$ assigning an integer $r(N)$ to each $N \subseteq M$ satisfies the rank postulates if

• $(\mathrm R_1)$ the rank of the null subset is zero;
• $(\mathrm R_2)$ for any subset $N$ and any element $e$ not in $N$, $r(N+e) = r(N) + k$ with $k = 0$ or $1$;
• $(\mathrm R_3)$ for any subset $N$ and elements $e_1, e_2$ not in $N$, if $r(N+e_1) = r(N+e_2) = r(N)$, then $r(N+e_1+e_2) = r(N)$.

With $\rho(N)$ the number of elements of $N$, the nullity is $n(N) = \rho(N) - r(N)$. An element $e$ is dependent on $N$ if $r(N+e) = r(N)$. A circuit of $r$ is a minimal dependent set: a subset $P$ with $n(P) > 0$ such that $n(N) = 0$ for every proper subset $N$ of $P$. 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 $N$.

Formalization targets

Goal: the two systems are equivalent

For every finite set $M$:

$$\text{(1)}\quad r \text{ satisfies } (\mathrm R) \;\Longrightarrow\; \mathcal C(r) \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C(r),\ r_{\mathcal C(r)} = r;$$ $$\text{(2)}\quad \mathcal C \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C \;\Longrightarrow\; r_{\mathcal C} \text{ satisfies } (\mathrm R),\ \mathcal C(r_{\mathcal C}) = \mathcal C,$$

where $\mathcal C(r)$ is the family of circuits of $r$ and $r_{\mathcal C}$ is the rank defined from $\mathcal C$. 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."

Milestones, in the order the argument uses them

• Lemma 5 (p. 512): each element of a circuit is dependent on the rest of the circuit.
• Lemma 6 (p. 512): if $e \notin P_1$ is dependent on $P_1$ but on no proper subset of $P_1$, then $P_1 + e$ is a circuit.
• Theorem 4 (p. 512): for $e \notin N$, some circuit in $N + e$ contains $e$ if and only if $e$ is dependent on $N$.
• Theorem 5 (p. 513): if $N = e_1 + \cdots + e_p$ is formed element by element, $n(N)$ is the number of indices $i$ for which some circuit in $e_1 + \cdots + e_i$ contains $e_i$.
• §5 (pp. 512–513): the circuits of a rank system satisfy $(\mathrm C_1)$ and $(\mathrm C_2)$.
• Lemma 7 (p. 516): $r(e_1, \dots, e_{q-2}, e_{q-1}, e_q) = r(e_1, \dots, e_{q-2}, e_q, e_{q-1})$ under $(\mathrm C_1)$, $(\mathrm C_2)$.
• Lemma 8 (p. 517): the rank of a subset defined from circuits does not depend on the ordering of its elements.
• §8 (p. 517): the rank defined from circuits satisfies $(\mathrm R_1)$–$(\mathrm R_3)$.

Significance

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 $\Gamma_i$, 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.

Difficulty

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 $(\mathrm C_1)$, $(\mathrm C_2)$ obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where $(\mathrm C_2)$ does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, $(\mathrm C_2)$ for circuits of a rank function requires turning the local postulate $(\mathrm R_3)$ 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.

Formalization scope

• The elements form a finite type α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set $e_1, \dots, e_n$.
• Ranks and nullities are integers (ℤ), so that $n(N) = \rho(N) - r(N)$ is a true difference.
• Ordered sets of elements are lists. Lemmas 7, 8 and Theorem 5 assume the list has no repetitions, as Whitney's "ordered set of elements" means. "A circuit in $e_1 + \cdots + e_i$" means a circuit contained in $\{e_1, \dots, e_i\}$.
• The rank of a subset from circuits is computed along one fixed enumeration N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.
• Tacit hypothesis made explicit. Whitney's circuits are nonempty, since a circuit of a rank system has positive nullity. The family $\{\emptyset\}$ satisfies $(\mathrm C_1)$, $(\mathrm C_2)$ vacuously, but its circuit rank is $\rho$, which has no circuits, so the round trip fails. Part (2) of the goal therefore assumes $\emptyset \notin \mathcal C$, and part (1) asserts $\emptyset \notin \mathcal C(r)$.
• Lemma 6 assumes $e \notin P_1$, which the paper leaves tacit.
• Ruled out. Neither system may be encoded as Mathlib's 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 $(\mathrm R_1)$–$(\mathrm R_3)$ or invariance of rankSeq under prefix-preserving changes.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• Mathlib, Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4

Motivation

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.

Setting

A matroid $M$ on a finite ground set $E$ is given here by Mathlib's Matroid structure, with rank function $r(X)$ for $X\subseteq E$ (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset $X\subseteq E$ as a matroid in its own right, a submatroid, with the rank function of $M$ restricted to subsets of $X$. For sets he writes $M_1+M_2$ for the union, $\rho(N)$ for the number of elements of $N$, and

$$n(N) = \rho(N) - r(N)$$

for the nullity of $N$.

Rank is subadditive: $r(X_1+X_2)\le r(X_1)+r(X_2)$. A submatroid $X$ is separable if it can be divided into two disjoint groups $X_1, X_2$, each containing at least one element, with

$$r(X) = r(X_1) + r(X_2),$$

and non-separable otherwise. Every single element is non-separable. A component of $M$ is a maximal non-separable part of $M$: a nonempty non-separable set $K\subseteq E$ contained in no strictly larger non-separable subset of $E$.

Formalization targets

Goal: Theorem 19

For two distinct elements $e_1\neq e_2$ of $E$,

$$\bigl(\exists K \text{ component of } M:\ e_1, e_2\in K\bigr) \iff \bigl(\exists P \text{ circuit of } M:\ e_1, e_2\in P\bigr).$$

Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.

Milestones (§10, in the paper's order)

• Theorem 11. If $r(M_1+M_2)=r(M_1)+r(M_2)$, $M_1'\subseteq M_1$ and $M_2'\subseteq M_2$, then $r(M_1'+M_2')=r(M_1')+r(M_2')$.
• Theorem 12. Under the same rank additivity, a non-separable $M'\subseteq M_1+M_2$ lies in $M_1$ or in $M_2$.
• Theorem 13. Two non-separable sets with a common element have a non-separable union.
• Theorem 14. Distinct components are disjoint.
• Theorem 15. The components cover $E$, and no other family of components does.
• Theorem 16. A set is non-separable of nullity $1$ if and only if it is a circuit.
• Lemma 9. If $M_1+M_2$ is non-separable, with $M_1, M_2$ nonempty and disjoint, some circuit inside $M_1+M_2$ meets both.
• Theorem 17. A non-separable set of nullity $n>0$ is built from a circuit by $n-1$ steps, each adding a set of elements that forms a circuit with elements already present, through non-separable sets of nullity $1,2,\dots,n$.
• Theorem 18. For distinct nonempty non-separable $M_1,\dots,M_p$ covering $E$, the following are equivalent: they are the components; they are pairwise disjoint and no circuit meets two of them; $r(E)=\sum_i r(M_i)$.

Significance

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.

Difficulty

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 $e_1$ and $e_2$ requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from $e_1$ to $e_2$ gives a connected chain of circuits, not one circuit.

Formalization scope

• Representation. A matroid is Mathlib's Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset $X\subseteq$ M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid $M = M_1 + M_2$" are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid $M_1+M_2$.
• Ranks are Mathlib's ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in $\mathbb Z$ as the number of elements minus the rank.
• Definitions. IsSeparable M X requires two nonempty, disjoint groups with union $X$ and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds $X\subseteq$ M.E. IsComponent M K requires $K$ nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.
• Tacit hypotheses made explicit. In Theorem 19 the two elements are distinct: for $e_1=e_2$ a coloop is its own component and lies on no circuit. In Theorem 18 the sets $M_1,\dots,M_p$ are distinct and nonempty: a loop listed twice would satisfy (3) but not (2), and an empty set would satisfy (2) and (3) but not (1). In Theorems 11 and 12 the two parts need not be disjoint, as Whitney's use of $M_1+M_2$ for overlapping sets in Theorem 13 indicates; the statements hold in that generality.
• Ruled out. Components must not be defined as the classes of the relation "lie on a common circuit": that would make the goal a tautology. Here they are the rank-defined maximal non-separable sets of §10, and circuits are Mathlib's Matroid.IsCircuit.
• Infrastructure. Solvers will need submodularity of M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside $X$ (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.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• D. König, Acta Litterarum ac Scientiarum Szeged, vol. 6, pp. 155–179, as cited by Whitney in footnote 11 (p. 159 for the notion of "Glied").
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011, Chapter 4 (connectivity).

Motivation

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.

Setting

Let $M$ be a finite set of elements $e_1, \dots, e_n$. Following Whitney, write $N + e$ for $N \cup \{e\}$, $M_1 + M_2$ for the union and $M_1 M_2$ for the intersection of subsets; $\rho(N)$ is the number of elements of $N$.

A rank system is a function $r$ on the subsets of $M$ satisfying

• (R₁) $r(\emptyset) = 0$;
• (R₂) for every subset $N$ and element $e \notin N$, $r(N + e) = r(N)$ or $r(N + e) = r(N) + 1$;
• (R₃) for every subset $N$ and elements $e_1, e_2 \notin N$, if $r(N + e_1) = r(N + e_2) = r(N)$ then $r(N + e_1 + e_2) = r(N)$.

The nullity of $N$ is $n(N) = \rho(N) - r(N)$, and $N$ is independent when $n(N) = 0$. The increment of (3.1) is $\Delta(M', N) = r(M' + N) - r(M')$, written $\Delta(M', e)$ when $N = \{e\}$.

An independence system is a predicate "independent" on the subsets of $M$ satisfying

• (I₁) any subset of an independent set is independent;
• (I₂) if $N$ and $N'$ are independent and $N'$ has exactly one element more than $N$, then $N + e'$ is independent for some $e' \in N'$ with $e' \notin N$.

From an independence system one recovers a rank by letting $r(N)$ be the number of elements in a largest independent subset of $N$. In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.

Formalization targets

Goal: (R) and (I) are equivalent (§6, p. 514)

1. If $r$ satisfies (R₁)–(R₃), then $\{N : \rho(N) = r(N)\}$ satisfies (I₁), (I₂), contains $\emptyset$, and

$$r(N) = \max\{\rho(I) : I \subseteq N,\ \rho(I) = r(I)\} \quad \text{for every } N.$$

2. If "independent" satisfies (I₁), (I₂) and $\emptyset$ is independent, then $r(N) = \max\{\rho(I) : I \subseteq N \text{ independent}\}$ satisfies (R₁)–(R₃), and $N$ is independent if and only if $\rho(N) = r(N)$.

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 $M$ agree under the two systems".

Milestones

• Lemma 1 (p. 510): $r(N) \ge 0$, $n(N) \ge 0$, and $N \subseteq M'$ implies $r(N) \le r(M')$, $n(N) \le n(M')$.
• Lemma 2 (p. 510): any subset of an independent set is independent, which is (I₁).
• Lemma 3 (p. 511): $\Delta(M + e_2, e_1) \le \Delta(M, e_1)$.
• Lemma 4 (p. 511): $\Delta(M + N, e) \le \Delta(M, e)$.
• Theorem 3 (p. 511): $\Delta(M + N_2, N_1) \le \Delta(M, N_1)$; equivalently

$$r(M + N_1 + N_2) \le r(M + N_1) + r(M + N_2) - r(M), \qquad r(M_1 + M_2) \le r(M_1) + r(M_2) - r(M_1 M_2).$$

• §4 (pp. 511–512): the independent sets of a rank system satisfy (I₂).

Significance

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.

Difficulty

The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound $r(N) \le \rho(N)$ 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.

Formalization scope

Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid $M$ 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 $\rho(N) < \rho(N')$. Postulates (R₂), (R₃) keep their hypotheses $e, e_1, e_2 \notin N$. Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets $M, N, N_1, N_2$; Lemma 1's monotonicity for arbitrary $N \subseteq M'$, 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 $0$, and the round trip fails; the goal therefore assumes $\emptyset$ 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.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• J. Kung (ed.), A Source Book in Matroid Theory, Birkhäuser, 1986. https://doi.org/10.1007/978-1-4684-9199-9
• Mathlib, Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.html

Motivation

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

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

$$f(A\cup B)+f(A\cap B)\le f(A)+f(B)\qquad(A,B\subseteq\mathcal N).$$

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. 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 $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. 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 $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

$$\max_{S\subseteq\mathcal N}f(S)\le 2\,\mathbb E[f(X_n)].$$

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ 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 $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

$$3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].$$

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

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.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

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 $0/0$ 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 $F$ for $f$ 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 $Y\setminus X$, 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.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

Motivation

A matching of a graph is a set of edges no two of which share a vertex. A matching with as many edges as possible is a basic object of combinatorial optimization. Assignment problems, pairing and scheduling problems, and the Chinese postman problem reduce to it, and it is the standard example of a problem with a polynomial-time algorithm that is not an instance of linear programming over a bipartite structure.

For bipartite graphs the problem was settled by the 1950s, through the theorems of König and Hall and the Hungarian method of Kuhn, whose correctness rests on linear programming duality. As Berge notes on p. 842, that duality "no longer subsists when the graph is not bipartite". C. Berge's three-page note of 1957 (doi:10.1073/pnas.43.9.842) gave the criterion that works for every graph: a matching is maximum exactly when it admits no augmenting chain.

Timeline.

• 1931–1935: König and Hall characterize maximum matchings and systems of distinct representatives in bipartite graphs.
• 1947: Tutte characterizes graphs with a perfect matching (doi:10.1112/jlms/s1-22.2.107).
• 1950: Gallai studies the structure of graphs with respect to their maximum matchings (cited by Berge as the source of his Lemma 1).
• 1955: Kuhn gives the Hungarian method for the bipartite assignment problem (doi:10.1002/nav.3800020109).
• 1957: Berge proves that a matching is maximum if and only if no alternating chain joins two neutral points (Theorem 1 of this paper).
• 1965: Edmonds turns the criterion into a polynomial-time algorithm for general graphs by shrinking odd cycles ("blossoms") (doi:10.4153/CJM-1965-045-4).

Setting

Let $G = (X, U)$ be a finite graph without loops or multiple edges, with vertex set $X$ and edge set $U$. A matching is a set $V_0 \subseteq U$ of edges no two of which have a vertex in common. Its size $|V_0|$ is its number of edges. A matching is maximum if no matching of $G$ has more edges. This is a statement about cardinality: a matching to which no edge can be added (maximal under inclusion) need not be maximum.

Fix a matching $V_0$. Its edges are strong, all other edges weak. A vertex is neutral if no strong edge contains it, and $N$ is the set of neutral points. An alternating chain is a walk in $G$ that does not use the same edge twice and in which, of any two consecutive edges, one is strong and the other weak. Vertices may repeat.

For the milestones, Berge adds a new vertex $\bar a$ joined by strong edges to every neutral point, which gives a graph $\bar G$. Whenever an alternating chain of $\bar G$ runs from $\bar a$ to a vertex $x$, its last edge $(z, x)$ carries an arrow from $z$ to $x$. The non-neutral vertices then fall into four classes:

• $I$, the inaccessible points, at which no edge carries an arrow;
• $W$, the weak points, which receive arrows on weak edges only;
• $S$, the strong points, which receive arrows on strong edges only;
• the medium points, which receive both kinds.

The mission's Lean development uses the same names: IsNeutral, IsAlternatingChain, IsMaximumMatching, barGraph, Arrow, IsInaccessible, IsWeakPt, IsStrongPt, IsMedium.

Formalization targets

Goal: Theorem 1 (p. 843)

$$V_0 \text{ is maximum} \iff \text{no alternating chain connects a neutral point } a \text{ to a neutral point } a' \ne a .$$

The statement fixes nothing beyond finiteness: the graph need not be connected, and no bound on its size is assumed.

Milestones

1. Proof of Theorem 1, first paragraph. An alternating chain $W$ between distinct neutral points makes $(V_0 \setminus W) \cup (W \setminus V_0)$ a larger matching.
2. Lemma 5. If $|N| \le 1$, then $V_0$ is maximum.
3. Lemma 2. If $\bar a$ is inaccessible, then $S \cup N$ is internally stable (an independent set).
4. Lemma 3. If $\bar a$ is inaccessible and there are no medium and no inaccessible points, then $S \cup N$ is a maximum internally stable set, $W$ is a minimum cover, and $V_0$ is maximum.
5. Lemma 4. If $\bar a$ is inaccessible, the edges leaving a connected component $Z$ of $I$ are weak and carry no arrow, the outside neighbours of $Z$ are weak points, and $|Z| \ge 2$.
6. Lemma 1 (Gallai), corrected. If $\bar a$ is inaccessible, the components of the medium points, enlarged by the neutral points that receive a weak arrow, have exactly one strong edge entering them, have all other boundary edges weak and directed outward, and have at least three vertices.

Significance

Theorem 1 reduces the optimality of a matching, a statement about all matchings of the graph, to the absence of one kind of local structure. Its consequences include:

• correctness of every augmenting-path algorithm for maximum matching, including Edmonds' blossom algorithm and the Hopcroft–Karp and Micali–Vazirani refinements;
• the standard proofs of the Tutte–Berge formula and of the Gallai–Edmonds structure theorem, which start from it.

A matching that is not maximum can be certified by exhibiting the chain, and a maximum matching is certified by the labelling of Lemmas 1–4.

Theorem 1 has been proved since 1957 and appears in every textbook on matching theory. It is not formalized in Mathlib at the revision this mission uses. Mathlib has matchings as subgraphs, perfect matchings, alternating cycles and Tutte's theorem, but no augmenting-path characterization. This mission adds a formal statement of the theorem, together with the labelling of Berge's proof in a form that later missions on Edmonds' algorithm can reuse.

Difficulty

The "only if" direction is a local computation: the symmetric difference along an augmenting chain is again a matching, with one more edge. Even this needs care, because an alternating chain is only a trail and may a priori revisit vertices, while the augmentation needs a path.

The converse is the substance. In bipartite graphs, a search from the neutral points that alternates weak and strong edges labels each vertex at most one way, and its failure yields a cover of the same size as the matching. In general graphs an odd cycle lets a vertex be reached both through a strong and through a weak edge (the medium points). The bipartite labelling then fails, and no cover of size $|V_0|$ need exist: in a triangle the maximum matching has one edge and the minimum cover two. The proof has to treat these odd structures separately, and that is what Lemmas 1 and 4 do.

Formalization scope

• Graphs and matchings. The graph is a Mathlib SimpleGraph V on a Fintype V. The paper's "unoriented graph (or 1-dimensional regular complex)" may have parallel edges, but a matching uses at most one edge of a parallel class, so nothing is lost. The matching is a subgraph M with M.IsMatching, and its size is M.edgeSet.ncard. Maximum means cardinality-maximum over all matching subgraphs. Internally stable sets and covers are Mathlib's IsIndepSet and IsVertexCover.
• Alternating chains. An alternating chain is a walk that is a trail (no repeated edge; vertices may repeat), with alternation between consecutive edges.
• $\bar G$ and arrows. $\bar G$ lives on Option V, with $\bar a$ = none. An arrow needs an alternating chain of positive length from $\bar a$.
• Readings of ambiguous phrases.
  • "$\bar a$ is inaccessible" means that no arrow is directed to $\bar a$. Read literally ("not adjacent to a directed edge"), the phrase fails whenever $N \neq \emptyset$.
  • "Edges adjacent to $Z$" (and to $Y$) are the edges with exactly one endpoint in the set.
  • The paper's medium class $M$ is IsMedium in Lean, because M names the matching.
• Results not formalized.
  • Lemma 1 is false as printed. On a triangle with one matched edge, the two medium points form $Y$ with $|Y| = 2$, and their neighbour is neutral. The mission states a corrected form, labelled as such, in which neutral blossom bases are added to $Y$.
  • Lemma 6 (shrinking) is false. On the path $u$–$x$–$y$–$v$ with extra edges $y$–$t$, $t$–$q$, the set $A = \{x, y, t\}$ and $V_0 = \{xy, tq\}$, the matching is maximum on $A$ and on the shrunk graph, yet $\{ux, yv, tq\}$ is larger.
  • Theorem 2 (a minimum cover built from the labels) is false. Take a neutral vertex joined to the stems of two triangles, with the stems and the triangles matched. The construction yields a cover of 6 vertices, while one of 5 exists.
  • Neither false result is formalized, and the cases of the proof of Theorem 1 that rest on them are not milestones. The algorithmic remarks on p. 844 are procedures, not claims, and are not formalized either.
• Ruled-out trivializations. None of the following is a faithful encoding:
  • reading "maximum" as inclusion-maximal;
  • allowing an alternating chain to join a neutral point to itself (the one-vertex chain would then always exist);
  • reading "$\bar a$ is inaccessible" in a way that is never or always true;
  • imposing alternation on only some pairs of edges.

Any proof of the goal is welcome, whether it follows Berge's induction, uses the symmetric difference of two matchings, or goes through the Tutte–Berge formula. Reusable infrastructure is especially welcome: augmentation along a path, the symmetric difference of two matchings as a union of paths and cycles, and trails that alternate with respect to a matching.

Selected references

• C. Berge, Two theorems in graph theory, Proc. Natl. Acad. Sci. USA 43(9) (1957), 842–844. doi:10.1073/pnas.43.9.842
• W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947), 107–111. doi:10.1112/jlms/s1-22.2.107
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. doi:10.1002/nav.3800020109
• J. Edmonds, Paths, trees, and flowers, Canadian J. Math. 17 (1965), 449–467. doi:10.4153/CJM-1965-045-4

Motivation

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 $O(\log m \log n)$, where $n$ is the number of elements and $m$ 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 $\alpha$ at least the optimal cost, and its guarantee (Theorem 3.4).

Setting

The ground set $X$ has $n = |X|$ elements and the family $\mathcal S$ has $m = |\mathcal S|$ sets; every set $S$ has a cost $c_S > 0$. Both are known to the algorithm in advance. For an element $j$, $\mathcal S_j$ denotes the sets containing $j$. Elements of an unknown subset of $X$ arrive one at a time in a sequence $\sigma$; on arrival each must be covered by a chosen set. The chosen family $\mathcal C$ can only grow. $\mathcal C_{OPT}$ is any family covering every arriving element, and $c(\mathcal C_{OPT}) = \sum_{S \in \mathcal C_{OPT}} c_S$.

The algorithm is given $\alpha \ge c(\mathcal C_{OPT})$. It discards sets costing more than $\alpha$, buys sets costing at most $\alpha/m$ outright, and rescales costs; on the resulting normalized instance $1 \le c_S \le m$ and $c_S \le \alpha$ for every set (p. 365).

The algorithm keeps a weight $w_S > 0$ for every set, initially $w_S = 1/m^2$; the weight of an element is $w_j = \sum_{S \in \mathcal S_j} w_S$. With $C$ the set of covered elements and $\chi_{\mathcal C}$ the indicator of $\mathcal C$, the potential is

$$\Phi = \sum_{j \notin C} n^{2 w_j} + n \cdot \exp\Big(\frac{1}{2\alpha} \sum_{S \in \mathcal S} \big(c_S \chi_{\mathcal C}(S) - 3 w_S c_S \log n\big)\Big),$$

with natural logarithms throughout. When $j$ arrives with $w_j \ge 1$ nothing happens; otherwise the algorithm performs weight augmentation steps while $w_j < 1$. In a step, for each $S \in \mathcal S_j$: (a) $w_S \leftarrow w_S (1 + \frac{1}{n c_S})$; (b) if $S \notin \mathcal C$, add $S$ to $\mathcal C$ when $\Phi$ does not exceed its value before (a); (c) if $\Phi$ 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.

Formalization targets

Goal: Theorem 3.4

On the normalized instance, with $\mathcal C_{OPT}$ covering $\sigma$, $c(\mathcal C_{OPT}) \le \alpha$, and $n \cdot n^{2/m} + n < n^2$, every reachable configuration is a running state (never FAIL) in which (i) every $j \in X$ with $w_j \ge 1$ is covered, and (ii)

$$\sum_{S \in \mathcal C} c_S \le 3 \log n \Big(1 + \Big(1 + \frac1n\Big)\alpha \log\Big(m^2\Big(1+\frac1n\Big)\Big)\Big) + 2\alpha \log n = (6 + o(1))\,\alpha \log m \log n.$$

Milestones

• Lemma 3.1 (p. 365): the number $N$ of augmentation steps satisfies $N \le \sum_{S \in \mathcal C_{OPT}} (n c_S + 1)\log(m^2(1 + 1/n)) \le (n+1)\alpha\log(m^2(1+1/n))$.
• Lemma 3.2 (p. 366): throughout, $\sum_S w_S c_S \le 1 + N/n \le 1 + (1 + 1/n)\alpha\log(m^2(1+1/n))$.
• Lemma 3.3 (p. 366): a per-set step with $c_S \le \alpha$ never increases $\Phi$; in particular the algorithm never fails.

The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant $\Phi < n^2$ assumed) is included as a supporting reference.

Significance

Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of $\alpha$ described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic $O(\log m \log n)$-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 $\Phi < n^2$ to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis $c_S \le \alpha$. 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 $o(1)$ terms replaced by explicit expressions.

Difficulty

The cost bound in the last step is short once two facts about the run are available: that $\Phi$ stays below $n^2$, and that the fractional cost $\sum_S w_S c_S$ 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 $S$ or not) does not increase $\Phi$; 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 $\alpha$. 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 $n^{2 w_j}$, where the initial bound $\Phi < n^2$ is a genuine size condition on $n$ and $m$.

Formalization scope

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 $\mathcal S_j$ 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 $\mathcal C_{OPT}$.

Conventions: costs, weights and $\alpha$ are real; $n$ and $m$ are the cardinalities of the finite types cast to $\mathbb R$; $\log$ is Real.log; $n^{2 w_j}$ and $n^{2/m}$ are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:

• Lemma 3.1: $(2 + o(1)) n\alpha\log m$ becomes $(n+1)\alpha\log(m^2(1+1/n))$;
• Lemma 3.2: $(2 + o(1))\alpha\log m$ becomes $1 + (1+1/n)\alpha\log(m^2(1+1/n))$, together with the intermediate bound $1 + N/n$;
• Theorem 3.4 (ii): $(6 + o(1))\alpha\log m\log n$ becomes $3\log n\,(1 + (1+1/n)\alpha\log(m^2(1+1/n))) + 2\alpha\log n$;
• "n and m large" becomes the hypothesis $n \cdot n^{2/m} + n < n^2$ used for the initial potential (it holds, for instance, when $n \ge 4$ and $m \ge 3$).

The goal is a statement about the configurations the algorithm actually reaches from $w_S = 1/m^2$ and the empty cover. Taking the invariant $\Phi < n^2$ 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 $\alpha$ 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.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024