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 Y⊆XY\subseteq X, i.e. with f(B)∉Yf(B)\not\in Y for all finite B⊂YB\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 X → X), (∀ (A : Finset X), f A ∉ A) → ∃ Y, Y.Infinite ∧ ∀ (B : Finset X), ↑B ⊆ Y → f B ∉ Y
OpenStatement only, no proof

Reported activity

Reported by these sources. 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