Skip to content

Erdős problem 1022

Is there a constant ctc_t, where ctc_t\to \infty as tt\to \infty, such that if F\mathcal{F} is a finite family of finite sets, all of size at least tt, and for every set XX there are <ctX<c_t\lvert X\rvert many AFA\in \mathcal{F} with AXA\subseteq X, then F\mathcal{F} has chromatic number 22 (in other words, has property B)?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1022.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1022.leanErdos1022.erdos_10221 lineExact file
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1022
  • PLBY Lean proofsErdosProblems.Erdos1022

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page