Combinatorics

Motivation

Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).

Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).

Setting

A game tree $\Gamma$ is a finite rooted tree. Each leaf is a finished play $\pi$ and carries the payoff $\mathfrak F_1(\pi) \in \mathbb R$ to player 1; player 2 receives $-\mathfrak F_1(\pi)$. Each internal node is a move $\mathfrak M$ of one of three kinds $k$, with alternatives $\sigma = 1, \dots, \alpha$ leading to subtrees $\Gamma_\sigma$:

• $k = 0$, a chance move, where alternative $\sigma$ occurs with probability $p(\sigma) \geqq 0$, $\sum_\sigma p(\sigma) = 1$;
• $k = 1$, a personal move of player 1, with $\alpha \geqq 1$;
• $k = 2$, a personal move of player 2, with $\alpha \geqq 1$.

A pure strategy $\tau_1$ of player 1 is a complete plan choosing an alternative at every node of kind 1; $\tau_2$ does the same at every node of kind 2. The normalized form $\mathcal H(\tau_1, \tau_2)$ is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,

$$v_1 = \operatorname{Max}_{\tau_1} \operatorname{Min}_{\tau_2} \mathcal H(\tau_1, \tau_2), \qquad v_2 = \operatorname{Min}_{\tau_2} \operatorname{Max}_{\tau_1} \mathcal H(\tau_1, \tau_2).$$

Always $v_1 \leqq v_2$; the game is strictly determined when $v_1 = v_2$ (14.4.2).

For a function $f(\sigma_1)$ of the alternatives of the first move $\mathfrak M_1$, of kind $k_1$, the operation $M^{k_1}_{\sigma_1}$ of (15:8) is $\sum_{\sigma_1} p_1(\sigma_1) f(\sigma_1)$, $\operatorname{Max}_{\sigma_1} f(\sigma_1)$ or $\operatorname{Min}_{\sigma_1} f(\sigma_1)$ for $k_1 = 0, 1, 2$. Applying these operations from the leaves back to the root gives the backward-induction value $v(\Gamma)$.

Formalization targets

Goal: 15.6.1 with (15:12)

For every finite game tree $\Gamma$,

$$v_1 = v_2 = v = M^{k_1}_{\sigma_1} M^{k_2(\sigma_1)}_{\sigma_2} \cdots M^{k_\nu(\sigma_1, \dots, \sigma_{\nu-1})}_{\sigma_\nu} \mathfrak F_1(\pi(\sigma_1, \dots, \sigma_\nu)).$$

Both the equality $v_1 = v_2$ and the value formula are part of the goal.

Milestones

• (13:E): for finite nonempty domains and $f$ ranging over all functions of $x$, $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Min}_f \operatorname{Max}_x \psi(x, f(x))$; and (13:G): $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Max}_x \operatorname{Min}_u \psi(x, u)$.
• (15:2)–(15:7): $v_k = M^{k_1}_{\sigma_1} v_{\sigma_1/k}$ for $k = 1, 2$, one milestone for each kind of first move, without assuming that any game is strictly determined.
• (15:C:a): a game of length $0$ is strictly determined with value $w$; (15:C:b): if every $\Gamma_{\sigma_1}$ is strictly determined, so is $\Gamma$.
• (15:13), (15:D:a)–(15:D:c): for games without chance moves whose plays end in $1, 0, -1$, the value is one of these three numbers, and it decides which player can force a win or whether both can force a tie.

Significance

The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.

Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.

Difficulty

The recursions (15:2)–(15:7) are not formal consequences of the definitions: $v_1$ and $v_2$ are extrema over whole plans of $\Gamma$, while the right-hand sides are extrema over plans of the separate games $\Gamma_{\sigma_1}$. At a personal move of player 1, $v_2 = \operatorname{Max}_{\sigma_1} v_{\sigma_1/2}$ requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over $\tau_1$ and the Min over $\tau_2$ as interchangeable without this step is circular.

A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of $\Gamma$ are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change $\mathcal H$.

Formalization scope

A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from $0$). The conditions $p \geqq 0$, $\sum p = 1$ and $\alpha \geqq 1$ at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; $\mathcal H$ is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.

Standing hypotheses and conventions taken from the book:

• finite strategy sets and attained extrema (13.2.1, 14.1.1): finite trees with finitely many alternatives at every move;
• perfect information, i.e. preliminarity equals anteriority (6.4.1, (15:B)): built into the tree model, which is the sequence of games (15:1);
• zero-sum two-person (15.3.1): one payoff $\mathfrak F_1$, player 2 receives $-\mathfrak F_1$ and minimizes $\mathcal H$;
• chance probabilities nonnegative and summing to one (15.4.2, 10.1.1); $\alpha \geqq 1$ at every move;
• (15:D) additionally assumes no chance moves and outcomes $1, 0, -1$ (15.7.1).

The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length $\nu$ for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.

Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make $v_1 = v_2$ trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.

Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of $\Gamma$ with the book's recursive description (15.4.2, 15.5.1).

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§6, 11, 13–15. https://doi.org/10.1515/9781400829460
• E. Zermelo, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels, Proc. Fifth International Congress of Mathematicians, vol. II, 1913, pp. 501–504.
• U. Schwalbe, P. Walker, Zermelo and the early history of game theory, Games and Economic Behavior 34 (2001), 123–137. https://doi.org/10.1006/game.2000.0794
• H. W. Kuhn, Extensive games and the problem of information, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton, 1953, 193–216. https://doi.org/10.1515/9781400881970-012

Motivation

Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.

The chapter illustrates this on the machine investment problem: first buy $m$ identical machines at cost $c$ each, knowing only the distribution of the processing times of $n$ jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.

Setting

Let $p_1, p_2, \dots$ be processing times: independent, identically distributed, nonnegative random variables on a probability space $(\Omega, \mathcal F, P)$ with mean $\mu = \mathbb E p_1 > 0$ and finite second moment $\mathbb E p_1^2 < \infty$. The instance with $n$ jobs uses the first $n$ of them.

An assignment of the $n$ jobs to $m \ge 1$ identical machines is a map $\sigma : \{1, \dots, n\} \to \{1, \dots, m\}$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ and the makespan of $\sigma$ is its largest load. The minimum makespan is

$$C^*_n(m) = \min_{\sigma} \max_{i=1,\dots,m} \sum_{j:\ \sigma(j) = i} p_j ,$$

and the machine investment problem is to minimize $Z_n(m) = cm + \mathbb E\, C^*_n(m)$ over integers $m$ (8.9).

List scheduling takes the jobs in the order $1, \dots, n$ and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is $C^H_n(m)$. Write $S_n = \sum_{j=1}^n p_j$ and $p_{\max} = \max_{j \le n} p_j$.

For §8.3, the estimate $Z'_n(m) = cm + n\mu/m$ is minimized over integers by the heuristic first-stage decision $m^{H1}_n$, the better of $\lfloor\sqrt{n\mu/c}\rfloor$ and $\lceil\sqrt{n\mu/c}\rceil$. A clairvoyant decision maker who sees the processing times first chooses $m^\circ_n(\omega) \ge 1$ minimizing $cm + C^*_n(m)$.

Formalization targets

Goal: Eq. (8.13)

For machine counts $m = m(n) \ge 1$ with $m(n) = O(\sqrt n)$,

$$P\Bigl\{ \lim_{n\to\infty} \frac{C^*_n(m)}{n\mu/m} = 1 \Bigr\} = 1 .$$

The machine count is allowed to grow with $n$; this is the regime the first-stage heuristic lives in, since $m^{H1}_n$ is of exact order $\sqrt n$.

Milestones

