The board / graph theory / #136
Erdős Problem #136
SOLVEDdatabase updated 2025-08-31
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.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
An edge colouring of `K_n` with `k` colours is a `(4, 5)`-colouring if the six edges of every copy of `K_4` receive at least five distinct colours.
`K_n` admits a `(4, 5)`-colouring with `k` colours.
`f n` is the least number of colours in a `(4, 5)`-colouring of `K_n`.
Let \(f(n)\) be the smallest number of colours required to colour the edges of \(K_n\) such that every \(K_4\) contains at least \(5\) colours. Determine the size of \(f(n)\). Asked by Erdős and Gyárfás [Er97b], who proved \(\frac56 (n - 1) < f(n) < n\) and \(f(9) = 8\); Erdős believed that the upper bound is closer to the truth. In fact \(f(n) \sim \frac56 n\), as shown by Bennett, Cushman, Dudek and Pralat [BCDP22]; Joos and Mubayi [JoMu22] found a shorter proof.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/136.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/136
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.