conjecture1

Specification

WOWII [Conjecture 1](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) For a simple connected graph `G` the maximum number of leaves of a spanning tree satisfies `Ls(G) ≥ n(G) + 1 - 2·m(G)` where `n(G)` counts vertices and `m(G)` is the size of a maximum matching.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem conjecture1 {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
    (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) :
    n G + 1 - 2 * m G ≤ Ls G

ID: WrittenOnTheWallII__GraphConjecture1__conjecture1

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.