Graphs · The Lumenary

Lens

MotivationH

Seven bridges, one walk

In the 18th century the city of Königsberg (today Kaliningrad) was built around two islands in the river Pregel, joined to the banks and to each other by seven bridges. A popular puzzle asked: can you take a walk that crosses every bridge exactly once? Nobody could find one, but nobody could prove that none existed — until Leonhard Euler, in 1736, saw that the answer has nothing to do with distances, angles or the shape of the river. All that matters is which land masses are joined by how many bridges.

That insight created a new kind of mathematics. Today the same idea describes road and rail networks, electrical circuits, molecules, friendships, the links between web pages, and the routes of rubbish trucks and postal workers — the "Chinese postman problem", posed by the mathematician Guan Meigu in 1960, asks for the shortest walk along every street of a town.

You may have met these ideas in dots and lines. In this lesson we make them precise and prove them.

IntuitionH

Forgetting everything except connections

Here is Euler's simplification. Shrink each land mass to a dot and draw one line for each bridge.

The Königsberg bridges as a graph: four land masses (vertices) and seven bridges (edges). Kneiphof island has $5$ bridges; each of the other three land masses has $3$.

A walk over the bridges becomes a walk along the lines. Now think about a vertex in the middle of a walk: every time the walk arrives there along one edge, it leaves along another. Visits use up edges in pairs. Only the start and the end of the walk can be left with an unpaired edge.

A drawing is only a picture of a graph. Moving the dots or bending the lines changes nothing, as long as the same pairs stay joined.

DefinitionsH

Definitions

Definition— graph

A simple graph $G = (V, E)$ consists of a finite set $V$ of vertices and a set $E$ of edges, each edge being a two-element subset $\{u, v\}$ of $V$ . We say $u$ and $v$ are adjacent, or neighbours, and that the edge joins them. A multigraph may also have several edges joining the same pair of vertices (parallel edges), like the Königsberg bridges.

Definition— degree

The degree $\deg(v)$ of a vertex $v$ is the number of edges that have $v$ as an end.

Definition— walk, trail, path, cycle

A walk is a sequence $v_0, e_1, v_1, e_2, \dots, e_k, v_k$ in which each edge $e_i$ joins $v_{i-1}$ and $v_i$ ; it is closed if $v_k = v_0$ . A trail is a walk that uses no edge twice; a path is a walk that visits no vertex twice. A cycle is a closed trail with at least one edge in which no vertex is repeated except that $v_k = v_0$ (in a simple graph a cycle has at least three edges).

Definition— connected

A graph is connected if every two vertices are joined by a walk (equivalently, by a path: a shortest walk between two vertices never repeats a vertex).

Definition— Euler trail and Euler circuit

An Euler trail is a trail that uses every edge of the graph exactly once. An Euler circuit is a closed Euler trail.

Definition— tree

A tree is a connected graph with no cycles. A leaf is a vertex of degree $1$ .

Definition— isomorphism

Graphs $G = (V, E)$ and $H = (W, F)$ are isomorphic if there is a bijection $f : V \to W$ that preserves adjacency in both directions: $\{u, v\} \in E$ exactly when $\{f(u), f(v)\} \in F$ . Such an $f$ is an isomorphism.

Some families have names: the complete graph $K_n$ ( $n$ vertices, every pair joined), the cycle $C_n$ ( $n$ vertices in a ring), the path $P_n$ ( $n$ vertices in a line) and the star with one centre joined to all the other vertices.

Worked examplesH

Examples and non-examples

Example— Degrees in a small network

Five towns are joined by roads: Arusha–Moshi, Arusha–Nairobi, Moshi–Nairobi, Nairobi–Mombasa, Moshi–Tanga, Tanga–Mombasa. The degrees are Arusha $2$ , Moshi $3$ , Nairobi $3$ , Mombasa $2$ , Tanga $2$ . They add up to $12$ , twice the number of roads.

Example— Complete graphs

In $K_n$ every vertex has degree $n - 1$ , and there is one edge for every pair of vertices, so $K_n$ has $\binom{n}{2} = \frac{n(n-1)}{2}$ edges (see combinatorics). A round-robin tournament of $10$ teams has $\binom{10}{2} = 45$ matches.

Example— Euler trail, but no Euler circuit

The "house" — a square with a triangular roof and both diagonals of the square drawn — can be drawn in one stroke without lifting the pen, but only if you start at one bottom corner and finish at the other. Those two corners are its only vertices of odd degree ( $3$ each); the other three vertices have even degree.

Example— Euler is not Hamilton

The cube graph (the corners and edges of a cube) has a Hamiltonian cycle — a cycle visiting every vertex exactly once: go round the top face, drop down, go round the bottom face in the opposite direction and climb back up. But every vertex has degree $3$ , which is odd, so it has no Euler circuit and not even an Euler trail. Euler circuits use every edge once; Hamiltonian cycles visit every vertex once. Deciding whether a graph has an Euler circuit is easy (count degrees); no comparably simple test is known for Hamiltonian cycles.

Example— A non-example: crossings are not vertices

If two edges of a drawing cross at a point that is not a dot, that crossing is not a vertex. The complete graph $K_4$ is often drawn as a square with both diagonals, which cross in the middle; it still has only $4$ vertices and $6$ edges.

ProofH

Theorems and proofs

Degrees

Theorem— Theorem 1 (handshake lemma)

In every graph (or multigraph), the sum of the degrees of the vertices is twice the number of edges:

\sum_{v \in V} \deg(v) = 2|E|.

Proof

Count the edge-ends in two ways. Each edge has exactly two ends, so there are $2|E|$ of them. On the other hand, the number of edge-ends at a vertex $v$ is $\deg(v)$ , so the total is $\sum_v \deg(v)$ .

∎

The name comes from a party: if everyone shakes some hands, the total number of hands shaken, counted person by person, is twice the number of handshakes.

Theorem— Corollary 2

Every graph has an even number of vertices of odd degree.

Proof

Split the sum of the degrees into the sum over the even-degree vertices and the sum over the odd-degree vertices. The total is even (Theorem 1) and the first part is a sum of even numbers, so the second part is even. A sum of odd numbers is even only when there is an even number of them.

∎

So, for example, there is no group of $7$ people in which everyone knows exactly $3$ others: the degrees would add up to $21$ , which is odd.

Euler trails and circuits

Theorem— Lemma 3 (edge-ends along a walk)

