---

Claim. Problem 800 asks whether $R(G)\ll n$, with an absolute implied constant, for every graph $G$ on $n$ vertices in which no two adjacent vertices both have degree at least three. Alon answers yes with the constant $12$: Proposition 1.3 of Subdivided graphs have linear Ramsey numbers states that

$$R(G)\le12n$$

for every finite simple graph $G$ on $n\ge1$ vertices whose vertices of degree at least three form an independent set, where $R(G)$ is the least $N$ such that every red-blue coloring of the edges of $K_N$ contains a monochromatic copy of $G$. The hypothesis is exactly the problem's; there is no bound on the maximum degree and isolated vertices are allowed. Theorem 1.1 of the same paper is the qualitative form, that these graphs form a linear Ramsey family. The proof chooses a maximal independent set containing every vertex of degree at least three, so that the remaining vertices form isolated vertices and isolated edges, and embeds an auxiliary graph of attachment pairs through the Goddard--Kleitman bound on $R(K_3,H)$, an external premise of the argument recorded on the result page. Alon writes that the constant can be improved somewhat and does not try to optimize it; a later refereed paper of Li, Rousseau and Šoltés (Discrete Math. 170 (1997)) reports the bound $6n$ for the same class, claims checked against the abstract only and recorded on its own claim page.

Scope. Full. The proposition is the problem's statement with an explicit absolute constant.

Depends on. Goddard--Kleitman triangle-versus-graph bound, the external premise of Alon's proof; the rest of the result rests on the cited paper.

Acceptance. Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED and credits this paper with the affirmative answer in the problem's commentary (as of 2026-09-09); the site's discussion thread and proof-claim tab are empty. Refereed: the paper appeared in J. Graph Theory 18 (1994), no. 4, 343--347, whose Wiley abstract states the $12n$ bound (Crossref record, issue dated July 1994,). The edition read is the author's five-page manuscript hosted on his publication list (the preprint link above), which carries no journal pagination and was not compared with the journal text. Read depth: the manuscript in full, the proof included, with the Goddard--Kleitman premise claims checked on its own result page; that reading is not acceptance evidence.

Formalization. Boris Alexeev's repository lean-proofs holds a Lean file for the problem, src/latest/ErdosProblems/Erdos800.lean, linked above at the commit of 15 September 2026. Its header declares it a formalization of a solution to the problem, names Alon as the informal author and names Codex and GPT-5.6 Sol as the formal authors; its theorem erdos_800 states that every graph on $n$ vertices with no adjacent pair of vertices of degree at least three has two-color Ramsey number at most $12n$, Alon's Proposition 1.3, and its own comment says that the proof follows Alon's paper with one input replaced by an elementary lemma of the file. Nothing of this Lean was built or audited in this corpus, so it gives no formalized evidence, and the acceptance above rests on the refereed publication and the curator's credit. The formal-conjectures statement file for the problem is recorded on the problem page; it carries no formal_proof annotation.

Dating. The page is dated by the issue month the journal record gives; the day in the page name is a placeholder, since the manuscript gives no date and no earlier posting is known.