Proofs from THE BOOK: verified results and open formalization tasks

This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's Proofs from THE BOOK. It combines results imported from the existing proof_in_the_book repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.

What is already verified

The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.

The imported source snapshot is 873d52e0c88cd351f594221e70c3c5b3559777a9. Imported results use Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.

The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.

Sixth-edition contribution targets

New milestones explicitly marked 6th ed. cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.

Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.

The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.

Chapter numbering and statement scope

Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.

Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.

How to contribute

Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.

Source repository: https://github.com/xiangyazi24/proof_in_the_book

Book: Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$. They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$, and every job has unit execution requirement $p_j=1$, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) are the case $q_i=1$; uniform machines ($Q$) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$. Resource $R_h$ has a positive integer size $s_h$, the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$. Its completion time is $C_j=S_j+1/q_{\mu(j)}$, and it is being executed at every time $t$ with $S_j\le t<C_j$. A schedule is feasible when:

• jobs on the same machine do not overlap in time;
• at every time $t$, the set $S_t$ of jobs being executed satisfies

$$\sum_{j\in S_t} r_{hj}\le s_h\qquad(h=1,\dots,l).$$

The makespan is $C_{\max}=\max_j C_j$.

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$, and every requirement satisfies $r_{hj}\le1$. A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$, whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$:

• PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
• PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$, required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

$$Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}\ \text{is NP-hard in the strong sense.}$$

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

1. The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
2. The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$.
3. Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
4. The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$, $q_2=1$ has a feasible schedule with $C_{\max}\le t$.

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$, so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

• Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$, and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
• Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
• Decision versions. "NP-hard" refers to the decision version with a threshold $y$. Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
• Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$, so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
• Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
• Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$-factor.
• Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$. A diagonal resource would make every job infeasible.
• Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

• J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.

Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune $14$-regular bipartite graph of at least that girth, and it has a perfect matching.

This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.

Setting

For a finite simple graph $G$ and a vertex set $A\subseteq V(G)$, the associated cut consists of all edges with one endpoint in $A$ and one in $V(G)\setminus A$. The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.

The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is $14$-regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.

The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, $K_1$ has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.

Formalization targets

Lemma 5 — immune high-girth graphs

The main theorem follows the paper's structural lemma:

$$\forall g\ge3\ \exists G, \quad G\text{ is finite, connected, bipartite, and $14$-regular},$$ $$\operatorname{girth}(G)\ge g, \qquad G\text{ has no matching cut}, \qquad G\text{ has a perfect matching}.$$

The graph may depend on $g$. The existence quantifier does not request an efficient algorithm or a numerical order bound.

Negative OPG consequence

A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:

$$\forall g\ge3\ \exists G, \qquad \overline d(G)=14<15, \quad \operatorname{girth}(G)\ge g, \quad G\text{ has no matching cut}.$$

Thus choosing $d=15$ refutes the intended universal assertion that some girth threshold works for every graph of average degree below $d$.

Significance

The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.

Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every $g\ge3$, Matching Cut is NP-complete even for bipartite graphs of girth at least $g$ and maximum degree at most $60$. Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.

Difficulty

Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.

A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.

Formalization scope

Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least $g$ means every such cycle has length at least $g$, so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.

The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the $K_1$ ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.

Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.

Selected references

• C. Feghali, F. Lucke, D. Paulusma, and B. Ries, Matching Cuts in Graphs of High Girth and H-Free Graphs, Algorithmica 87 (2025), 1199–1221. https://doi.org/10.1007/s00453-025-01318-8
• C. Feghali, F. Lucke, D. Paulusma, and B. Ries, ISAAC 2023 version. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.31
• A. Lubotzky, R. Phillips, and P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988), 261–277. https://doi.org/10.1007/BF02126799
• Open Problem Garden, Matching cut and girth. https://www.openproblemgarden.org/op/matching_cut_and_girth

[VM-STATUS-20260908-R05-PROVED]

Status update (2026-09-08): The root theorem OPG500Counterexample.eight_vertex_counterexample is now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.

---

