The board / graph theory / #1028
Erdős Problem #1028
SOLVED LEANdatabase updated 2026-01-19
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).
The imbalance of a finite set `X` under a colouring `f`, that is, \(\left\lvert \sum_{x<y\in X} f(x,y)\right\rvert\).
`H n` is the minimum, over all colourings `f` of pairs from `{1, …, n}` with values in `{-1, 1}`, of the largest imbalance of a subset `X ⊆ {1, …, n}`.
Let \[H(n)=\min_f \max_{X\subseteq \{1,\ldots,n\}} \left\lvert \sum_{x<y\in X} f(x,y)\right\rvert,\] where \(f\) ranges over all functions \(f:\{1,\ldots,n\}^2\to \{-1,1\}\). Estimate \(H(n)\). Erdős [Er63d] proved \[\frac{n}{4}\leq H(n) \ll n^{3/2}.\] Erdős and Spencer [ErSp71] proved that \(H(n)\gg n^{3/2}\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/1028.Prizenone
Topicsgraph theory, discrepancy
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1028
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.