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

Why canonical paths matter

A finite Markov chain moves among states according to transition probabilities. Its second largest eigenvalue measures how slowly some variation in the starting state can disappear. Directly computing that eigenvalue is often difficult when the state space is large. A geometric bound can be more useful: choose a route between each ordered pair of states and measure how much weighted traffic the routes impose on each transition. Diaconis and Stroock present this route-based bound as Proposition 7 of their 1991 paper, following the canonical-path method of Jerrum and Sinclair (Diaconis–Stroock, §3B). It makes a spectral estimate depend on the geometry of chosen routes and the stationary weight of each edge.

The paper's purpose is to compare methods for bounding eigenvalues of reversible chains. Its earlier Poincaré estimate uses weighted path lengths. Proposition 7 instead passes through a bottleneck constant and Cheeger's inequality. These are different summaries of the same chain: one examines a system of paths, and the other examines flow across every cut. The comparison is useful on graphs where paths are easy to choose but the cut minimizing the bottleneck constant is not apparent (Diaconis–Stroock, pp. 52–55).

Finite reversible chains and directed path congestion

Let $V$ be a finite state space with at least two states. A transition matrix $P$ has entries $P(x,y)\geq 0$ and each row sums to one. It is irreducible when every state can be reached from every other state in some number of steps. A stationary distribution $\pi$ is a nonnegative probability vector satisfying $\pi P=\pi$. The chain is reversible when it satisfies detailed balance: $\pi(x)P(x,y)=\pi(y)P(y,x)$. Write $Q(x,y)=\pi(x)P(x,y)$ for the stationary edge flow. These are the standing assumptions of the paper's §1A, restated in §3B (Diaconis–Stroock, pp. 36, 54).

For every distinct ordered pair $(x,y)$, choose a finite walk $\gamma_{xy}$ from $x$ to $y$. Every consecutive step $(u,v)$ of the walk must have $Q(u,v)>0$. The walk may revisit a vertex or an edge; §3B places no no-repetition condition on these choices. An oriented edge is an ordered pair $(u,v)$ with positive flow. A walk contains it when one of its consecutive steps traverses it in that direction. The canonical-path congestion of the chosen walk system $\Gamma$ is the paper's quantity

$$\eta(\Gamma)=\max_{e:Q(e)>0}\frac{1}{Q(e)} \sum_{x\ne y:\,e\in\gamma_{xy}}\pi(x)\pi(y).$$

The sum assigns weight $\pi(x)\pi(y)$ to an ordered pair, once for each directed edge that its chosen walk uses. Irreducibility ensures that walks between different states exist. Under the mission's assumptions the positive-flow edge set is nonempty, so the maximum has its ordinary finite meaning (Diaconis–Stroock, (3.2), p. 54).

For a nonempty set $S\subseteq V$ with $\pi(S)\leq\tfrac12$, let $Q(S\times S^{\mathrm c})$ be the total stationary flow from $S$ to its complement. The bottleneck constant is

$$h=\min_{\varnothing\ne S\subseteq V,\,\pi(S)\leq 1/2} \frac{Q(S\times S^{\mathrm c})}{\pi(S)}.$$

The denominator is positive under irreducibility. Write $\beta_1$ for the largest eigenvalue of $P$ other than the simple eigenvalue $1$, and write $\lambda_1=1-\beta_1$ for the spectral gap. These conventions match §1A and equation (3.4) (Diaconis–Stroock, pp. 36, 56).

Formalization targets

The mission's goal is Proposition 7, for every valid choice of $\Gamma$:

$$\beta_1\leq 1-\frac{1}{8\eta(\Gamma)^2}.$$

Its milestones record the source's cut argument: a selected walk from $S$ to $S^{\mathrm c}$ crosses an oriented cut edge; the total pair weight obeys $\pi(S)\pi(S^{\mathrm c})\leq\eta Q(S\times S^{\mathrm c})$; and consequently $h\geq 1/(2\eta)$. The final milestone is the already formalized version of the paper's equation (3.4), $h^2/2\leq\lambda_1\leq 2h$ (Diaconis–Stroock, pp. 54, 56).

The companion result is the graph specialization (3.3). For simple random walk on a connected graph $G=(V,E)$, let $d_*$ be the maximum degree and let $b$ be the maximum number of ordered-pair walks traversing an oriented edge. It gives

$$\beta_1\leq 1-\frac12\left(\frac{|E|}{d_*^2b}\right)^2.$$

This statement uses the exact displayed bound of Remark 3.1; the earlier sentence in that remark uses a different normalization of $\eta$ (Diaconis–Stroock, p. 55).

What the bound supplies

The proposition converts any usable path system into an explicit spectral estimate. Once a graph or chain supplies paths whose edge loads can be bounded, the formula bounds $\beta_1$ without diagonalizing $P$ or finding the set that minimizes $h$. In the graph case, equation (3.3) expresses the estimate using only the edge count, maximum degree, and maximum directed path load. The paper compares that bound with its Poincaré bound on examples including cycles, cubes, and binary trees (Diaconis–Stroock, pp. 55–56).

