Source labels openChecked July 26, 2026

Erdős Problem 623

Let $X$ be a set of cardinality $\aleph_\omega$ and $f$ be a function from the finite subsets of $X$ to $X$ such that $f(A)\not\in A$ for all $A$ . Must there exist an infinite $Y\subseteq X$ that is independent - that is, for all finite $B\subset Y$ we have...

Mathematical logic AMS 3

Mathematical statement

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_623

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_623 : answer(sorry) ↔ ∀ (X : Type u) (hX : #X = ℵ_ ω)    (f : Finset X → X), (∀ A : Finset X, f A ∉ A) →    (∃ Y : Set X, Set.Infinite Y ∧ (∀ (B : Finset X), ↑B ⊆ Y → f B ∉ Y)) := 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

Pinned Formal Conjectures sourceformalization erdosproblems.com/623background