Operations Research

Motivation

Many collective decisions are taken by coalitions that either carry the vote or do not: committees, legislatures, shareholder meetings, councils with weighted votes. In such a situation the only aim of a participant is to be part of a coalition that wins, and nothing is left to bargain about except the division of the prize inside the winning coalition. Chapter X of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) isolates exactly this class of zero-sum $n$-person games, the simple games, and studies their numerical description by weighted majorities and their finite main simple solutions.

The chapter is the origin of a large later literature: simple games and weighted voting games are the standard model of voting bodies in political science and social choice (for instance the Shapley–Shubik power index, 1954). The characterization of which simple games admit homogeneous weights, and the solutions they carry, starts here.

Setting

A zero-sum $n$-person game with players $I = \{1, \dots, n\}$ is represented by its characteristic function $v$, a real function on the subsets of $I$ with $v(\ominus) = 0$, $v(-S) = -v(S)$ ($-S$ the complement) and $v(S \cup T) \geqq v(S) + v(T)$ for disjoint $S, T$. An imputation is a vector $\vec\alpha$ with $\alpha_i \geqq v((i))$ and $\sum_i \alpha_i = 0$; $\vec\alpha$ dominates $\vec\beta$ if some nonempty $S$ has $\sum_{i\in S}\alpha_i \leqq v(S)$ and $\alpha_i > \beta_i$ for $i \in S$; a solution is a set $V$ of imputations none of which dominates another and which dominates every imputation outside it (30.1.1). The game is inessential when its reduced form vanishes identically, essential otherwise.

A coalition $S$ is flat if $v(S) = \sum_{k\in S} v((k))$. The losing coalitions $L_\Gamma$ are the flat sets, and the winning coalitions $W_\Gamma$ are the sets whose complement is flat. The game is simple if it is essential and every coalition is winning or losing. $W^m$ denotes the minimal winning coalitions, those of which no proper subset wins.

Weights $w_1, \dots, w_n$ define the winning system $W = \{S : \sum_{i\in S} w_i > \tfrac12 \sum_i w_i\}$, and under the conditions (50:B) (non-negative weights, no player with half the total weight, no ties) this is the weighted majority game $[w_1,\dots,w_n]$. The weights are homogeneous if the advantage $a_S = \sum_{i\in S} w_i - \sum_{i\in -S} w_i$ is the same for all $S$ in $W^m$.

In §50 the game is taken in reduced form with $\gamma = 1$, so $v((i)) = -1$. For numbers $x_i \geqq 0$ and a coalition $S$ let $\vec\alpha^S$ give $-1$ to the players outside $S$ and $-1 + x_i$ to player $i$ in $S$. When the $x_i$ satisfy $\sum_{i \in S} x_i = n$ for every $S \in W^m$, the set $V$ of all $\vec\alpha^S$, $S \in W^m$, is a main simple solution.

Formalization targets

Goal: (50:K), p. 444

$$\text{Every homogeneous weighted majority game possesses a main simple solution,}$$

namely the set of $\vec\alpha^S$, $S \in W^m$, with $x_i = \frac{n}{b} w_i$, $b = \frac12(\sum_i w_i + a)$, $a$ the common advantage. Conversely, if $x_i \geqq 0$ solve $\sum_{i\in S} x_i = n$ on $W^m$, then $w_i = x_i$ are homogeneous weights for the game if and only if

$$\sum_{i=1}^n x_i < 2n .$$

Milestones

1. (49:C) $L_\Gamma$ contains the empty set and all one-element sets.
2. (49:A) $W_\Gamma, L_\Gamma$ are mapped onto each other by complementation, $W_\Gamma$ is closed under supersets, and $L_\Gamma$ is closed under subsets.
3. (49:B) $W_\Gamma \cap L_\Gamma = \ominus$ if and only if the game is essential. If the game is inessential, every set is both winning and losing.
4. (49:F) The pairs $W, L$ of simple games are exactly those satisfying (48:A:a)–(48:A:d) and (49:C).
5. (50:A) The essential three-person game is simple: it is the direct majority game.
6. (50:B) Non-negative weights define a winning system with (49:W*) if and only if (50:B:a), (50:B:b) hold.
7. (50:D) $a_S > 0$ on $W$, $a_S < 0$ on $L$, and $a_S = 0$ never occurs.
8. (50:G) An imputation $\vec\beta$ is undominated by $V = \{\vec\alpha^S : S \in U\}$ if and only if $R(\vec\beta) \in U^+$.
9. (50:J) The exact criterion (50:8*), (50:9*) for $V$ to be a solution.

Significance

The result links two descriptions of a simple game. One is numerical: a vector of weights, normalized by homogeneity. The other is game-theoretic: a finite solution in which each minimal winning coalition forms and divides a fixed total among its members. When the weights are homogeneous they are, up to scale, the shares in the main simple solution. When a main simple solution exists, its shares are homogeneous weights exactly under the inequality (50:20). The criterion (50:J) behind it is the chapter's general tool for deciding which systems of "profitable" minimal winning coalitions yield a finite solution. It is used again in the enumeration of simple games in §§51–55.

All of the results are proved in the book. As far as a search of the Prove2Me library shows (queries on simple game, weighted majority, winning coalition and stable set, 2026-09-28), none of them has been machine-checked. The only stable-set statements on the platform concern feasible payoff vectors of convex games, which is a different domain. The mission therefore asks for a formal proof of the known results, including the case analysis of §50.5–50.6, and in doing so it produces a reusable Lean theory of simple games and their winning systems.

Difficulty

The characterizations of §49 are set-theoretic, but they depend on superadditivity to show that subsets of flat sets are flat, and on the strategic-equivalence description of essentiality. The substantial part is (50:J). Deciding whether $V$ is a solution means classifying every imputation $\vec\beta$ by the set $R(\vec\beta)$ where it meets the shares $-1 + x_i$.

The natural first attempt is to check only the minimal winning coalitions. It fails, because domination can be exercised through any winning coalition. The book's argument has to exclude sets of $U^+$ with $\sum_{i\in T} x_i < n$ by producing infinitely many undominated imputations against a finite $V$. It also has to handle indifferent players with $x_i = 0$, whose presence makes $R(\vec\beta)$ larger than the coalition that generated $\vec\beta$. For the converse half of the goal, the obstacle is the strict inequality $a > 0$: the equations (50:17) are linear and say nothing about it.

Formalization scope

