LovaszPlummerConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 4 contain sorry, 0 declared as axioms

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

References:

Wikipedia
[LP86] Lovász, L. and Plummer, M. D. (1986). Matching Theory. North-Holland.
[EKKKN11] Esperet, L., Kardoš, F., King, A. D., Král', D. and Norine, S. (2011). "Exponentially many perfect matchings in cubic graphs." Adv. Math. 227, pp. 1646--1664. arXiv:1012.2878
[Sh77] Sheehan, J. (1977). "The multiplicity of Hamiltonian circuits in a graph." In Recent Advances in Graph Theory, Academia, Prague, pp. 477--480.
[Th98] Thomassen, C. (1998). "Independent dominating sets and a second Hamiltonian cycle in regular graphs." J. Combin. Theory Ser. B 72, pp. 104--109.

Imports (1)

FormalConjecturesUtil

def LovaszPlummerConjecture.perfectMatchingCount The number of perfect matchings of G line 44 source
Source documentation
The number of perfect matchings of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: Set.ncard, SimpleGraph.Subgraph, Set.ofPred, SimpleGraph.Subgraph.IsPerfectMatching
```
noncomputable def perfectMatchingCount (G : SimpleGraph V) : ℕ :=
…
```
theorem LovaszPlummerConjecture.lovasz_plummer_conjecture The Lovász–Plummer conjecture (1970s), proved by Esperet, Kardoš, King, Král' and Norine (2011) sorry line 56 source
Source documentation
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}$.

depends on sorry what this means
Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, SimpleGraph.IsBridgeless, LE.le, HPow.hPow, HMul.hMul and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: c, LovaszPlummerConjecture.perfectMatchingCount
theorem LovaszPlummerConjecture.lovasz_plummer_conjecture.variants.explicit The explicit bound of Esperet–Kardoš–King–Král'–Norine (2011) sorry line 71 source
Source documentation
The explicit bound of Esperet–Kardoš–King–Král'–Norine (2011).
Every bridgeless cubic graph on $n$ vertices has at least $2^{n/3656}$ perfect matchings.
Reference: [EKKKN11].

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, OfNat.ofNat, SimpleGraph.IsBridgeless, LE.le, Real, HPow.hPow, HDiv.hDiv, Fintype.card, LovaszPlummerConjecture.perfectMatchingCount
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lovasz_plummer_conjecture.variants.explicit
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hcubic : ∀ v, G.degree v = 3) (hbridgeless : G.IsBridgeless) :
    (2 : ℝ) ^ ((Fintype.card V : ℝ) / 3656) ≤ perfectMatchingCount G := by
…
```
Mentions: LovaszPlummerConjecture.perfectMatchingCount
def LovaszPlummerConjecture.IsHamiltonianCycle A Hamiltonian cycle of G: a cycle passing through every vertex line 78 source
Source documentation
A Hamiltonian cycle of G: a cycle passing through every vertex.

no axioms what this means
Statement uses: SimpleGraph, SimpleGraph.Walk
Proof uses: And, SimpleGraph.Walk.IsCycle, Membership.mem, List, SimpleGraph.Walk.support
1 instances, coercions and auxiliary constants left out.
```
def IsHamiltonianCycle (G : SimpleGraph V) {v : V} (c : G.Walk v v) : Prop :=
…
```
Mentions: c
theorem LovaszPlummerConjecture.sheehan_conjecture Sheehan's conjecture (1977) sorry line 90 source
Source documentation
Sheehan's conjecture (1977).
Every $4$-regular graph with a Hamiltonian cycle has a second Hamiltonian cycle (one with a different edge set). Sheehan's conjecture would settle the last open case of the question, raised by Smith's theorem for cubic graphs, of which regular Hamiltonian graphs have a second Hamiltonian cycle: Thomassen [Th98] proved it for all $r$-regular graphs with $r \ge 300$.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, OfNat.ofNat, SimpleGraph.Walk, LovaszPlummerConjecture.IsHamiltonianCycle, Exists, And, Ne, Finset, Sym2, List.toFinset and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem sheehan_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      (∀ v, G.degree v = 4) →
      ∀ (v : V) (c : G.Walk v v), IsHamiltonianCycle G c →
        ∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧
          c'.edges.toFinset ≠ c.edges.toFinset := by
…
```
Mentions: c, LovaszPlummerConjecture.IsHamiltonianCycle
theorem LovaszPlummerConjecture.sheehan_conjecture.variants.thomassen Thomassen (1998): regular graphs of large degree sorry line 106 source
Source documentation
Thomassen (1998): regular graphs of large degree.
Every $r$-regular Hamiltonian graph with $r \ge 300$ has a second Hamiltonian cycle.
Reference: [Th98].

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, LE.le, OfNat.ofNat, Eq, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, SimpleGraph.Walk, LovaszPlummerConjecture.IsHamiltonianCycle, Exists, And, Ne, Finset, Sym2 and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem sheehan_conjecture.variants.thomassen
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (r : ℕ) (hr : 300 ≤ r) (hreg : ∀ v, G.degree v = r)
    (v : V) (c : G.Walk v v) (hc : IsHamiltonianCycle G c) :
    ∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧
      c'.edges.toFinset ≠ c.edges.toFinset := by
…
```
Mentions: c, LovaszPlummerConjecture.IsHamiltonianCycle