Erdős ProblemsMathematical logic
Erdős Problem 602
Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?
Mathematical statement
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.
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_602
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- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References