---

Claim. There is an absolute constant $c>0$ such that, for every integer $k\ge2$,

$$R(3;k)\ge\Bigl(\frac{ck^{1/3}}{\log k}\Bigr)^k,$$

where $R(3;k)$ is the least $n$ such that every coloring of the edges of $K_n$ with $k$ colors has a monochromatic triangle (the coloring need not use every color; the logarithm is natural). Since $k^{1/3}/\log k\to\infty$, the $k$th roots $R(3;k)^{1/k}$ tend to $+\infty$, which determines the limit the problem asks for; no upper bound and no limit-existence argument is needed. The claimant is OpenAI, whose announcement attributes the argument to an internal model and the manuscript to humans working with it; no individual authors are named. The theorem is Chapter 9, Theorem 1.1 of the report, paged at Theorem 1.1 of the library's source card, which describes the August 6, 2026 revision; the report was announced on August 1, 2026 with an original version, which the source card does not describe.

Depends on. Chapter 9, Theorem 1.1 of the report, the claimant's own argument.

Acceptance. Reviewed: the site's curator, T. F. Bloom, labels the problem SOLVED (LEAN) and credits the proof, in the problem's commentary, to an internal model at OpenAI in the form $R(3;k)\ge k^{(1/3-o(1))k}$ for all $k\ge2$ (page last edited 1 September 2026, accessed 2026-10-07); the discussion thread (six comments, accessed 2026-10-07) records the announcement on 1 August 2026 and no objection, and the proof-claim tab is empty. The site also hosts, under its proof expositions, Rob Morris's The OpenAI lower bound on $R_k(3)$ (7 pages; the file's metadata dates it 31 August 2026; read in full), a self-contained write-up that states the result as Theorem 1.1 (OpenAI, 2026), proves the construction in its own words through a first step with $2k$ colors and an inductive lemma, and closes with the author's statement that they wrote the file themselves and is responsible for any errors: a named expert's independent account of the proof, which this page counts with the curator's credit as the reviewed evidence. The report itself is not refereed and claims no peer review, so refereed is not listed. Beside these outside attestations, and not counted as acceptance, this corpus reconstructed the chapter's five results and the root-limit deduction and passed them through its own fresh-context review and distinct grade, as the lower-route review records.

Formalization. The pinned upstream file, at the commit linked above, declares erdos_183 for the divergent root limit and erdos_problem_183_explicit for the limit together with the bound for every $k\ge2$ with $c=1/(6e^{38})$; the repository's manifest reports no sorry and the three standard axioms. This repository examined its definitions and endpoint statements only: the proof and its dependency closure were not audited, and no build, axiom check or statement-fidelity review was performed, so formalized is not listed as evidence. The community database points to this file as the formal proof. Boris Alexeev's lean-proofs repository holds a port of the same file to a later toolchain, linked above and first added on 26 August 2026. Its header names Astra (internal OpenAI model) as the author of the informal proof, and Astra with the OpenAI team as the formalizers. It is not built here and adds no evidence.