---

The claim. Hong Wang, Proof of the Erdős--Faudree conjecture on quadrilaterals, Graphs and Combinatorics 26 (2010), no. 6, 833--877, doi:10.1007/s00373-010-0948-3; received 12 September 2006, revised 16 April 2010, published online 19 May 2010 (this page's date) and in print in November 2010. The edition read is the publisher's version of record, carded at its library home. Theorem B (p. 834, paged at theorem_b) states that a graph of order $4k$ with minimum degree at least $2k$ contains $k$ disjoint cycles of length $4$, where disjoint means having no common vertex (p. 833); this is the statement of the problem for every positive integer $k$, with no further hypothesis, so the claim is full. The $k$ four-cycles use all $4k$ vertices, so the conclusion is a spanning subgraph of $k$ disjoint copies of $C_4$. The proof (pp. 835--877) argues by contradiction from a chain of a triangle and $k-1$ disjoint four-cycles chosen to maximize the number of chords of the four-cycles: a two-page sketch derives Theorem B from Claims 2.5--2.7 by counting the edges from the leftover vertex and the triangle into the four-cycles, and the remaining 42 pages prove Claims 2.1--2.7 through 22 lemmas. The paper's introduction attributes the conjecture to Erdős's 1990 Bielefeld report, the site's [Er90c], which is not held, and records the earlier partial results of Randerath, Schiermeyer and Wang (1999) and Wang (2004).

Acceptance. Refereed: Graphs and Combinatorics is a refereed journal, and the paper is its version of record. Reviewed: the site's curator, Thomas Bloom, labels the problem PROVED and, in the commentary of erdosproblems.com/577 (accessed 2026-10-07; empty discussion thread and proof-claim tab), credits the proof to this paper; Bloom took no part in the paper, and the community database records the problem as proved. Theorem B, the sketch and the derivation of Theorem B from Claims 2.5--2.7 were read; the proofs of the claims were read for structure only, and no case analysis was checked. No independent review of the proof is recorded in this repository and none is claimed; no second paper attesting the theorem is on record.

Formalization, not evidence. A public Lean 4 development in Boris Alexeev's lean-proofs repository, Erdos577.lean with its supporting modules under Erdos577/ (linked above at a pinned revision; the file entered the repository on 2026-08-28), says in its docstring that its proof follows Theorem B of this paper, and its theorems erdos_faudree and erdos_577 state Theorem B for every $k$, with $k=0$ and $k=1$ handled explicitly. The corpus has not built or audited the development, so it gives no formalized evidence and the evidence stays reviewed and refereed.

Depends on. Nothing in this wiki: the proof is the paper's.