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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/183.lean

Formal Conjectures

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.

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

construction
VibeMathed
Machine
Astra (internal preview)
Reported outcome
candidate
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Reported activity

Continue

Search problems.science