brualdi-ch11-5

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch11-5

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

goals/brualdi-ch11-5.lean

import Mathlib

theorem brualdi_ch11_5 (n : ℕ) (h_n: n ≥ 2) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    ∃ v1 v2, v1 ≠ v2 ∧ G.degree v1 = G.degree v2 := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.