Erdős Problems 552 and 85:
A Formal Proof of Chen's Bound, an Equivalence, and Three Corrections

1. The problems

Write \(R(n)=R(C_4,K_{1,n})\). Equivalently, \(R(n)\) is the least \(N\) such that every \(C_4\)-free graph on \(N\) vertices has a vertex with at least \(n\) non-neighbours. Problem 552 (Burr, Erdős, Faudree, Rousseau and Schelp; a $100 prize) asks to determine \(R(n)\), and in particular whether \(R(n)\le n+\sqrt n-c\) for infinitely many \(n\), for every \(c>0\). It is known that \(n+\sqrt n-6n^{11/40}\le R(n)\le n+\lceil\sqrt n\rceil+1\), and the exact value is known for \(n\le38\) (OEIS A006672; Boza, arXiv:2409.12770). The page also asks whether \(R(n+1)=R(n)\) infinitely often, and whether \(R(n+1)\le R(n)+2\) for all \(n\).

Problem 85 lets \(f(n)\) be the least \(k\) such that every graph on \(n\) vertices with minimum degree at least \(k\) contains a \(C_4\), and asks whether \(f(n+1)\ge f(n)\) for all large \(n\).

2. Chen's bound, formally verified

The bound fails for \(n=0\): \(R(1)=4\) and \(R(0)=1\). Chen's theorem answers the question "is \(R(n+1)\le R(n)+2\) for all \(n\)?" listed under Problem 552; Boza cites it as Lemma 1. We found the argument above independently and then found Chen's paper while checking priority.

The Lean statement uses SimpleGraph.graphRamsey, copied verbatim from Google DeepMind's formal-conjectures, so it is the statement used there:

theorem erdos_552.variants.succ_le_add_two (n : ℕ) (hn : 1 ≤ n) :
    SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
        (completeBipartiteGraph (Fin 1) (Fin (n + 1))) ≤
      SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
        (completeBipartiteGraph (Fin 1) (Fin n)) + 2

• The source is agnt-gg/erdos-lean (commit 8e5972f) and in the archive. The friendship theorem comes from Mathlib's Archive.
• #print axioms reports only propext, Classical.choice and Quot.sound. There is no sorry and no custom axiom. It builds on Lean v4.33.1 with Mathlib v4.33.1 (commit 0df444a), with warnings treated as errors.
• Negative control: without the hypothesis \(n\ge1\), the proof fails.
• The file also proves that \(2n+2\) vertices always suffice, so the Ramsey number is finite, and that \(R(n)\ge n+2\).
• Submitted to formal-conjectures as a solved variant of Problem 552: pull request #6904.

3. Problem 85 is a question about plateaus of \(R\)

So Problem 85 holds if and only if the answer to the Problem 552 question "is \(R(n+1)=R(n)\) infinitely often?" is no. Among the 38 known values the only plateau is \(R(1)=R(2)=4\), which corresponds to \(n=3\), below the range of Problem 85. Table 1 gives \(f(n)\) for \(4\le n\le44\), computed from the known values with the lemma; it never decreases.

If \(R(n)\in\{n+\lceil\sqrt n\rceil,\,n+\lceil\sqrt n\rceil+1\}\) for all \(n\ge2\), as Zhang, Chen and Cheng speculate, then a plateau needs \(\lceil\sqrt{s+1}\rceil=\lceil\sqrt s\rceil\) with \(R(s)=s+\lceil\sqrt s\rceil+1\) and \(R(s+1)=s+1+\lceil\sqrt{s+1}\rceil\). We have no proof that this pattern occurs, or that it occurs only finitely often.

4. Three corrections

