---

Claim. Theorem 1 of On the ratio of $R(k,\ell)$ and $R(k,\ell+1)$, a three-page manuscript hosted by OpenAI, states that for every fixed integer $k\ge2$

$$\lim_{\ell\to\infty}\frac{R(k,\ell+1)}{R(k,\ell)}=1,$$

where $R(k,\ell)$ is the least $N$ such that every graph on $N$ vertices has a $K_k$ or an independent set of $\ell$ vertices. For $k\ge3$ this is the statement of Problem 1014; the case $k=2$ is $R(2,\ell)=\ell$. Remark 1 adds that the proof gives, for each fixed $k\ge2$, a constant $c_k>0$ with $R(k,\ell+1)/R(k,\ell)\le1+\ell^{-c_k}$ for all large $\ell$, without a value for any $c_k$. The claimant is OpenAI: the manuscript names no author, and its abstract attributes the proof to an internal model at OpenAI. The theorem and remark are paged at Theorem 1 and Remark 1 of the library's source card. The proof (pp. 2--3) takes a graph $G$ on $R(k,\ell+1)-1$ vertices with no $K_k$ and independence number at most $\ell$, so that every vertex has at least $R(k,\ell+1)-R(k,\ell)-1$ neighbors; dependent random choice, in the Fox--Sudakov form, extracts a set $U$ in which every $\lceil k/2\rceil$-subset has at least $R(\lfloor k/2\rfloor,\ell+1)$ common neighbors, so $U$ spans no $K_{\lceil k/2\rceil}$ and no independent $(\ell+1)$-set; the Erdős--Szekeres upper bound and a probabilistic lower bound on $R(k,\ell)$ make the two bounds on $|U|$ incompatible unless $(R(k,\ell+1)-R(k,\ell))/R(k,\ell+1)\to0$.

Standing. Accepted. Reviewed: the site's curator, T. F. Bloom, relabeled the problem PROVED (LEAN) on 24 April 2026, the day after a thread comment linked the manuscript, with commentary crediting the solution to an internal model at OpenAI and stating the quantitative bound the proof gives; the curator is independent of the claimant, and this crediting is the one evidence kind listed. The manuscript has no refereed publication, no arXiv version and no written expert review (Crossref and arXiv searches of 2026-09-18, recorded on the problem page), so refereed is not listed; its Lemma 2, the probabilistic lower bound $R(k,\ell)\gg_k(\ell/\log\ell)^{k/2}$, is stated without proof or citation (it follows from Spencer's 1977 Theorem 2.2, recorded on the problem page). The thread also records a formalization report and one reader's request for an expert review before the label changes, and the proof-claim tab is empty. The page is named by the PDF's metadata date, 22 April 2026, the earliest date attached to the posting; the manuscript's text is undated.

Formalizations. Two external Lean developments prove the theorem for their own definitions of the Ramsey number at the pinned commits; neither is built or audited here. The file src/v4.29.1/ErdosProblems/Erdos1014.lean of Boris Alexeev's repository plby/lean-proofs (the repository head of 2026-09-18; 3,511 lines) names the internal model as informal author and Codex and Boris Alexeev as formal authors, and its header's URL list points at OpenAI's GPT-5.5 announcement, the file's pointer rather than the manuscript's attribution; it defines ramseyNumber k l over SimpleGraph (Fin n) and proves erdos1014 (k : ℕ) (hk : 3 ≤ k) : Tendsto (fun l => (ramseyNumber k (l + 1) : ℝ) / ramseyNumber k l) atTop (𝓝 1) with no sorry, its closing comment recording the three standard axioms; the thread comment of 23 April 2026 announced it, and the formal-conjectures statement erdos_1014 (a sorry body over SimpleGraph.classicalRamsey) names it in its formal_proof attribute. The repository maokami/ramsey-ratio-lean (head of 29 April 2026, toolchain v4.28.0-rc1) defines ramsey k ℓ as an infimum, proves ramsey_ratio_tendsto_one for every $k\ge2$ and the Remark 1 form ramsey_ratio_quantitative, ends with #print axioms, and says in its README that it reproduces this manuscript. The three definitions of the Ramsey number differ and no bridge was reviewed, so formalized is not listed.

Depends on. Nothing in this wiki; the manuscript's proof rests on the Erdős--Szekeres bound, a probabilistic lower bound and dependent random choice, taken at statement level.