Submit proof — Erdős Problem 602

Environment

Lean 4.29.1 · Mathlib v4.29.1

Ubuntu 24.04 LTS · x86_64 · toolchain via elan

timeout 120s lake env lean Check.lean

Details

Posted 12 days ago

Language Lean 4 / Mathlib

textarea

import Mathlib

/--
Does every almost-disjoint family of countably infinite sets whose pairwise
intersections all have size ≠ 1 have Property B?

Formally: let `α` be any type, let `(A_i)_{i ∈ I}` be a family of countably infinite subsets
of `α` such that for all `i ≠ j`, the intersection `A_i ∩ A_j` is finite and
`|A_i ∩ A_j| ≠ 1`. Does there exist a 2-colouring `f : α → Fin 2` such that no `A_i` is
monochromatic?

This is an open question about Property B for almost-disjoint families with a
forbidden intersection size of 1.

**Note:** This generalises the formulation in which the ground set is `ℕ`. Since every
countably infinite set is in bijection with `ℕ`, the two formulations are equivalent, but
working over an arbitrary ground type makes the statement apply immediately to, e.g.,
almost-disjoint families of countable subsets of an uncountable space. -/
@[category research open, AMS 3 5]
theorem erdos_602 : answer(sorry) ↔
    ∀ {α : Type*} {I : Type*} (A : I → Set α),
      (∀ i, (A i).Countable ∧ (A i).Infinite) →
      (∀ i j, i ≠ j → (A i ∩ A j).Finite) →
      (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) →
      HasPropertyB I A := by
  sorry

⬆

Drop your .lean file here

or click to browse

Solana wallet for reward

Verifying with Lean 4…