---

Claim. For integers $k\ge1$ and $n\ge k+2$ let $g_k(n)$ be the maximum number of edges of an $n$-vertex graph with no cycle having a vertex incident with at least $k$ chords. Theorem 1.3 of Xiaozheng Chen and Bo Ning, On Erdős Problem 767: Cycles with Chords, arXiv:2609.15330v1 (14 September 2026; 22 pages), states that for all $k\ge1$ and $n\ge k+2$

$$g_k(n)=\max\Bigl\{\Bigl\lfloor\tfrac{(k+1)n}2\Bigr\rfloor,\ \max\Bigl\{a(n-a)+\Bigl\lfloor\tfrac{a(k+1-a)}2\Bigr\rfloor: a\in\mathbb Z,\ \Bigl\lfloor\tfrac{k+1}2\Bigr\rfloor+1\le a\le k+1\Bigr\}\Bigr\}$$

(the abstract's display omits the outer "max"; the paper's Theorem 1.3 prints it). For $k\ge2$ the theorem gives $g_k(n)=(k+1)(n-k-1)$ for all $n\ge\lceil(5k+1)/2\rceil$, and the threshold is sharp: Construction 3.3 (pp. 4--5), a set $X$ of $a$ vertices identified with $\mathbb Z_a$ and carrying the differences $1,\ldots,\lfloor(k+1-a)/2\rfloor$ (plus a half-shift matching when $k+1-a$ is odd), joined completely to an independent set $Y$ of $n-a$ vertices, has $a(n-a)+\lfloor a(k+1-a)/2\rfloor$ edges and no cycle with $k$ chords at one vertex, and Remark 3.4 takes $a=k$ at $n=\lceil(5k+1)/2\rceil-1$ to get $(k+1)(n-k-1)+1$ edges. The lower bound for small $n$ is a second, nearly regular construction (Section 3); the upper bound (Section 5) builds on the stability theorem of Ma and Ning (Combinatorica 40 (2020), 105--147) for Bondy's theorem on long cycles. The paper restates Jiang's theorem as its Theorem 1.2 with the hypotheses $k\ge1$ and $n\ge3k+3$, credits Erdős's conjecture of the formula for $n\ge2k+2$ to his 1969 paper, says that Lewin disproved that conjecture, citing B. Bollobás, Extremal Graph Theory (1978), p. 398, Problem 12, and takes Bollobás's question with an unspecified threshold $n(k)$ from Problem 13 of the same page; its reference [19] is Pósa's Problem 127, from which the case $k=1$ of the formula follows. The preprint was named in the site's discussion thread on 15 September 2026, and the site's reference list did not carry it as of 2026-09-18.

For Problem 767, the formula gives $g_k(n)=(k+1)n-(k+1)^2$ for all large $n$, for every $k\ge1$ (the case $k=1$ is Pósa's $2n-4$ for $n\ge4$, on its claim page), so it settles the question a second time, after Jiang, and names the exact threshold at which the equality begins, which Jiang's $3k+3$ bounds from above. Since $\lceil(5k+1)/2\rceil$ equals $2k+2$ for $k=2,3$ and exceeds it from $k=4$ on, the sharpness places the failure of Erdős's range $n\ge2k+2$ at $k\ge4$, in agreement with Erdős's 1975 report that Lewin's examples exist for large $k$.

AI assistance and formalization. The paper's declaration of AI usage (p. 21) says that the work began while the authors were using GPT-5.5 Pro, that the authors proved the cases $k\le7$ and a stability version of Jiang's theorem themselves, and that, given those manuscripts, the system's second proposed general conjecture became the main theorem; the authors wrote and checked the final text. The same declaration says that every original result of the paper, Theorem 1.3 included, has been formalized and machine-checked in Lean 4, with the source at the repository linked above (its one commit, of 10 September 2026, is the pin; the repository describes itself as a Lean 4 formalization for Erdős Problem 767). The repository's README says that its development targets the authors' final manuscript, that its public claim is the verification of the paper's internal conclusions conditional on nine cited literature theorems packaged as hypotheses, which it does not prove, and that theorem_1_3 is its entry point. Because the development declares itself a formalization of this paper's result, it is a link on this page and not its own claim. This corpus has not built, audited or kernel-checked it, so it gives no formalized evidence.

Standing. Claimed. A preprint with its authors' Lean development: no refereed version is recorded, no outside reviewer has published an examination, and the Lean is unbuilt here. The problem's standing rests on the refereed claim above.