Motivation and historical context

Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.

Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.

The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.

Setting

Let $G$ be a finite simple graph. A positive edge-length assignment is a function

$$\ell:E(G)\longrightarrow \mathbb R$$

such that $\ell(e)>0$ for every edge $e$. The length of a finite path or cycle is the sum of the lengths of its edges.

A simple cycle $C$ is $\ell$-geodesic when, for every pair of vertices $x,y$ on $C$, at least one of the two $x$–$y$ arcs of $C$ has length equal to the shortest-path distance between $x$ and $y$ in $G$. Equivalently, there is no $x$–$y$ path in $G$ whose length is strictly smaller than both $x$–$y$ arcs of $C$. The definition concerns vertices of the cycle and permits ties between shortest paths.

A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.

Fix the graph $H$ on vertices $0,1,\ldots,7$. The vertices $0,1,2,3$ induce $K_4$. For each $i\in\{0,1,2,3\}$, set $y_i=7-i$ and join $y_i$ to exactly the three core vertices other than $i$. The four vertices $y_i$ are pairwise nonadjacent. Thus the frozen edge set is

$$\{01,02,03,04,05,06,12,13,14,15,17,23,24,26,27,35,36,37\}.$$

The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.

Formalization targets

Main target: the universal eight-vertex obstruction

Formalize the following statement for the fixed graph $H$:

$$H\text{ is 3-connected}\quad\text{and}\quad \forall\ell:E(H)\to\mathbb R_{>0},\; \exists C,\; C\text{ is an $\ell$-geodesic simple cycle of $H$ and is not peripheral}.$$

The existential cycle may depend on $\ell$. The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.

Supporting targets

The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of $H$, the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.

Significance

A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.

A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.

Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.

Difficulty

The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.

The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.

Formalization scope

The Lean development will use Fin 8 for the vertices of $H$ and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.

The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.

Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.

Selected references

• A. Georgakopoulos and P. Sprüssel, Geodetic topological cycles in locally finite graphs, Electronic Journal of Combinatorics 16 (2009), R144. Section 3.1, Theorem 3.1; Section 5, Problem 3. https://arxiv.org/abs/0911.3999v1
• Open Problem Garden, Geodesic cycles and Tutte's Theorem, problem statement and vertex-based definition. https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem
• W. T. Tutte, How to draw a graph, Proceedings of the London Mathematical Society 13 (1963), 743–768. Cited as reference [18] by Georgakopoulos and Sprüssel for peripheral-cycle generation.
• Vibe Mathing, frozen OPG-500 candidate repository at commit a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924

Motivation

Graphs are the most basic combinatorial model of pairwise relations: road networks, frequency interference between radio stations, schedules, circuit layouts. Chapter 5 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) introduces the vocabulary of graph theory and proves its first structural theorems: when a graph can be traversed edge by edge (Euler, 1736), when it can be toured vertex by vertex (Dirac, 1952), when it can be colored with two colors, and how far the chromatic number can drift from the size of the largest clique.

Hamiltonicity is the vertex analogue of Euler's edge-traversal problem and behaves very differently: Euler's problem has a simple parity characterization, while deciding whether a graph has a hamiltonian cycle is NP-complete (Karp, 1972). Sufficient conditions are therefore the main tool, and the minimum-degree condition of Dirac (1952) is the first and most cited of them; Ore's condition (1960) and the Bondy–Chvátal closure (1976) refine it.

Setting

A graph $G = (V, E)$ consists of a finite vertex set $V$ and a set $E$ of 2-element subsets of $V$, the edges; $xy \in E$ means $x$ and $y$ are adjacent. The degree $\deg_G(v)$ is the number of neighbours of $v$. The mission uses Mathlib's SimpleGraph V with [Fintype V]; "a graph on $n$ vertices" means Fintype.card V = n.