Players are Fin n (the book's player $i$ is index $i - 1$), coalitions are Finset (Fin n), and characteristic functions are Finset (Fin n) → ℝ. Imputations are vectors Fin n → ℝ, and systems of coalitions are Set (Finset (Fin n)). A game is identified with its characteristic function (by 26.1 every $v$ satisfying (25:3:a)–(25:3:c) arises from a game). The theory is the "old" one of 30.1.1 (49.1.1), with no excess. The definitions of imputation, domination and solution are the same as in mission V of this series and are restated here, because a draft cannot import another draft.

The standing hypotheses, stated in each theorem where the book has them in force:

• (25:3:a)–(25:3:c) on $v$ in every theorem;
• simplicity (essential + (49:1:b)) in (50:G), (50:J), (50:K);
• the reduced form with $\gamma = 1$, as $v((i)) = -1$ for all $i$ (50.4.1), in (50:G), (50:J), (50:K);
• $U \subseteq W^m$, (50:7) $x_i \geqq 0$ and (50:8) $\sum_{i\in S} x_i = n$ for $S \in U$ (50.5.1) in (50:G), (50:J);
• (50:B) on the weights in (50:D) and in the first half of (50:K);
• non-negative weights in (50:B). The book states (50:B) for arbitrary real weights, but its "only if" direction is false without $w_i \geqq 0$: $[10, 10, 10, -\tfrac1{10}]$ is a counterexample. The corrected statement is recorded in the item.

The numbers $x_i$ are given for every player. Players in no minimal winning coalition, for whom the book defines no $x_i$, do not affect any $\vec\alpha^S$. In the converse of (50:K) the derived weights are $w_i = x_i$ for every player.

The goal is not the bare solvability of (50:17). A statement that only asserted "$x$ exists with (50:7), (50:17)" would reduce to linear algebra. The goal asserts that the set of $\vec\alpha^S$ is a solution in the sense of 30.1.1, with domination requiring a nonempty effective set, and it adds the converse equivalence with (50:20). The set $V$ is built from $W^m$ only, never from all of $W$.

Welcome contributions: proofs of the §49 milestones, which form a small reusable library on winning and losing systems; a proof of (50:G) and (50:J); and lemmas connecting $W_\Gamma$ of a simple reduced game with the explicit formula (49:2), $v(S) = n - |S|$ on $W$ and $-|S|$ on $L$.

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary ed., Princeton University Press, 2007 (reprint of the 3rd ed., 1953), Chapter X, §§48–50, pp. 420–444. https://doi.org/10.1515/9781400829460
• L. S. Shapley, M. Shubik, "A method for evaluating the distribution of power in a committee system", American Political Science Review 48 (1954) 787–792. https://doi.org/10.2307/1951053

Motivation

Chapter VI of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) opens the general theory of zero-sum games with more than two players. The authors propose to describe everything that can be said about coalitions, compensations between partners and fights between coalitions through one numerical object, the characteristic function $v(S)$: the amount a group of players $S$ can secure for itself against all the others (25.2.1). The whole later theory of the book (imputations, domination, solutions, simple games, decomposition) is built on this set function, and the same object, under the name "coalitional game" or "TU game", is the starting point of cooperative game theory as a field (cores, Shapley value, nucleolus).

§§25–27 settle two foundational questions about it. First, which set functions arise as characteristic functions of actual games? Second, which characteristic functions describe the same strategic situation, and how is a canonical representative chosen? The answers (a complete characterization by three conditions, and the reduced form under strategic equivalence) are what later chapters, and much of the cooperative literature, use when they take "a characteristic function" as a primitive without reference to any game.

Setting

A zero-sum $n$-person game in normalized form $\Gamma$ (11.2.3, 25.1.3) has players $k = 1, \dots, n$. Player $k$ chooses a pure strategy $\tau_k \in \{1, \dots, \beta_k\}$, $\beta_k \geqq 1$, uninformed about the others' choices, and then receives the real amount $\mathcal H_k(\tau_1, \dots, \tau_n)$, subject to (25:1)

$$\sum_{k=1}^n \mathcal H_k(\tau_1, \dots, \tau_n) \equiv 0 .$$

Let $I = \{1, \dots, n\}$ and, for $S \subseteq I$, $-S = I \setminus S$. The book defines $v(S)$ in 25.1.3 through a fictitious two-person game: all players of $S$ form one composite player $1'$, all players of $-S$ another, $2'$. The pure strategies of $1'$ are the aggregates $\tau^S$ (one choice $\tau_k$ for each $k \in S$), those of $2'$ are the aggregates $\tau^{-S}$, and $1'$ receives (25:2)

$$\overline{\mathcal H}(\tau^S, \tau^{-S}) = \sum_{k \in S} \mathcal H_k(\tau_1, \dots, \tau_n).$$

A mixed strategy of $1'$ is a probability vector $\xi$ on the set of all aggregates $\tau^S$, and one of $2'$ is a probability vector $\eta$ on the aggregates $\tau^{-S}$. With $K(\xi, \eta) = \sum_{\tau^S, \tau^{-S}} \overline{\mathcal H}(\tau^S, \tau^{-S})\, \xi_{\tau^S} \eta_{\tau^{-S}}$,

$$v(S) = \operatorname{Max}_\xi \operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_\eta \operatorname{Max}_\xi K(\xi, \eta).$$

The coalition therefore randomizes jointly: $\xi$ is one distribution over its members' strategy tuples, not a product of independent mixtures. The empty set and $I$ are coalitions too (footnote 2, p. 241).

The three conditions of 25.3.1 on a set function $v$ are

$$\text{(25:3:a)}\ v(\ominus) = 0, \qquad \text{(25:3:b)}\ v(-S) = -v(S), \qquad \text{(25:3:c)}\ v(S \cup T) \geqq v(S) + v(T) \ \text{ if } S \cap T = \ominus .$$

From 26.2 on, every set function satisfying them is called a characteristic function.

Two such functions are strategically equivalent (27.1) if $v'(S) = v(S) + \sum_{k \in S} \alpha^0_k$ for numbers $\alpha^0_k$ with $\sum_k \alpha^0_k = 0$ ((27:1), (27:2)). A function is reduced if all one-element coalitions have the same value, (27:3); with that common value written $-\gamma$, (27:5). A game is inessential if the reduced form of its characteristic function is $\equiv 0$, and essential otherwise (27.3).

Formalization targets

Goal: the characterization of characteristic functions (26.2)

$$v \text{ satisfies (25:3:a)–(25:3:c)} \iff \exists\, \Gamma \text{ zero-sum } n\text{-person game with } v_\Gamma = v .$$

The "only if" half is 25.3.1; the "if" half is 26.1.1, which requires a single game $\Gamma$ realizing $v$ on every coalition simultaneously.

