---

Claim. The answer to Problem 927 is no: $g(n)$, the largest number of different sizes of cliques (maximal complete subgraphs) in a graph on $n$ vertices, is not $n-\log_2n-\log_*n+O(1)$. The claimed result is the main bound of J. H. Spencer, On cliques in graphs, Israel J. Math. 9 (1971), no. 4, 419--421 (p. 419, logarithms to the base $2$): for every $N>33000$, $g(N)\ge N-\log N-4$. The paper reprints Erdős's question, printed as whether $\lim(g(n)-(n-\log n))=\infty$; since Moon and Moser's upper bound keeps $g(n)-(n-\log n)$ below $1$, the divergence in question is that of $(n-\log n)-g(n)$, and the paper answers it negatively by an explicit graph in the style of Moon and Moser and of Erdős's 1966 construction, with blocks of sizes $2^{i-1}+1$ whose unions realize a clique of every size from $3$ to about $N-\log N$, padded in two further cases to cover every $N$ between consecutive block counts. The refutation is one line: if $g(n)\le n-\log_2n-\log_*n+C$ for all large $n$, then Spencer's bound gives $\log_*n\le C+4$ for every $n>33000$, which fails since $\log_*n\to\infty$. With Moon and Moser's upper bound $g(n)\le n-\lfloor\log_2n\rfloor$ for $n\ge4$ (their claim page) the result is $g(n)=n-\log_2n+O(1)$, the estimate the site records. The constant $4$ is the paper's headline as printed; by the construction's own counts the third of its three cases, the window $2^n+2^{\lfloor n/2\rfloor-2}\le N<2^{n+1}$, realizes only $N-\lfloor\log_2N\rfloor-5$ clique sizes, so the counts give $N-\lfloor\log_2N\rfloor-5\le g(N)\le N-\lfloor\log_2N\rfloor$ for $N>33000$, with $-4$ outside that window; the disproof needs only a fixed constant.

Acceptance. Refereed: Israel Journal of Mathematics (Crossref record accessed: volume 9, issue 4, pp. 419--421, issued February 1971; the day is the issue's nominal first day, used for this page's date). Reviewed: Erdős himself attests the result in the note added in proof to item 10 of his 1971 problem list (item_10, printed p. 101), and the site's curator, Thomas Bloom, labels the problem disproved and credits the paper with $g(n)>n-\log_2n-O(1)$. The source has a library source card. Read depth: the definitions, the question and the main bound clause by clause, and the construction in full with its vertex counts followed; its clique checks are not checked, and the closing bounds use a bracket the paper leaves undefined, a filing observation that does not touch the disproof. The acceptance rests on the publication, Erdős's attestation and the site's acceptance; nothing is independently reviewed by this project.

Formalization. The file Erdos927.lean (93,655 bytes, 2,130 lines) of a GitHub gist at its only revision, committed 2026-06-05 (the formalization link above), declares itself a formalization of Spencer's disproof: its header names John Jennings and the automated formalization system Aristotle (Harmonic) as authors, and its docstring cites the paper and its headline bound. The account JohnJennings announced it on the problem's discussion thread the same day, saying that Aristotle had formalized Spencer's disproof in Lean 4, with a link to a Lean web editor page loading the gist against Mathlib v4.28.0. The file defines g n as the largest number of maximal-clique sizes over graphs on Fin n and logStar as the iterated-logarithm count with the site's threshold; encodes the conjecture as erdos927_conjecture : ∃ C : ℕ, ∀ n : ℕ, n ≥ 2 → g n + Nat.log 2 n + logStar n ≤ n + C, the upper half of the problem's formula, $g(n)\le n-\lfloor\log_2n\rfloor-\log_*n+C$, whose negation is what the disproof needs; builds a graph spGraph n on spN n vertices and proves spencer_lower_bound : spN n ≤ g (spN n) + Nat.log 2 (spN n) + 6 for n ≥ 16, the constant $6$ along a sequence of $N$ where the paper has $4$ for every $N>33000$; and ends with theorem erdos927_disproof : ¬ erdos927_conjecture. It imports Mathlib, has no sorry and no axiom, and uses native_decide five times, which puts the compiled evaluator inside what the proof trusts. Two further copies are linked above: the file src/latest/ErdosProblems/Erdos927.lean of Boris Alexeev's repository plby/lean-proofs (in the repository since 2026-08-26, linked at the commit of 15 September 2026), whose header names Spencer's paper as the informal proof and John Jennings and Aristotle (Harmonic) as the formal authors, says that Jake Mallen replaced the native evaluation with kernel-checked proofs, and cites the gist and the copy in the repository Jayyhk/erdos-lean (linked at its commit of 25 August 2026); the lean-proofs file proves not_erdos_927, that no constant bounds $g(n)+\lfloor\log_2n\rfloor+\log_*n-n$ from above for all large $n$, and records the axioms propext, Classical.choice and Quot.sound in a comment. All three are self-declared formalizations of Spencer's disproof; the formal-conjectures statement erdos_927 names the lean-proofs file in its formal_proof attribute (the problem page records that file). This project has not built, replayed or audited any of them, so the page lists no formalized evidence. The disproof rests on the refereed paper, not on these files.