Equation (3.4) already has a proved formalization in the published MarkovMixing library, under the same finite reversible-chain conventions. This mission adds the paper's path-congestion definition and cut estimates, then states the still-needed Proposition 7 and graph specialization against that library. The result is a reusable connection between a chosen family of walks and a chain's existing bottleneck and spectral objects.

Where the difficulty lies

The route load $\eta$ concerns individual directed edges, whereas $h$ takes a minimum over all admissible cuts. A single heavily loaded edge does not by itself identify the minimizing cut. The central difficulty is to control, for every cut at once, all weighted ordered pairs whose walks leave it. The direction of a crossing matters: $Q(S\times S^{\mathrm c})$ counts edges directed out of $S$, and $\eta$ must count traversals of those same orientations. Omitting an orientation or allowing negative unused edge flow would invalidate the intermediate cut estimate.

There is also a printed discrepancy. Proposition 6 on p. 52 displays a stronger upper bound on $\beta_1$ than the inequality established in §3C. The mission uses equation (3.4), whose lower gap bound yields the $1/(8\eta^2)$ constant actually stated in Proposition 7 (Diaconis–Stroock, pp. 52, 54, 56).

Formalization scope

Lean represents the state space as a finite type, the chain as a real matrix, and the stationary distribution as a real function. It imports the published MarkovMixing definitions of stochasticity, irreducibility, stationarity, detailed balance, $Q$, $h$, $\beta_1$, and simple random walk. A local definition represents each selected walk by its vertex list and derives directed edges from consecutive vertices. The hypothesis $2\leq |V|$ makes $\beta_1$ the paper's second eigenvalue and excludes the one-state junk value of the real supremum used in its definition. Positivity of $\eta$ follows from the chain and walk assumptions; it is not inserted as an extra assumption.

The walk system is universally quantified: the theorem concerns every valid selection, rather than one favorable selection. The local definition ignores equal-endpoint choices because they do not cross any $S$-to-$S^{\mathrm c}$ cut; §3B mentions all ordered pairs, so this convention gives a slightly stronger target and is stated explicitly. The cut lemma retains stochasticity and nonnegative stationary weights to keep the flow of unused cut edges nonnegative. The graph companion derives its Markov-chain properties from connectedness rather than assuming them.

The shared vertex-list representation and the cut crossing statement can serve later path-based bounds. Contributions toward positivity and finiteness of congestion, the uniform cut estimate, the bottleneck estimate, and the graph specialization all fit the mission. A definition that forces $\eta>0$ by fiat, or a goal that assumes the bottleneck estimate or Cheeger's inequality, would erase the mathematical content.

Selected references

• Persi Diaconis and Daniel Stroock, Geometric bounds for eigenvalues of Markov chains, Annals of Applied Probability 1(1):36–61, 1991. DOI.
• David A. Levin, Yuval Peres, and Elizabeth L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009, Chapter 13. Book 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

Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.

Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.

Timeline.

• 1983: Ajtai, Komlós and Szemerédi use bounded-degree bipartite expanders to build sorting networks of depth $O(\log n)$.
• 1984: Tanner (SIAM J. Alg. Disc. Meth. 5) bounds the neighbourhood size of a set in a regular bipartite graph by its second eigenvalue, the direction "eigenvalue gap implies expansion".
• 1985: Alon and Milman (J. Combin. Theory Ser. B 38) prove isoperimetric inequalities for graphs in terms of $\lambda(G)$ and introduce enlargers.
• 1986: Alon proves the converse direction, "expansion implies an eigenvalue gap" (Lemma 2.4 and Theorem 3.4 of the paper).

Setting

All graphs are finite and simple. For a graph $G = (V, E)$ and a set $X \subseteq V$, $N(X) = \{v \in V : vx \in E \text{ for some } x \in X\}$ is the set of neighbours of $X$; it may meet $X$.

The Laplacian of $G$ is $Q_G = \mathrm{diag}(d(v))_{v \in V} - A_G$, where $A_G$ is the 0–1 adjacency matrix and $d(v)$ the degree of $v$. It is symmetric with eigenvalues $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$, counted with multiplicity, and $\lambda(G) = \lambda_1$ is its second-smallest eigenvalue. It is positive exactly when $G$ is connected.

• An $(n, d, c)$-magnifier is a graph on $n$ vertices with maximal degree $d$ in which every $X \subseteq V$ with $|X| \le n/2$ satisfies $|N(X) - X| \ge c|X|$.
• An $(n, d, \varepsilon)$-enlarger is a graph on $n$ vertices with maximal degree $d$ and $\lambda(G) \ge \varepsilon$.
• A bipartite graph $G = (I, O; E)$ has inputs $I$, outputs $O$ and edges only between $I$ and $O$. It is a strong $(n, d, c)$-expander if $|I| = |O| = n$, the maximal degree is $d$, and for every $X \subseteq I$

