The board / graph theory / #557
Erdős Problem #557
PROVED LEANdatabase updated 2026-09-03
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 \(R_k(G)\) denote the minimal \(m\) such that if the edges of \(K_m\) are \(k\)-coloured then there is a monochromatic copy of \(G\). Is it true that \[R_k(T)\leq kn+O(1)\] for any tree \(T\) on \(n\) vertices? The answer is yes, with an absolute constant: \(R_k(T) \leq kn + 3\) for all \(k\) and \(n\). For \(n \geq 2\) this follows from the explicit bound \(R_k(T) \leq k(n-2)+3\), a consequence of the Erdős–Sós theorem (Erdős problem 548) by the pigeonhole principle, as recorded on the problem page; Reed and Stein [ReSt26] derived that bound for \(n\) large in terms of \(k\) from their dense-graph case of Erdős–Sós. For the one-vertex tree, \(R_k(T) \leq 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/557.Prizenone
Topicsgraph theory, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/557
Attempts
submit one →Read our working report →
verified \(R_q(T)\leq q(n-2)+2\) for all sufficiently large fixed-bounded-degree trees (modulo Pokrovskiy Theorem 1.16), certified every \(R_3(T)\) for \(|T|\leq5\), and isolated the unresolved all-tr
PARTIAL