1. Problem 85: the formula. The page gives \(f(n)=\min\{m: m\ge R(C_4,K_{1,n-m})\}\). This does not reproduce the page's own value \(f(4)=2\). The correct relation is the lemma of §3. A brute-force search over all graphs on at most 7 vertices gives \(f(4),\dots,f(7)=2,3,3,3\); the lemma reproduces them and the page's formula gives none, 4, 4, 5. The page's other relation, \(R(C_4,K_{1,n})=\min\{m: f(m)\le m-n\}\), is correct.
2. Problem 85: the bound \(f(n)<\sqrt n+1\). It fails at \(n=15\). The 4-regular graph below has 15 vertices, 30 edges and no \(C_4\), so \(f(15)\ge5>\sqrt{15}+1\approx4.873\). It was found with the z3 solver and checked separately without it. From the known Ramsey values, the bound also fails at \(n=16,34,35,36\); even "\(\le\)" fails at \(n=15,34,35\). The bound holds only asymptotically, as \(f(n)=(1+o(1))\sqrt n\).

   0-1  0-2  0-7  0-8  1-3  1-8  1-14  2-5  2-7  2-12  3-10  3-11  3-14  4-6  4-7  4-9  4-14  5-9  5-10  5-12  6-7  6-11  6-13  8-9  8-13  9-10  10-11  11-13  12-13  12-14

3. Problem 552: the prize and a settled question. The community database listed no prize, though the problem carries Erdős's $100. The question "is \(R(n+1)\le R(n)+2\) for all \(n\)?" is answered by Chen's theorem (§2).

These are submitted as pull request #456 and issue #457 to the community database maintained by Thomas Bloom and Terence Tao.

5. Verification

6. What remains open

Problem 552 asks for \(R(n)\) itself, and whether \(R(n)\le n+\sqrt n-c\) infinitely often for every \(c\). Problem 85, by §3, asks whether \(R\) has only finitely many plateaus. Both are open. One sufficient condition is elementary. Suppose some \(C_4\)-free graph on \(R(s)-1\) vertices, in which every vertex has fewer than \(s\) non-neighbours, contains a set \(S\) of at least \(R(s)-1-s\) vertices, no two with a common neighbour. Join a new vertex to \(S\). The result has \(R(s)\) vertices, has no \(C_4\) (a 4-cycle through the new vertex needs two members of \(S\) with a common neighbour), and every vertex has at most \(s\) non-neighbours. So \(R(s+1)>R(s)\), and there is no plateau at \(s\). Whether such witnesses always exist is the question we intend to study next.

7. Reproduction

python -m pip install networkx z3-solver
python battery_552.py          # brute force, all graphs on at most 7 vertices
python f85_from_ramsey.py      # f(n), plateaus and the sqrt bound from OEIS A006672
python witness_f85.py 15 4     # the 15-vertex graph, found and checked

# Lean: in lean/ of the archive, or a clone of agnt-gg/erdos-lean
lake exe cache get
lake build

8. Artifact ledger

Principal hash: lean/Erdos/Erdos552.lean 48d6293771ee532d7e079904798f1bfb7f93e81614bf0011cc5c7290f55ea350.

References

1. S. Burr, P. Erdős, R. J. Faudree, C. C. Rousseau and R. H. Schelp, "Some complete bipartite graph-tree Ramsey numbers," Annals of Discrete Mathematics 41 (1989), 79–89.
2. Chen Guantao, "A result on \(C_4\)-star Ramsey numbers," Discrete Mathematics 163 (1997), 243–246.
3. T. D. Parsons, "Ramsey graphs and block designs I," Transactions of the AMS 209 (1975), 33–44.
4. X. Zhang, Y. Chen and T. C. E. Cheng, "Some values of Ramsey numbers for \(C_4\) versus stars," Finite Fields and Their Applications 45 (2017), 73–85.
5. L. Boza, "Exact values and bounds for Ramsey numbers of \(C_4\) versus a star graph," arXiv:2409.12770 (2024–2026).
6. T. F. Bloom, Erdős Problems #552 and #85; OEIS A006672.
7. N. Wilbanks and Annie, "erdos-lean," GitHub, 2026, agnt-gg/erdos-lean, commit 8e5972f.
8. The mathlib Community, "The Lean Mathematical Library," CPP 2020, 367–381; friendship theorem in Mathlib's Archive/Wiedijk100Theorems/FriendshipGraphs.lean.