$$|N(X)| \ge \Bigl(1 + c\Bigl(1 - \frac{|X|}{n}\Bigr)\Bigr)|X|.$$

Formalization targets

Goal: Theorem 3.4

Let $G = (I, O; E)$ be a $d$-regular bipartite graph with $|I| = |O| = n$ and $\lambda = \lambda(G)$.

1. If $G$ is a strong $(n, d, c)$-expander then

$$\lambda \ge \frac{c^2}{1024 + 2c^2}.$$

2. If $\lambda \ge \varepsilon$ then $G$ is a strong $(n, d, c)$-expander with

$$c = \frac{2d\varepsilon - \varepsilon^2}{d^2}.$$

Milestones, in the order of the paper

• Lemma 2.2 (Alon–Milman, already on the platform): for disjoint sets $A, B$ at distance $\varrho > 1$, $b \le (1-a)/(1 + (\lambda/d)a\varrho^2)$.
• Corollary 2.3: every $(n, d, \varepsilon)$-enlarger is an $(n, d, 2\varepsilon/(d+2\varepsilon))$-magnifier.
• Eq. (2.1): if $f$ is an eigenvector of $Q_G$ for $\lambda(G)$ and $g$ its positive part, then $\sum_{uv \in E}(g(u)-g(v))^2 \le \lambda \sum_v g^2(v)$.
• Lemma 2.4: every $(n, d, c)$-magnifier has $\lambda(G) \ge c^2/(4 + 2c^2)$.
• Lemma 3.1: a strong $(n, d, c)$-expander is a $(2n, d, c/16)$-magnifier.
• Proof of Lemma 3.3, spectrum: the two largest eigenvalues of $C^TC$, with $C$ the $I \times O$ biadjacency matrix, are $d^2$ and $(d - \lambda)^2$.
• Proof of Lemma 3.3, Tanner's bound: $|N(X)| \ge d^2|X| / \bigl(\alpha(d^2 - (d-\lambda)^2) + (d-\lambda)^2\bigr)$ with $\alpha = |X|/n$.
• Lemma 3.3: a $d$-regular bipartite graph is a strong $(n, d, (2d\lambda - \lambda^2)/d^2)$-expander.

Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.

Significance

The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.

The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.

Difficulty

The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of $C^TC$. The converse is the hard one. A first attempt bounds $\lambda(G)$ from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on $\lambda$: any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs $(u, u)$ of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.

Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.

Formalization scope

Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities $|N(X)|$ are Set.ncard. "Maximal degree $d$" is read as G.maxDegree ≤ d; every statement is monotone in $d$ or fixes $d$ by regularity (G.IsRegularOfDegree d). The condition $|X| \le n/2$ is written $2|X| \le n$ in $\mathbb{N}$. All constants are real, and every subtraction and division is taken in $\mathbb{R}$.

Reused published items:

• $\lambda(G)$ is AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is $0$ by convention on fewer than two vertices.
• $N(X)$ is AKSSorting.Core.neighbours.
• Lemma 2.2 is AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that $G$ is connected and $n \ge 2$; outside them the inequality is trivial.

The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:

• $n \ge 1$ and $c \ge 0$ in Theorem 3.4 (1);
• $\varepsilon > 0$ in Theorem 3.4 (2);
• $n \ge 2$ and $c \ge 0$ in Lemma 2.4;
• $n \ge 2$ in Lemma 3.1 and in the $C^TC$ statement;
• $d \ge 1$ in Lemma 3.3;
• $\varepsilon \ge 0$ in Corollary 2.3.

Eq. (2.1) is stated in multiplied form, so no quotient by $\sum g^2$ appears.

The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in $c$, because $c' \le c$; their content is algorithmic.

Several encodings would trivialize the mission and are excluded:

• a $\lambda$ other than the published second-smallest Laplacian eigenvalue, in particular one defined as the best constant of a quotient;
• expansion or magnifier conditions with a negative constant in a hypothesis;
• $|X| \le n/2$ with truncating natural-number division.

Contributions are welcome:

• Tanner's bound in Lean, which is reusable for any regular bipartite graph;
• a max-flow min-cut theorem for finite networks;
• the corrected flow lemma behind Eqs. (2.2)–(2.3);
• the spectral facts about $\lambda(G)$ for bipartite graphs ($\lambda \le d$ for $n \ge 2$, and $\lambda = d - \sigma_2(C)$).

Selected references

• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• N. Alon and V. D. Milman, λ₁, 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
• R. M. Tanner, Explicit concentrators from generalized N-gons, SIAM J. Algebraic Discrete Methods 5 (1984) 287–293. https://doi.org/10.1137/0605030
• M. Ajtai, J. Komlós and E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3 (1983) 1–19. https://doi.org/10.1007/BF02579338

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