• A cycle is a sequence $(x_1, \dots, x_n)$ of $n \ge 3$ distinct vertices with $x_i x_{i+1} \in E$ for $i < n$ and $x_1 x_n \in E$; its length is $n$. A graph is acyclic if it has no cycle, and a tree if it is connected and acyclic. A leaf of a tree is a vertex of degree $1$.
• A hamiltonian cycle is a sequence $(x_1, \dots, x_n)$ in which every vertex appears exactly once, $x_i x_{i+1} \in E$ for $i < n$, and $x_1 x_n \in E$. A graph is hamiltonian if it has one (AppliedComb.Graphs.IsHamiltonian).
• An eulerian circuit is a sequence $(x_0, \dots, x_t)$, repetition allowed, with $x_0 = x_t$, consecutive entries adjacent, and every edge equal to $x_i x_{i+1}$ for exactly one $i < t$. A graph without isolated vertices is eulerian if it has one (IsEulerian).
• A proper coloring assigns colors to vertices so that adjacent vertices differ; the chromatic number $\chi(G)$ is the least number of colors in a proper coloring, and the clique number $\omega(G)$ is the largest size of a set of pairwise adjacent vertices.
• An interval graph is the intersection graph of closed intervals $[a_v, b_v] \subset \mathbb R$, $v \in V$: distinct $u, v$ are adjacent iff their intervals meet (IsIntervalGraph).

Formalization targets

Goal: Dirac's theorem (Theorem 5.18)

$$\text{If } |V| = n \ge 1 \text{ and } \deg_G(v) \ge \left\lceil \tfrac n2 \right\rceil \text{ for all } v \in V, \text{ then } G \text{ is hamiltonian.}$$

Milestones

In the book's order:

1. Proposition 5.11. A tree on $n \ge 2$ vertices has at least two leaves.
2. Theorem 5.13 (Euler). A graph without isolated vertices is eulerian if and only if it is connected and every degree is even.
3. Theorem 5.21. $\chi(G) \le 2$ if and only if $G$ contains no odd cycle.
4. Proposition 5.24 (generalized pigeonhole). If $f : X \to Y$ and $|X| \ge (m-1)|Y| + 1$, some fibre of $f$ contains $m$ distinct elements.
5. Proposition 5.25. For every $t \ge 3$ there is a finite graph $G_t$ with $\chi(G_t) = t$ and $\omega(G_t) = 2$.
6. Theorem 5.28. Every finite interval graph satisfies $\chi(G) = \omega(G)$.

The book's proof of Theorem 5.18 uses only the pigeonhole principle, so none of these results lies on its path. The milestones are the chapter's other theorems about the same objects (cycles, degrees, colorings), and they share the goal's definitions. Cayley's formula (Theorem 5.39, $n^{n-2}$ labelled trees on $n$ vertices) is already on the platform as GYGraphTheory.cayley_tree_formula and is included as a reference item.

Significance

Dirac's theorem is sharp: the complete bipartite graph $K_{k,k+1}$ has minimum degree $k = \lceil n/2 \rceil - 1$ and no hamiltonian cycle. It is the starting point for the theory of degree conditions for hamiltonicity (Ore, Pósa, Chvátal) and for its extremal and random-graph analogues. Euler's theorem gives linear-time recognition of eulerian graphs; Theorem 5.21 characterizes bipartite graphs; Proposition 5.25 shows that local sparsity (no triangles) does not bound the chromatic number; Theorem 5.28 is the first step towards perfect graphs.

All of these results have been proved for a long time. What is missing is their formalization. Mathlib provides SimpleGraph, chromaticNumber, cliqueNum, degree-sum identities, and definitions of eulerian and hamiltonian walks. It contains no Dirac theorem, no converse of the eulerian degree condition, and no interval-graph theory. On the platform, FamousTheorems.two_colorable_iff_no_odd_cycle_6b is stated with odd closed walks rather than odd cycles, and triangle_free_chromatic_number asserts only $\chi \ge k$ rather than $\chi = t$ with $\omega = 2$ exactly.

Difficulty

