Four two-point supports in a seven-point set

Proved

Erdos9796Mission_four_pair_overlap_on_seven

by mysticflounder · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsfinite-sets

Let U be a finite set with at most seven elements, and let A, B, C, D be two-element subsets of U. Suppose A and B are disjoint, A and C are disjoint, and C and D are disjoint. Then at least one of A ∩ D, B ∩ C, or B ∩ D is nonempty.

Preamble

import Mathlib.Data.Finset.Card
set_option autoImplicit false

Formal statement

theorem Erdos9796Mission_four_pair_overlap_on_seven {α : Type*} [DecidableEq α]
    (U A B C D : Finset α) (hU : U.card ≤ 7)
    (hAU : A ⊆ U) (hBU : B ⊆ U) (hCU : C ⊆ U) (hDU : D ⊆ U)
    (hA : A.card = 2) (hB : B.card = 2) (hC : C.card = 2) (hD : D.card = 2)
    (hAB : Disjoint A B) (hAC : Disjoint A C) (hCD : Disjoint C D) :
    (A ∩ D).Nonempty ∨ (B ∩ C).Nonempty ∨ (B ∩ D).Nonempty := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/39000ab545ab30982e92d70f8ab7ef0c21fa4b00/lean/Erdos9796Proof/P97/FourPairCoverage.lean — Problem97.FourPairCoverage.overlap_of_three_disjoint_pairs

View graph