The board / additive combinatorics / #781
Erdős Problem #781
DISPROVEDdatabase updated 2025-08-31
The statement as posed is false.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A \(k\)-term *descending wave* is a sequence \(x_1<\cdots <x_k\) such that, for \(1<j<k\), \(x_j \geq \frac{x_{j+1}+x_{j-1}}{2}\).
`f k` is the minimal `n` such that any \(2\)-colouring of \(\{1,\ldots,n\}\) (identified with `Fin n`) contains a monochromatic \(k\)-term descending wave.
Let \(f(k)\) be the minimal \(n\) such that any \(2\)-colouring of \(\{1,\ldots,n\}\) contains a monochromatic \(k\)-term descending wave: a sequence \(x_1<\cdots <x_k\) such that, for \(1<j<k\), \[x_j \geq \frac{x_{j+1}+x_{j-1}}{2}.\] Estimate \(f(k)\). Brown, Erdős, and Freedman [BEF90] proved \(k^2-k+1\leq f(k) \leq \frac{k^3-4k+9}{3}\). Resolved by Alon and Spencer [AlSp89] who proved that in fact \(f(k) \gg k^3\), so that \(f(k)\asymp k^3\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/781.Prizenone
Topicsadditive combinatorics
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/781
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.