For Dirac's theorem the obvious approach, induction on $n$ (deleting a vertex), fails: deleting a vertex lowers degrees, and the hypothesis $\deg \ge \lceil n/2 \rceil$ is not inherited by the smaller graph. The degree condition is global, and so is the argument that uses it. In Lean the argument also has to reverse and splice vertex sequences while keeping distinctness and every adjacency along the way. The sufficiency half of Euler's theorem has to construct a circuit that uses every edge exactly once, not just show that one exists up to parity. In Theorem 5.21 the obstruction is a cycle with distinct vertices; producing one from a failed 2-coloring takes more work than producing an odd closed walk. Proposition 5.25 needs a concrete infinite family of graphs and exact computation of both invariants. The upper bound $\chi \le t$ is easy, but the lower bound $\chi \ge t$ is not.

Formalization scope

• Graphs are SimpleGraph V on a Fintype V. The number of vertices is always Fintype.card V, never a free parameter; in Theorem 5.18 the ceiling $\lceil n/2 \rceil$ is (n + 1) / 2 in $\mathbb N$, with Fintype.card V = n.
• "Hamiltonian" is the book's definition (p. 79), a list of all vertices without repetition with consecutive and first/last entries adjacent. It is not Mathlib's Walk.IsHamiltonianCycle, which needs at least three vertices: under that notion Theorem 5.18 would be false for $K_2$. The goal assumes $V$ nonempty, as the book's proof does ($n$ positive). Degenerate readings are ruled out: a predicate satisfied by a cycle through only some vertices, or a statement in which $n$ is not the number of vertices, would make the goal vacuous or false, and neither is used here.
• "Eulerian" follows p. 75. Since the book defines it only for graphs without isolated vertices, Theorem 5.13 carries that hypothesis explicitly.
• Cycles are the book's cycles (distinct vertices, length $\ge 3$), not closed walks. Theorem 5.21 is stated with odd cycles.
• $\chi$ is Mathlib's chromaticNumber ($\mathbb N_\infty$-valued) and $\omega$ is cliqueNum; on finite graphs both agree with the book's definitions (pp. 81, 84).
• Planarity (Section 5.5: Euler's formula 5.32, the bound $3n - 6$ in 5.33, Kuratowski 5.34, the Four Color Theorem 5.37) is excluded. The book defines planar drawings through polygonal arcs in $\mathbb R^2$ and faces, which is a topological development rather than a chapter mission. Kuratowski's theorem and the Four Color Theorem are not proved in the book.
• Contributions reusable beyond this mission are welcome: path/cycle manipulation lemmas for list-based sequences, the Euler circuit construction, bipartiteness via distance parity, and the Mycielski construction.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 5. https://www.appliedcombinatorics.org/
• G. A. Dirac, Some theorems on abstract graphs, Proc. London Math. Soc. (3) 2 (1952), 69–81. https://doi.org/10.1112/plms/s3-2.1.69
• L. Euler, Solutio problematis ad geometriam situs pertinentis, Commentarii Academiae Scientiarum Petropolitanae 8 (1741), 128–140 (read 1736). https://scholarlycommons.pacific.edu/euler-works/53/
• J. Mycielski, Sur le coloriage des graphs, Colloquium Mathematicum 3 (1955), 161–162. https://doi.org/10.4064/cm-3-2-161-162
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations (1972), 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

The Hitchcock transportation problem asks how to ship a commodity from $m$ supply points to $n$ demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.

The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply $\sum_i a_i$, which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to $\max(m,n)$ times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.

Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).

Setting

The network of Figure 1 (p. 259) has a source $s$, a sink $t$, supply nodes $s_1,\dots,s_m$ and demand nodes $t_1,\dots,t_n$, with $m,n\ge 1$. Its arcs are $(s,s_i)$ with capacity $a_i$ and cost $0$; $(s_i,t_j)$ with capacity $+\infty$ and cost $d_{ij}\ge 0$; $(t_j,t)$ with capacity $b_j$ and cost $0$; and the return arc $(t,s)$ with capacity $+\infty$ and cost $0$. The supplies $a_i$ and demands $b_j$ are positive integers with $\sum_i a_i=\sum_j b_j=:B$.