Let $W$ be a trail from $a$ to $b$ and let $v$ be a vertex. The number of edge-ends at $v$ belonging to edges of $W$ is even if $v$ is neither or both of $a$ and $b$ (in particular whenever $W$ is closed, $a = b$ ), and odd if $v$ is exactly one of them.

Proof

Each time the trail passes through $v$ — arriving along one edge and leaving along another — it uses two edge-ends at $v$ . Starting at $v$ uses one edge-end, and finishing at $v$ uses one more. So the count is $2 \times (\text{number of passes through } v)$ , plus $1$ if $v = a$ , plus $1$ if $v = b$ .

∎

Theorem— Theorem 4 (Euler's theorem)

Let $G$ be a connected graph or multigraph with at least one edge.

$G$ has an Euler circuit if and only if every vertex has even degree.
$G$ has an Euler trail that is not closed if and only if exactly two vertices have odd degree; the trail then starts at one of them and ends at the other.

Proof

Necessity. An Euler trail uses every edge, so the edge-ends of its edges are all the edge-ends, and the count in Lemma 3 is exactly $\deg(v)$ . For an Euler circuit every degree is therefore even. For an Euler trail from $a$ to $b \ne a$ , exactly $a$ and $b$ have odd degree. (Connectedness is not needed for this half.)

Sufficiency for circuits. Suppose every degree is even.

Step 1: from any vertex $u$ of positive degree, there is a closed trail starting at $u$ . Walk from $u$ along unused edges, choosing any unused edge each time. Whenever you arrive at a vertex $w \ne u$ , you have used an odd number of its edge-ends (two for each earlier pass, one for arriving), and $\deg(w)$ is even, so an unused edge remains and you can leave. The graph is finite, so the walk must stop — and the only place it can stop is $u$ . This gives a closed trail.

Step 2. Let $C$ be a closed trail using as many edges as possible. Suppose some edge is not in $C$ . Then some vertex $u$ on $C$ has an edge not in $C$ : otherwise, take an unused edge, a path from a vertex of $C$ to one of its ends (the graph is connected), and look at the first edge of this path that leaves the vertices of $C$ — it touches $C$ but is not in $C$ . Delete the edges of $C$ . By Lemma 3, $C$ used an even number of edge-ends at every vertex, so in what is left every degree is still even, and $u$ still has positive degree. Step 1 gives a closed trail $C'$ from $u$ in the remaining edges. Following $C$ to $u$ , going round $C'$ , and then finishing $C$ is a closed trail longer than $C$ — a contradiction. So $C$ uses every edge: it is an Euler circuit.

Sufficiency for trails. If exactly $a$ and $b$ have odd degree, add a new edge joining $a$ and $b$ (it may be parallel to an existing one). Now every degree is even and the graph is still connected, so there is an Euler circuit. Start it just after the new edge; removing the new edge leaves an Euler trail from $a$ to $b$ .

∎

Step 1 and Step 2 together are an algorithm, essentially Hierholzer's algorithm (1873): walk until you are stuck, then splice in detours. The computation section runs it.

Example— Königsberg, settled

The four land masses have degrees $5$ , $3$ , $3$ and $3$ — four odd vertices. By Theorem 4 there is no Euler trail and no Euler circuit: no walk crosses every bridge exactly once. (Adding one bridge between the two banks would leave exactly two odd land masses, and then such a walk would exist.)

Trees

Theorem— Lemma 5 (leaves)

Every tree with at least two vertices has at least two leaves.

Proof

Take a longest path $v_0, v_1, \dots, v_k$ in the tree; since the tree is connected and has two vertices, $k \ge 1$ . A neighbour of $v_k$ outside the path would give a longer path, and a neighbour $v_i$ with $i < k - 1$ would close the cycle $v_i, v_{i+1}, \dots, v_k, v_i$ . So $v_{k-1}$ is the only neighbour of $v_k$ : $v_k$ is a leaf. The same argument applies to $v_0$ .

∎

Theorem— Theorem 6 (trees)

Let $T$ be a tree with $n$ vertices. Then

$T$ has exactly $n - 1$ edges;
any two vertices of $T$ are joined by exactly one path.

Proof

1. Induction on $n$ . A tree with one vertex has no edges. If $n \ge 2$ , Lemma 5 gives a leaf $v$ ; remove it and its single edge. What is left has no cycles (we removed things), and it is still connected: a path between two other vertices never passes through $v$ , because a vertex in the middle of a path needs two edges. So it is a tree with $n - 1$ vertices, which by induction has $n - 2$ edges, and $T$ has $n - 1$ .

2. A path exists because $T$ is connected. Suppose $P$ and $Q$ were two different paths from $u$ to $v$ . Both start at $u$ ; let $w$ be the last vertex before they first go different ways. Follow $P$ from $w$ until it first meets a vertex $x$ of $Q$ again (it must, since $P$ ends at $v$ , which is on $Q$ ). The part of $P$ from $w$ to $x$ and the part of $Q$ between $x$ and $w$ share only $w$ and $x$ , and they are not the same single edge (because $P$ and $Q$ leave $w$ along different edges), so together they form a cycle — impossible in a tree.

∎

Conversely, a graph in which every two vertices are joined by exactly one path is a tree. And for a graph with $n$ vertices, any two of "connected", "no cycles" and " $n - 1$ edges" imply the third. For instance, if $G$ has no cycles and $n - 1$ edges, each of its $c$ connected pieces is a tree, with $n_i$ vertices and $n_i - 1$ edges; adding up, $n - c = n - 1$ edges, so $c = 1$ and $G$ is connected.

Isomorphism

To prove that two graphs are isomorphic, exhibit an isomorphism. To prove that they are not, find an invariant — a property preserved by every isomorphism — on which they differ: the number of vertices or edges, the list of degrees (the degree sequence), connectedness, the number of triangles, the length of the shortest cycle…

Theorem— Theorem 7 (isomorphisms preserve degrees)

If $f$ is an isomorphism from $G$ to $H$ , then $\deg_H(f(v)) = \deg_G(v)$ for every vertex $v$ . Hence isomorphic graphs have the same degree sequence.

Proof

Since $f$ preserves adjacency in both directions, it maps the neighbours of $v$ one-to-one onto the neighbours of $f(v)$ .

∎

Example— Two trees that differ

The path $P_4$ (degrees $1, 2, 2, 1$ ) and the star with three leaves (degrees $3, 1, 1, 1$ ) both have $4$ vertices and $3$ edges, and both are trees. They are not isomorphic: the star has a vertex of degree $3$ and the path does not.

Example— Same degrees, still different

The hexagon $C_6$ and two separate triangles both have six vertices, six edges, and every degree equal to $2$ . They are not isomorphic, because the hexagon is connected and two triangles are not (equally: two triangles contain a triangle, the hexagon does not). Matching degree sequences is necessary for isomorphism, not sufficient.

Example— Different drawings, same graph

Draw five dots $0, 1, 2, 3, 4$ around a circle. The pentagon joins neighbours $0$ – $1$ – $2$ – $3$ – $4$ – $0$ ; the pentagram joins every second dot, $0$ – $2$ – $4$ – $1$ – $3$ – $0$ . They look different, but the bijection $0 \mapsto 0$ , $1 \mapsto 2$ , $2 \mapsto 4$ , $3 \mapsto 1$ , $4 \mapsto 3$ carries each pentagon edge to a pentagram edge: both are the cycle $C_5$ .

Formal mathematicsF

Graphs in Lean

For the handshake lemma and Euler's theorem we need multigraphs, because Königsberg has parallel bridges. So we build a small model: a multigraph is a list of edges, each an unordered pair s(a, b) (Mathlib's Sym2).

