Erdős Problem a Daythe open tracker
The board / graph theory / #183

Erdős Problem #183

SOLVED LEANdatabase updated 2026-08-01

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. 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).

`n` forces a monochromatic triangle on `k` colours when every `k`-colouring of the edges of `K_n` has a colour class containing a triangle.

\(R(3;k)\), the minimal `n` such that every `k`-colouring of the edges of `K_n` contains a monochromatic triangle.

Let \(R(3;k)\) be the minimal \(n\) such that if the edges of \(K_n\) are coloured with \(k\) colours then there must exist a monochromatic triangle. Determine \[\lim_{k\to \infty}R(3;k)^{1/k}.\] There is no finite limit: \(R(3;k)^{1/k}\to\infty\). This was established by OpenAI [OpenAI26] along with the explicit superexponential lower bound in `erdos_183.variants.explicit_lower_bound`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/183.
Prize$250
Topicsgraph theory, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA003323
Original pageerdosproblems.com/183

Attempts

submit one →
WORKING REPORT BY THIS SITE · JUL 26, 2026

Read our working report →

verified a five-class near-colouring of PG(7,2) with exactly one monochromatic Fano plane and proved by a standalone exhaustive checker that every proper five-colouring is at fixed-label Hamming dista

PARTIAL
← #182the board#184 →