A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write $f_{0i}=f(s,s_i)$, $f_{ij}=f(s_i,t_j)$, $f_{j0}=f(t_j,t)$; the value of $f$ is $f(t,s)$, and a maximum flow is one of largest value. Its cost is $\sum_{i,j} d_{ij} f_{ij}$; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real $u_i, v_j$ with $u_i-v_j+d_{ij}\ge 0$ for all $i,j$ and $f_{ij}=0$ whenever $u_i-v_j+d_{ij}>0$.

An augmenting path relative to $f$ is a sequence of distinct nodes from $s$ to $t$ in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount $\varepsilon$ along it and raises $f(t,s)$ by $\varepsilon$.

For $p\ge 0$, Problem $p$ has the same network and costs, with capacities $\lfloor a_i/2^p\rfloor$ and $\lfloor b_j/2^p\rfloor$. Choose $l$ with every $a_i,b_j<2^l$. The scaling method solves Problems $l-1,l-2,\dots,0$ in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem $l-1$ starts from the zero flow, and Problem $p-1$ starts from twice the final flow of Problem $p$.

Formalization targets

Goal: Theorem 9

For every run of the scaling method, the total number $\sum_{p<l} K_p$ of flow augmentations satisfies

$$\sum_{p=0}^{l-1} K_p \;\le\; \max(m,n)\left(2+\left\lfloor \log_2\frac{\sum_{i=1}^m a_i}{\max(m,n)}\right\rfloor\right).$$

The bound holds for every $l$ admissible for the data and every choice of costs, and is stated with the paper's constant exactly.

Milestones

1. §1.1: augmentation preserves feasibility and raises the value by $\varepsilon>0$; a flow is maximum iff no augmenting path exists.
2. Theorem 8: a maximum flow is extreme iff there are potentials $u_0,\dots,u_m$, $v_0,\dots,v_n$ with (5a)–(5f).
3. §2.2: a pseudo-extreme maximum flow is extreme.
4. Lemma 3: if $f$ is pseudo-extreme in Problem $p$, then $2f$ is pseudo-extreme in Problem $p-1$.
5. The maximum-flow value of Problem $p$ is $f_p^*=\min\big(\sum_i\lfloor a_i/2^p\rfloor,\sum_j\lfloor b_j/2^p\rfloor\big)$.
6. Eq. (6): $\sum_p K_p\le f_0^*-\sum_{p=1}^{l-1} f_p^*$.
7. $f_p^*\ge\max\big(0,\,B/2^p-\max(m,n)\big)$.

Significance

The result. Theorem 9 shows that scaling reduces the number of augmentations from order $B$ to order $\max(m,n)\log_2(B/\max(m,n))$, which is roughly the length of the binary encoding of the data. Combined with the $O(mn)$ cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.

Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.

Difficulty

The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only $B$. The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem $p$ must give a feasible, still pseudo-extreme, starting flow for Problem $p-1$ (Lemma 3). Second, the gap between that start and the optimum of Problem $p-1$ must be small, which requires the exact maximum-flow value $f_p^*$ of each scaled problem. Third, the telescoping sum of the gaps must be estimated against $\log_2(B/\max(m,n))$ with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.

Formalization scope

Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem $p$ uses natural-number division for $\lfloor a_i/2^p\rfloor$. Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.

A run of the scaling method (IsScalingRun) is a family of phases $F\,p\,0,\dots,F\,p\,(K\,p)$ for $p<l$. It starts from $0$ in Problem $l-1$, restarts from $2F\,p\,(K\,p)$ in Problem $p-1$, and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs $\bar\Delta$) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.

The goal compares the count, cast to $\mathbb{Z}$, with $\max(m,n)\,(2+\lfloor\log_2(B/\max(m,n))\rfloor)$, using Real.logb 2 and Int.floor. The constant is the printed one; neither $O(\cdot)$ nor a weaker constant is acceptable. Positivity of all $a_i,b_j$ is a hypothesis, because without it the printed bound is false (for $m=5$, $n=1$, $a=(1,0,0,0,0)$, $b=(1)$ one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with $m=n=1$, $a=b=(1)$, $l=1$ and one augmentation).

