Erdős problem 1014 · problems.science

Let $R(k,l)$ be the Ramsey number, so the minimal $n$ such that every graph on at least $n$ vertices contains either a $K_k$ or an independent set on $l$ vertices.

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1014.lean

Retained formal statement1 of 2

Let $R(k,l)$ be the Ramsey number, so the minimal $n$ such that every graph on at least $n$ vertices contains either a $K_k$ or an independent set on $l$ vertices.

Prove, for fixed $k\geq 3$ , that $\lim_{l\to \infty}\frac{R(k,l+1)}{R(k,l)}=1.$

This has been [solved](https://cdn.openai.com/pdf/6dc7175d-d9e7-4b8d-96b8-48fe5798cd5b/Ramsey.pdf) by an internal model at OpenAI.

FormalConjectures/ErdosProblems/1014.leanErdos1014.erdos_10141 lineExact file

1∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun l => ↑R(k, l + 1) / ↑R(k, l)) Filter.atTop (nhds 1)

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