MultigraphLean 4Formally verified

/-- A finite **multigraph** on the vertices `0, 1, …, n − 1`, given as a list of edges. An edge
is an unordered pair `s(a, b)` (Mathlib's `Sym2`), and the same pair may occur several times:
parallel edges, like the two bridges joining the island of Kneiphof to each river bank. -/
abbrev Multigraph (n : ℕ) := List (Sym2 (Fin n))

Axioms used: No axiomsformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

endsLean 4Formally verified

/-- How many ends of the edge `e` lie at the vertex `v`: `0`, `1` or `2` (a loop `s(v, v)`
has both of its ends at `v`). -/
def ends {n : ℕ} (v : Fin n) : Sym2 (Fin n) → ℕ :=
  Sym2.lift ⟨fun a b => (if a = v then 1 else 0) + (if b = v then 1 else 0),
    fun _ _ => Nat.add_comm _ _⟩

Axioms used: Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

degreeLean 4Formally verified

/-- The **degree** of `v` in `G`: the number of edge-ends at `v`. -/
def degree {n : ℕ} (G : Multigraph n) (v : Fin n) : ℕ := (G.map (ends v)).sum

Axioms used: propext, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

The handshake lemma is proved by induction on the list of edges — each new edge adds exactly $2$ to the total — and Corollary 2 follows from it:

handshakeLean 4Proved here from basic factsFormally verified

/-- **The handshake lemma:** the degrees add up to twice the number of edges. Induction on the
list of edges: an edge `s(a, b)` contributes one end at `a` and one at `b`, so adding it raises
the total degree by exactly `2`. -/
theorem handshake {n : ℕ} (G : Multigraph n) : ∑ v, degree G v = 2 * G.length := by
  induction G with
  | nil => simp [degree]
  | cons e G ih =>
    have he : ∑ v, ends v e = 2 := by
      induction e using Sym2.ind with
      | h a b => simp [ends, sum_add_distrib]
    simp only [degree, List.map_cons, List.sum_cons, sum_add_distrib, List.length_cons] at ih ⊢
    rw [he, ih]
    omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

even_card_odd_degreeLean 4Proved here from basic factsFormally verified

/-- **The number of odd-degree vertices is even.** Split the degree sum into the odd-degree and
the even-degree vertices. The total is even (handshake lemma) and the even-degree part is even,
so the odd-degree part is even; but a sum of odd numbers is even only when there is an even
number of them. -/
theorem even_card_odd_degree {n : ℕ} (G : Multigraph n) :
    Even #{v | Odd (degree G v)} := by
  set O := ({v | Odd (degree G v)} : Finset (Fin n))
  -- each odd degree is `2q + 1`, each even degree is `2q`
  have hodd : ∑ v ∈ O, degree G v = 2 * ∑ v ∈ O, degree G v / 2 + #O := by
    rw [mul_sum, card_eq_sum_ones, ← sum_add_distrib]
    refine sum_congr rfl fun v hv => ?_
    have h1 := Nat.odd_iff.1 (mem_filter.1 hv).2
    have h2 := Nat.div_add_mod (degree G v) 2
    omega
  have heven : ∑ v ∈ univ.filter (fun v => ¬ Odd (degree G v)), degree G v =
      2 * ∑ v ∈ univ.filter (fun v => ¬ Odd (degree G v)), degree G v / 2 := by
    rw [mul_sum]
    refine sum_congr rfl fun v hv => ?_
    have h1 := Nat.not_odd_iff.1 (mem_filter.1 hv).2
    have h2 := Nat.div_add_mod (degree G v) 2
    omega
  have htotal := handshake G
  rw [← sum_filter_add_sum_filter_not univ (fun v => Odd (degree G v)), hodd, heven] at htotal
  rw [Nat.even_iff]
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

A walk is a list of vertices $w_0, w_1, \dots, w_m$ , and it crosses the edges $s(w_0, w_1), s(w_1, w_2), \dots$ . It is an Euler trail when this list of edges is a rearrangement (List.Perm) of the edges of the graph — every edge crossed exactly once.

walkEdgesLean 4Formally verified

/-- The edges crossed by a walk that visits the vertices `w₀, w₁, …, wₘ` in this order:
`s(w₀, w₁), s(w₁, w₂), …, s(wₘ₋₁, wₘ)`. -/
def walkEdges {n : ℕ} : List (Fin n) → Multigraph n
  | a :: b :: rest => s(a, b) :: walkEdges (b :: rest)
  | _ => []

Axioms used: propextformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

IsEulerTrailLean 4Formally verified

/-- `w` is an **Euler trail** of `G`: a walk whose edges are exactly the edges of `G`, each
crossed once (the two lists are rearrangements of each other). -/
def IsEulerTrail {n : ℕ} (G : Multigraph n) (w : List (Fin n)) : Prop :=
  w ≠ [] ∧ (walkEdges w).Perm G

Axioms used: propextformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

IsEulerCircuitLean 4Formally verified

/-- An **Euler circuit** is an Euler trail that ends where it started. -/
def IsEulerCircuit {n : ℕ} (G : Multigraph n) (w : List (Fin n)) : Prop :=
  IsEulerTrail G w ∧ w.head? = w.getLast?

Axioms used: propextformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

Lemma 3 becomes an exact equation, proved by induction along the walk. Here rest.getLastD a is the last vertex of the walk a :: rest:

degree_walkEdgesLean 4Proved here from basic factsFormally verified

/-- **Counting edge-ends along a walk.** Each time a walk passes *through* a vertex it uses two
edge-ends there, one arriving and one leaving; only the start and the finish are left with a
single end. Precisely: for the walk `a, …` whose last vertex is `rest.getLastD a`, the degree of
`v` in the walk's edges, plus `1` if the walk starts at `v`, plus `1` if it finishes at `v`, is
twice the number of visits to `v`. Induction on the walk. -/
theorem degree_walkEdges {n : ℕ} (a : Fin n) (rest : List (Fin n)) (v : Fin n) :
    degree (walkEdges (a :: rest)) v + (if a = v then 1 else 0) +
      (if rest.getLastD a = v then 1 else 0) = 2 * (a :: rest).count v := by
  induction rest generalizing a with
  | nil =>
    simp only [walkEdges, degree, List.map_nil, List.sum_nil, List.getLastD_nil,
      List.count_singleton, beq_iff_eq]
    by_cases hav : a = v <;> simp [hav]
  | cons b rest ih =>
    have h := ih b
    have hab : ends v s(a, b) = (if a = v then 1 else 0) + (if b = v then 1 else 0) := rfl
    simp only [walkEdges, degree, List.map_cons, List.sum_cons, List.getLastD_cons,
      List.count_cons, beq_iff_eq, hab] at h ⊢
    by_cases hav : a = v <;> by_cases hbv : b = v <;> simp [hav, hbv] at h ⊢ <;> omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

degree_permLean 4Proved here from basic factsFormally verified

/-- Rearranging the list of edges does not change any degree. -/
theorem degree_perm {n : ℕ} {G H : Multigraph n} (h : G.Perm H) (v : Fin n) :
    degree G v = degree H v :=
  (h.map (ends v)).sum_eq

Axioms used: propext, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

From it, the necessity half of Euler's theorem, for circuits and for trails:

euler_circuit_evenLean 4Proved here from basic factsFormally verified

/-- **Euler's theorem, necessity (circuits).** If a multigraph has an Euler circuit, every
vertex has even degree: the circuit's start and finish coincide, so every visit to a vertex
uses an even number of edge-ends there. -/
theorem euler_circuit_even {n : ℕ} {G : Multigraph n} {w : List (Fin n)}
    (h : IsEulerCircuit G w) (v : Fin n) : Even (degree G v) := by
  obtain ⟨⟨hne, hperm⟩, hends⟩ := h
  obtain ⟨a, rest, rfl⟩ := List.exists_cons_of_ne_nil hne
  -- the walk finishes where it starts
  have hlast : rest.getLastD a = a := by
    simp only [List.head?_cons, List.getLast?_cons, Option.some.injEq] at hends
    rw [List.getLastD_eq_getLast?]
    exact hends.symm
  have key := degree_walkEdges a rest v
  rw [hlast, degree_perm hperm v] at key
  rw [Nat.even_iff]
  by_cases hav : a = v <;> simp [hav] at key <;> omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

euler_trail_oddLean 4Proved here from basic factsFormally verified

/-- **Euler's theorem, necessity (trails).** In an Euler trail, every vertex of odd degree is
the start or the finish of the trail. So a multigraph with more than two odd-degree vertices
has no Euler trail. -/
theorem euler_trail_odd {n : ℕ} {G : Multigraph n} {w : List (Fin n)}
    (h : IsEulerTrail G w) (v : Fin n) (hv : Odd (degree G v)) :
    w.head? = some v ∨ w.getLast? = some v := by
  obtain ⟨hne, hperm⟩ := h
  obtain ⟨a, rest, rfl⟩ := List.exists_cons_of_ne_nil hne
  have key := degree_walkEdges a rest v
  rw [degree_perm hperm v] at key
  rw [List.head?_cons, List.getLast?_cons, ← List.getLastD_eq_getLast?]
  rw [Nat.odd_iff] at hv
  by_contra hcon
  simp only [not_or, Option.some.injEq] at hcon
  simp only [hcon.1, hcon.2, ite_false] at key
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

And Königsberg, settled by machine:

konigsbergLean 4Formally verified

/-- **The bridges of Königsberg** (1736). Land masses: `0` = the island of Kneiphof,
`1` = the north bank, `2` = the south bank, `3` = the eastern island. Seven bridges: two from
Kneiphof to each bank, one from Kneiphof to the eastern island, and one from each bank to the
eastern island. -/
def konigsberg : Multigraph 4 :=
  [s(0, 1), s(0, 1), s(0, 2), s(0, 2), s(0, 3), s(1, 3), s(2, 3)]

Axioms used: propextformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

konigsberg_degreesLean 4Proved here from basic factsFormally verified

/-- The degrees of the four land masses are `5, 3, 3, 3` — all odd. Lean counts the bridge
ends. -/
theorem konigsberg_degrees :
    degree konigsberg 0 = 5 ∧ degree konigsberg 1 = 3 ∧ degree konigsberg 2 = 3 ∧
      degree konigsberg 3 = 3 := by
  decide

Axioms used: propext, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

konigsberg_no_euler_trailLean 4Proved here from basic factsFormally verified

/-- **There is no walk crossing every bridge of Königsberg exactly once.** All four land masses
have odd degree, so by `euler_trail_odd` each of the four would have to be the start or the
finish of the walk — but a walk has only one start and one finish. -/
theorem konigsberg_no_euler_trail : ¬ ∃ w, IsEulerTrail konigsberg w := by
  rintro ⟨w, hw⟩
  obtain ⟨d0, d1, d2, d3⟩ := konigsberg_degrees
  have h0 := euler_trail_odd hw 0 (by rw [d0]; decide)
  have h1 := euler_trail_odd hw 1 (by rw [d1]; decide)
  have h2 := euler_trail_odd hw 2 (by rw [d2]; decide)
  have h3 := euler_trail_odd hw 3 (by rw [d3]; decide)
  rcases h0 with h0 | h0 <;> rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;>
    rcases h3 with h3 | h3 <;> simp_all

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

Mathlib's SimpleGraph has the same facts for simple graphs, including Euler's degree condition for its own notion of an Eulerian walk:

handshake_libraryLean 4Applies a library theoremFormally verified

/-- The handshake lemma for Mathlib's simple graphs. This applies
`SimpleGraph.sum_degrees_eq_twice_card_edges`. -/
theorem handshake_library {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] : ∑ v, G.degree v = 2 * #G.edgeFinset :=
  G.sum_degrees_eq_twice_card_edges

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

eulerian_even_degree_iffLean 4Applies a library theoremFormally verified

/-- Euler's degree condition in Mathlib: if `p` is an Eulerian trail from `u` to `v` (it uses
every edge exactly once), then `w` has even degree exactly when it is not an end of an open
trail. This applies `SimpleGraph.Walk.IsEulerian.even_degree_iff`. -/
theorem eulerian_even_degree_iff {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V}
    [DecidableRel G.Adj] {u v : V} {p : G.Walk u v} (hp : p.IsEulerian) (w : V) :
    Even (G.degree w) ↔ (u ≠ v → w ≠ u ∧ w ≠ v) :=
  hp.even_degree_iff

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

