Erdős problem 183 · problems.science

Let $R(3;k)$ be the least $n$ such that every $k$ -colouring of the edges of $K_n$ contains a monochromatic triangle. Determine $\lim_{k\to\infty} R(3;k)^{1/k}$ (a $250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

183.lean

Retained formal statement1 of 2

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.

FormalConjectures/ErdosProblems/183.leanErdos183.erdos_1831 lineExact file

1Filter.Tendsto (fun k => ↑(Erdos183.multicolourTriangleRamsey k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science