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