---

Claim. For every $n\ge2$, among the graphs with $2n+1$ vertices and at least $n^2+n$ edges, $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; so for every $n\ge2$ every graph with $2n+1$ vertices and at least $n^2+n+1$ edges contains such a pair, which is the whole corrected Statement of Problem 816 in the stronger "at least" form. This is Theorem 1.3 of Z. Liu and Q. Zeng, A complement of the Erdős--Hajnal problem on paths with equal-degree endpoints, arXiv:2505.00523 (v1 1 May 2025; v2 4 August 2025, 14 pp.), as printed on p. 1 of v2, the edition on its source card. The authors describe their method as different from Chen and Ma's and suited to graphs with large equal degrees, state the even-order analog for $n\ge3$ (Theorem 1.5), and say in their concluding remarks (p. 10) that, with Chen and Ma's theorem, it resolves the question of Erdős and Hajnal completely.

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

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 covers every $n\ge2$, the range of Theorem 1.3, with exactly $n^2+n+1$ edges, and its docstring notes that $K_3$ is a counterexample at $n=1$. 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 theorem, so the page lists no formalized evidence.

Standing. Claimed: a preprint with no journal record found in the Crossref and Semantic Scholar queries of 2026-09-18, not cited by the site, and with no independent review found; its proof (Sections 2--3 and the appendix, pp. 2--14) is unread.