Erdős problem 599 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

599.lean

Retained formal statement1 of 3

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].

FormalConjectures/ErdosProblems/599.leanErdos599.erdos_59913 linesExact file

1True ↔2  ∀ (V : Type) (G : SimpleGraph V) (A B : Set V),3    Disjoint A B →4      G.IsIndepSet A →5        G.IsIndepSet B →6          ∃ ι a b p S,7            (∀ (i : ι), a i ∈ A) ∧8              (∀ (i : ι), b i ∈ B) ∧9                (∀ (i : ι), (p i).IsPath) ∧10                  (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧11                    S ⊆ {v | ∃ i, v ∈ (p i).support} ∧12                      (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧13                        ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

SolvedStatement only, no proof

Sources

Search problems.science