The site labels the problem DISPROVED (LEAN); its Lean clause is treated under Formalization. The refuting paper is Spencer's [Sp71] (Israel J. Math. 9 (1971), 419--421; a refereed journal): with a clique a maximal complete subgraph and all logarithms to the base $2$, "for $N$ sufficiently large ($>33000$ will do) $g(N)\ge N-\log N-4$" (p. 419; paged at Spencer 1971, Main bound (p. 419)). Its result is also attested in print by Erdős himself, in the note added in proof to item 10 of his 1971 problem list ([Er71], printed p. 101: "Spencer proved $f(n)>n-\frac{\log n}{\log2}-c$", where the paper's $f(n)$ is this page's $g(n)$), and the site's curator, Thomas Bloom, accepts it, crediting Spencer with $g(n)>n-\log_2n-O(1)$. With the upper bound of Moon and Moser, $g(n)\le n-[\log_2n]$ for $n\ge4$ ([MoMo65], Theorem 4, printed p. 27; paged at Moon and Moser 1965, Theorem 4 (p. 27); its claim page (Moon and Moser, 1965)), this gives $g(n)=n-\log_2n+O(1)$, the site's estimate. The constant $4$ is the paper's headline as printed; the construction's own counts realize only $N-[\log_2N]-5$ clique sizes in the third of its three cases, the window $2^n+2^{\lfloor n/2\rfloor-2}\le N<2^{n+1}$, and $-4$ or better elsewhere, so what the printed argument delivers for every $N>33000$ is $N-[\log_2N]-5\le g(N)\le N-[\log_2N]$ (authored, from the two printed bounds, the card's counts and the integrality of $g$); any fixed constant refutes the conjecture. The bracket $\{\log N\}$ in the paper's closing bounds is undefined in print, and the card records the reading the counts fix (a filing observation, not a review verdict). The Lean file named in the site's discussion thread encodes a construction with $g(N)\ge N-\lfloor\log_2N\rfloor-6$ along a sequence of $N$ (Formalization). The claim page is Spencer (accepted on the refereed publication, Erdős's attestation and the site's acceptance); the bounds of Moon and Moser and of Erdős 1966 are accepted partial claims on the estimate. The Lean developments that declare themselves formalizations of his disproof, the gist of June 2026 and the lean-proofs copy that formal-conjectures names, are formalization links on that page, not built by this project, and add no evidence. The frontmatter is derived from it; the label's Lean clause is a separate matter (Formalization).