Milestones

1. 25.3.1: every $v_\Gamma$ satisfies (25:3:a)–(25:3:c).
2. (25:A): the three conditions are equivalent to $v(S_1) + \dots + v(S_p) \leqq 0$ on decompositions of $I$ for $p = 1, 2, 3$, with equality for $p = 1, 2$.
3. 26.1.1: every $v$ satisfying (25:3:a)–(25:3:c) is $v_\Gamma$ for some game $\Gamma$.
4. (27:A): every characteristic function is strategically equivalent to exactly one reduced characteristic function, given by (27:2), (27:4).
5. (27:7): for reduced $\bar v$ and every $p$-element $S$, $-p\gamma \leqq \bar v(S) \leqq (n-p)\gamma$, with equality in the stated boundary cases.
6. (27:B): inessential iff $\sum_j v((j)) = 0$; essential iff $\sum_j v((j)) < 0$.
7. (27:C) and (27:D): inessential iff $v$ is additive, $v(S) \equiv \sum_{k \in S} \alpha^0_k$, equivalently iff (25:3:c) always holds with equality.

Significance

The characterization makes the three conditions (25:3:a)–(25:3:c) the complete axiomatics of zero-sum characteristic functions. Every later result in the book that is stated "for a characteristic function" (the solutions of the three-person game in §32, the simple games of Chapter X, the decomposition theory of Chapter IX) is thereby a result about zero-sum games, and conversely no further constraint on $v$ is hidden in the game model. The reduced form of §27 cuts the parameter space of characteristic functions by $n$ and turns essentiality into a sign condition, which is used throughout the rest of the book.

These results are proved in the book. As far as a search of the Prove2Me catalog shows (queries on characteristic function, coalition, strategic equivalence, inessential, superadditive), none of them is formalized there; the existing cooperative-game definitions on the platform use other normalizations ($v(\emptyset) = 0$ only, no complementarity condition) and are not this object. The mission produces a machine-checked link between the non-cooperative model of an $n$-person game and the cooperative set function, including the book's explicit game construction behind 26.1.1.

Difficulty

The "only if" direction requires comparing values of different two-person games: (25:3:c) asks that the coalition $S \cup T$ can guarantee as much as $S$ and $T$ separately, which rests on the coalition mixing jointly, and (25:3:b) needs the minimax theorem, since $v(-S)$ is a Max-Min for the opposite side. The "if" direction is an existence claim: from an abstract $v$ one must produce one finite game whose characteristic function matches $v$ on all $2^n$ coalitions at once. Producing, for each $S$ separately, a game with the right value $v_\Gamma(S)$ is easy and proves nothing. The §27 results are finite linear algebra over set functions, but the uniqueness in (27:A) and the boundary equalities in (27:7) depend on using all three conditions.

Formalization scope