1. Eq. (8.10): the deterministic sandwich $S_n/m \le C^*_n(m) \le C^H_n(m) \le S_n/m + p_{\max}$, divided by $n\mu/m$.
2. Eq. (8.11): the strong law of large numbers, $(S_n - n\mu)/(n\mu) \to 0$ almost surely (a published platform theorem).
3. Lemma 8.1 (i): $p_{\max}/\sqrt n \to 0$ almost surely.
4. Eq. (8.12): $m\, p_{\max}/(n\mu) \to 0$ almost surely when $m = O(\sqrt n)$.
5. Lemma 8.1 (ii): $\mathbb E\, p_{\max}/\sqrt n \to 0$.
6. p. 207: $\mathbb E\, C^*_n(m)/(n\mu/m) \to 1$ when $m = O(\sqrt n)$.
7. p. 211, asymptotic clairvoyance: almost surely

$$\lim_{n\to\infty} \frac{c\, m^{H1}_n + C^{H2}_n(m^{H1}_n)}{c\, m^\circ_n + C^*_n(m^\circ_n)} = 1 ,$$

where $C^{H2}_n$ is the list-scheduling makespan.

Significance

Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function $n\mu/m$ of the data and the first-stage decision. Its expectation version replaces the intractable term $\mathbb E\,C^*_n(m)$ in (8.9) by $n\mu/m$, and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.

All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).

Difficulty

The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls $S_n/n$, but the error term $m\, p_{\max}/(n\mu)$ is of order $p_{\max}/\sqrt n$ once $m$ grows like $\sqrt n$, and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth $m(n) = O(\sqrt n)$ is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice $m^\circ_n$ is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.

Formalization scope

Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's $p_j$ is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and $\mu > 0$ are not printed in the book; they are implicit in "processing times" and in the division by $n\mu$. Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.

