Erdős problem 566 — wave 6d
Date: 2026-07-27 (UTC)
0. Mandatory live-page gate
I fetched https://www.erdosproblems.com/566 through the Bright Data browser
path (not datacenter curl) on 2026-07-27. The rendered live page said
OPEN.
The live-page statement, verbatim, is:
> Let \(G\) be such that any subgraph on \(k\) vertices has at most \(2k-3\)
> edges. Is it true that, if \(H\) has \(m\) edges and no isolated vertices,
> then
> \[ > R(G,H)\ll m? > \]
The accompanying live-page known-result paragraph, verbatim, is:
> In other words, is \(G\) Ramsey size linear? This fails for a graph \(G\)
> with \(n\) vertices and \(2n-2\) edges (for example with \(H=K_n\)).
> Erdős, Faudree, Rousseau, and Schelp [EFRS93] have shown that any graph
> \(G\) with \(n\) vertices and at most \(n+1\) edges is Ramsey size linear.
The page also says “Implies [567]”, has no comments, and was last edited
18 January 2026. I read every collaboration/proof marker:
0 comments on this problem0 claimed proofs for this problemLikes this problem: NoneInterested in collaborating: NoneCurrently working on this problem: NoneThis problem looks difficult: ebarschkisThis problem looks tractable: NoneThe results on this problem could be formalisable: NoneI am working on formalising the results on this problem: NoneFormalised statement? Yes
Thus neither stop condition was present and I proceeded.
Claim labels
The mathematical claims below are labelled as requested:
- (a) elementary-rigorous;
- (b) rigorous modulo the explicitly named theorem/source;
- (c) plausible or structural but unverified;
- (d) computational-only.
The usual interpretation of the displayed sparsity condition starts at
\(k=2\); otherwise the literal inequality at \(k=1\) would read
\(0\leq-1\). Equivalently, for subgraphs \(J\) on at least three vertices,
\[ m_2(G):=\max_{J\subseteq G}\frac{e(J)-1}{v(J)-2}\leq 2. \]This equivalence is (a).
1. Primary-source literature audit
I searched the exact phrase “Ramsey size linear”, the \(m_2(G)\leq2\)
formulation, the \(2k-3\) density condition, and the three named boundary
graphs through July 2026. I downloaded and read the primary PDFs rather than
relying on search-result summaries.
1. Erdős–Faudree–Rousseau–Schelp (1993).
P. Erdős, R. J. Faudree, C. C. Rousseau, R. H. Schelp,
Ramsey Size Linear Graphs, Combinatorics, Probability and Computing 2
(1993), 389–399,
DOI 10.1017/S096354830000078X.
Section 5, Question 1 is exactly the live-page density question. The
paper proves that connected \(G\) with \(e(G)\leq v(G)+1\) is Ramsey
size-linear, that \(e(G)\geq2v(G)-2\) prevents size-linearity, and that
\(\operatorname{ex}(N,G)=O(N^{3/2})\) suffices. It identifies the
five-vertex graph \(K_4^*\) (one edge of \(K_4\) subdivided once) as the
sole unresolved graph of order at most five, and explicitly asks about
\(K_4^*,K_{3,3}\), and the cube \(Q_3\). (b)
2. Balister–Schelp–Simonovits (2002).
P. N. Balister, R. H. Schelp, M. Simonovits,
A Note on Ramsey Size-Linear Graphs, Journal of Graph Theory 39 (2002),
1–5,
They prove that a sufficiently long new path between two vertices of a
Ramsey size-linear graph preserves size-linearity. Their Corollary 2
requires path length at least \(d(x,y)+3\), and their Question 2 asks
whether the length-two operation always works. The latter operation is
precisely “add a new degree-two vertex with two prescribed neighbours”;
applied to \(K_4-e\), it produces \(K_4^*\). (b)
3. Bradač–Gishboliner–Sudakov (2024).
D. Bradač, L. Gishboliner, B. Sudakov,
On Ramsey Size-Linear Graphs and Related Questions, SIAM Journal on
Discrete Mathematics 38 (2024), 225–242,
Their introduction states the \(m_2(G)\leq2\) problem and says it remains
out of reach. Their Theorem 3 proves
\(R(K_4^*,F)=O(e(F))\) for bipartite \(F\) without isolates, and their
Theorem 4 proves that every subdivision of \(K_4\) on at least six
vertices is Ramsey size-linear. For clique targets they record only
\(R(K_4^*,K_n)=O(n^{5/2})\), while size-linearity already requires the
stronger \(O(n^2)\). (b)
4. Later adjacent papers.
Y. Wigderson,
Infinitely many minimally non-Ramsey size-linear graphs,
European Journal of Combinatorics 128 (2025), 104175,
DOI 10.1016/j.ejc.2025.104175,
arXiv:2409.05931, proves existence of
infinitely many minimal non-size-linear graphs but explicitly does not
construct one beyond \(K_4\); it does not settle the \(m_2\leq2\)
conjecture. (b)
E. K. Hng, M. Ji, A. Lamaison,
Ramsey size linear and generalization,
arXiv:2603.25453, treats odd-cycle
constants and clique/multicolour variants, not Problem 566. (b)
I found no primary source claiming a proof or counterexample to the general
statement. This is a search report, not a proof that no such paper exists.
2. A clean structural reduction and the precise existing obstruction
The density condition defines the \((2,3)\)-sparse graphs. Sparse edge sets
are the independent sets of the \((2,3)\)-sparsity matroid, so every such
graph on a fixed vertex set extends to a \((2,3)\)-tight (Laman) graph on the
same vertex set. See A. Lee and I. Streinu, *Pebble Game Algorithms and
Sparse Graphs*, Discrete Mathematics 308 (2008), 1425–1437,
DOI 10.1016/j.disc.2007.07.104.
Because every subgraph of a Ramsey size-linear graph is Ramsey size-linear,
it is enough to prove the conjecture for Laman graphs. (b)
The Henneberg–Laman theorem constructs every Laman graph from \(K_2\) using:
1. Henneberg I: add a vertex adjacent to two old vertices;
2. Henneberg II: delete an old edge \(uv\), add a vertex \(x\), and add
\(xu,xv,xw\) for a third old vertex \(w\).
Consequently, closure of Ramsey size-linearity under both moves would prove
Problem 566. (b) This is an exact sufficient reduction, not a claim that
these are the only possible proof methods.
The first closure statement already contains the smallest unresolved case:
\(K_4-e\) is Ramsey size-linear by EFRS93, while adding a degree-two vertex
whose neighbours are the endpoints of the missing edge gives \(K_4^*\).
Thus even Henneberg I is not presently available. (b) Balister–Schelp–
Simonovits Question 2 is exactly this missing closure lemma.
3. An exact infinite target family for the smallest unresolved graph
Let \(K_4^*\) denote \(K_4\) with one edge subdivided once.
Theorem
For every \(n\geq2\),
\[ R(K_4^*,nK_2)=2n+2. \]Also \(R(K_4^*,K_2)=5\). (a)
I do not claim that this formula is new to the literature; it is a
from-scratch result obtained and checked in this run. It gives a sharp
linear answer for an infinite family of allowed targets \(H\), with
\(e(H)=n\).
Lower bound
Colour \(K_{2n+1}\) so that the blue graph is
\[ K_{2n-1}\ \cup\ 2K_1. \]Its maximum matching has \(n-1\) edges. The red graph is the complete
tripartite graph \(K_{1,1,2n-1}\).
Now \(\alpha(K_4^*)=2\). Any embedding of five vertices into
\(K_{1,1,2n-1}\) puts at least three of them in the large independent part,
which would give an independent triple in \(K_4^*\). Hence there is no red
\(K_4^*\), proving \(R(K_4^*,nK_2)\geq2n+2\). (a)
Upper bound
Consider any red/blue colouring of \(K_{2n+2}\) with no red \(K_4^*\), and
let \(M\) be a maximum blue matching. Suppose \(|M|\leq n-1\). The set
\(U\) of vertices uncovered by \(M\) has
\[ |U|=2n+2-2|M|\geq4. \]Maximality of \(M\) makes every edge inside \(U\) red.
If \(|U|\geq5\), then the red \(K_5\) on \(U\) contains \(K_4^*\), a
contradiction. Hence \(|U|=4\), \(|M|=n-1\), and \(M\neq\varnothing\).
Choose a blue matching edge \(xy\in M\).
If \(x\) had red edges to two vertices of the red \(K_4=U\), that \(K_4\)
together with \(x\) would contain \(K_4^*\): use \(x\) as the subdivision
vertex. Therefore \(x\) has at least three blue neighbours in \(U\); the
same holds for \(y\). Two subsets of a four-set, each of size at least
three, admit distinct representatives \(u,v\). Replacing \(xy\) in \(M\)
by the two blue edges \(xu,yv\) gives a larger matching, the final
contradiction. Thus \(|M|\geq n\), proving the upper bound. (a)
4. Exact small-target computation
I also determined \(R(K_4^*,H)\) for every isomorphism type of graph \(H\)
with no isolated vertices and \(e(H)\leq4\). (d) Here \(T_5\) is the
five-vertex tree with degree sequence \((3,2,1,1,1)\), “paw” is a triangle
with a pendant edge, + denotes disjoint union, and \(rK_2\) is a matching.
| \(e(H)\) | \(H\) | \(R(K_4^*,H)\) |
|---:|:---|---:|
| 1 | \(K_2\) | 5 |
| 2 | \(P_3\) | 5 |
| 2 | \(2K_2\) | 6 |
| 3 | \(K_3\) | 9 |
| 3 | \(K_{1,3}\) | 7 |
| 3 | \(P_4\) | 7 |
| 3 | \(P_3+K_2\) | 7 |
| 3 | \(3K_2\) | 8 |
| 4 | paw | 9 |
| 4 | \(C_4\) | 8 |
| 4 | \(K_{1,4}\) | 9 |
| 4 | \(T_5\) | 9 |
| 4 | \(P_5\) | 9 |
| 4 | \(K_3+K_2\) | 9 |
| 4 | \(K_{1,3}+K_2\) | 8 |
| 4 | \(2P_3\) | 8 |
| 4 | \(P_4+K_2\) | 8 |
| 4 | \(P_3+2K_2\) | 9 |
| 4 | \(4K_2\) | 10 |
The checker independently enumerates all no-isolate target graphs, obtaining
exactly \(1,2,5,11\) isomorphism types with \(1,2,3,4\) edges. It does not
start from the table and assume completeness. (d)
For each target and proposed value \(r\), it builds a CNF whose variables are
the red edges of \(K_N\):
def ramsey_cnf(target, host_order):
clauses = [
[-variable for variable in copy]
for copy in pattern_copies(K4_STAR, host_order)
]
clauses.extend(
[variable for variable in copy]
for copy in pattern_copies(target, host_order)
)
return clauses
The negative clauses forbid red \(K_4^*\); the positive clauses forbid blue
\(H\). CaDiCaL 1.9.5 and Glucose 4.2 independently return SAT at \(N=r-1\)
and UNSAT at \(N=r\). Every SAT model is then checked by a separate direct
subgraph routine. (d) The largest instance has 45 edge variables; the
largest clause count is 15,120. A clean rerun took 20.668 seconds wall time
on this VM. (d)
The UNSAT results are deliberately labelled computational-only: no DRAT/LRAT
proof certificates were retained, and the table is not being presented as a
formal theorem.
5. Reproduction and independent checks
The standalone verifier is
runs/erdos566_wave6d_reverify.py. Run:
python runs/erdos566_wave6d_reverify.py
It checks, from graph definitions:
- the \(2k-3\) sparsity of \(K_4^*\) and \(\alpha(K_4^*)=2\);
- the local embedding and matching-augmentation facts in the exact proof;
- explicit lower-bound colourings for \(2\leq n\leq8\);
- completeness of the \(1,2,5,11\) small-target isomorphism classes;
- all 38 SAT/UNSAT boundary instances with both solvers;
- every lower-bound SAT witness without trusting the SAT solver's
interpretation.
The clean final output was:
Structural checks and matching lower constructions: PASS
From-scratch target enumeration: 1, 2, 5, 11 types: PASS
...
Two-solver SAT cross-check and direct witness validation: PASS
ALL CHECKS PASSED
6. What remains, without overclaiming
The matching formula and the 19-entry finite table do not supply the
uniform bound over arbitrary \(H\), so they do not close Problem 566.
Already for the five-vertex \(K_4^*\), the necessary clique-target estimate
\(R(K_4^*,K_n)=O(n^2)\) is not known in the primary literature found here;
the recorded general upper bound is \(O(n^{5/2})\). (b) Exact finite SAT
cannot bridge that asymptotic exponent or provide the uniformity in \(H\).
At the structural level, a sufficient route is now isolated exactly: prove
that Ramsey size-linearity survives both Henneberg moves. The Henneberg-I
case alone would settle \(K_4^*\), and it is the length-two path question
left open in 2002. (b) A proof needs a genuinely new embedding lemma that
turns a linear-size supply of red copies of the old graph into a red copy
with a common two-neighbour attachment, or else embeds arbitrary \(H\) in
blue. Current long-path averaging and dependent-random-choice arguments do
not provide that two-neighbour attachment at linear cost. (c)
PARTIAL: Proved \(R(K_4^*,nK_2)=2n+2\) for every \(n\ge2\) and computationally determined \(R(K_4^*,H)\) for every no-isolate \(H\) with at most four edges; the uniform \((2,3)\)-sparse problem remains open.