For trees we use Mathlib throughout. Its proof that a tree has $n - 1$ edges pairs every vertex except a chosen root with the first edge of its unique path to the root — a different proof from our leaf-removal induction. Our own tree_two_leaves then goes the other way, deducing Lemma 5 from the edge count by adding up degrees, rather than from a longest path:

tree_card_edgesLean 4Applies a library theoremFormally verified

/-- **A tree with `n` vertices has `n − 1` edges** (stated as `|E| + 1 = |V|`). This applies
Mathlib's `SimpleGraph.IsTree.card_edgeFinset`, whose proof pairs each vertex other than a
chosen root with the first edge of its unique path to the root. -/
theorem tree_card_edges {V : Type*} [Fintype V] {G : SimpleGraph V} [Fintype G.edgeSet]
    (hG : G.IsTree) : #G.edgeFinset + 1 = Fintype.card V :=
  hG.card_edgeFinset

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

tree_unique_pathLean 4Applies a library theoremFormally verified

/-- **Trees are exactly the graphs with a unique path between any two vertices** (and at
least one vertex). This applies Mathlib's `SimpleGraph.isTree_iff_existsUnique_path`. -/
theorem tree_unique_path {V : Type*} {G : SimpleGraph V} :
    G.IsTree ↔ Nonempty V ∧ ∀ v w : V, ∃! p : G.Walk v w, p.IsPath :=
  SimpleGraph.isTree_iff_existsUnique_path

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

