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.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1014.lean

Formal Conjectures

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:1014
PLBY Lean proofsErdosProblems.Erdos1014

Reported activity

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

AI standalone
Erdős AI contributions wiki · 23 Apr, 2026
Machine
OpenAI internal model
Open the source record
Conditional on conjectures
GPT-Erdős
Open the source record
argument
VibeMathed
Machine
OpenAI internal model
Reported outcome
resolved
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science