The board / combinatorics / #191
Erdős Problem #191
PROVED LEANdatabase updated 2026-08-24
The statement as posed is true, and a proof exists. 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).
Let \(C>0\) be arbitrary. Is it true that, if \(n\) is sufficiently large depending on \(C\), then in any \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) there exists some \(X\subseteq \{2,\ldots,n\}\) such that \(\binom{X}{2}\) is monochromatic and \[\sum_{x\in X}\frac{1}{\log x}\geq C?\] The answer is yes, which was proved by Rödl [Ro03]. In the same article Rödl also proved a lower bound for this problem, constructing, for all \(n\), a \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) such that if \(X\subseteq \{2,\ldots,n\}\) is such that \(\binom{X}{2}\) is monochromatic then \[\sum_{x\in X}\frac{1}{\log x}\ll \log\log\log n.\] In the same paper Rödl proves that the answer to the main problem is negative if we consider \(3\)-colourings. This bound is best possible, as proved by Conlon, Fox, and Sudakov [CFS13], who proved that, if \(n\) is sufficiently large, then in any \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) there exists some \(X\subseteq \{2,\ldots,n\}\) such that \(\binom{X}{2}\) is monochromatic and \[\sum_{x\in X}\frac{1}{\log x}\geq 2^{-8}\log\log\log n.\] A \(2\)-colouring of the pairs of \(\{2,\ldots,n\}\) is a graph `G` on this vertex set; a monochromatic set is a clique or an independent set of `
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/191.Prizenone
Topicscombinatorics, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/191
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.