Players are Fin n (the book's $1, \dots, n$ are $0, \dots, n-1$), coalitions are Finset (Fin n), $-S$ is the complement Sᶜ, and set functions are Finset (Fin n) → ℝ. A game is a structure ZeroSumGame n with strategy sets Fin (β k), a field β k > 0 (finitely many and at least one pure strategy per player), real payoffs H τ k, and the zero-sum condition (25:1) as a field. An aggregate $\tau^S$ is a dependent function on the members of $S$; mixed strategies are elements of Mathlib's stdSimplex, and the coalition's $\xi$ is a single distribution on aggregates, as in 25.1.3. The Max and Min in $v(S)$ are written as ⨆/⨅ over the simplices; these are nonempty and the bilinear form is bounded on them, so no junk value arises. No lower bound on $n$ is imposed: the book's statements remain true for $n = 0$ and $n = 1$, so dropping the implicit $n \geqq 1$ is a harmless strengthening.

Standing hypotheses instantiated in the statements: finiteness of the strategy sets and (25:1) (25.1.3) are part of ZeroSumGame; the §27 results carry (25:3:a)–(25:3:c) as a hypothesis, the book's standing assumption from 26.2 on ("characteristic function"); (27:7) carries reducedness (27:3) and the definition (27:5) of $\gamma$; strategic equivalence includes (27:1). The reduced form is the explicit function of (27:2), (27:4), with $\frac1n$ as a real division that only matters for $n \geqq 1$.

A trivializing reading of the goal, "for every $S$ there is a game with $v_\Gamma(S) = v(S)$", is excluded: the statement asks for one game $\Gamma$ with $v_\Gamma = v$ as functions. The coalition value is not the value under independent mixtures of the members, which is smaller in general and for which (25:3:c) can fail.

A complete development needs the minimax theorem for finite matrix games (the platform's AGT.zero_sum_minimax covers it for matrices indexed by Fin (m+1), and can be transported to the aggregate types), bookkeeping for splitting and joining strategy profiles along $S$ and $-S$, and the construction of 26.1 with its zero-sum check. The profile-splitting lemmas and the value facts for coalition games are reusable for the book's Chapter XI (general games) and for any work on coalitional values of strategic games. Contributions welcome: the §27 milestones, which are self-contained, and the two directions of the goal.

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§25–27, pp. 238–254. https://doi.org/10.1515/9781400829460
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320 (the minimax theorem used for $v(S)$). https://doi.org/10.1007/BF01448847
• M. Maschler, E. Solan and S. Zamir, Game Theory, Cambridge University Press, 2013, Ch. 16 (coalitional games with transferable utility). https://doi.org/10.1017/CBO9780511794216

Motivation

Game theory as von Neumann and Morgenstern built it measures every outcome by a single number, the utility a player attaches to it, and combines those numbers linearly when an outcome is uncertain: a lottery that yields $u$ with probability $\alpha$ and $v$ with probability $1-\alpha$ is worth $\alpha\,\mathrm v(u) + (1-\alpha)\,\mathrm v(v)$. Every later chapter of Theory of Games and Economic Behavior uses this without comment, from the value of a zero-sum game to the characteristic function of a coalition. Section 3 of the book justifies it: it states axioms on preferences and on the combination of alternatives with probabilities, and claims that they force utility to be a number, unique up to the choice of a zero and a unit. The proof, announced in 3.6.1 as "somewhat lengthy", was added as the Appendix The Axiomatic Treatment of Utility in the second edition (1947).

The result, the expected utility theorem, is the foundation of decision theory under risk and of expected-payoff reasoning in game theory, statistics and operations research. The axiomatics were later recast by Marschak (1950), Herstein and Milnor (1953) in the language of mixture spaces (Herstein–Milnor). This mission formalizes the original statement and its original proof structure.

Setting

A system of utilities (3.6.1) is an abstract set $U$ of entities $u, v, w, \dots$, together with

1. a relation $u > v$ ("$u$ is preferable to $v$"); write $u < v$ for $v > u$;
2. for every number $\alpha$ with $0 < \alpha < 1$, an operation producing an element written $\alpha u + (1-\alpha) v$ of $U$ from $u, v \in U$.

The axioms are:

• (3:A) $>$ is a complete ordering: (3:A:a) for any $u, v$ exactly one of $u = v$, $u > v$, $u < v$ holds; (3:A:b) $u > v$, $v > w$ imply $u > w$.
• (3:B) Ordering and combining: (3:B:a) $u < v$ implies $u < \alpha u + (1-\alpha)v$; (3:B:b) $u > v$ implies $u > \alpha u + (1-\alpha)v$; (3:B:c) $u < w < v$ implies $\alpha u + (1-\alpha)v < w$ for some $\alpha$; (3:B:d) $u > w > v$ implies $\alpha u + (1-\alpha)v > w$ for some $\alpha$.
• (3:C) Algebra of combining: (3:C:a) $\alpha u + (1-\alpha)v = (1-\alpha)v + \alpha u$; (3:C:b) $\alpha(\beta u + (1-\beta)v) + (1-\alpha)v = \gamma u + (1-\gamma)v$ with $\gamma = \alpha\beta$.

All weights lie strictly between $0$ and $1$, and $=$ is identity. The expression $\alpha u + (1-\alpha)v$ is notation for an abstract operation: $U$ carries no linear structure. The Appendix mostly writes the operation as $(1-\gamma)u + \gamma v$, and writes $u \leqq v$ for "$u = v$ or $u < v$". In the Lean development the system is the structure UtilitySystem U with fields gt and mix; S.cmb γ u v is $(1-\gamma)u + \gamma v$.

A numerical utility (3.5.1) is a map $\mathrm v : U \to \mathbb R$ with

$$\text{(i)}\quad u > v \implies \mathrm v(u) > \mathrm v(v), \qquad \text{(ii)}\quad \mathrm v\big((1-\gamma)u + \gamma v\big) = (1-\gamma)\mathrm v(u) + \gamma\,\mathrm v(v) \quad (0<\gamma<1).$$

Formalization targets

Goal: (A:V) and (A:W), p. 627

For every system of utilities satisfying (3:A)–(3:C):

$$\exists\, \mathrm v : U \to \mathbb R \ \text{with (i), (ii)}, \qquad\text{and}\qquad \forall\, \mathrm v, \mathrm v' \text{ with (i), (ii)}:\ \exists\, \omega_0 > 0,\ \omega_1,\ \forall w,\ \ \mathrm v'(w) = \omega_0\,\mathrm v(w) + \omega_1 .$$

The constants $\omega_0, \omega_1$ are chosen before $w$. No assumption on the size of $U$ is made.

Milestones

The milestones follow the Appendix's own chain:

• (A:A) if $u < v$ and $\alpha < \beta$ then $(1-\alpha)u + \alpha v < (1-\beta)u + \beta v$;
• (A:B), (A:C) for $u_0 < v_0$, the map $\alpha \mapsto (1-\alpha)u_0 + \alpha v_0$ is a one-to-one, monotone map of $(0,1)$ onto the utility interval $u_0 < w < v_0$;
• (A:E), (A:F) the interval function $f_{u_0,v_0}$ of (A:D) (value $0$ at $u_0$, $1$ at $v_0$, and the weight $\alpha$ in between) is monotone and linear toward each endpoint, and is characterized by these properties;
• (A:R), (A:S) for fixed $u^* < v^*$, the normalized mapping $h$ with $h(u^*) = 0$, $h(v^*) = 1$, monotone, and linear on combinations of $u < v$, exists and is unique;
• (A:T) $(1-\gamma)u + \gamma u = u$ always;
• (A:U) $h$ is linear on all combinations, without the restriction $u < v$.

Significance

The theorem turns an ordinal preference over uncertain prospects into a cardinal scale on which expectation is meaningful. It is what licenses replacing a player's preferences by numerical payoffs whose mixtures are averaged, which the rest of the book, and most of game theory and stochastic optimization after it, assumes. The uniqueness part (A:W) states exactly how much freedom the scale has: a positive linear transformation, i.e. zero and unit may be fixed at will and nothing else.

The theorem has been proved many times since 1947, in textbooks and in the mixture-space literature, but the book's axiom system differs from the later ones (it uses a strict order with identity, strict monotony, and the two algebraic axioms (3:C) only). As far as the curators know, neither this axiom system nor the Appendix's derivation has a machine-checked proof, and Mathlib has no mixture-space or expected-utility module. The mission produces a checked proof of the original theorem under its original hypotheses and a reusable abstract mixture-space layer.

Difficulty

The obvious argument treats $U$ as a convex set and $\alpha u + (1-\alpha)v$ as a convex combination, then reads the utility off the segment between two reference points. None of that is available. The operation is formal, so identities that hold in a vector space, idempotence $(1-\gamma)u + \gamma u = u$ included, must be derived from (3:B) and (3:C) alone; only one associativity rule (3:C:b), for a repeated right argument, is given. The correspondence between a utility interval and a numerical interval requires the continuity axioms (3:B:c), (3:B:d) and the completeness of the reals. The local scales on different intervals have to be fitted into one global function, and the linearity for pairs $u > v$ and $u = v$ has to be recovered from the case $u < v$.

Formalization scope

• $U$ is an arbitrary type (Type*); the relation is gt : U → U → Prop and the operation mix : OpenUnit → U → U → U, where OpenUnit is the subtype $(0,1)$ of $\mathbb R$. mix α u v stands for $\alpha u + (1-\alpha)v$. The operation is not defined at $\alpha = 0, 1$ (3.6.1, footnote 4) and is not extended there.
• Axiom (3:A:a) is stated literally ("exactly one of the three relations"), so the order is a strict total order and indifference is identity (A.1.2). The weak-order generalization of §66 is not this theorem.
• Numbers are real numbers. Monotony is strict, as in (3:1:a).
• Standing hypotheses: every item assumes (3:A)–(3:C), bundled in UtilitySystem. The items from (A:E) on assume fixed $u_0 < v_0$ or $u^* < v^*$ as explicit hypotheses, as the book does "from now on until we get to (A:V) and (A:W)"; the goal does not, since (A:V), (A:W) hold for every $U$.
• The interval function $f_{u_0,v_0}$ is a total Lean function; its value outside $u_0 \leqq w \leqq v_0$ is a placeholder that no statement uses.
• A formalization in which $U$ is a convex subset of a vector space, or a space of probability measures, assumes more than the book and makes (A:T) free; it does not count. Neither does a weak monotony, under which constant maps satisfy (A:V) and (A:W) fails.

A complete development needs only order theory and the completeness of the reals from Mathlib. The mixture-space layer (the structure, (A:A)–(A:C), (A:T)) is reusable for any later work on expected utility, including the generalization in §66 and 67 of the book. Proofs of any milestone, alternative routes to the goal (for instance through the Herstein–Milnor axioms, once shown to follow from (3:A)–(3:C)), and statements of the omitted intermediate results (A:G)–(A:Q) are all welcome.

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §3 and Appendix. https://doi.org/10.1515/9781400829460
• I. N. Herstein, J. Milnor, An axiomatic approach to measurable utility, Econometrica 21 (1953), 291–297. https://doi.org/10.2307/1905540
• J. Marschak, Rational behavior, uncertain prospects, and measurable utility, Econometrica 18 (1950), 111–141. https://doi.org/10.2307/1907264

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. Deciding whether two bins suffice is NP-hard (it contains the partition problem), so no polynomial-time algorithm guarantees a ratio below $3/2$ unless P = NP. The natural question is therefore asymptotic: how small can the additive error $A(I) - OPT(I)$ be made, as a function of the optimum $OPT(I)$?

• 1974: D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey and R. L. Graham analysed First Fit and First Fit Decreasing, with asymptotic ratios $17/10$ and $11/9$ (SIAM J. Comput. 3(4)).
• 1981: W. Fernandez de la Vega and G. S. Lueker gave an asymptotic approximation scheme: for every $\varepsilon > 0$, $(1+\varepsilon)\,OPT(I) + 1$ bins in linear time (Combinatorica 1).
• 1982: N. Karmarkar and R. M. Karp replaced the multiplicative error by an additive one: $OPT(I) + O(\log^2 OPT(I))$ bins in polynomial time (Proc. 23rd FOCS). This mission formalizes that bound.
• 2017: R. Hoberg and T. Rothvoss improved the additive error to $O(\log OPT)$ (SODA 2017). Whether $OPT(I) + O(1)$ is achievable remains open.

Its main device, geometric grouping followed by rounding a linear program over bin configurations, recurs in later additive results and in cutting-stock problems.

Setting

An instance $I$ is a finite multiset of piece sizes in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, $SIZE(I)$ for the total size and $a(I)$ for the smallest size. A packing is a multiset of bins whose union is $I$ and in each of which the sizes sum to at most $1$; its cost is the number of bins, and $OPT(I)$ is the least cost.

A configuration is a nonempty multiset of sizes occurring in $I$ that fits in one bin. The fractional bin-packing problem is the linear program

$$(I)\qquad \min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x \ge 0,\quad Ax \ge b,$$

with one variable $x_j$ per configuration, where $A_{tj}$ counts the pieces of size $t$ in configuration $j$ and $b_t$ the pieces of size $t$ in $I$. Its value is $LIN(I)$. A basic feasible solution is an extreme point of the feasible region.

Geometric grouping with parameter $k$ sorts the pieces in non-increasing order and cuts them into consecutive groups $G_1, G_2, \dots, G_q$, each the shortest run of pieces of total size at least $k$. Within each group $G_i$ ($i \ge 2$) only as many of the largest pieces as $G_{i-1}$ has are kept; they are rounded up to the largest size in $G_i$, giving $G_i'$. The rounded pieces form $J$, and $G_1$ together with the unrounded leftovers $\Delta G_i$ form $J'$.

ALGORITHM 2 with a positive integer $k$ and a positive real $g$:

1. Eliminate all pieces of size $\le g$.
2. While $SIZE > 1 + \frac{1}{1-1/k}\ln\frac1g$: group the current instance into $J, J'$; pack $J'$ in at most $2k[2 + \ln\frac1g]$ bins; obtain a basic feasible solution $x$ of the LP of $J$ with cost at most $LIN(J)+1$; open $\lfloor x_j\rfloor$ bins of each configuration $j$, fill them with pieces, and delete the pieces so packed.
3. Pack the remaining pieces in at most $2 + \frac{2}{1-1/k}\ln\frac1g$ bins.
4. Reinsert the eliminated pieces, using a new bin only when necessary.

Its cost on $I$ is written $A(I)$.

Formalization targets

Goal: Theorem 4 with explicit constants

For every instance $I$ with $SIZE(I) \ge 2$, every packing that ALGORITHM 2 with $k=2$ and $g = 1/SIZE(I)$ can output is a packing of $I$ with

$$A(I) \le OPT(I) + \bigl(1 + \log_2 OPT(I)\bigr)\bigl(9 + 4\ln OPT(I)\bigr) + 2 + 4\ln OPT(I).$$

This is the paper's $A(I) \le OPT(I) + O(\log^2 OPT(I))$, with the constants that its proof yields.

The general bound for ALGORITHM 2

For integers $k \ge 2$, $0 < g \le \tfrac12$ and $SIZE(I) \ge 1$:

$$A(I) \le \max\Bigl\{(1+2g)\,OPT(I) + 1,\ OPT(I) + \Bigl[1 + \frac{\ln SIZE(I)}{\ln k}\Bigr]\Bigl[1 + 4k + 2k\ln\frac1g\Bigr] + 2 + \frac{2}{1-\frac1k}\ln\frac1g\Bigr\}.$$

Milestones

In attack order: Lemmas 1–3; Theorem 2 (items 1–3, the bound on $J'$, item 4 corrected); the per-iteration shrinking of $SIZE$; the bound on the number $t$ of iterations; the telescoping of $LIN$; the bin count after Step 3; the general bound.

Significance

The bound gives a polynomial-time algorithm whose additive error is polylogarithmic in the optimum, hence a fully polynomial asymptotic approximation scheme ($O(\log^2 OPT) = o(OPT)$). Varying $k$ and $g$ trades running time for error, as the paper notes after Theorem 4. The scheme of solving the rounded LP, keeping its integer part and re-grouping the residual is reused by later additive results, including the $O(\log OPT)$ bound of Hoberg and Rothvoss.

The result has been proved since 1982. No machine-checked proof of it, or of any bin-packing approximation guarantee of this kind, is known to exist in Lean or Mathlib. The mission produces a formal version whose hypotheses and constants are explicit. It also corrects two printed statements whose published forms are false: Theorem 2, item 4, and the chain of inequalities in the analysis that relies on it. The corrections are disclosed in the statements.

Difficulty

Rounding a single LP solution does not suffice. A basic solution of the configuration LP has at most $m$ fractional variables, and after rounding down, the leftover pieces form an instance of size at most $m(J)$. With linear grouping that leftover is of order $1/\varepsilon^2$ and costs a constant factor. The difficulty is making the residual shrink geometrically. Geometric grouping must produce an instance $J$ with $m(J) \le SIZE/k + O(\ln(1/g))$ distinct sizes while discarding only $O(k\ln(1/g))$ in $J'$. The residual must then be re-grouped and re-solved. Each step must be accounted for simultaneously in $SIZE$, $LIN$ and $OPT$, with an additive loss per iteration; the harmonic-sum estimate behind $SIZE(J')$ and the telescoping of $LIN$ across iterations carry most of the weight.

Formalization scope

• Model. An instance is a Multiset ℝ with sizes in the open interval $(0,1)$; real sizes generalize the paper's rationals, and the interval is open because a group of size at least $k$ must contain more than $k$ pieces. Packings are Multiset (Multiset ℝ). $OPT$ and $LIN$ are infima over nonempty sets. LP solutions are finitely supported functions on configurations; "basic" means extreme point.
• Subroutine contract. The Fractional Bin-Packing procedure is modelled only by its stated output: any basic feasible solution of cost at most $LIN(J)+1$. The ellipsoid method of §6 is not modelled.
• Runs. ALGORITHM 2 is a relation Alg2Run k g I P, witnessed by a trace. Every bound holds for every run: every admissible subroutine output, every packing at Steps 2 and 3 within the prescribed counts, every choice of pieces for the principal bins (which must fill every available slot), and every order of the Step 4 insertion. A separate well-definedness item states that a run exists, so the bounds are not vacuous.
• Explicit constants. $O(\log^2 OPT(I))$ in Theorem 4 is replaced by $(1+\log_2 OPT)(9 + 4\ln OPT) + 2 + 4\ln OPT$. The asymptotic threshold is made explicit as $SIZE(I) \ge 2$. $\ln$ is Real.log and $\log_2$ is Real.logb 2.
• Corrected statements. The last group of geometric grouping may fall short of $k$, which the paper ignores. For it, $\Delta G_q$ consists of the $\max(0, l_q - l_{q-1})$ smallest pieces. Theorem 2, item 4 is stated as $m(J) \le SIZE(J)/k + \ln(1/a(I)) + 1$; the printed version without $+1$ fails for $I = \{0.95, 0.95, 0.95, 0.9\}$, $k = 2$. Theorem 2 is stated for integers $k \ge 2$, which its proof needs. The iteration bound is stated for $t \ge 1$ and for the instance after Step 1.
• Out of scope. Running times, polynomiality, the function $T(m,n)$, the number of subroutine calls, §6, ALGORITHM 3 and Theorem 5.
• Ruling out trivial versions. "There exists a packing with at most $OPT(I) + \dots$ bins" is trivially true and is not the goal. The goal bounds every output of the algorithm, and the existence item shows that outputs exist.

Contributions welcome: milestone proofs; a harmonic-sum bound $\sum_{j=a}^{b} 1/j \le \ln\frac{b}{a-1}$; extreme-point facts for $\{x \ge 0 : Ax \ge b\}$ (at most as many nonzero coordinates as rows; an optimal extreme point exists), reusable beyond bin packing; monotonicity of $LIN$ and $OPT$ under the piecewise order.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982), IEEE, pp. 312–320, 1982. https://doi.org/10.1109/SFCS.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1 + ε in linear time, Combinatorica 1(4), 349–355, 1981. https://doi.org/10.1007/BF02579456
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-case performance bounds for simple one-dimensional packing algorithms, SIAM J. Comput. 3(4), 299–325, 1974. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoss, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. 28th ACM-SIAM SODA, 2616–2625, 2017. https://doi.org/10.1137/1.9781611974782.172

Motivation

How many times can $n$ points and $t$ lines in the plane meet? The question is the prototype of incidence geometry, and the answer controls a long list of problems in discrete and computational geometry: the number of lines rich in points, the number of distinct distances or unit distances among $n$ points, the complexity of arrangements, and sum–product estimates in additive combinatorics. Erdős asked for the order of magnitude when $t = n$ and conjectured that the answer is $n^{4/3}$; Erdős and Purdy asked for the matching bound on the number of lines containing at least $k$ of the points.

Szemerédi and Trotter settled both questions in Extremal Problems in Discrete Geometry (Combinatorica 3 (1983) 381–392, doi:10.1007/BF02579194). Their principal theorem bounds the number of point–line incidences by $c_1 n^{2/3} t^{2/3}$ over the whole range $\sqrt n \le t \le \binom n2$, and the same paper derives from it the Erdős–Purdy bound on $k$-rich lines, a version of Dirac's conjecture (proved independently by Beck, Combinatorica 3 (1983)), and a bound on the number of sequences of line densities.

Timeline.

• Erdős conjectures $O(n^{4/3})$ incidences for $n$ points and $n$ lines, and shows by a grid construction that this order would be sharp.
• 1983: Szemerédi and Trotter prove the bound $c_1 n^{2/3} t^{2/3}$ for $\sqrt n \le t \le \binom n2$, with $c_1 = 10^{60}$, by a minimal-counterexample argument and a covering lemma for squares from their earlier paper.
• 1990: Clarkson, Edelsbrunner, Guibas, Sharir and Welzl give a second proof by cuttings, with a far smaller constant (Discrete Comput. Geom. 5 (1990) 99–160).
• 1997: Székely derives the bound in a few lines from the crossing lemma (Combin. Probab. Comput. 6 (1997) 353–358).

Setting

Work in the Euclidean plane $\mathbb R^2$, written Plane in the Lean development. A line is an affine subspace $l \subseteq \mathbb R^2$ whose direction space has dimension one (IsLine l). Let $\mathcal P$ be a finite set of $n$ points and $\mathcal L$ a finite family of $t$ distinct lines. The number of incidences is

$$I(\mathcal P, \mathcal L) = \#\{(p, l) \in \mathcal P \times \mathcal L : p \in l\},$$

written incidences P L. The degree $d_i$ of a point $p_i$ is the number of lines of $\mathcal L$ through it (degree L p), and the density $y_j$ of a line $l_j$ is the number of points of $\mathcal P$ on it (density P l); so $I = \sum_i d_i = \sum_j y_j$.

For the covering lemma, coordinate axes are fixed and a square is a closed axis-parallel square $Q(a,b,s) = [a, a+s] \times [b, b+s]$ with side $s > 0$ (closedSquare (a, b, s)); its interior is the open square $(a, a+s) \times (b, b+s)$ (openSquare). A square contains the points of $\mathcal P$ in the closed square, and a family of squares covers the points lying in at least one of them.

Formalization targets

Goal: Theorem 1 (p. 381, restated and proved on p. 383)

There is an absolute constant $c_1$ such that for every finite point set $\mathcal P$ with $|\mathcal P| = n$ and every finite family $\mathcal L$ of $t$ distinct lines,

$$\sqrt n \le t \le \binom n2 \quad\Longrightarrow\quad I(\mathcal P, \mathcal L) \le c_1\, n^{2/3}\, t^{2/3}.$$

The goal leaves $c_1$ unspecified. The paper's proof gives $c_1 = 10^{60}$, and later proofs give much smaller values; any improvement of the constant still proves this statement.

Milestones, in the order the proof uses them

1. Section 3, display on p. 383. Two distinct lines meet in at most one point, so the number of good intersections is at most the number of pairs of lines:

$$\sum_{i} \binom{d_i}{2} \le \binom t2, \qquad \frac{I^2}{2n} - \frac I2 \le \frac{t^2}{2}.$$

2. Section 3, inequality (1), p. 384. $0.6\,x + (1-x)^{2/3} \le 1$ for $0 < x \le 1/2$.
3. Section 3, inequality (5), p. 385. $x^{2/3} + (1-x)/100 + 2^{-1/3}(1-x)^{2/3} \le 1$ for $0 < x \le 0.1$, and the reverse strict inequality holds somewhere in $(0.1, 0.2)$.
4. Section 3, display on p. 387. With $M = 10^{10}$, $2^{i/3}(1 - 2/M)^{4i/3} \ge 200/((0.1)^{1/3} 2^{2/3})$ for every integer $i \ge 30$.
5. Section 2, Lemma (covering lemma), p. 382. For integers $1 \le r_1 \le n$ and $r_2 \ge 256 r_1$, every set of $n$ points is covered, to at least $n/16$ of its points, by a family of squares with pairwise disjoint interiors, each containing between $r_1$ and $r_2$ of the points.

Significance

The result. The bound $n^{2/3} t^{2/3}$ is sharp up to the constant throughout the range $\sqrt n \le t \le \binom n2$, as integer-grid configurations show. Outside that range the trivial bounds $n + t^2$ and $t + n^2$ take over. Theorem 1 is the source of the $O(n^2/k^3)$ bound on $k$-rich lines (the paper's Theorem 2), of Beck's theorem (Theorem 3), and, through them, of the unit-distance bound $O(n^{4/3})$, of the Elekes sum–product estimate and of many algorithmic bounds on arrangements. It is the first nontrivial case of the polynomial-partitioning incidence theory developed since 2010.

Formalizing it. The theorem has been proved, and reproved in several ways, for four decades. To the best of the mission's knowledge Mathlib has no statement of it, of the crossing lemma, or of any point–line incidence bound in the Euclidean plane. This mission produces a checked statement of the theorem with lines as genuine one-dimensional affine subspaces and an absolute constant. It also produces checked statements of the auxiliary facts the 1983 proof uses. A complete proof may follow the original argument, the cutting argument or Székely's crossing-lemma argument; any of them closes the goal.

Difficulty

Counting pairs of lines through common points (milestone 1) gives only $I \lesssim n^{1/2} t + n$, and its dual gives $I \lesssim t^{1/2} n + t$. These Cauchy–Schwarz bounds use only the fact that two lines meet at most once, a property shared by lines in finite projective planes, where the incidence count genuinely reaches order $n^{3/2}$. Any proof of the $n^{2/3} t^{2/3}$ bound must therefore use a property of the real plane that the finite geometries lack: order, continuity, or the planarity of drawings. Szemerédi and Trotter use it through a covering lemma for axis-parallel squares, whose proof is only cited in the paper ([7]). The remaining difficulty is keeping the constants of a multi-stage minimal-counterexample argument under control.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). A line is an AffineSubspace ℝ Plane whose direction has Module.finrank equal to $1$. Every statement requires IsLine of each member of $\mathcal L$, so neither the whole plane nor a single point counts as a line. The points form a Finset Plane and the lines a Finset (AffineSubspace ℝ Plane), which makes the $t$ lines distinct. Incidences, degrees and densities are Finset.filter cardinalities under classical decidability. Powers $n^{2/3}$, $t^{2/3}$ are Real.rpow of the counts cast to $\mathbb R$, and $\binom n2$ is Nat.choose.

In the goal, the constant $c_1$ is quantified before the points and the lines. The form "for every configuration there is a $c_1$" is trivially true (take $c_1 = I + 1$) and is not this theorem. Both ends of the range $\sqrt n \le t \le \binom n2$ are kept exactly: without the lower end, a single line through $n$ collinear points has $n$ incidences, more than $c_1 n^{2/3}$ for large $n$.

The goal follows the wording of p. 381 ("at most"). The restatement on p. 383 says "less than", which fails at $n = t = 0$ and is equivalent for $n \ge 1$ after doubling $c_1$. The covering lemma is stated with the added non-degeneracy hypotheses $1 \le r_1 \le n$. As printed it fails when $0 < n < r_1$ (no square can hold $r_1$ points), and when $r_1 = r_2 = 0$ with $n > 0$.

A full development needs a real-plane incidence toolkit: a crossing lemma or a cutting lemma, or the covering lemma with its quadtree proof. That toolkit is reusable for $k$-rich lines, Beck's theorem, unit distances and sum–product bounds, and contributions of such infrastructure as separate theorems are welcome. The three numerical milestones are self-contained real-analysis exercises.

Selected references

• E. Szemerédi, W. T. Trotter, Jr., Extremal problems in discrete geometry, Combinatorica 3 (1983) 381–392. https://doi.org/10.1007/BF02579194
• E. Szemerédi, W. T. Trotter, Jr., A combinatorial distinction between the Euclidean and projective planes, European J. Combin. 4 (1983) 385–394. https://doi.org/10.1016/S0195-6698(83)80036-5
• J. Beck, On the lattice property of the plane and some problems of Dirac, Motzkin and Erdős in combinatorial geometry, Combinatorica 3 (1983) 281–297. https://doi.org/10.1007/BF02579184
• K. L. Clarkson, H. Edelsbrunner, L. J. Guibas, M. Sharir, E. Welzl, Combinatorial complexity bounds for arrangements of curves and spheres, Discrete Comput. Geom. 5 (1990) 99–160. https://doi.org/10.1007/BF02187783
• L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. 6 (1997) 353–358. https://doi.org/10.1017/S0963548397002976

Motivation

Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each $0$–$1$ matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.

Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without $Q_6$ or $b(Q_6)$ minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.

Setting

All sets are finite. A clutter $\mathbf L$ is a finite collection of finite sets, no member of which is contained in another; $\emptyset$ and $\{\emptyset\}$ are the two trivial clutters. Its ground set is $E(\mathbf L)=\bigcup_{A\in\mathbf L}A$. The blocker $b(\mathbf L)$ is the collection of minimal subsets of $E(\mathbf L)$ that meet every member of $\mathbf L$, and $\tau(\mathbf L)$ is the minimum cardinality of a member of $b(\mathbf L)$.

$\mathbf L$ is Mengerian if $\mathbf L=\{\emptyset\}$, or if for every weight map $w:E(\mathbf L)\to\mathbb Z^+$ there is an integral packing $q:\mathbf L\to\mathbb Z^+$ with $\sum_{A\ni x}q(A)\le w(x)$ for each $x\in E(\mathbf L)$ and

$$\sum_{A\in\mathbf L}q(A)=\min_{B\in b(\mathbf L)}\sum_{x\in B}w(x).$$

For a set $Z$, the deletion is $\mathbf L\setminus Z=\{A\in\mathbf L:A\cap Z=\emptyset\}$ and the contraction $\mathbf L/Z$ is the collection of minimal members of $\{A-Z:A\in\mathbf L\}$ (minimal, not minimal nonempty). A minor of $\mathbf L$ is any clutter obtained by a finite sequence of deletions and contractions.

A clutter is binary if $|A\cap B|$ is odd for all $A\in\mathbf L$ and $B\in b(\mathbf L)$; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally

$$Q_6=\{\{1,3,5\},\{1,4,6\},\{2,3,6\},\{2,4,5\}\},$$

the triangles of $K_4$ with its edges labelled $1,\dots,6$.

For the structure theory, a circuit of a binary clutter is a minimal nonempty $C\subseteq E(\mathbf L)$ with $|C\cap B|$ even for every $B\in b(\mathbf L)$; $x$ and $y$ are parallel when $\{x,y\}$ is a circuit, and the point $\langle x\rangle$ is the parallel class of $x$. With $mb(\mathbf L)=\{B\in b(\mathbf L):|B|=\tau(\mathbf L)\}$, $\mathbf L$ is critical if $E(mb(\mathbf L))=E(\mathbf L)$. In a critical binary clutter, $x\to y$ means that every member of $mb(\mathbf L)$ containing $x$ contains $y$ while $y\notin\langle x\rangle$, and $y$ is initial if no $x$ has $x\to y$. MBC abbreviates "Mengerian binary clutter".

Formalization targets

Goal: Seymour's theorem (p. 209)

For every binary clutter $\mathbf L$,

$$\mathbf L\ \text{is Mengerian}\iff \mathbf L\ \text{has no minor isomorphic to } Q_6 .$$

Milestones

In the order the proof uses them:

• (2.3) Every minor of a Mengerian clutter is Mengerian.
• Section 1, p. 193. $Q_6$ is not Mengerian. With (2.3) this is the "only if" direction.
• (3.6)(i) Circuits of a binary clutter have at least two elements.
• (3.6)(iii) If $Z\subseteq E(\mathbf L)$ meets every member of $b(\mathbf L)$ evenly, then $Z$ is a disjoint union of circuits. If it meets every member oddly, then $Z$ is a disjoint union of circuits and one member of $\mathbf L$.
• (4.3) In a critical MBC, $x\to y$ implies $y\not\to x$.
• (4.4) In a critical MBC, $x\to y$ gives a circuit $C\ni x,y$ with $|C|\ge3$, $z\to y$ for $z\in C-\{y\}$, and $|B-(C-\{y\})|\ge\tau(\mathbf L)-1$ for $B\in b(\mathbf L)$.
• (4.5) In a critical MBC, a non-initial $x$ lies on a circuit $C$ with $|C|\ge3$ whose other elements are initial and point to $x$, and $|B\cap(C-\{x\})|\le1$ for $B\in mb(\mathbf L)$.
• (4.6) A nontrivial critical MBC has a member consisting of initial elements.
• (5.1) A binary clutter with six elements $x_1,y_1,x_2,y_2,x_3,y_3$ whose only circuits are the three sets $\{x_i,y_i,x_j,y_j\}$, together with a member $A$ that meets each pair $\{x_i,y_i\}$ once and satisfies a minimality condition, has a $Q_6$ minor.

Significance

The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system $Mx\ge1$, $x\ge0$ has integral optimal primal and dual solutions for every integral cost vector, and it identifies $Q_6$ as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid $M$ the port $\Omega(M)$ is Mengerian for every element $\Omega$ if and only if $M$ is binary and has no $F_7^*$ minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining $s$ to $s'$ or $t$ to $t'$ is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).

