The board / set theory / #623
Erdős Problem #623
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
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 \(f(B)\not\in Y\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open. The authoritative wording is on erdosproblems.com/623.Prizenone
Topicsset theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/623
Attempts
submit one →Read our working report →
Live page status OPEN with 0 claimed proofs, but “Currently working on this problem” lists Ritvik_Nayak (accessed 2026-07-31), so the mandatory no-collision rule requires stopping.
SKIPPED