A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of $f_p^*$, the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact $\bar\Delta$ path rule showing that it satisfies the invariant.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5:247–255, 1985. https://doi.org/10.1007/BF02579369
• J. B. Orlin, A faster strongly polynomial minimum cost flow algorithm, Proc. STOC 1988, 377–387. https://doi.org/10.1145/62212.62249

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$-approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$, nonnegative, $d(a,b)\ge 0$, and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$. A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$; having reached $\tau(k)$, it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$. The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$. Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$, $L_{i+1}=2L_i+2l_i$. The graph $G_i$ adds two closing edges to $F_i$, and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$.

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

$$\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .$$

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

1. (2.12): the difference equation $L_{i+1}=2L_i+2l_i$, $L_1=2$, has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$, so its ratio is $(L_i+l_i-1)/n$.
8. The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$.

The instance for $m$ is $\bar G_{m-1}$.

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ($\frac13$ against $\frac12$) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$.

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$. Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$. Checking small cases by computer does not give either property for all $i$.

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$, a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$, the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$, as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$, the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$, $G_i$, $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$, middle node $2^i-1$, right node $2^{i+1}-2$); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$.

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
• J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

Motivation

Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.

Setting

A finite directed graph with arc set $\mathcal{A}$, real arc lengths $a_{ij}$, origin $s$ and destination $t \ne s$ (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).

