Erdős problem 183

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

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

183.lean

Retained formal statement2 of 2

The explicit bound behind erdos_183: for every $k\geq 2$ , $R(3;k)\geq \left(\frac{k^{1/3}}{6e^{38}\log k}\right)^k.$

FormalConjectures/ErdosProblems/183.leanErdos183.erdos_183.variants.explicit_lower_bound1 lineExact file

1∀ (k : ℕ), 2 ≤ k → (1 / (6 * Real.exp 38) * ↑k ^ (1 / 3) / Real.log ↑k) ^ k ≤ ↑(Erdos183.multicolourTriangleRamsey k)

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.