FormalConjectures/ErdosProblems/599.lean

GitHub source file

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

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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 599

References:

Imports (1)
  1. theorem Erdos599.erdos_599 Erdős Problem 599 (the Erdős–Menger conjecture) sorry line 47 source

    Source documentation

    Erdős Problem 599 (the Erdős–Menger conjecture).

    Let $G$ be a (possibly infinite) graph and let $A, B$ be disjoint independent sets of vertices. Must there exist a family $P$ of pairwise vertex-disjoint paths from $A$ to $B$, and a set $S$ of vertices containing exactly one vertex from each path in $P$, such that every path from $A$ to $B$ contains at least one vertex of $S$?

    For finite $G$ this is equivalent to Menger's theorem. The answer is yes, proved by Aharoni and Berger [AhBe09].

    depends on sorry what this means

    Statement uses: Iff, True, SimpleGraph, Set, Disjoint, SimpleGraph.IsIndepSet, Exists, SimpleGraph.Walk, And, Membership.mem, SimpleGraph.Walk.IsPath, Pairwise, Set.ofPred, List, SimpleGraph.Walk.support, LE.le, ExistsUnique

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_599 : answer(True) ↔
    ∀ (V : Type) (G : SimpleGraph V) (A B : Set V),
      Disjoint A B → G.IsIndepSet A → G.IsIndepSet B →
      ∃ (ι : Type) (a b : ι → V) (p : ∀ i, G.Walk (a i) (b i)) (S : Set V),
        (∀ i, a i ∈ A) ∧ (∀ i, b i ∈ B) ∧ (∀ i, (p i).IsPath) ∧
        (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧
        S ⊆ {v | ∃ i, v ∈ (p i).support} ∧
        (∀ i, ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧
        (∀ a' ∈ A, ∀ b' ∈ B, ∀ q : G.Walk a' b', q.IsPath → ∃ v ∈ q.support, v ∈ S) := by
…
  2. theorem Erdos599.erdos_599.variants.aharoni_berger Menger's theorem for infinite graphs (Aharoni–Berger [AhBe09]) sorry line 68 source

    Source documentation

    Menger's theorem for infinite graphs (Aharoni–Berger [AhBe09]).

    The theorem actually proved by Aharoni and Berger holds for arbitrary vertex sets $A$ and $B$: in any (possibly infinite) graph $G$ there is a family $P$ of pairwise vertex-disjoint $A$--$B$ paths together with an $A$--$B$ separator $S$ consisting of the choice of exactly one vertex from each path in $P$. The disjointness and independence hypotheses of erdos_599 are not needed.

    depends on sorry what this means

    Statement uses: SimpleGraph, Set, Exists, SimpleGraph.Walk, And, Membership.mem, SimpleGraph.Walk.IsPath, Pairwise, Disjoint, Set.ofPred, List, SimpleGraph.Walk.support, LE.le, ExistsUnique

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_599.variants.aharoni_berger :
    ∀ (V : Type) (G : SimpleGraph V) (A B : Set V),
      ∃ (ι : Type) (a b : ι → V) (p : ∀ i, G.Walk (a i) (b i)) (S : Set V),
        (∀ i, a i ∈ A) ∧ (∀ i, b i ∈ B) ∧ (∀ i, (p i).IsPath) ∧
        (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧
        S ⊆ {v | ∃ i, v ∈ (p i).support} ∧
        (∀ i, ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧
        (∀ a' ∈ A, ∀ b' ∈ B, ∀ q : G.Walk a' b', q.IsPath → ∃ v ∈ q.support, v ∈ S) := by
…
  3. theorem Erdos599.erdos_599.test.empty_A Documented declaration: empty_A line 84 source

    Source documentation

    Sanity check: when $A = \varnothing$ the conclusion of erdos_599 holds trivially, with the empty family of paths and $S = \varnothing$ (the covering condition is vacuous since there is no path starting in $\varnothing$).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, Set, Exists, SimpleGraph.Walk, And, Membership.mem, EmptyCollection.emptyCollection, SimpleGraph.Walk.IsPath, Pairwise, Disjoint, Set.ofPred, List, SimpleGraph.Walk.support, LE.le, ExistsUnique

    Proof uses: Exists.intro, Empty, Empty.elim, And.intro, Ne, False.elim, absurd, Set.notMem_empty

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_599.test.empty_A (V : Type) (G : SimpleGraph V) (B : Set V) :
    ∃ (ι : Type) (a b : ι → V) (p : ∀ i, G.Walk (a i) (b i)) (S : Set V),
      (∀ i, a i ∈ (∅ : Set V)) ∧ (∀ i, b i ∈ B) ∧ (∀ i, (p i).IsPath) ∧
      (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧
      S ⊆ {v | ∃ i, v ∈ (p i).support} ∧
      (∀ i, ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧
      (∀ a' ∈ (∅ : Set V), ∀ b' ∈ B, ∀ q : G.Walk a' b', q.IsPath →
        ∃ v ∈ q.support, v ∈ S) := by
…