Counting & logic

Königsberg: count odd vertices

Compute the parity obstruction behind the seven-bridges puzzle.

-- Top 100 #54: Königsberg: count odd vertices
-- History: 1736 · Euler.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The four land masses have degrees 3, 3, 3, and 5.
-- Scope: Checks the four odd degrees and the failure of the necessary ≤2 condition for an Euler trail. The trail criterion itself is not proved here.
-- Source: https://lurch.plus/100/

def oddVertices (degrees : List Nat) : Nat :=
  (degrees.filter fun d => d % 2 == 1).length

def konigsberg : List Nat := [3, 3, 3, 5]

example : oddVertices konigsberg = 4 := by decide
example : ¬ oddVertices konigsberg ≤ 2 := by decide

-- Each bridge is counted twice in the sum of vertex degrees.
example : konigsberg.foldl (· + ·) 0 = 2*7 := by decide

#eval oddVertices konigsberg

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

1736 · Euler

The four land masses have degrees 3, 3, 3, and 5.

Checks the four odd degrees and the failure of the necessary ≤2 condition for an Euler trail. The trail criterion itself is not proved here.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

Exercise

Change the degree list to [1,2,2,1]. This passes the parity test; connectivity still matters.