Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Problem 163, the Burr--Erdős conjecture, asks whether every graph in which each subgraph has a vertex of degree at most (a -degenerate graph) has . Lee proves it. Lee's Theorem 1.1 states that there is an absolute constant such that for all , and , in every two-coloring of the edges of a complete graph on at least vertices one color contains every -degenerate -colorable graph on at most vertices. Since a -degenerate graph is -colorable, the case gives for every -degenerate on at least vertices, and the finitely many smaller graphs are absorbed into the constant; the problem page's Current assessment writes out this bridge. The proof uses dependent random choice with a random greedy embedding.
Scope. Full. The site states the conjecture in three forms (a union of forests, average degree at most in every subgraph, degeneracy at most ). The arboricity and edge-density forms are Burr and Erdős's own equivalent statements (the conjecture "could equally well have been stated" for the edge density), and their Lemma 3.3, which places the degeneracy between the edge density and twice it, bridges the edge-density form to the degeneracy form the theorem proves, so the theorem settles all three up to the constant. The size of the constant is not the problem's question: Lee's bound is doubly exponential in and the site records the conjecture , which remains open.
Depends on. Nothing in this wiki; the result rests on the cited paper alone.
Acceptance. Reviewed: the site's curator (T. F. Bloom) marks the problem PROVED, solved in the affirmative, and credits Lee's paper with the solution and the bound in the problem's commentary (as of 2026-09-18); of the thread's two comments one concerns the constant and the other a reference key since corrected on the site, and the proof-claim tab is empty. Refereed: the paper is Lee, Ramsey numbers of degenerate graphs, Ann. of Math. (2) 185 (2017), no. 3, 791--829 (issue dated 1 May 2017 in its Crossref record). The version cited is the arXiv v2 of 1 December 2016; the Annals text is not held and was not compared with it. Read depth: the statement of Theorem 1.1 and the remarks after it; the proof was not read.
Postings. arXiv:1505.04773, v1 of 18 May 2015 (the first posting, which dates this page) and v2 of 1 December 2016, the version cited; the journal article; the site's problem page, whose thread has one comment on the constant and one on a reference key, and whose proof-claim tab was empty on 2026-09-18.
Formalization, not evidence. Boris Alexeev's lean-proofs repository
holds Erdos163.lean (first committed 20 August 2026, linked above at its
commit of 15 September 2026). Its header declares it a Lean formalization of
a solution to Problem 163, with Choongbum Lee as informal author and Codex
and GPT-5.6 Sol as formal authors. Its theorem erdos_163 gives, for every
, a natural constant such that every -degenerate graph on
vertices has Ramsey number at most . Since 19 September 2026 the
formal-conjectures statement file links it through a formal_proof
attribute. This corpus has not built it, so it adds no formalized evidence.