---

The statement as the site displays it asks for a prime divisor $p<n/2$ of $\binom nk$ whenever $1<k<n-1$, apart from $\binom73$. It is false: $\binom42=6$ has the prime divisors $2$ and $3$, and no prime is below $4/2=2$. The Lean file Erdos384.lean in Boris Alexeev's repository of Lean proofs (first committed 2026-08-17; the link pins the 2026-09-15 revision) states this strict formulation as Erdos384StrictStatement, with $2p<n$ for $p<n/2$ and the exception at both $(7,3)$ and $(7,4)$, and proves its negation not_erdos_384 from that witness. The file's header names Ecklund as the informal author and the AI systems Codex and GPT-5.6 Sol as its formal authors, and says that the non-strict bound $p\leq n/2$ of Ecklund's theorem is the one that holds; the submitter of the repository is the claimant here. The same observation appears on this corpus's problem page with the witness $\binom62=15$, whose prime divisors are $3=n/2$ and $5$, and a comment of 2026-02-04 in the site's discussion thread had already pointed out that Ecklund's bound is $p\leq n/2$ while the page prints $p<n/2$.

The refutation rests on nothing but the arithmetic of the witness. Ecklund's theorem, on the page Ecklund 1969, proves the corrected Statement and plays no part in it.

Why it is rejected. It answers the site's wording, not the corrected statement. Problem 384 judges the corrected Statement, with the bound $p\leq n/2$ that Erdős and Graham's own report of the problem requires and that Ecklund's theorem proves; the problem page's Notes give the evidence. The witness $\binom42=6$ has the prime divisor $2=n/2$, so it is no counterexample to the corrected Statement, whose only exception is $\binom73=\binom74=35$, and the refutation settles no instance of it. The record is kept because the formal-conjectures record names the file as the formal proof of its strict variant, and the site's Lean qualification dates from the file's last change; the problem page's Notes credit the result.

Standing. The site's curator labels the problem proved and credits Ecklund's theorem, so no outside reviewer has accepted a refutation of the problem; and the Lean file is third-party work that this corpus has not built or audited, so it gives a formalization link and no formalized evidence. The formal-conjectures record at the linked commit tags the variant erdos_384.variants.strict as answer(False) and names this file as its formal proof; the file's last change, on 24 August 2026, is the date from which the community database records the formal status Lean shown in the site's label.