Proved. The statement is the Hajnal--Szemerédi theorem of 1970 in its clique form. The status-defining text is Theorem 1 of Kierstead, Kostochka, Mydlarz and Szemerédi, A fast algorithm for equitable coloring, Combinatorica 30 (2010), 217--224 (refereed): "Every graph with maximum degree at most $r$ has an equitable $(r+1)$-coloring", which the paper attributes to Hajnal and Szemerédi (1970) as a theorem "which had been conjectured by Erdős" and proves again in its Section 2. The one-line transfer to the site's statement is written below. The site's two proof sources are not held: the original proof [HaSz70] (a Bolyai Society volume of 1970, print only) and the short proof [KiKo08] (Combin. Probab. Comput. 17 (2008), 265--270), so their exact statements are known through the 2010 paper's attribution and the site; the cases $r=2$ (Dirac's theorem, claim page (Dirac, 1952)) and $r=3$ ([CoHa63], not held; claim page (Corrádi–Hajnal, 1963)) are second-hand, each an accepted partial claim on the site's credit and its journal publication. Acceptance evidence: the refereed 2010 paper, which states the theorem and proves it; the site's label; the community database. The site's "(LEAN)" attaches to an external Lean proof of the clique form, inspected statically and described under Formalization; it gives no formalized evidence. The claim pages are Hajnal and Szemerédi (accepted on the site's credit and Kierstead and Kostochka's independent refereed proof; the 2010 paper shares an author with it), Kierstead and Kostochka and Kierstead, Kostochka, Mydlarz and Szemerédi (accepted, refereed), from which the frontmatter standing is derived; the external Lean proof behind the site's suffix declares itself a formalization of Kierstead and Kostochka's proof and is recorded as a formalization link on their page; this project has not built it.