Skip to content

Erdős problem 623

Let XX be a set of cardinality ω\aleph_\omega and ff a function from the finite subsets of XX to XX such that f(A)∉Af(A)\not\in A for all AA. Must there exist an infinite independent YXY\subseteq X, i.e. with f(B)∉Yf(B)\not\in Y for all finite BYB\subset Y? Claimed resolution: the positive assertion is equivalent to Koepke's free-subset property, hence independent of ZFC, with consistency strength exactly a measurable cardinal.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/623.lean

Formal Conjectures

FormalConjectures/ErdosProblems/623.leanErdos623.erdos_6234 linesExact file
True  ∀ (X : Type u),    Cardinal.mk X = Cardinal.aleph Ordinal.omega0      ∀ (f : Finset XX), (∀ (A : Finset X), f AA) → ∃ Y, Y.Infinite ∧ ∀ (B : Finset X), ↑BYf BY
OpenStatement only, no proof

Reported activity

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

  • AI collaborating with humans

    Erdős AI contributions wiki · 4 Jun, 2026

    Machine
    GPT-5.5 Pro
    People
    Sungchul Lee
    Open the source record
  • argument

    VibeMathed

    Machine
    GPT-5.5 Pro
    People
    Sungchul Lee
    Reported outcome
    candidate
    Open the source record

Continue

Search problems.science

Find a Problem, Result, source, or page