tree_two_leavesLean 4Proved here from basic factsFormally verified

/-- **Every finite tree with at least two vertices has at least two leaves** (vertices of
degree `1`). Degree counting: the degrees add up to `2|E| = 2(n − 1)`; every degree is at least
`1` because the tree is connected; if at most one vertex had degree `1`, the others would have
degree at least `2` and the sum would be at least `2n − 1`. -/
theorem tree_two_leaves {V : Type*} [Fintype V] [DecidableEq V] [Nontrivial V]
    {G : SimpleGraph V} [DecidableRel G.Adj] (hG : G.IsTree) :
    2 ≤ #{v | G.degree v = 1} := by
  have hsum := G.sum_degrees_eq_twice_card_edges
  have hedges := hG.card_edgeFinset
  have hpos : ∀ v, 1 ≤ G.degree v := fun v => hG.connected.preconnected.degree_pos_of_nontrivial v
  -- the leaves contribute their number to the degree sum …
  have hleaves : ∑ v ∈ univ.filter (fun v => G.degree v = 1), G.degree v =
      #(univ.filter fun v => G.degree v = 1) := by
    rw [card_eq_sum_ones]
    exact sum_congr rfl fun v hv => (mem_filter.1 hv).2
  -- … and every other vertex has degree at least 2
  have hrest : 2 * #(univ.filter fun v => ¬ G.degree v = 1) ≤
      ∑ v ∈ univ.filter (fun v => ¬ G.degree v = 1), G.degree v := by
    rw [mul_comm, ← smul_eq_mul, ← sum_const]
    refine sum_le_sum fun v hv => ?_
    have := hpos v
    have := (mem_filter.1 hv).2
    omega
  have hsplit := sum_filter_add_sum_filter_not univ (fun v => G.degree v = 1) (fun v => G.degree v)
  have hcard := card_filter_add_card_filter_not (s := univ) (fun v => G.degree v = 1)
  rw [card_univ] at hcard
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

Finally, isomorphism (G ≃g H in Mathlib) preserves degrees, which proves that the path and the star are different:

iso_degreeLean 4Applies a library theoremFormally verified

