The board / combinatorics / #1025
Erdős Problem #1025
SOLVED LEANdatabase updated 2026-09-15
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`X` is independent for a set mapping `f` on pairs if `f s(x, y) ∉ X` whenever `x ≠ y` are in `X`.
`g n` is the largest `k` such that every set mapping `f` on the pairs of an `n`-element set with `f(x, y) ∉ {x, y}` admits an independent set of size at least `k`.
Let \(f\) be a function from all pairs of elements in \(\{1,\ldots,n\}\) to \(\{1,\ldots,n\}\) such that \(f(x,y)\neq x\) and \(\neq y\) for all \(x,y\). We call \(X\subseteq \{1,\ldots,n\}\) independent if whenever \(x,y\in X\) we have \(f(x,y)\not\in X\). Let \(g(n)\) be such that, in every function \(f\), there is an independent set of size at least \(g(n)\). Estimate \(g(n)\). A question of Erdős and Hajnal [ErHa58], who could prove \(n^{1/3} \ll g(n) \ll (n\log n)^{1/2}\). Spencer [Sp72] proved \(g(n)\gg n^{1/2}\). Conlon, Fox, and Sudakov [CFS16] proved \(g(n)\ll n^{1/2}\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/1025.Prizenone
Topicscombinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1025
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.