The algorithm state (BertsekasLCState) carries labels $d_j \in \overline{\mathbb{R}}$, the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$, all other labels $\infty$, UPPER $= \infty$, OPEN $= \{s\}$. One iteration (BertsekasLCStep, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$, and put $j$ in OPEN if $j \ne t$, or update UPPER if $j = t$. The algorithm terminates when OPEN is empty.

Target

$$\text{OPEN} = \varnothing \implies \text{UPPER} = \operatorname{dist}(s, t) \in \overline{\mathbb{R}},$$

for every execution, under the nonnegative arc length assumption of §2.3 ($a_{ij} \ge 0$ for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from $s$, which needs neither (label_correcting_invariant).

The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$, and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample $s=0$, $t=2$, $a_{02}=1$, $a_{01}=2$, $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$. Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.

Significance

Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.

Difficulty

Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.

Formalization scope

Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. Bellman, On a routing problem, Quart. Appl. Math. 16 (1958), 87–90. https://doi.org/10.1090/qam/102435

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

An expander is a sparse graph in which every set of vertices has many neighbours outside itself. Expanders are the building blocks of superconcentrators (sparse directed graphs that route any $r$ inputs to any $r$ outputs along vertex-disjoint paths), of sorting and switching networks, and of many constructions in complexity theory and coding; the survey of Hoory, Linial and Wigderson (Bull. AMS 2006) describes these uses. Random regular graphs are expanders with high probability, but applications need explicit families with fixed degree and a uniform expansion constant.

Alon and Milman (J. Combin. Theory Ser. B 38 (1985)) replace combinatorial expansion by a spectral quantity, the second-smallest eigenvalue $\lambda_1$ of the matrix $Q = D - A$ of a graph, which Fiedler called the algebraic connectivity (Czech. Math. J. 1973). Their Theorem 4.3 shows that a regular graph with $\lambda_1$ bounded away from $0$ yields an expander. This mission formalizes their Section 4 source of such graphs: Cayley graphs of the finite quotients of a group with Kazhdan's property (T).

Timeline:

• 1967: Kazhdan introduces property (T) and proves that $SL(n,\mathbb{Z})$, $n \ge 3$, has it (Funct. Anal. Appl. 1 (1967)).
• 1973: Margulis uses property (T) to give the first explicit expander family (Probl. Inf. Transm. 9 (1973)).
• 1981: Gabber and Galil give a variant of Margulis' construction with an explicit expansion constant, proved by Fourier analysis (J. Comput. Syst. Sci. 22 (1981)).
• 1985: Alon and Milman state the construction in terms of $\lambda_1$ (Lemma 4.8, Theorem 4.9) and link it to the concentration property of Section 2 of their paper.

Setting

Let $T$ be a finite group. A finite multigraph on $T$ is a symmetric matrix $M = (M_{w,u})$ of nonnegative integers, $M_{w,u}$ being the number of edges joining $w$ and $u$ (diagonal entries count loops). It is $k$-regular if every row sums to $k$. Its matrix is $Q = \operatorname{diag}(d(v)) - M$ with $d(v) = \sum_u M_{v,u}$, a real symmetric positive semidefinite matrix. Its eigenvalues, repeated according to multiplicity, are $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{|T|-1}$, and $\lambda_1(G)$ denotes the second of them.

Let $H$ be a group, $S \subseteq H$ a finite set with $S = S^{-1}$, and $\phi : H \to T$ a homomorphism onto $T$. The Cayley multigraph $G(T, \phi(S))$ joins $w$ and $u$ by as many edges as there are $s \in S$ with $w u^{-1} = \phi(s)$. It is $|S|$-regular, and its matrix is $Q = |S| \cdot I - \sum_{s\in S} \pi(\phi(s))$, where $\pi(t)$ is the permutation matrix of the left regular representation, $(\pi(t))_{w,u} = 1$ iff $w u^{-1} = t$.

An $(n,k,\varepsilon)$-enlarger (Definition 4.1) is a $k$-regular graph on $n$ vertices with $\lambda_1 \ge \varepsilon$.

A unitary representation $\pi$ of $H$ in a complex Hilbert space $V$ is essentially nontrivial (Definition 4.5) if no nonzero vector is fixed by every $\pi(h)$. A discrete group $H$ has property (T) (Definition 4.6) if there are $\varepsilon > 0$ and a finite $K \subseteq H$ such that for every essentially nontrivial unitary representation $\pi$ and every unit vector $y$ some $h \in K$ satisfies $|(\pi(h)y, y)| < 1 - \varepsilon$.

Formalization targets

Goal: Theorem 4.9

Let $H$ have property (T), let $S$ be a finite generating set of $H$ with $S = S^{-1}$, and let $\phi_i : H \to T_i$ be surjective homomorphisms onto finite groups with $|T_i| \to \infty$. Then there is one $\varepsilon > 0$ with

$$G(T_i, \phi_i(S)) \text{ is a } (|T_i|,\ |S|,\ \varepsilon)\text{-enlarger for every } i \text{ with } |T_i| \ge 2 .$$

The constant is unspecified: the theorem asserts uniformity in $i$, not a value.

Milestones, in the order the paper's argument uses them

1. Lemma 4.7. For any generating set $S$ of a property (T) group there is $\varepsilon > 0$ such that every essentially nontrivial unitary representation and every unit vector $y$ admit $s \in S$ with $|(\pi(s)y,y)| < 1-\varepsilon$.
2. Proof of Lemma 4.8, essential nontriviality. For $\phi$ onto $T$, every nonzero vector of $W = \{v : \sum_t v_t = 0\}$ is moved by some $\pi(\phi(h))$.
3. Proof of Lemma 4.8, Rayleigh's principle. For the Cayley multigraph, $\min\{(Qy,y) : y \in W,\ \|y\| = 1\} = \lambda_1(G)$.
4. Lemma 4.8. With $H$, $S$ and $\varepsilon$ as in Lemma 4.7, $S$ finite and $S = S^{-1}$, and $\phi$ onto a finite group $T$, the Cayley graph $G(T,\phi(S))$ is a $(|T|, |S|, \varepsilon)$-enlarger.

Significance

Theorem 4.9 turns an analytic property of one infinite group into a uniform spectral bound for infinitely many finite graphs of fixed degree. With Theorem 4.3 of the paper it produces explicit families of linear expanders, hence of linear superconcentrators; for $H = SL(n,\mathbb{Z})$, $n \ge 3$, and its reductions modulo $i$ the paper obtains infinitely many explicit families of $(n, 4, \varepsilon)$-enlargers. The same mechanism underlies later work on expanders from groups, surveyed in Lubotzky's monograph (Birkhäuser 1994).

The result is proved in the paper, modulo Lemma 4.7, which the paper refers to Margulis for. The formalization adds a checked account of every step, including Lemma 4.7 itself. At the pinned Mathlib revision there is no notion of property (T), of Kazhdan constants, or of the algebraic connectivity of a multigraph, and no machine-checked version of Theorem 4.9 is known on this platform.

Difficulty

The combinatorial and linear-algebra steps are routine; the substance is in two places. First, Lemma 4.7: Definition 4.6 supplies a constant for one finite set $K$, nothing in the definition relates $K$ to a given generating set $S$, the paper gives no proof, and the standard references state the textbook form $\|\pi(h)y - y\| \ge \varepsilon$ rather than the paper's absolute-value form $|(\pi(h)y,y)| < 1-\varepsilon$. Second, the uniformity: a spectral gap for each fixed quotient is easy, since a connected graph has $\lambda_1 > 0$, but a bound that does not decay as $|T_i| \to \infty$ is exactly what cannot come from any finite computation and must come from property (T) through Lemma 4.8. The Rayleigh quotient of milestone 3 is taken over real vectors, while Lemma 4.7 is stated for complex Hilbert spaces.

Formalization scope

Groups are Lean types with a Group instance; the finite groups $T$ carry Fintype and DecidableEq. Graphs are multigraphs given by symmetric matrices Matrix T T ℕ, with loops allowed. This matters: when $\phi$ identifies two generators or sends one to the identity, the degree is still $|S|$, and a loop contributes $0$ to $Q$. Mathlib's SimpleGraph Cayley graph forgets these multiplicities and is not used. $\lambda_1$ is the second-smallest eigenvalue with multiplicity of the real symmetric matrix $Q$ (via Matrix.IsHermitian.eigenvalues₀). It is defined spectrally, as in the paper, and not as a Rayleigh minimum. It is only meaningful for $|T| \ge 2$, and the goal excludes trivial quotients explicitly. Unitary representations are homomorphisms into the unitary group of bounded operators on a complex Hilbert space in universe Type. Compact subsets of a discrete group are finite sets.

A trivializing formalization is ruled out. Property (T) is not replaced by the hypothesis that the regular representations of the quotients have no almost-invariant vectors, which would make Theorem 4.9 a restatement of its hypothesis. And $\lambda_1$ is not defined as the minimum of $(Qy,y)$ over zero-sum unit vectors, which would make milestone 3 true by definition.

A complete development needs basic Kazhdan-constant manipulations, Courant–Fischer for real symmetric matrices, and the regular representation of a finite group as a unitary representation. The regularity of Cayley multigraphs and the identity $Q = |S| I - \sum_s \pi(\phi(s))$ are short. The spectral and representation-theoretic lemmas are reusable beyond this mission. Contributions of intermediate lemmas, such as the variational characterization of eigenvalues₀ or the invariance of the zero-sum subspace, are welcome.

Selected references

• N. Alon, V. D. Milman, λ1, Isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• D. A. Kazhdan, Connection of the dual space of a group with the structure of its closed subgroups, Funct. Anal. Appl. 1 (1967) 63–65. https://doi.org/10.1007/BF01075866
• G. A. Margulis, Explicit constructions of concentrators, Probl. Inf. Transm. 9 (1973) 325–332. http://mi.mathnet.ru/ppi1162
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Comput. Syst. Sci. 22 (1981) 407–420. https://doi.org/10.1016/0022-0000(81)90040-4
• M. Fiedler, Algebraic connectivity of graphs, Czech. Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• A. Lubotzky, Discrete Groups, Expanding Graphs and Invariant Measures, Birkhäuser, 1994. https://doi.org/10.1007/978-3-0346-0332-4
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Cambridge University Press, 2008. https://doi.org/10.1017/CBO9780511542749
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8