---

Claim. For positive integers $n$ and $k$ let $g_k(n)$ be the maximum number of edges of a graph on $n$ vertices that contains no cycle with $k$ chords incident to one vertex of the cycle. Then $g_k(n)=(k+1)n-(k+1)^2$ for all $n\ge3k+3$. This is the theorem of T. Jiang, A note on a conjecture about cycles with many incident chords, J. Graph Theory 46 (2004), no. 3, 180--182 (published online 7 April 2004, the date in this page's name; print July 2004), as its abstract states it: the abstract attributes the conjecture, with an unspecified threshold $n(k)$, to Bollobás's Extremal Graph Theory (p. 398, Problem 13), where Erdős's papers of 1964 to 1976 state it as his own, and says the proof uses "an old result of Bondy". The paper is not held; its abstract is known as deposited in the Crossref record. The theorem as printed, any hypothesis the abstract omits, the identity of Bondy's result and the proof are therefore known only through the abstract; the 2026 preprint of Chen and Ning restates the theorem as its Theorem 1.2, with the hypotheses $k\ge1$ and $n\ge3k+3$, and a third-party Lean proof of the $n\ge3k+3$ form is recorded below.

For Problem 767 this is the site's statement in the site's notation, with $n(k)\le3k+3$, so the answer is yes. The problem page's Formulation converts Erdős's own indexing, which counts $k-1$ diagonals and the least forcing number, to the site's $g_k(n)$.

Acceptance. Refereed: Journal of Graph Theory, as the publisher's Crossref record gives it (volume, issue, pages, dates and abstract). Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED and records the theorem as proving the conjectured equality for $n\ge3k+3$ in the problem's commentary (last edited 6 October 2025). Context, not review: the community database mirrors the site's label, listing the problem as proved as of its last update on 31 August 2025, and Chen and Ning's preprint of 14 September 2026, on its claim page, restates the theorem as confirmed and extends it to every $n\ge k+2$. The acceptance recorded here rests on the abstract of a refereed note and the site's acceptance, not on a reading of the text; the problem page records this as its first remaining gap.

Formalization. The file src/latest/ErdosProblems/Erdos767.lean of Boris Alexeev's plby/lean-proofs repository, linked above at a pinned commit, declares itself a Lean formalization of a solution to Erdős Problem 767 and names Tao Jiang as its informal author and Codex and GPT-5.6 Sol as its formal authors; the note ErdosProblems/Erdos767.md calls it a formalized proof of the problem, and the file (1,583 lines) was added to the repository on 17 August 2026. Its theorem erdos_767 states that for $k>0$ and $n\ge3k+3$ the maximum number of edges of an $n$-vertex graph with no cycle carrying $k$ distinct chords at one cycle vertex is $(k+1)n-(k+1)^2$, the abstract's theorem with its threshold; its docstring cites Jiang's note and refers the mathematical proof and a map of the formalization to a note tex/767.tex, its imports name longest-cycle and Dirac modules of the repository, and it ends with a #print axioms command whose output is not recorded. The formal-conjectures statement of the problem, FormalConjectures/ErdosProblems/767.lean (added 2026-09-21; linked at the commit that added it), states erdos_767 in the same $n\ge3k+3$ form, tags it research solved and names the repository file in its formal_proof attribute. Because the file names Jiang as the informal author, it is a link on this page and not its own claim; this corpus has not built, audited or kernel-checked it, so it is no formalized evidence.