The Lovász–Plummer conjecture (proved 2011) and Sheehan's conjecture

Theorem · lovasz_plummer_conjecture

**The Lovász–Plummer conjecture (1970s), proved by Esperet, Kardoš, King, Král' and Norine (2011).**

Every bridgeless cubic graph on $n$ vertices has exponentially many perfect matchings: there is a constant $c > 0$ such that the number of perfect matchings is at least $2^{cn}$ . [EKKKN11] prove this with $2^{n/3656}$ .

Formal statement · Lean 4.lean

theorem lovasz_plummer_conjecture :
    ∃ c : ℝ, 0 < c ∧ ∀ {V : Type} [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj],
      (∀ v, G.degree v = 3) → G.IsBridgeless →
      (2 : ℝ) ^ (c * Fintype.card V) ≤ perfectMatchingCount G := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