The book writes "$m = 0(\sqrt n)$"; this is read as $m$ a function of $n$ with $m(n) \ge 1$ and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed $m$ would trivialize it into the strong law and is ruled out. "$\Pr\{\lim \dots = 1\} = 1$" means that almost surely the limit exists and equals $1$. Expectations are Bochner integrals of functions that are measurable and bounded by $S_n$, hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over $m \ge 1$ (the book writes $m \in \mathbb N$; no machine cannot process any job, and the Lean value $C^*_n(0)$ is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.

Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at $0$ and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.

Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.

Selected references

• A. H. G. Rinnooy Kan, L. Stougie, "Stochastic Integer Programming", in Yu. Ermoliev, R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 8, pp. 201–213. https://doi.org/10.1007/978-3-642-61370-8
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, 3rd edition, Wiley, 1968 (cited by the chapter for Lemma 8.1).
• M. A. H. Dempster, M. L. Fisher, L. Jansen, B. J. Lageweg, J. K. Lenstra, A. H. G. Rinnooy Kan, "Analysis of heuristics for stochastic programming: results for hierarchical scheduling problems", Mathematics of Operations Research 8 (1983) 525–537. https://doi.org/10.1287/moor.8.4.525
• J. K. Lenstra, A. H. G. Rinnooy Kan, L. Stougie, "A framework for the design and analysis of hierarchical planning systems", Annals of Operations Research 1 (1984) 23–42. https://doi.org/10.1007/BF01874451
• R. L. Graham, "Bounds on multiprocessing timing anomalies", SIAM Journal on Applied Mathematics 17 (1969) 416–429. https://doi.org/10.1137/0117039

Motivation

Chapter 16 of Keller and Trotter's Applied Combinatorics (2017 Edition, CC BY-SA 4.0) is a survey of seven topics. Two of them are self-contained results with complete proofs on the page, and this mission formalizes both.

The first is the Lovász Local Lemma. It was introduced by Erdős and Lovász in 1975 to show that certain hypergraphs are 3-colourable (Erdős–Lovász 1975), and it has become a standard tool of the probabilistic method. The classical probabilistic argument shows that a random object has a property with probability close to one. The local lemma is different: it shows that a good object exists even when it is exceedingly rare, provided that each "bad" event depends on only a few of the others. It underlies lower bounds for Ramsey numbers such as $R(3,n) \ge c\,n^2/\ln^2 n$, the subject of Section 16.8. It also underlies results on colouring, satisfiability and Latin transversals, and the algorithmic version of Moser–Tardos (2010).

The second is the Gale–Ryser Theorem, proved independently by Gale (1957) and Ryser (1957). It decides when a zero–one matrix with prescribed row and column sums exists. Equivalently, it decides when a pair of sequences is the degree sequence of a bipartite graph. Its condition is a comparison in the dominance order on integer partitions.

Setting

A finite probability space is a finite set $\Omega$ with a function $P$ defined on all subsets, finitely additive, with $P(\emptyset) = 0$ and $P(\Omega) = 1$. Let $\mathcal F = (A_i)_{i \in \iota}$ be a finite family of events. For a subfamily $G \subseteq \iota$ write

$$\prod_{j \in G} \overline{A_j} = \bigcap_{j \in G} (\Omega \setminus A_j),$$

the event that every event of $G$ fails; for $G = \emptyset$ it is $\Omega$. Fix, for each $i$, a subfamily $N(i) \subseteq \iota \setminus \{i\}$. The event $A_i$ is independent of any event not in $N(i)$ if $P(A_i \mid \prod_{j\in G}\overline{A_j}) = P(A_i)$ for every $G$ with $i \notin G$ and $G \cap N(i) = \emptyset$. In the formalization this condition is IndepOutside μ A N i, written as

$$P\Big(A_i \cap \prod_{j\in G}\overline{A_j}\Big) = P(A_i)\,P\Big(\prod_{j\in G}\overline{A_j}\Big).$$

A partition of a positive integer $t$ is a non-increasing string $V = (v_1, \dots, v_m)$ of positive integers with sum $t$; $\mathcal P(t)$ is the set of partitions of $t$. It is partially ordered by $V \ge W$ iff $V$ is no longer than $W$ and every partial sum $v_1 + \dots + v_j$ is at least $w_1 + \dots + w_j$ (Dominates). $V$ covers $W$ when $V > W$ with nothing in between (Covers). The dual partition $V^d$ has $v_1$ entries, the $j$-th being the number of $i$ with $v_i \ge j$ (dual). A zero–one matrix with row sum string $R$ and column sum string $C$ is an $m \times n$ matrix with entries in $\{0,1\}$ whose row $i$ sums to $r_i$ and column $j$ to $c_j$ (IsZeroOneMatrixWithSums).

Formalization targets

Goal: the asymmetric local lemma (Lemma 16.14)

If $0 < x(i) < 1$ and $P(A_i) \le x(i)\prod_{j \in N(i)}(1 - x(j))$ for every $i$, then for every non-empty $G \subseteq \iota$

$$P\Big(\prod_{i \in G}\overline{A_i}\Big) \ge \prod_{i\in G}\big(1 - x(i)\big), \qquad\text{and}\qquad P\Big(\prod_{i\in\iota}\overline{A_i}\Big) > 0 .$$

Milestone: the symmetric local lemma (Lemma 16.15)

If $0 < p < 1$, $d \ge 1$, $P(A_i) \le p$, $|N(i)| \le d$ and $e\,p\,(d+1) < 1$, then

$$P\Big(\prod_{i\in\iota}\overline{A_i}\Big) \ge \Big(1 - \frac1{d+1}\Big)^{|\mathcal F|} > 0 .$$

Milestones: covers in $\mathcal P(t)$ and Gale–Ryser (Proposition 16.11, Theorem 16.12)

If $V$ covers $W$ in $\mathcal P(t)$, then $W$ arises from $V$ by moving one unit from a part $v_i$ to a later part $v_j$ (possibly a new part of size one), and all parts strictly between equal $v_i - 1$. For partitions $R, C$ of $t > 0$,

$$\exists\, M \in \{0,1\}^{m\times n} \text{ with row sums } R \text{ and column sums } C \iff R^d \ge C \text{ in } \mathcal P(t).$$

The Erdős–Ko–Rado bound of Theorem 16.8 enters as the published reference FamousTheorems.erdos_ko_rado.

Significance

The local lemma is the entry point to the probabilistic method's rare-event side. A formal statement in the book's form — finite spaces and the book's conditional notion of independence — is a reusable interface for formalizing its applications: Ramsey lower bounds, hypergraph colouring and $k$-SAT with bounded occurrences. The symmetric form is the version most applications call. Mathlib has no local lemma. The platform has a conditional-probability bound from an unrelated paper mission (Erdos390.WholePaper.finiteAsymmetricLocalLemma_conditionalBound), which bounds $P(A_i \cap \prod_{j\in s}\overline{A_j})$ with $0 \le x < 1$ and does not state the product lower bound for the joint failure.

Gale–Ryser is the prototype of margin problems for $\{0,1\}$-matrices and of degree-sequence characterizations (compare Erdős–Gallai for graphs). Formalizing it produces the dominance order, conjugate partitions and covering relations on sorted lists of positive integers. Mathlib has Nat.Partition but no dominance order or conjugate. None of these results is formalized on the platform. The results themselves are classical and proved; the work is formalizing the proofs.

Difficulty

For the local lemma, the naive induction on $|G|$ fails. Conditioning on the joint failure of a subfamily requires that failure to have positive probability, and that is only known after the inductive bound has been proved for smaller subfamilies. The induction must therefore carry the lower bound and the positivity of every smaller joint failure at once. It must also split each conditioning family into the part inside $N(i)$ and the part outside. The independence hypothesis controls only the part outside, and only through intersections of complements, not through arbitrary events.

For Gale–Ryser, necessity is an exchange argument, but sufficiency needs the fine structure of covers in the dominance order (Proposition 16.11): the case analysis of where the moved unit lands, including a new last part, and the fact that a maximal chain from $R^d$ down to $C$ exists. Converting the list-level statements into matrix constructions over Fin m × Fin n is the other main cost.

Formalization scope

• Probability space. Fintype Ω with DiscreteMeasurableSpace Ω and a measure μ with IsProbabilityMeasure μ; every subset is an event and probabilities are μ.real, as in the book's finite probability spaces.
• Family and neighbourhoods. The family is A : ι → Set Ω over a Fintype ι, so repeated events are allowed. Neighbourhoods are N : ι → Finset ι with i ∉ N i.
• Weights. 0 < x i < 1 is strict on both sides, as on the page.
• Independence. The conditional-probability equation is stated multiplicatively. This agrees with the book whenever the conditioning event has positive probability, and it is automatic otherwise.
• Excluded trivialization. The independence hypothesis is not full mutual independence of the family, which would make the product formula immediate. It is not pairwise independence either, under which the lemma is false. It is exactly the book's condition on intersections of complements.
• Explicit constant (Lemma 16.15). The book's displayed conclusion is misprinted: it mentions $\mathcal G$ and $x$, which are never introduced. The statement uses the bound the book's proof yields with $x(E) = 1/(d+1)$, namely $(1 - 1/(d+1))^{|\mathcal F|}$, with $|\mathcal F|$ = Fintype.card ι, together with positivity. Here $p$ and $d$ are real and $e$ is Real.exp 1.
• Partitions. Partitions are List ℕ, non-increasing with positive entries. Entries are 1-based through entry, and partial sums are (V.take j).sum.
• Dual partition. The page's rule "at least $n+1-j$" lists the conjugate in increasing order, and its example is misprinted (it sums to 40, not 42). The definition is the conjugate partition in non-increasing order, the only reading under which Theorem 16.12 holds.
• Matrices. Matrices are Matrix (Fin m) (Fin n) ℕ with entries in $\{0,1\}$.

Not included.

• The on-line colouring and antichain-partitioning results of Section 16.1 (Theorems 16.2, 16.4, 16.5) need a formal model of adaptive Builder/Assigner games.
• Theorem 16.9 (regular Markov chains) is stated without proof.
• Theorem 16.13 (van der Waerden) is stated without proof and followed by "Material will be added here".

Welcome contributions. Reusable infrastructure: a finite-space conditional-probability API, and the dominance order as a PartialOrder on sorted partitions linked to Nat.Partition.

Selected references

• M. T. Keller, W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 16, pp. 315–330. https://www.appliedcombinatorics.org/
• P. Erdős, L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and Finite Sets, 1975. https://www.renyi.hu/~p_erdos/1975-34.pdf
• D. Gale, A theorem on flows in networks, Pacific J. Math. 7 (1957). https://doi.org/10.2140/pjm.1957.7.1073
• H. J. Ryser, Combinatorial properties of matrices of zeros and ones, Canad. J. Math. 9 (1957). https://doi.org/10.4153/CJM-1957-044-3
• R. A. Moser, G. Tardos, A constructive proof of the general Lovász Local Lemma, J. ACM 57 (2010). https://doi.org/10.1145/1667053.1667060
• P. Erdős, C. Ko, R. Rado, Intersection theorems for systems of finite sets, Quart. J. Math. 12 (1961). https://doi.org/10.1093/qmath/12.1.313

Motivation

Many counting questions ask for the number of objects up to symmetry: necklaces of coloured beads that may be rotated and flipped, musical scales up to transposition, chemical isomers up to the symmetries of a molecule, graphs on $n$ vertices up to relabelling. Counting all configurations and dividing by the number of symmetries fails, because some configurations are fixed by some symmetries. The standard tool for such questions is the enumeration theorem of Redfield (1927) and Pólya (1937), which turns the symmetry group into a generating function recording not only how many inequivalent configurations there are but how many use each colour a prescribed number of times.

This mission formalizes Chapter 15 of Keller and Trotter's Applied Combinatorics (2017 Edition), which develops the theorem from Burnside's Lemma for an undergraduate audience. The chapter's footnotes record the history: the orbit-counting lemma was known to Cauchy and Frobenius before it appeared in Burnside's book, and Redfield's paper anticipating Pólya's work was rediscovered only around 1960.

Setting

Let $S$ be a finite set with $|S| = r$. A permutation group $G$ of $S$ is a set of bijections $S \to S$ containing the identity and closed under composition and inverses. Every permutation $\pi$ splits $S$ into disjoint cycles; a fixed point is a cycle of length $1$. Write $j_k(\pi)$ for the number of cycles of length $k$, so that $j_1 + 2j_2 + \cdots + r j_r = r$. The cycle index of $G$ is the polynomial with rational coefficients

$$P_G(x_1, \ldots, x_r) = \frac{1}{|G|} \sum_{\pi \in G} x_1^{j_1(\pi)} x_2^{j_2(\pi)} \cdots x_r^{j_r(\pi)}.$$

For the eight symmetries $D_8$ of a square, $P_{D_8} = \tfrac18(x_1^4 + 2x_1^2x_2 + 3x_2^2 + 2x_4)$.

A coloring of $S$ with colours $c_1, \ldots, c_m$ is a map $f : S \to \{c_1, \ldots, c_m\}$; $\mathcal C$ denotes the set of all $m^r$ of them. A permutation acts on colorings by $\pi^*(f) = f \circ \pi^{-1}$, and two colorings are equivalent when some $\pi \in G$ carries one to the other. The weight of $f$ is the monomial $\prod_{s \in S} f(s) = c_1^{a_1} \cdots c_m^{a_m}$ in commuting variables, where $a_i$ counts the points coloured $c_i$. The pattern inventory is the polynomial whose coefficient of $c_1^{a_1}\cdots c_m^{a_m}$ is the number of equivalence classes of colorings using each $c_i$ exactly $a_i$ times.

More generally, for a finite group $G$ acting on a finite set $\mathcal C$, the orbit (equivalence class) of $C$ is $\langle C\rangle$, the stabilizer of $C$ is $\operatorname{stab}_G(C) = \{\pi \in G : \pi^*(C) = C\}$, and the fixed set of $\pi$ is $\operatorname{fix}_{\mathcal C}(\pi) = \{C : \pi^*(C) = C\}$.

Formalization targets

Milestone: Proposition 15.8

For a finite group $G$ acting on a finite set $\mathcal C$ and every $C \in \mathcal C$,

$$\sum_{C' \in \langle C\rangle} |\operatorname{stab}_G(C')| = |G|.$$

Milestone: Lemma 15.9 (Burnside's Lemma)

If $N$ is the number of equivalence classes of $\mathcal C$ induced by the action, then

$$N = \frac{1}{|G|}\sum_{\pi \in G} |\operatorname{fix}_{\mathcal C}(\pi)|.$$

Goal: Theorem 15.11 (Pólya's Enumeration Theorem)

For a permutation group $G$ of $S$ with $|S| = r$ and colours $c_1, \ldots, c_m$,

$$P_G\Bigl(\sum_{i=1}^m c_i,\ \sum_{i=1}^m c_i^2,\ \ldots,\ \sum_{i=1}^m c_i^r\Bigr) = \sum_{\langle f \rangle \in \mathcal C/\sim}\ \prod_{s \in S} f(s),$$

an identity of polynomials in $c_1, \ldots, c_m$ with rational coefficients: substituting power sums of the colours into the cycle index yields the pattern inventory.

Significance

The result itself. The theorem reduces counting inequivalent configurations to a computation with the cycle structure of the symmetry group, which is usually available in closed form (cyclic, dihedral and symmetric groups, and the pair group acting on edges of a graph). Setting all $c_i = 1$ gives the number of inequivalent colorings, $P_G(m, \ldots, m)$; reading off one coefficient answers refined questions such as the number of necklaces with a prescribed number of beads of each colour. The book applies it to musical scales, isomers of hydrocarbons and nonisomorphic graphs.

Formalizing it. Burnside's Lemma is in Mathlib (MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group), and so is the orbit–stabilizer theorem, so the two milestones are short; they are kept because they are the book's route to the goal. Mathlib has Equiv.Perm.cycleType but no cycle index and no pattern inventory, and no statement of Pólya's theorem was found on the platform (searches for Pólya, cycle index, pattern inventory, necklace and orbit counting, September 2026). The mission therefore produces the first machine-checked cycle index and Pólya enumeration theorem in this environment.

Difficulty

Burnside's Lemma counts orbits by fixed points; Pólya's theorem is a weighted Burnside lemma. Two steps separate them. First, the weight-enumerator of the colorings fixed by $\pi$ must be matched with the monomial of $\pi$ evaluated at power sums. This needs the cycles of $\pi$ as subsets of $S$, including its fixed points, whereas Mathlib's cycleType records only the lengths of the nontrivial cycles. Second, the weighted orbit count needs the weight to be invariant under the action and Burnside's argument to be carried out inside a polynomial ring rather than in $\mathbb N$. Neither step is a direct instance of a Mathlib lemma. Proving the identity only after substituting integers for the $c_i$ does not suffice: it determines the number of classes, not the coefficient of each monomial.

Formalization scope

• $S$ is a Fintype with decidable equality, $r$ = Fintype.card S; a permutation group is a Subgroup (Equiv.Perm S), and $|G|$ = Nat.card G $\ge 1$.
• $j_k(\pi)$ is cycleCount π k: the number of fixed points for $k = 1$ and the multiplicity of $k$ in Equiv.Perm.cycleType for $k \ge 2$. $P_G$ is cycleIndex G : MvPolynomial (Fin r) ℚ, the variable with index $k$ standing for $x_{k+1}$.
• Colours are Fin m, colorings are S → Fin m, and $\pi^*(f) = f \circ \pi^{-1}$; the induced relation is colorSetoid G m. Composing with $\pi$ instead of $\pi^{-1}$ gives the same classes.
• The pattern inventory is patternInventory G m : MvPolynomial (Fin m) ℚ, the sum over the quotient of the weight $\prod_{s} X_{f(s)}$ of a representative (Quotient.out); that the weight is a class invariant is part of the theorem.
• The substitution is MvPolynomial.bind₁ sending $x_{k+1}$ to $\sum_i c_i^{k+1}$.
• For the milestones, a group action is a Mathlib MulAction G 𝒞 with Fintype G and Fintype 𝒞; $N$ is the number of MulAction.orbitRel classes and the identity is stated in $\mathbb Q$.
• The book's statements contain no $O(\cdot)$, approximations or unspecified constants; no constant is instantiated.
• Ruled out: the cycle index is defined from the cycle structure of each permutation alone. Defining $P_G$, or its substituted form, through colorings, fixed sets or orbit weights would make the goal a restatement of its definitions.

Reusable beyond this mission: the cycle index of a permutation group and the pattern inventory, both needed for any later count of necklaces, graphs up to isomorphism, or de Bruijn's generalization with a group acting on the colours. Contributions of cycle indices of specific groups (cyclic, dihedral, symmetric) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 15, pp. 291–314. https://www.appliedcombinatorics.org/
• G. Pólya, "Kombinatorische Anzahlbestimmungen für Gruppen, Graphen und chemische Verbindungen", Acta Mathematica 68 (1937), 145–254. https://doi.org/10.1007/BF02546665
• J. H. Redfield, "The Theory of Group-Reduced Distributions", American Journal of Mathematics 49 (1927), 433–455. https://doi.org/10.2307/2370675
• N. G. de Bruijn, "Pólya's theory of counting", in E. F. Beckenbach (ed.), Applied Combinatorial Mathematics, Wiley, 1964, 144–184.

Motivation

Moving as much as possible of something — freight, water, data — from an origin to a destination through connections of limited capacity is one of the basic problems of operations research. Its mathematical form, the maximum flow problem, was posed in the 1950s in work on rail networks and solved independently by Ford and Fulkerson (Maximal flow through a network, Canadian J. Math. 8 (1956)) and by Elias, Feinstein and Shannon (A note on the maximum flow through a network, IRE Trans. Inform. Theory 2 (1956)). The answer, the Max Flow–Min Cut Theorem, is a min–max duality: the largest amount that can be shipped equals the smallest total capacity whose removal disconnects the destination from the origin. It is a standard example of linear-programming duality with a combinatorial proof, and it is the source of Hall's matching theorem, Menger's theorem and Dilworth's theorem via network constructions.

This mission formalizes Chapter 13 of Keller and Trotter's Applied Combinatorics (2017 Edition), together with the two theorems of Chapter 14 that apply it, in the book's own model of a network.

Setting

A network consists of a finite vertex set $V$, a set of directed edges $(x, y)$, a source $S$ and a sink $T$ with $S \ne T$, and a capacity $c(x, y) \ge 0$ (a real number) on each edge. The underlying directed graph is an oriented graph: for any two vertices $x, y$ at most one of $(x, y)$, $(y, x)$ is an edge. Every edge at $S$ points away from $S$ and every edge at $T$ points into $T$.

A flow is a function $\phi$ on the edges with $0 \le \phi(x, y) \le c(x, y)$, extended by $\phi(x, y) = 0$ on pairs that are not edges, satisfying the conservation laws

$$\sum_x \phi(S, x) = \sum_x \phi(x, T), \qquad \sum_x \phi(x, y) = \sum_x \phi(y, x)\quad (y \ne S, T).$$

The value of $\phi$ is $\operatorname{value}(\phi) = \sum_x \phi(S, x)$.

A cut is a partition $V = L \cup U$ with $S \in L$, $T \in U$. Its capacity is

$$c(L, U) = \sum_{x \in L,\ y \in U} c(x, y),$$

summed over the edges directed from $L$ to $U$ only.

Given a flow $\phi$, an edge $(x, y)$ is used if $\phi(x, y) > 0$ and has spare capacity if $\phi(x, y) < c(x, y)$. An augmenting path is a sequence $P = (x_0, \dots, x_m)$ of distinct vertices from $x_0 = S$ to $x_m = T$ such that each step either follows an edge $(x_{i-1}, x_i)$ with spare capacity (a forward edge) or traverses a used edge $(x_i, x_{i-1})$ backwards (a backward edge). Its augmentation amount is $\delta = \min\{\delta_1, \delta_2\}$, where $\delta_1$ is the least spare capacity of a forward edge and $\delta_2$ the least flow on a backward edge ($\delta = \delta_1$ when there is no backward edge).

For Chapter 14: in a finite simple graph with bipartition $V = V_1 \cup V_2$, a matching is a set of edges no two of which share an endpoint; it saturates a vertex that is an endpoint of one of its edges; and $N(A)$ is the set of neighbors of the vertices in $A$.

Formalization targets

Goal: the Max Flow–Min Cut Theorem (Theorem 13.10)

For every network there is a real number $v_0$ with

$$v_0 = \max\{\operatorname{value}(\phi) : \phi \text{ a flow}\} = \min\{c(L, U) : V = L \cup U \text{ a cut}\},$$

that is, $v_0$ is attained by some flow and bounds every flow value from above, and $v_0$ is attained by some cut and bounds every cut capacity from below.

Milestones

• Theorem 13.4. For every flow $\phi$ and every cut, $\operatorname{value}(\phi) \le c(L, U)$.
• Proposition 13.7. If $P$ is an augmenting path for a flow $\phi$ of value $v$ and $\delta$ is its augmentation amount, the function obtained by adding $\delta$ on the forward edges of $P$ and subtracting $\delta$ on its backward edges is a flow of value $v + \delta$.
• Theorem 14.1. If every capacity is an integer, some maximum flow has $\phi(x, y) \in \mathbb Z$ on every edge.
• Theorem 14.7 (Hall). In a finite bipartite graph with bipartition $V_1 \cup V_2$ there is a matching saturating every vertex of $V_1$ if and only if $|N(A)| \ge |A|$ for every $A \subseteq V_1$.

Significance

The result. Theorem 13.10 turns every maximum-flow computation into a certified one: a flow and a cut of equal value prove each other optimal, and Theorem 13.4 shows no certificate can do better. Together with the integrality theorem 14.1 it is the engine behind the combinatorial applications of Chapter 14: maximum matchings in bipartite graphs, Hall's theorem, and the computation of the width of a poset with a minimum chain partition. Beyond the book, the same duality underlies Menger's theorem, König's theorem, the analysis of image segmentation by graph cuts, and the combinatorial theory of totally unimodular linear programs.

Formalizing it. The results are classical and proved. Mathlib has no theory of network flows. The platform has a Max-Flow Min-Cut theorem in the model of Bertsimas and Tsitsiklis (a general digraph on Fin n with capacities in $(0, \infty]$, value compared in EReal), which does not cover the book's networks with zero capacities and is stated for a different encoding. This mission produces the theory in the book's model: finite oriented networks with real non-negative capacities, flows as functions on vertex pairs, cuts as vertex subsets, and the augmenting-path step that the Ford–Fulkerson labeling algorithm iterates. Hall's theorem is in Mathlib in its indexed-family form; the graph form stated here is new to the platform.

Difficulty

Theorem 13.4 is a finite-sum rearrangement. The difficulty of the goal is the existence of a maximum flow. The textbook argument runs the labeling algorithm until it halts, then reads off a cut from the labeled vertices. With real capacities this algorithm need not halt: with badly chosen augmenting paths and irrational capacities the flow values can converge to a limit strictly below the maximum, so "repeat until no augmenting path exists" does not by itself produce a maximum flow. The existence of an optimal flow is therefore not a by-product of the algorithm's description; it has to be established in its own right before the absence of augmenting paths can be turned into a cut of equal capacity. A formalization that assumes a maximum flow exists proves a strictly weaker statement. Proposition 13.7 is elementary but bookkeeping-heavy: backward edges subtract flow, and conservation must be checked at every interior vertex of the path.

Formalization scope

The vertex set is a type V with [Fintype V] [DecidableEq V]. A network (AppliedComb.Flows.Network) bundles an edge relation adj, the source S and sink T with S ≠ T, and a real capacity function cap, together with the axioms of an oriented graph, the orientation of edges at S and T, and 0 ≤ cap x y on edges. Flows are functions ϕ : V → V → ℝ satisfying IsFlow, which includes $\phi = 0$ off the edges and keeps the first conservation law as part of the definition, as on the page. The value is $\sum_x \phi(S, x)$. A cut is its part L : Finset V with S ∈ L, T ∉ L. Augmenting paths are injective maps Fin (m + 1) → V, and $\delta_1, \delta_2, \delta$ are computed in WithTop ℝ so that an empty minimum is $\top$ and $\delta = \delta_1$ when there is no backward edge. Hall's theorem uses Mathlib's SimpleGraph with a given bipartition into two Finsets and matchings as sets of Sym2 V edges.

No explicit constants arise: the chapter has no asymptotic or approximate statements.

The book's sentence of Theorem 13.10 reads "if $v_0$ is the maximum value of a flow and $c_0$ the minimum capacity of a cut, then $v_0 = c_0$". A formalization that takes $v_0$ and $c_0$ as hypothetical extrema of possibly empty or unattained sets would be trivial or vacuous; the goal here asserts the existence of a maximum flow and a minimum cut at the same number, and the existence of a maximum flow for real capacities is part of what must be proved.

Needed infrastructure: finite-sum manipulation over Finset (reindexing, splitting over L and Lᶜ), existence of maximizers of a linear function over the set of flows, and, for Theorem 14.1, control of integrality. The definitions of networks, flows, cuts and augmenting paths are reusable for Menger's theorem, König's theorem and the chain-partition network of Section 14.3. Contributions of alternative proofs (via linear-programming duality) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapters 13–14. https://www.appliedcombinatorics.org/book/
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• P. Elias, A. Feinstein and C. E. Shannon, A note on the maximum flow through a network, IRE Transactions on Information Theory 2 (1956), 117–119. https://doi.org/10.1109/TIT.1956.1056816
• P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• U. Zwick, The smallest networks on which the Ford–Fulkerson maximum flow procedure may fail to terminate, Theoretical Computer Science 148 (1995), 165–170. https://doi.org/10.1016/0304-3975(95)00022-O

Motivation

Ramsey theory studies the principle that complete disorder is impossible: every sufficiently large structure contains a large, perfectly uniform substructure. Its most familiar instance concerns graphs. In any graph on six vertices there are three vertices that are pairwise adjacent or three that are pairwise non-adjacent, and the same phenomenon persists at every scale. The quantity that measures it, the Ramsey number $R(m, n)$, is one of the most studied and least understood functions in combinatorics. Only a handful of values are known exactly ($R(3,3) = 6$, $R(4,4) = 18$), while $R(5,5)$ is only known to lie between 43 and 49 (Radziszowski, Small Ramsey Numbers).

The subject has a short, well-documented history. F. P. Ramsey proved the general theorem in 1930 as a lemma in decidability (Ramsey 1930). Erdős and Szekeres (1935) gave the upper bound $R(m, n) \le \binom{m+n-2}{m-1}$ (Erdős–Szekeres 1935). In 1947 Erdős proved an exponential lower bound for the diagonal numbers $R(n, n)$ by counting graphs (Erdős 1947); this argument is now regarded as the origin of the probabilistic method. In 1959 Erdős used the same method to show that graphs of large girth and large chromatic number exist (Erdős 1959). For decades the exponential bases $\sqrt 2$ and $4$ stood essentially unchanged; the upper base was lowered below $4$ only in 2023 (Campos–Griffiths–Morris–Sahasrabudhe).

This mission formalizes these results as presented in Chapter 11 of Keller and Trotter, Applied Combinatorics (2017 Edition).

Setting

A graph $G$ is a finite simple graph: a finite vertex set with a symmetric, irreflexive adjacency relation (no loops, no multiple edges). A complete subgraph on $m$ vertices is a set of $m$ pairwise adjacent vertices; an independent set of size $n$ is a set of $n$ pairwise non-adjacent vertices.

A non-negative integer $N$ is a Ramsey bound for $(m, n)$ if every graph with at least $N$ vertices contains a complete subgraph on $m$ vertices or an independent set of size $n$. The Ramsey number $R(m, n)$ is the least positive Ramsey bound. In Lean these are AppliedComb.Ramsey.IsRamseyBound m n N and AppliedComb.Ramsey.ramseyNumber m n.

More generally, write $[n] = \{1, \dots, n\}$ and $C(X, s)$ for the family of $s$-element subsets of $X$. For a string $h = (h_1, \dots, h_r)$, the number $R(s : h_1, \dots, h_r)$ is the least positive $N$ such that for every $n \ge N$ and every colouring $\phi : C([n], s) \to [r]$ some colour $\alpha$ has a set $H_\alpha \subseteq [n]$ of size $h_\alpha$ all of whose $s$-subsets receive colour $\alpha$ (hypergraphRamseyNumber s r h).

The girth of a graph is the smallest number of vertices on a cycle, and infinite for a forest; the chromatic number $\chi(G)$ is the least number of colours in a proper vertex colouring.

Formalization targets

Goal: Erdős's lower bound (Theorem 11.4)

For every positive integer $n$,

$$R(n, n) \;\ge\; \frac{n}{e\sqrt 2}\, 2^{n/2}.$$

Equivalently, below this threshold there is a graph on each number of vertices with neither a complete subgraph on $n$ vertices nor an independent set of size $n$. The statement is for every $n \ge 1$, with no asymptotic slack.

Milestones

• Lemma 11.1. Every graph with at least six vertices has a complete subgraph on 3 vertices or an independent set of size 3.
• Theorem 11.2 (Ramsey's Theorem for Graphs). For positive integers $m, n$ the least positive integer $R(m, n)$ exists.
• Theorem 11.6. For positive integers $r, s$ and $h_1, \dots, h_r \ge s$, the least positive integer $R(s : h_1, \dots, h_r)$ exists.
• Theorem 11.7 (Erdős). For all integers $g \ge 3$ and $t$ there is a graph with $\chi(G) > t$ and girth greater than $g$.

A further item, not a milestone because the book does not number it, records the bound that the proof of Theorem 11.2 establishes: every graph with at least $\binom{m+n-2}{m-1}$ vertices has a complete subgraph on $m$ vertices or an independent set of size $n$.

Significance

The goal is the diagonal lower bound that every later improvement is measured against. With the upper bound from the proof of Theorem 11.2 it shows that $R(n,n)$ grows exponentially, with base between $\sqrt 2$ and $4$. No explicit construction is known to give $R(n, n) > c^n$ for any constant $c > 1$. Theorem 11.7 is the standard example of a statement whose only known proofs for decades were probabilistic, and it shows that chromatic number is not a local property.

On the formal side, Mathlib has cliques, independent sets, girth and chromatic number, but no Ramsey numbers, no Erdős lower bound and no high-girth theorem. The platform already has weaker or differently shaped relatives, all checked for this mission. Erdos1947.ramsey_lower_bound gives a graph on $2^{\lfloor k/2 \rfloor}$ vertices without monochromatic $k$-sets, a weaker bound than the goal's. BookSixth.high_girth_chromatic is a single-parameter form of Theorem 11.7 in another Lean environment. ramsey_theory_upper_bound is a diagonal $4^k$ bound. The goal statement carries the constant $1/(e\sqrt2)$ exactly, which requires an explicit, non-asymptotic lower bound for $n!$ where the book writes "Stirling's approximation".

Difficulty

The obvious route to the goal is to count graphs with a large clique or independent set and compare the result with the total number of graphs. Two steps of that route do not go through as written in the text. First, the book replaces $n!$ by its Stirling approximation, which is only asymptotic; a statement for every $n \ge 1$ needs an inequality valid for all $n$, and the constant $1/(e\sqrt2)$ leaves no room for a cruder estimate such as $n! \ge (n/e)^n$ alone. Second, the counting argument yields a graph on each $t$ below the threshold, whereas $R(n,n)$ is defined as a least threshold over all graphs with at least that many vertices; the two have to be connected.

Theorem 11.7 needs random graphs with edge probability depending on $n$, a first-moment bound on short cycles and on independent sets, and a deletion step. The book states Theorem 11.6 without proof.

Formalization scope

• Graphs are Mathlib SimpleGraph V on a finite type V : Type (Theorems 11.1, 11.2, 11.4) or on Fin N (Theorem 11.7). Cliques and independent sets are SimpleGraph.IsNClique and SimpleGraph.IsNIndepSet on a Finset.
• IsRamseyBound m n N quantifies over every graph with at least $N$ vertices, as the book does; ramseyNumber m n is the sInf of the positive Ramsey bounds. Theorem 11.2 is stated as IsLeast {N | 0 < N ∧ IsRamseyBound m n N} (ramseyNumber m n), so its content is the nonemptiness of that set. The same pattern is used for Theorem 11.6.
• The goal compares real numbers: (n : ℝ) / (Real.exp 1 * Real.sqrt 2) * (2 : ℝ) ^ ((n : ℝ) / 2) ≤ (ramseyNumber n n : ℝ), with a real power. Explicit constant: the book says "use the Stirling approximation … after some algebra"; the statement keeps the book's constant $1/(e\sqrt 2)$ and holds for every $n \ge 1$ with no threshold.
• The bound of the proof of Theorem 11.2 is stated as the Ramsey property at $\binom{m+n-2}{m-1}$, not as an inequality on ramseyNumber, so it cannot hold through an empty defining set.
• Girth is Mathlib's SimpleGraph.egirth (valued in $\mathbb N \cup \{\infty\}$, $\infty$ for forests), not SimpleGraph.girth, which is $0$ on forests. Chromatic number is SimpleGraph.chromaticNumber in $\mathbb N \cup \{\infty\}$. The parameter $t$ of Theorem 11.7 is a natural number; negative $t$ is trivial.
• Theorem 11.6 is printed with typos: $h_i \ge s$ is read for all $i = 1, \dots, r$, the undefined $n_0$ is read as $R(s : h_1, \dots, h_r)$, and $C([n], s]$ as $C([n], s)$. Colourings are functions on the subtype of $s$-element subsets of Fin n, with colours in Fin r.
• Trivializing formalizations ruled out. A Ramsey number defined as an arbitrary upper bound, or as a supremum with junk value $0$, would make the goal vacuous or false. Here the goal's right-hand side is positive, so it forces the defining set to be nonempty, and every graph is simple on exactly its vertex type, with no loops or multiple edges.
• Reusable infrastructure: IsRamseyBound/ramseyNumber, the hypergraph version, an all-$n$ lower bound for $n!$, and counting over the $2^{\binom{t}{2}}$ labelled graphs on $t$ vertices. Proofs of any milestone are welcome contributions.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 11, pp. 229–238. https://www.appliedcombinatorics.org/
• F. P. Ramsey, On a problem of formal logic, Proc. London Math. Soc. 30 (1930), 264–286. https://doi.org/10.1112/plms/s2-30.1.264
• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/
• P. Erdős, Some remarks on the theory of graphs, Bull. Amer. Math. Soc. 53 (1947), 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-1
• P. Erdős, Graph theory and probability, Canad. J. Math. 11 (1959), 34–38. https://doi.org/10.4153/CJM-1959-003-9
• S. Radziszowski, Small Ramsey Numbers, Electron. J. Combin. Dynamic Survey DS1. https://doi.org/10.37236/21
• M. Campos, S. Griffiths, R. Morris and J. Sahasrabudhe, An exponential improvement for diagonal Ramsey, 2023. https://arxiv.org/abs/2303.09521

Motivation

Linear recurrences with constant coefficients are among the first tools of enumerative combinatorics and the analysis of algorithms: the Fibonacci numbers, the number of binary strings avoiding a pattern, the running time of a divide-and-conquer loop and the number of tilings of a strip all satisfy relations of the form $c_0 a_{n+k} + c_1 a_{n+k-1} + \cdots + c_k a_n = 0$. Chapter 9 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org) treats such relations as linear equations in an operator, the advancement operator, in direct analogy with linear differential equations with constant coefficients. The chapter's Principal Theorem says that the solution set of such an equation is a vector space whose dimension equals the order of the recurrence; everything else in the chapter (general solutions for distinct and repeated roots, and the reduction of nonhomogeneous equations to homogeneous ones) is organised around it.

This mission formalizes that theorem, in the book's model of functions on all of $\mathbb{Z}$, together with the numbered lemmas of Section 9.5 on which its outline rests.

Setting

Let $V$ be the real vector space of all functions $f : \mathbb{Z} \to \mathbb{R}$, with pointwise addition and scalar multiplication. The advancement operator $A : V \to V$ is

$$A f(n) = f(n+1) \qquad (n \in \mathbb{Z}),$$

a linear operator with $A^p f(n) = f(n+p)$ for $p \ge 0$. For a nonnegative integer $k$ and real constants $c_0, c_1, \dots, c_k$, the advancement operator polynomial is

$$p(A) = c_0 A^k + c_1 A^{k-1} + c_2 A^{k-2} + \cdots + c_k,$$

so that $p(A) f(n) = c_0 f(n+k) + c_1 f(n+k-1) + \cdots + c_k f(n)$. The solution space of the homogeneous equation $p(A) f = 0$ is

$$W = \{ f \in V : p(A) f = 0 \},$$

the kernel of $p(A)$, a linear subspace of $V$. In Lean, $A$ is AppliedComb.Recurrence.advance : Module.End ℝ (ℤ → ℝ), $p(A)$ is opPoly k c for a coefficient vector c : Fin (k + 1) → ℝ with c i multiplying $A^{k-i}$, and $W$ is solutionSpace k c := LinearMap.ker (opPoly k c). A factor $A - r$ is advance - r • 1.

Formalization targets

Goal: Theorem 9.18 (the Principal Theorem)

For a positive integer $k$ and real constants $c_0, \dots, c_k$ with $c_0 \neq 0$ and $c_k \neq 0$,

$$\dim_{\mathbb{R}} \{ f : \mathbb{Z} \to \mathbb{R} \;:\; (c_0 A^k + c_1 A^{k-1} + \cdots + c_k) f = 0 \} = k.$$

Milestones

1. Lemma 9.19. If $r \neq 0$ and $(A - r) f = 0$, then $f(n) = f(0)\, r^n$ for every $n \in \mathbb{Z}$.
2. Lemma 9.20. If $c_0, c_k \neq 0$, $g \in V$ is arbitrary and $p(A) f_0 = g$, then every solution of $p(A) f = g$ is $f = f_0 + f_1$ with $f_1 \in W$.
3. Theorem 9.21. If $r_1, \dots, r_k$ are distinct nonzero reals, every solution of $(A - r_1)(A - r_2)\cdots(A - r_k) f = 0$ has the form

$$f(n) = c_1 r_1^n + c_2 r_2^n + \cdots + c_k r_k^n \qquad (n \in \mathbb{Z}).$$

4. Lemma 9.22. If $k \ge 1$ and $r \neq 0$, then $(A - r)^k f = 0$ holds exactly when

$$f(n) = c_1 r^n + c_2 n r^n + c_3 n^2 r^n + \cdots + c_k n^{k-1} r^n \qquad (n \in \mathbb{Z})$$

for some real constants $c_1, \dots, c_k$.

Significance

The result itself. Theorem 9.18 is what justifies the standard recipe for solving a recurrence: once $k$ linearly independent solutions are found, every solution is a linear combination of them, and $k$ initial values pin down a unique solution. Theorems 9.21 and 9.22 name those $k$ solutions when the characteristic polynomial splits over $\mathbb{R}$, and Lemma 9.20 reduces nonhomogeneous recurrences, the ones arising from counting problems with a forcing term, to one particular solution plus the homogeneous space.

Formalizing it. The book states Theorem 9.18 without a full proof ("we won't prove the full result") and leaves Lemma 9.22 as an exercise, so a formalization supplies arguments the source omits. Mathlib's LinearRecurrence develops the $\mathbb{N}$-indexed, monic version (LinearRecurrence.solSpace_rank); the bi-infinite, two-sided setting of the book, in which the constant term $c_k$ must be nonzero, is not in Mathlib or on the platform as of this mission.

Difficulty

The subspace part of Theorem 9.18 is immediate; the content is the dimension count, in both directions. On $\mathbb{Z}$ a solution must extend to negative indices as well as positive ones, so an argument that works for sequences indexed by $\mathbb{N}$ does not transfer: there the constant term plays no role and the dimension is $k$ whatever the constant term, while on $\mathbb{Z}$ a vanishing $c_k$ changes the answer. The outline in the book proceeds through factorisations of $p(A)$, which over $\mathbb{R}$ need not exist (complex roots), so the goal cannot be obtained by combining Theorems 9.21 and 9.22 alone. Lemma 9.22 requires showing that the functions $n^j r^n$ solve $(A - r)^k f = 0$ and that they exhaust its solutions, for $n$ ranging over all integers.

Formalization scope

• Functions are $\mathbb{Z} \to \mathbb{R}$ (the real space $V$ of Section 9.5, p. 199), not $\mathbb{N} \to \mathbb{R}$ and not $\mathbb{Z} \to \mathbb{C}$. Powers $r^n$ with $n$ negative are integer powers (zpow), always of a nonzero base.
• Dimension in the goal is Module.rank ℝ (solutionSpace k c) = k, a cardinal equality, so it also asserts finite-dimensionality.
• The coefficient vector is c : Fin (k + 1) → ℝ; c 0 is the leading coefficient $c_0$ and c (Fin.last k) the constant term $c_k$.
• Theorem 9.21 asserts one inclusion, as on the page ("every solution has the form"); Lemma 9.22 asserts both ("the general solution"), as an iff.
• Lemma 9.22 carries the hypothesis $r \neq 0$, the standing assumption of Section 9.5.2 (p. 200), which the lemma's own sentence does not repeat.
• No O(·), "≈" or unspecified threshold occurs in these statements, so no explicit constant is instantiated.
• Ruling out the trivial reading: $W$ is defined as the kernel of the operator polynomial $p(A)$, never as the span of $k$ chosen functions, so the goal is not a statement about the rank of a spanning family.

Needed infrastructure: linear operators on the function space ℤ → ℝ, powers and products in Module.End, Module.rank/Module.finrank, and finite sums; Mathlib's LinearRecurrence may be adapted for the forward half. The definitions advance, opPoly and solutionSpace are reusable for any later mission on recurrences or on generating functions for bi-infinite sequences. Contributions of the milestone lemmas, of a proof of the goal that avoids factorisation over $\mathbb{C}$, and of a complex-valued variant are welcome.

Selected references

• Mitchel T. Keller and William T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 9 (Recurrence Equations), CC BY-SA 4.0. appliedcombinatorics.org
• Mathlib, Mathlib/Algebra/LinearRecurrence.lean (ℕ-indexed linear recurrences, LinearRecurrence.solSpace_rank). Mathlib docs
• Ronald L. Graham, Donald E. Knuth and Oren Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994, Section 7.3 (solving recurrences). ISBN 978-0-201-55802-9.

Motivation

Generating functions are the standard device of enumerative combinatorics for turning a counting sequence into a single algebraic or analytic object: a sequence $\{a_n : n \ge 0\}$ is recorded as the power series $\sum_{n\ge0} a_n x^n$, and operations on series (products, powers, derivatives) become operations on the counts. Chapter 8 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org), an open textbook used in undergraduate combinatorics courses, develops the method up to one of its classical applications: extending the binomial theorem to real exponents, as Newton did, and reading off an identity about central binomial coefficients that is awkward to prove by direct counting.

The identity in question,

$$2^{2n} = \sum_{k=0}^{n} \binom{2k}{k}\binom{2n-2k}{n-k},$$

appears in standard collections of binomial identities such as Graham, Knuth and Patashnik's Concrete Mathematics (1994).

Setting

For a real number $p$ and a nonnegative integer $k$, the book defines a number $P(p, k)$ by the recursion

$$P(p, 0) = 1, \qquad P(p, k) = p\,P(p-1, k-1) \quad (k > 0),$$

so that $P(p, k) = p(p-1)\cdots(p-k+1)$ with no requirement $p \ge k$. The generalized binomial coefficient is

$$\binom{p}{k} = \frac{P(p,k)}{k!}.$$

For integers $p \ge k \ge 0$ this is the usual binomial coefficient; for integers $0 \le p < k$ it is $0$; for other real $p$ it is in general nonzero for every $k$. In the Lean development $P(p,k)$ is AppliedComb.GenFun.fallingP p k and $\binom pk$ is AppliedComb.GenFun.binomReal p k.

The generating function of a real sequence $a = (a_n)_{n\ge0}$ is the formal power series $A(x) = \sum_{n\ge0} a_n x^n$, in Lean PowerSeries.mk a : PowerSeries ℝ. When a closed-form function such as $(1+x)^p$ or $(1-4x)^{-1/2}$ is called the generating function of a sequence, the statements below read this as convergence of $\sum_n a_n x^n$ to the function's value on an explicit real interval around $0$.

The central binomial coefficients are $\binom{2n}{n}$: $1, 2, 6, 20, 70, \dots$

Formalization targets

Goal: Corollary 8.14

For every integer $n \ge 0$,

$$2^{2n} = \sum_{k=0}^{n} \binom{2k}{k}\binom{2n-2k}{n-k},$$

stated as an identity of natural numbers.

Milestones

• Lemma 8.11. For every real $p$ and integer $k \ge 0$, $P(p, k+1) = P(p, k)\,(p - k)$.
• Lemma 8.12. For every integer $k \ge 0$, $\binom{-1/2}{k} = (-1)^k \binom{2k}{k} / 2^{2k}$.
• Theorem 8.10 (Newton's Binomial Theorem). For real $p \ne 0$ and real $|x| < 1$,

$$(1+x)^p = \sum_{n=0}^{\infty} \binom{p}{n} x^n .$$

• Theorem 8.13. For real $|x| < 1/4$,

$$(1-4x)^{-1/2} = \sum_{n=0}^{\infty} \binom{2n}{n} x^n .$$

• Proposition 8.3. For real sequences $a$, $b$, the product of their generating functions is the generating function of $\bigl(\sum_{k=0}^n a_k b_{n-k}\bigr)_{n\ge0}$.
• Theorem 8.16 (already on the platform). For each $n \ge 1$, the number of partitions of $n$ into distinct parts equals the number of partitions of $n$ into odd parts.

The first five follow the chapter's own chain toward the goal; Theorem 8.16 is the chapter's other main result and is included as a reference.

Significance

Corollary 8.14 says that the sequence of central binomial coefficients convolved with itself is the sequence $4^n$; equivalently, the generating function of $\binom{2n}{n}$ is a square root of $1/(1-4x)$. Central binomial coefficients count lattice paths with $n$ up-steps and $n$ down-steps, and the identity says that the pairs consisting of a balanced path of length $2k$ and one of length $2n-2k$, summed over $k$, are equinumerous with all $4^n$ strings over a four-letter alphabet. The same generating function reappears in the book's Section 9.7, and Newton's theorem with exponent $-1/2$ or $1/2$ is the standard route to closed forms for Catalan-type sequences.

On the formalization side, Mathlib has the central binomial coefficient (Nat.centralBinom), formal power series, and Newton's series in the complex-analytic form Complex.one_add_cpow_hasFPowerSeriesOnBall_zero, which is also published on the platform as FamousTheorems.newton_binomial_series_6b and included in this mission as a reference. It does not contain the convolution identity of Corollary 8.14, and it does not contain the book's recursive $P(p,k)$ or the closed form of $\binom{-1/2}{k}$. The mission produces a machine-checked version of the chapter's chain from the book's own definitions to the identity.

Difficulty

The identity is not a special case of the Vandermonde convolution $\sum_k \binom{a}{k}\binom{b}{n-k} = \binom{a+b}{n}$: both factors depend on the summation index in their upper argument as well as their lower one. Induction on $n$ does not close directly, since the sum for $n+1$ is not a simple combination of the sum for $n$. A counting proof is possible but not obvious, which is why the chapter's route goes through a generating function with a non-integer exponent. That route passes from formal power series to real analysis: $(1-4x)^{-1/2}$ is a real function, and the passage from an identity of functions on an interval to an identity of coefficients requires the uniqueness of power series coefficients on an open interval and the product of two convergent series. The book asserts Newton's theorem without proof.

Formalization scope

• Numbers. $P(p,k)$ and $\binom pk$ are real-valued, defined by the book's recursion (Definition 8.8) and quotient (Definition 8.9) in the definition item AppliedComb.GenFun.binomReal. Mathlib's descPochhammer and Ring.choose compute the same values; they are not used in the statements so that Lemma 8.11 is a statement about the book's recursion rather than a definitional unfolding.
• Pinned readings. The book treats generating functions as formal power series and states Theorems 8.10 and 8.13 without a domain for $x$. Here both are stated analytically: Theorem 8.10 for real $p \ne 0$ and real $x$ with $|x| < 1$, Theorem 8.13 for real $x$ with $|x| < 1/4$, with the real power Real.rpow of a positive base on the left and HasSum (unconditional convergence of the series) on the right. The book's hypothesis $p \ne 0$ is kept. No other explicit constants replace informal ones: the chapter's statements contain no $O(\cdot)$, "$\approx$" or "sufficiently large".
• Proposition 8.3 is stated for formal power series PowerSeries ℝ with the sum written as $\sum_{k=0}^{n} a_k b_{n-k}$ over Finset.range (n + 1).
• Goal. Corollary 8.14 is an identity in ℕ with Nat.choose; the subtractions $2n-2k$ and $n-k$ occur only for $k \le n$ and are exact. A statement asserting only that the square of the formal power series $\sum_n \binom{2n}{n}X^n$ equals $\sum_n 4^n X^n$, or a purely formal version of Theorem 8.13, would hide the identity in a coefficient comparison and is not the book's statement; the goal is the explicit sum identity.
• Theorem 8.16 is referenced as FamousTheorems.card_odds_eq_card_distincts, stated for all $n$ with Mathlib's Nat.Partition, whose partitions are multisets of positive integers, as in the book (p. 168); the case $n = 0$ it adds is immediate.

A complete development needs real power series on an interval (Cauchy products, identity theorem for coefficients), the real power function, and elementary manipulation of binomial coefficients; the identification of binomReal with Ring.choose is reusable for any later statement using the generalized binomial coefficient. Proofs of any milestone are welcome independently, and so is a direct proof of Corollary 8.14 that bypasses the analytic chain.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, CC BY-SA 4.0. Chapter 8. https://www.appliedcombinatorics.org/
• R. L. Graham, D. E. Knuth and O. Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994. ISBN 978-0-201-55802-9.
• Mathlib, Complex.one_add_cpow_hasFPowerSeriesOnBall_zero (Newton's binomial series). https://github.com/leanprover-community/mathlib4