/-- **An isomorphism preserves degrees:** if `f : G ≃g H` then `v` and `f v` have the same
degree. This applies Mathlib's `SimpleGraph.Iso.degree_eq`. -/
theorem iso_degree {V W : Type*} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W]
    {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (f : G ≃g H) (v : V) : H.degree (f v) = G.degree v :=
  f.degree_eq v

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

path_not_iso_starLean 4Proved here from basic factsFormally verified

/-- **Same counts, different graphs.** The path `0 — 1 — 2 — 3` and the star with centre `0`
both have four vertices and three edges, and both are trees. They are not isomorphic: the star's
centre has degree `3`, an isomorphism would send it to a vertex of degree `3` in the path, and
every vertex of the path has degree at most `2`. -/
theorem path_not_iso_star :
    IsEmpty (SimpleGraph.pathGraph 4 ≃g SimpleGraph.starGraph (0 : Fin 4)) := by
  constructor
  intro f
  have hstar : (SimpleGraph.starGraph (0 : Fin 4)).degree 0 = 3 := by decide
  have hpath : ∀ v, (SimpleGraph.pathGraph 4).degree v ≤ 2 := by decide
  have h := iso_degree f (f.symm 0)
  rw [f.apply_symm_apply, hstar] at h
  have := hpath (f.symm 0)
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphBasics.leanTry it in the Lean web editor

ComputationC

Every small graph, checked

Euler trails on every graph with five verticesPythonExhaustive finite checkExact computationComputationally tested

"""Euler trails: an exhaustive check of Euler's theorem on small graphs.

For every one of the 2^10 = 1024 simple graphs on five labelled vertices,
a search through all possible trails decides whether the graph has an Euler
circuit (a closed walk using every edge exactly once) or an Euler trail, and
the answer is compared with Euler's degree condition. The search knows
nothing about degrees, so the agreement is genuine evidence. Then the
Konigsberg multigraph is searched (no trail exists), the handshake lemma is
checked, and Hierholzer's algorithm - the constructive half of the lesson's
proof - builds an Euler circuit of the complete graph K5.
"""

import itertools
from functools import lru_cache

KONIGSBERG = [(0, 1), (0, 1), (0, 2), (0, 2), (0, 3), (1, 3), (2, 3)]

def degrees(n, edges):
    """Degree of each vertex 0..n-1: the number of edge-ends there."""
    deg = [0] * n
    for a, b in edges:
        deg[a] += 1
        deg[b] += 1
    return deg

def is_connected(n, edges):
    """True if all n vertices lie in one piece (n >= 1)."""
    seen, stack = {0}, [0]
    while stack:
        v = stack.pop()
        for a, b in edges:
            for x, y in ((a, b), (b, a)):
                if x == v and y not in seen:
                    seen.add(y)
                    stack.append(y)
    return len(seen) == n

def euler_trail_exists(n, edges, closed):
    """Search every trail; True if one uses each edge exactly once."""
    m = len(edges)
    full = (1 << m) - 1

    @lru_cache(maxsize=None)
    def finish(v, used, start):
        if used == full:
            return not closed or v == start
        for i, (a, b) in enumerate(edges):
            if not used >> i & 1 and v in (a, b):
                if finish(b if v == a else a, used | 1 << i, start):
                    return True
        return False

    return any(finish(v, 0, v) for v in range(n))

def hierholzer(n, edges, start=0):
    """An Euler circuit (as a vertex list) of a connected all-even graph."""
    unused = list(range(len(edges)))
    stack, circuit = [start], []
    while stack:
        v = stack[-1]
        nxt = next((i for i in unused if v in edges[i]), None)
        if nxt is None:
            circuit.append(stack.pop())
        else:
            unused.remove(nxt)
            a, b = edges[nxt]
            stack.append(b if v == a else a)
    return circuit[::-1]

def check_all_graphs(n):
    """Count connected graphs on n vertices and disagreements with Euler."""
    pairs = list(itertools.combinations(range(n), 2))
    connected = disagreements = 0
    for mask in range(1 << len(pairs)):
        edges = [p for i, p in enumerate(pairs) if mask >> i & 1]
        if not is_connected(n, edges):
            continue
        connected += 1
        odd = sum(d % 2 for d in degrees(n, edges))
        if euler_trail_exists(n, edges, True) != (odd == 0):
            disagreements += 1
        if euler_trail_exists(n, edges, False) != (odd in (0, 2)):
            disagreements += 1
    return connected, disagreements

def main():
    connected, bad = check_all_graphs(5)
    print("All 1024 simple graphs on 5 labelled vertices:")
    print(f"  connected graphs: {connected}")
    print(f"  disagreements with Euler's criterion: {bad}")
    print()
    deg = degrees(4, KONIGSBERG)
    print(f"Konigsberg: degrees {deg}, sum {sum(deg)} = 2 x 7 bridges")
    print(f"  Euler trail exists: {euler_trail_exists(4, KONIGSBERG, False)}")
    k5 = list(itertools.combinations(range(5), 2))
    circuit = hierholzer(5, k5)
    print(f"K5: degrees {degrees(5, k5)}; Hierholzer's Euler circuit:")
    print("  " + " - ".join(str(v) for v in circuit))
    used = {frozenset(e) for e in zip(circuit, circuit[1:])}
    print(f"  {len(circuit) - 1} steps, {len(used)} different edges, "
          f"back at {circuit[-1]}")
    print()
    print("Epistemic status: exhaustive search over every graph with five")
    print("labelled vertices, so the criterion is verified there and only")
    print("there. The lesson proves Euler's theorem for all finite graphs;")
    print("Lean checks the necessity half.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Counting trees and sorting graphs by isomorphismPythonExhaustive finite checkExact computationComputationally tested

"""Trees and isomorphism, by exhaustive search on small vertex sets.

Every set of n - 1 edges on the vertices 0..n-1 (n <= 7) is examined: it is
connected exactly when it has no cycle, exactly when it is a tree - the
"two out of three" property proved in the lesson - and the labelled trees
number n^(n-2), as Cayley's formula predicts. The trees are then sorted into
isomorphism classes with a canonical code (Aho-Hopcroft-Ullman: root the tree
at its centre and encode it recursively). Finally an isomorphism between a
pentagon and a pentagram is found by trying all 120 bijections, and two
graphs with the same degrees are told apart by connectedness.
"""

import itertools

def components(n, edges):
    """Number of connected pieces, by merging endpoints (union-find)."""
    parent = list(range(n))

    def root(v):
        while parent[v] != v:
            v = parent[v]
        return v

    for a, b in edges:
        parent[root(a)] = root(b)
    return len({root(v) for v in range(n)})

def has_cycle(n, edges):
    """True if some edge joins two vertices already joined by a path."""
    parent = list(range(n))

    def root(v):
        while parent[v] != v:
            v = parent[v]
        return v

    for a, b in edges:
        ra, rb = root(a), root(b)
        if ra == rb:
            return True
        parent[ra] = rb
    return False

def tree_census(n):
    """(edge sets of size n-1, connected ones, acyclic ones), all trees."""
    pairs = list(itertools.combinations(range(n), 2))
    total = conn = acyc = 0
    trees = []
    for edges in itertools.combinations(pairs, n - 1):
        total += 1
        c, a = components(n, edges) == 1, not has_cycle(n, edges)
        conn, acyc = conn + c, acyc + a
        if c:
            trees.append(edges)
    return total, conn, acyc, trees

def canonical_tree(n, edges):
    """A code equal for two trees exactly when they are isomorphic (AHU)."""
    nbrs = {v: set() for v in range(n)}
    for a, b in edges:
        nbrs[a].add(b)
        nbrs[b].add(a)
    layer, left = [v for v in nbrs if len(nbrs[v]) <= 1], set(nbrs)
    while len(left) > 2:  # strip leaves until the centre (1 or 2 vertices)
        left -= set(layer)
        layer = [v for v in left if len(nbrs[v] & left) <= 1]

    def code(v, parent):
        return "(" + "".join(sorted(code(w, v) for w in nbrs[v]
                                    if w != parent)) + ")"

    return min(code(c, None) for c in left)

def find_isomorphism(n, edges1, edges2):
    """A bijection of 0..n-1 carrying edges1 onto edges2, or None."""
    target = {frozenset(e) for e in edges2}
    for perm in itertools.permutations(range(n)):
        if {frozenset((perm[a], perm[b])) for a, b in edges1} == target:
            return perm
    return None

def main():
    print(" n  edge sets  connected  acyclic  trees  n^(n-2)  classes")
    for n in range(2, 8):
        total, conn, acyc, trees = tree_census(n)
        classes = len({canonical_tree(n, t) for t in trees})
        print(f"{n:2d}  {total:9d}  {conn:9d}  {acyc:7d}  {len(trees):5d}"
              f"  {n ** (n - 2):7d}  {classes:7d}")
    print("(n = 1: one tree, one class.)")
    print()
    pentagon = [(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]
    pentagram = [(0, 2), (2, 4), (4, 1), (1, 3), (3, 0)]
    print(f"Pentagon -> pentagram isomorphism: "
          f"{find_isomorphism(5, pentagon, pentagram)}")
    hexagon = [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 0)]
    triangles = [(0, 1), (1, 2), (2, 0), (3, 4), (4, 5), (5, 3)]
    print("Hexagon vs two triangles: all six degrees 2 in both;")
    print(f"  pieces {components(6, hexagon)} vs "
          f"{components(6, triangles)}; isomorphism: "
          f"{find_isomorphism(6, hexagon, triangles)}")
    print()
    print("Epistemic status: exhaustive search over all edge sets for n <= 7")
    print("(evidence for the tree theorems and Cayley's formula, which hold")
    print("for every n) and over all bijections for the two examples (a")
    print("complete check, so those isomorphism verdicts are certain).")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Two things in this table are worth a second look. First, the "connected" and "acyclic" columns agree exactly, as the "two out of three" property predicts. Second, the numbers of labelled trees are $1, 3, 16, 125, 1296, 16807$ — that is $n^{n-2}$ . This is Cayley's formula, a theorem (stated by Arthur Cayley in 1889, and proved in many ways since, for example with Prüfer sequences); the program only checks it for $n \le 7$ . The last column counts trees up to isomorphism: there are just $3$ different shapes of tree on $5$ vertices — the path, the star, and a "T" shape.

Explore

Explore: walks, trees and drawings

Can you cross every bridge exactly once?

Dots joined by lines: count degrees, walk along edges, colour vertices, grow spanning trees and count walks with a matrix.

|V| = 4|E| = 7Click edges one after another to walk along them, or pick a starting vertex first.

No walk yet.

4 vertices have odd degree: A, B, C, D.

So no Euler trail is possible. A trail enters and leaves each vertex in its middle in pairs, so only its two ends can have odd degree, and this graph has 4 such vertices.

Try to build an Euler trail by clicking bridges one after another. The widget tells you when you are stuck — and the Degrees tab shows why you always will be.

Spanning trees of the cube

Dots joined by lines: count degrees, walk along edges, colour vertices, grow spanning trees and count walks with a matrix.

|V| = 8|E| = 12Click edges to choose them for a spanning tree.

Edges chosen: 0. A spanning tree on 8 vertices has exactly 7 edges (|V| − 1).

No cycle ✓
Reaches every vertex ✗The chosen edges leave 8 separate pieces.
A spanning tree ✗

Altogether this graph has 384 different spanning trees (counted exactly by Kirchhoff's matrix-tree theorem).

Build a spanning tree of the cube: a tree that uses all $8$ vertices. However you do it, you will use exactly $7$ edges. The widget also counts how many spanning trees there are in all (Kirchhoff's matrix-tree theorem). On the Walk tab, look for a Hamiltonian cycle — and convince yourself there is no Euler trail.

A pentagon

Dots joined by lines: count degrees, walk along edges, colour vertices, grow spanning trees and count walks with a matrix.

|V| = 5|E| = 5Select a vertex to see the edges that meet there.

deg(0) = 2deg(1) = 2deg(2) = 2deg(3) = 2deg(4) = 2

2 + 2 + 2 + 2 + 2 = 10 = 2 × 5

Every edge has two ends, so it adds exactly 2 to the total: the degrees add up to 10 = 2 × 5. This is the handshake lemma, Σ deg(v) = 2|E|.

Vertices of odd degree: 0. This number is always even, because the total is even.

A pentagram

Dots joined by lines: count degrees, walk along edges, colour vertices, grow spanning trees and count walks with a matrix.

|V| = 5|E| = 5Select a vertex to see the edges that meet there.

deg(0) = 2deg(1) = 2deg(2) = 2deg(3) = 2deg(4) = 2

2 + 2 + 2 + 2 + 2 = 10 = 2 × 5

Every edge has two ends, so it adds exactly 2 to the total: the degrees add up to 10 = 2 × 5. This is the handshake lemma, Σ deg(v) = 2|E|.

Vertices of odd degree: 0. This number is always even, because the total is even.

The pentagon and the pentagram are the same graph drawn differently. Relabel the pentagram's vertices by $0 \mapsto 0$ , $2 \mapsto 1$ , $4 \mapsto 2$ , $1 \mapsto 3$ , $3 \mapsto 4$ (the inverse of the isomorphism in the examples) and its edges become exactly the pentagon's.

Exercises

1. Graphs

Warm-upHuman

A graph has seven vertices, with degrees $3, 3, 2, 2, 2, 1, 1$ . How many edges does it have?

2. Graphs

Warm-upHuman

Can there be a group of $7$ people in which every person knows exactly $3$ of the others (knowing being mutual)?

Choose one

No: the numbers of acquaintances would add up to

7 \times 3 = 21

, which is odd, but they must add up to twice the number of pairs who know each other.Yes: arrange the

7

people in a circle and let each know their neighbours and the person opposite.No, because

3

is more than half of

7

.Yes, but only if one person knows nobody.

3. Graphs

CoreHuman

An engineering cooperative lays water pipes to connect $50$ villages in a region of Bolivia so that water can flow between any two villages, using as few pipes as possible: the network has no loops. Each pipe joins two villages. How many pipes are there?

4. Graphs

CoreHuman

A connected graph has six vertices with degrees $2, 4, 3, 3, 4, 2$ . Which statement is true?

Choose one

It has an Euler trail that starts at one vertex of degree

3

and ends at the other, but no Euler circuit.It has an Euler circuit.It has no Euler trail at all.Such a graph cannot exist, because the degrees add up to an odd number.

5. Graphs

CoreHuman

The cube graph has the $8$ corners of a cube as vertices and its $12$ edges as edges. Which statements are true? (Choose all that apply.)

Choose all that apply

It has a Hamiltonian cycle (a cycle visiting every vertex exactly once).It has an Euler circuit.It has no Euler trail.It has

\frac{8 \times 3}{2} = 12

edges, consistent with the handshake lemma.

6. Graphs

CoreHuman

To prove that a tree with at least two vertices has a leaf, we take a longest path $v_0, v_1, \dots, v_k$ and show that $v_k$ is a leaf. Why can $v_k$ have no neighbour other than $v_{k-1}$ ?

Choose one

A neighbour outside the path would give a longer path, and a neighbour

v_i

with

i < k - 1

would close a cycle.Because a tree with

n

vertices has

n - 1

edges.Because the degrees add up to twice the number of edges.Because

v_k

was chosen to have the smallest degree.

7. Graphs

StretchHuman

How many trees with $5$ vertices are there up to isomorphism — that is, how many different shapes?

8. Graphs

StretchFormal

In the lesson's Lean model, IsEulerCircuit G w says that the walk w crosses every edge of the multigraph G exactly once and ends where it started. Which statement is a correct formalisation of the necessity half of Euler's theorem for circuits?

Choose one

IsEulerCircuit G w → ∀ v, Even (degree G v)(∀ v, Even (degree G v)) → ∃ w, IsEulerCircuit G wIsEulerCircuit G w → ∃ v, Even (degree G v)IsEulerCircuit G w → ∀ v, Odd (degree G v)

9. Graphs

StretchComputational

A connected multigraph on the vertices $0, 1, \dots, n - 1$ is given as a list of edges (a, b) (pairs may repeat). Write euler_status(n, edges) that returns "circuit" if it has an Euler circuit, "trail" if it has an Euler trail but no circuit, and "none" otherwise, using Euler's theorem. (Assume at least one edge.)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"The drawing is the graph." A graph records only which pairs of vertices are joined. Very different drawings — a pentagon and a pentagram, a tangle and a neat diagram — can show the same graph, and a single graph has infinitely many drawings.

Misconception

Confusing Euler circuits with Hamiltonian cycles. An Euler circuit uses every edge exactly once (vertices may be revisited); a Hamiltonian cycle visits every vertex exactly once (most edges are not used). The cube has a Hamiltonian cycle but no Euler circuit; a "bow tie" — two triangles sharing a vertex — has an Euler circuit but no Hamiltonian cycle.

Misconception

"Same degree sequence means isomorphic." The hexagon and two triangles have identical degrees and are not isomorphic. Invariants can prove that graphs are different; to prove they are the same, you need an isomorphism.

Misconception

"A tree is any graph without cycles." It must also be connected. A graph without cycles is a forest: a collection of trees.

Misconception

"Even degrees guarantee an Euler circuit." Only for a connected graph (apart from isolated vertices). Two separate triangles have all degrees even, but no single walk can use the edges of both.

ViewpointsH

Other ways of seeing

Topology— Where topology began

Euler's solution ignores lengths and angles and keeps only connections — exactly the attitude of topology, and Königsberg is often called its first theorem. A graph can be viewed as a space built from points and segments, and some of its numbers are topological invariants: for a connected graph, $|E| - |V| + 1$ counts its independent cycles (for a tree it is $0$ , which is Theorem 6 again). For a connected graph drawn in the plane without crossings, Euler's later formula $V - E + F = 2$ relates vertices, edges and faces; see surfaces and the Euler characteristic and graph theory.

Algebra— Graphs as matrices

Number the vertices $1, \dots, n$ and let $A$ be the adjacency matrix: $A_{ij} = 1$ if $i$ and $j$ are adjacent, $0$ otherwise. The row sums of $A$ are the degrees, and the entry $(A^k)_{ij}$ counts the walks of length $k$ from $i$ to $j$ — try the Matrix tab above. Two graphs are isomorphic exactly when one adjacency matrix can be turned into the other by renumbering the vertices, that is $A' = P A P^{\mathsf{T}}$ for a permutation matrix $P$ . Similar matrices have the same eigenvalues, so the eigenvalues of $A$ are an isomorphism invariant (though, like degrees, not a complete one); see linear algebra.

Computation— Easy and hard questions

Euler's criterion turns "is there an Euler circuit?" into degree-counting, which a computer does in time proportional to the size of the graph, and Hierholzer's algorithm finds the circuit just as fast. For Hamiltonian cycles no efficient method is known: the problem is NP-complete, so an efficient algorithm for it would settle the famous P versus NP question; see complexity theory. Graph isomorphism sits in between: in 2015 László Babai announced an algorithm running in quasi-polynomial time, but whether isomorphism can be decided in polynomial time remains open.

Category theory— Maps between graphs

A graph homomorphism $f : G \to H$ sends vertices to vertices so that adjacent vertices go to adjacent vertices. Graphs and homomorphisms form a category, and an isomorphism is exactly a homomorphism with an inverse homomorphism — the general pattern of structure-preserving maps. Colourings fit too: a colouring of $G$ with $k$ colours is a homomorphism from $G$ to $K_k$ .

Set-theoretic connectionH

Set-theoretic connection

A simple graph is pure set theory: a set $V$ together with a set $E$ of two-element subsets of $V$ . Equivalently, adjacency is a relation on $V$ that is symmetric ( $u \sim v$ implies $v \sim u$ ) and irreflexive (no $v \sim v$ ). An isomorphism is a bijection that carries this relation onto the other graph's relation, and a property is an invariant exactly when it can be stated using only $V$ and the relation.

History & global context

History and global context

Euler (1736). Leonhard Euler's paper on the Königsberg bridges (published in 1741) stated the degree conditions and showed why they are necessary. He asserted, but did not prove, that they are also sufficient; the first published proof is Carl Hierholzer's, from 1873, which appeared after his death.
Drawing in one stroke. Among the Chokwe people of north-eastern Angola and neighbouring regions, storytellers trace sona — figures drawn in the sand around a grid of dots, many of them in a single continuous line that returns to its start. The mathematician Paulus Gerdes studied their geometry, including their connection with Euler circuits. Some kolam designs drawn at thresholds in Tamil Nadu, in southern India, are likewise single closed lines looping around a grid of dots.
Trees. Gustav Kirchhoff used trees to analyse electrical networks (1847), and Arthur Cayley counted trees in connection with chemical molecules (1857 and later); J. J. Sylvester introduced the word graph in 1878, from chemical diagrams. Dénes Kőnig wrote the first textbook on graph theory in 1936.
Routes. In 1960 the Chinese mathematician Guan Meigu (Kwan Mei-Ko) asked for the shortest closed walk covering every street of a town at least once — the "Chinese postman problem", solved with Euler's theorem when every degree is even.

Seven bridges, one walk

Forgetting everything except connections

Definitions

Examples and non-examples

Theorems and proofs

Degrees

Euler trails and circuits

Trees

Isomorphism

Graphs in Lean

Every small graph, checked

Explore: walks, trees and drawings

Exercises

Common misconceptions

Other ways of seeing

Set-theoretic connection

History and global context

Further reading