---

Claim. For $n\ge600$, among the graphs with $2n+1$ vertices and at least $n^2+n$ edges, the complete bipartite graph $K_{n,n+1}$ is the only one in which no two vertices of equal degree are the ends of a path with three edges. Hence for $n\ge600$ every graph with $2n+1$ vertices and at least $n^2+n+1$ edges contains two vertices of the same degree joined by a path of length $3$, which is the corrected Statement of Problem 816 for those $n$, in the stronger "at least" form: the property is not monotone in the edge set, since adding edges changes degrees, so the statement for at least $n^2+n+1$ edges is genuinely stronger than the statement for exactly $n^2+n+1$ edges. The result is Theorem 2 of K. Chen and J. Ma, A problem of Erdős and Hajnal on paths with equal-degree endpoints, J. Combin. Theory Ser. B 179 (2026), 1--18, first posted as arXiv:2503.19569 on 2025-03-25; the corpus states it on its result page. In the paper's notation, $p_3(2n+1)=n^2+n$ for $n\ge600$, where $p_3(m)$ is the largest number of edges of an $m$-vertex graph without such a pair. The proof bounds the maximum degree $\Delta$ from above by $n+\sqrt{2n}+\frac32$ and from below by $\frac{17}{16}n$, which is impossible for $n\ge600$; the authors say a sharper estimate would lower the constant below $150$. Theorem 3 of the paper gives the even-order analog, $K_{n-1,n+1}$ unique with at least $n^2-1$ edges for large $n$, which the problem does not ask.

Covers. The corrected Statement for every $n\ge600$. For $2\le n\le599$ this theorem says nothing; the case $n=2$ is checked on the problem page, and the whole range $n\ge2$ is the subject of the pending full claim of Liu and Zeng.

Depends on. Nothing in this wiki; the argument is self-contained.

Acceptance. refereed: the Journal of Combinatorial Theory, Series B is a refereed journal; the Crossref record of the DOI (2026-09-18) gives volume 179 (July 2026), pages 1--18, and the paper link's date is the issue's nominal first day. reviewed: the site's curator, Thomas Bloom, labels the problem PROVED and credits Chen and Ma with the proof, in the stronger form that for $n\ge600$ only $K_{n,n+1}$, among the graphs with $2n+1$ vertices and at least $n^2+n$ edges, lacks such a pair (the site's page on 2026-09-18, with an empty thread and an empty proof-claim tab); the curator is independent of the authors, and the site's label is the discussion link. The community database lists the problem as proved, an entry last updated on 31 August 2025, and as formalized, an entry last updated on 20 September 2026. Page numbers are those of the arXiv version, the only one, the edition on its source card; Problem 1, Theorems 2 and 3 and the non-monotonicity remark were checked (pp. 1--2), the proof (pp. 2--11) was read for its structure only, and the journal text was not compared, so the published constant was not compared with the preprint's $600$.

Formalization. Boris Alexeev's repository plby/lean-proofs holds, at its commit of 15 September 2026, the file src/latest/ErdosProblems/Erdos816.lean (Lean 4.33.0, Mathlib 4.33.0), whose header declares it a formalization of a solution to Problem 816 with Kaizhe Chen, Jie Ma, Zhen Liu and Qinghou Zeng as informal authors and Codex and GPT-5.6 Sol as formal authors, and the repository's notes page for the problem. Its theorem erdos_816 states that for every $n\ge2$ a graph with $2n+1$ vertices and $n^2+n+1$ edges has two vertices of equal degree joined by a path with three edges, and its docstring notes that the restriction to $n\ge2$ is necessary because $K_3$ is a counterexample at $n=1$; the range $n\ge2$ is that of Liu and Zeng's theorem, and the file names both pairs of authors, so it is linked from both pages. The formal-conjectures statement file for the problem, added on 2026-09-20, points its formal proof at this file. Only the file's header and docstring were read; the corpus has not built, audited or kernel-checked the development, and the formal statement was not compared with the problem's wording, so the page lists no formalized evidence.