On Erdős Problem 767: Cycles with Chords
Xiaozheng Chen, Bo Ning
math.CO
Sep 14, 2026 · v1
TL;DR
All lemmas, claims, and the main theorem determining g_k(n) are formalized and machine-checked in Lean 4 with Mathlib, with a public repository.
Abstract
For integers $k\ge 1$ and $n\ge k+2$, let $g_k(n)$ be the maximum number of edges in an $n$-vertex graph containing no cycle with a vertex incident with at least $k$ chords. Erdős conjectured that $g_k(n)=(k+1)(n-k-1)$ for $n\ge 2k+2$. Lewin found a counterexample. Bollobás later conjectured that there exists a function $n(k)$ such that $g_k(n)=(k+1)(n-k-1)$ for all $n\ge n(k)$. Jiang confirmed this by proving the formula for all $n\ge3k+3$ when $k\ge1$. In this paper, we determine $g_k(n)$ completely. For all $k\ge1$ and $n\ge k+2$, we prove $g_k(n)=\big\{\lfloor\frac{(k+1)n}{2}\rfloor,\max\{a(n-a)+\lfloor\frac{a(k+1-a)}{2}\rfloor : a\in\mathbb Z,\; \lfloor {(k+1)}/{2}\rfloor+1\le a\le k+1\}\big\}$. For $k\ge2$, we prove $g_k(n)=(k+1)(n-k-1)$ when $n\ge \lceil(5k+1)/2\rceil$, and this threshold is sharp. Our proof builds on the method developed by Ma and the second author in [Ma and Ning, 2020].
Problem
Erdős Problem 767 asks for g_k(n), the maximum number of edges in an n-vertex graph with no cycle having a vertex incident with at least k chords. Jiang proved g_k(n)=(k+1)(n-k-1) for n≥3k+3, which left the range k+2≤n≤3k+2 open.
Approach
The authors reduce the problem to forbidding (k+2)-path-fans and give two lower-bound constructions: a nearly regular circulant graph and join-type graphs. The upper bound uses a minimal counterexample, closure, edge-switching, and circumference stability results that build on Ma and Ning's method. AI helped formulate the general conjecture. All results were formalized and machine-checked in Lean 4 with Mathlib.
Results
g_k(n) is determined for all k≥1 and n≥k+2 as the maximum of floor((k+1)n/2) and a family of join-type values. For k≥2, g_k(n)=(k+1)(n-k-1) exactly when n≥ceil((5k+1)/2), and this threshold is sharp.