The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.

Difficulty

The "only if" direction is short: minors of Mengerian clutters are Mengerian, and $Q_6$ fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a $Q_6$-free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and $Q_6$ itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the $Q_6$ minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.

Formalization scope

Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, $E(\mathbf L)$ is the union of members, and deletion and contraction take an arbitrary finite set $Z$. Weights $w$ and packings $q$ are $\mathbb N$-valued. The minimum in the Mengerian condition is expressed as "some $B\in b(\mathbf L)$ of least weight has weight equal to the packing value", never as an infimum. $\{\emptyset\}$ is Mengerian by the paper's convention, and $\tau(\{\emptyset\})$, which the paper leaves undefined, has the junk value $0$ in Lean; every item reading $\tau$ excludes $\{\emptyset\}$ or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a $Q_6$ minor" means that some minor equals the image of $Q_6$ (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.

Four readings would change the theorem and are ruled out: real-valued packings $q$ (the weak max-flow min-cut property, which $Q_6$ has, so the goal would be false), a non-minimal blocker or one not restricted to $E(\mathbf L)$, dropping the $\{\emptyset\}$ exception, and reading "$Q_6$ minor" as literal equality instead of isomorphism.

A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation $\mathbf L_w$. The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts $b(b(\mathbf L))=\mathbf L$, (2.1) and (2.2), and of the equivalences in (3.2) are welcome.

Selected references

• P. D. Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977) 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• J. Edmonds and D. R. Fulkerson, Bottleneck extrema, J. Combin. Theory 8 (1970) 299–306. https://doi.org/10.1016/S0021-9800(70)80083-7
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956) 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conf. Ser. in Appl. Math. 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105