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