---

Claim. Let $f(n)$ be the least, over all $2$-colorings of the pairs of $\{2,\ldots,n\}$, of the largest weight $\sum_{x\in X}1/\log x$ of a set $X$ whose pairs are monochromatic. Rödl proved that $f(n)\to\infty$, which answers the question: for every $C>0$ and every $n$ large enough in terms of $C$, each $2$-coloring has a monochromatic $X$ of weight at least $C$. The two second-hand accounts agree on his rate: the introduction of Conlon, Fox and Sudakov (p. 2 of the preprint read) and Erdős's 1982 report (p. 78), which announced the result before publication, both give

$$f(n)=\Omega\Bigl(\frac{\log\log\log\log n}{\log\log\log\log\log n}\Bigr),$$

Erdős writing it as $c_1\log\log\log\log n/\log\log\log\log\log n<F(n)$ in his notation. Both accounts are second-hand, since the paper is not held here, and the claim recorded here is the divergence. The same paper gives a coloring showing $f(n)=O(\log\log\log n)$ (an upper bound on the forced weight, which the site calls a lower bound for the problem) and shows that the analogous statement fails for three colors.

Depends on. Nothing in this wiki; the result rests on the cited paper alone.

Acceptance. Refereed: V. Rödl, On homogeneous sets of positive integers, J. Combin. Theory Ser. A 102 (2003), no. 1, 229--240, in the April 2003 issue; the DOI record was created on 23 April 2003 (Crossref), the date this page is named by. Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED (LEAN) and credits the paper with the affirmative answer in the problem's commentary (page last edited 8 February 2026). Conlon, Fox and Sudakov also credit the paper with verifying Erdős's conjecture in the introduction of their refereed 2013 paper.

Formalization. The file src/latest/ErdosProblems/Erdos191.lean of Boris Alexeev's lean-proofs repository (GitHub user plby), linked above at a pinned commit and first added on 17 August 2026, declares itself a Lean formalization of a solution to the problem, with Rödl as its informal author and Codex and GPT-5.6 Sol as its formal authors; its module comment describes the proof as a qualitative finite specialization of the block argument of Rödl and of Conlon, Fox and Sudakov, and it is the artifact behind the site's "(Lean)" suffix. The file is unbuilt here and has no fidelity review, and its AI-tool authorship is provenance only, so formalized is not listed.

Read depth. The paper is not held here; the publisher's record marks it open archive. Everything attributed to it here is second-hand, from pp. 2--3 of Conlon, Fox and Sudakov (the library's Theorem 1.1 page restates the construction), from Erdős's 1982 report and from the site. Reopening condition: a copy of the paper read at its main theorem.