Strong matchings and covers in hypergraphs

DefinitionMatching in a hypergraph#✓fully proved

For a hypergraph on a vertex set \(V\) whose edges form a set \(E\) of finite subsets of \(V\), a set \(M\) is a matching when \(M \subseteq E\) and any two distinct members of \(M\) are disjoint.

def IsMatching {V : Type} (E M : Set (Finset V)) : Prop :=
  M ⊆ E ∧ M.Pairwise Disjoint

Used by 1

Used byStrongly maximal matching

DefinitionStrongly maximal matching#✓fully proved

For a hypergraph with edge set \(E\), a set \(M\) is a strongly maximal matching (Aharoni) when \(M\) is a matching of \(E\) and every matching \(M'\) of \(E\) satisfies \(|M' \setminus M| \le |M \setminus M'|\), comparing the cardinalities as cardinal numbers.

def IsStronglyMaximal {V : Type} (E M : Set (Finset V)) : Prop :=
  IsMatching E M ∧ ∀ M', IsMatching E M' → Cardinal.mk ↥(M' \ M) ≤ Cardinal.mk ↥(M \ M')

Uses 1 · Used by 1

Statement usesMatching in a hypergraph

Used byStrongly maximal matchings in hypergraphs with bounded edges

DefinitionStrongly maximal matchings in hypergraphs with bounded edges#✓fully proved

The statement that for every vertex set \(V\) and every set \(E\) of finite subsets of \(V\) such that some natural number \(k\) bounds the number of elements of every edge in \(E\), the hypergraph with edge set \(E\) has a strongly maximal matching.

This is the claim from the EGRES list of open problems; it has since been refuted.

def boundedEdgesStronglyMaximalMatching : Prop :=
  ∀ (V : Type) (E : Set (Finset V)) (k : ℕ), (∀ e ∈ E, e.card ≤ k) →
    ∃ M, IsStronglyMaximal E M

def IsStronglyMaximal {V : Type} (E M : Set (Finset V)) : Prop :=
  IsMatching E M ∧ ∀ M', IsMatching E M' → Cardinal.mk ↥(M' \ M) ≤ Cardinal.mk ↥(M \ M')

WantedExt/Combinatorics/StronglyMaximalMatchingAMR29Problem0084Wanted.lean:43

Uses 1 · Used by 1

Statement usesStrongly maximal matching

Used byBounded edge size does not guarantee a strongly maximal matching

TheoremBounded edge size does not guarantee a strongly maximal matching#●ready to prove

There are a vertex set \(V\), a set \(E\) of finite subsets of \(V\) and a natural number \(k\) such that every edge in \(E\) has at most \(k\) elements, but the hypergraph with edge set \(E\) has no strongly maximal matching.

Hollom and Randall Shaw (Theorem 1.2) construct a \(3\)-uniform (infinite) hypergraph with no strongly maximal matching, so bounded edge size does not suffice.

public theorem_wanted boundedEdgesStronglyMaximalMatching_refuted :
    ¬ boundedEdgesStronglyMaximalMatching

def boundedEdgesStronglyMaximalMatching : Prop :=
  ∀ (V : Type) (E : Set (Finset V)) (k : ℕ), (∀ e ∈ E, e.card ≤ k) →
    ∃ M, IsStronglyMaximal E M

WantedExt/Combinatorics/StronglyMaximalMatchingAMR29Problem0084Wanted.lean:48

Sources

EGRES Open (Egerváry Research Group), list of open problems, Strongly maximal matchings, https://oldlemon.cs.elte.hu/egres/open/Strongly_maximal_matchings; resolution: L. Hollom and B. Randall Shaw, Counterexamples to conjectures on strong maximality and minimality, Electron. J. Combin. 33(2) (2026), P2.11; arXiv:2511.13709, Theorem 1.2: there is a 3-uniform hypergraph H₁ with no strongly maximal matching (refuting Conjecture 1.1 for matchings and Aharoni's question), https://doi.org/10.37236/14948.

Uses 1

Statement usesStrongly maximal matchings in hypergraphs with bounded edges

DefinitionVertex cover of a hypergraph#✓fully proved

Let \(E\) be a set of finite subsets of a type \(V\), the edges of a hypergraph. A set \(X \subseteq V\) is a (vertex) cover of \(E\) if it meets every edge: every \(e \in E\) contains some \(v \in X\).

def IsVertexCover {V : Type} (E : Set (Finset V)) (X : Set V) : Prop :=
  ∀ e ∈ E, ∃ v ∈ e, v ∈ X

Used by 1

Used byStrongly minimal cover

DefinitionStrongly minimal cover#✓fully proved

Let \(E\) be a set of finite subsets of a type \(V\), the edges of a hypergraph. A set \(X \subseteq V\) is a strongly minimal cover of \(E\) (Aharoni) if \(X\) is a cover of \(E\), that is, it meets every edge in \(E\), and \(|X \setminus X'| \le |X' \setminus X|\), as cardinals, for every cover \(X'\) of \(E\).

def IsStronglyMinimalCover {V : Type} (E : Set (Finset V)) (X : Set V) : Prop :=
  IsVertexCover E X ∧ ∀ X', IsVertexCover E X' → Cardinal.mk ↥(X \ X') ≤ Cardinal.mk ↥(X' \ X)

Uses 1 · Used by 1

Statement usesVertex cover of a hypergraph

Used byAharoni's strongly minimal cover conjecture

DefinitionAharoni's strongly minimal cover conjecture#✓fully proved

The statement that for every type \(V\), every set \(E\) of finite subsets of \(V\) (the edges of a hypergraph, possibly infinitely many) and every natural number \(k\) such that each edge in \(E\) is nonempty and has at most \(k\) elements, the hypergraph with edge set \(E\) has a strongly minimal cover.

def boundedEdgesStronglyMinimalCover : Prop :=
  ∀ (V : Type) (E : Set (Finset V)) (k : ℕ), (∀ e ∈ E, e.Nonempty ∧ e.card ≤ k) →
    ∃ X, IsStronglyMinimalCover E X

def IsStronglyMinimalCover {V : Type} (E : Set (Finset V)) (X : Set V) : Prop :=
  IsVertexCover E X ∧ ∀ X', IsVertexCover E X' → Cardinal.mk ↥(X \ X') ≤ Cardinal.mk ↥(X' \ X)

WantedExt/Combinatorics/StronglyMinimalCoverOpenGardenProblem690Wanted.lean:49

Uses 1 · Used by 1

Statement usesStrongly minimal cover

Used byAharoni's strongly minimal cover conjecture is false

TheoremAharoni's strongly minimal cover conjecture is false#●ready to prove

There are a type \(V\), a set \(E\) of finite subsets of \(V\) (the edges of a hypergraph) and a natural number \(k\) such that every edge in \(E\) is nonempty and has at most \(k\) elements, but no strongly minimal cover of \(E\) exists. Here a cover of \(E\) is a set \(X \subseteq V\) that meets every edge in \(E\), and a cover \(X\) is strongly minimal if \(|X \setminus X'| \le |X' \setminus X|\), as cardinals, for every cover \(X'\) of \(E\).

Hollom and Randall Shaw (Section 3.4) show that the graph on \(\mathbb{N}\) whose edges are the pairs \(\{u, v\}\) with \(2u \le v\) has no strongly minimal vertex cover, so already hypergraphs with all edges of size \(2\) need not have a strongly minimal cover.

public theorem_wanted boundedEdgesStronglyMinimalCover_refuted : ¬ boundedEdgesStronglyMinimalCover

def boundedEdgesStronglyMinimalCover : Prop :=
  ∀ (V : Type) (E : Set (Finset V)) (k : ℕ), (∀ e ∈ E, e.Nonempty ∧ e.card ≤ k) →
    ∃ X, IsStronglyMinimalCover E X

WantedExt/Combinatorics/StronglyMinimalCoverOpenGardenProblem690Wanted.lean:54

Sources

Open Problem Garden, Strong matchings and covers (node 690; R. Aharoni), http://www.openproblemgarden.org/op/strong_matchings_and_covers; resolution: L. Hollom and B. Randall Shaw, Counterexamples to conjectures on strong maximality and minimality, Electron. J. Combin. 33(2) (2026), #P2.11, doi:10.37236/14948; arXiv:2511.13709, Section 3.4 (Strongly minimal vertex-covers): the graph G on N with edges {u, v} such that 2u ≤ v has no strongly minimal vertex-cover; the introduction defines strongly minimal vertex-covers by |C \ C'| ≤ |C' \ C| for every vertex-cover C', https://doi.org/10.37236/14948.

Uses 1

Statement usesAharoni's strongly minimal cover conjecture

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.