brualdi-ch11-59

open

difficulty 4

credited

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

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-59.lean

import Mathlib

open SimpleGraph

theorem brualdi_ch11_59 {V : Type*} [Fintype V] [DecidableEq V]
    (T : SimpleGraph V) (hT : IsTree T) (e : Sym2 V) (he : e ∈ T.edgeSet) :
    ∃ (T1 T2 : SimpleGraph V), IsTree T1 ∧ IsTree T2 ∧
    T1.edgeSet ∪ T2.edgeSet = T.edgeSet \ {e} ∧
    Disjoint (T1.support) (T2.support) := by
  sorry

Runs (0)

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