---

Claim. Let $SF(N)$ be the largest size of a subset of $\{1,\ldots,N\}$ no nonempty subset of which has a square sum. There are absolute constants $C_*$ and $N_0$ with $SF(N)\le C_*N^{1/3}(\log\log N)^{16}$ for every $N\ge N_0$ (the note takes logarithms base $2$ and the Lean statement the natural logarithm, a difference the constant absorbs). With the development's lower bound $N^{1/3}/4\le SF(N)$ for $N\ge64$, Erdős's construction, this gives $N^{1/3-\varepsilon}\le SF(N)\le N^{1/3+\varepsilon}$ for large $N$ and every $\varepsilon>0$, the order $N^{1/3+o(1)}$ that answers Problem 587 as the Formulation on that page reads it, and it does so without Lemma 4.2 of Nguyen and Vu, the step the same development disputes (recorded on their page). The proof is the note Independent reconstruction of the log-log bound for Erdős 587, headed as a proof dated 27 August 2026, in Boris Alexeev's repository plby/lean-proofs, and its Lean formalization: the file Erdos587.lean states loglog_upper_bound, the bound $K\,N^{1/3}\max(1,\log\log N)^{16}$ for large $N$, lower_bound, and erdos_587, the two-sided bound with exponents $1/3\mp\varepsilon$. The note builds on a resilient seed theorem and an iterated-sumset lower bound from Conlon, Fox and Pham's Homogeneous structures in subset sums and non-averaging sets (arXiv:2311.01416) and on divisor-sum estimates of Koukoulopoulos and Tao and of Nair and Tenenbaum; it says that it is not the unavailable manuscript of Conlon, Fox and Pham and that it leaves the development's logarithmic proof of Nguyen and Vu's bound unchanged. The argument was not checked here.

Claimant. The note names no author. The Lean file's header names Nguyen and Vu as informal authors and Codex and GPT-5.6 Sol as formal authors, and Alexeev's repository posts both; the page carries the repository owner's slug. The reconstruction is recorded as its own result, not as a formalization of the paper, because it proves a bound the paper does not and avoids its disputed lemma.

Acceptance. None: nothing is refereed, no outside reviewer has examined the development, the site's page does not mention it, and this corpus has not built or audited it, so no formalized evidence is listed.

Depends on. No page of this wiki.