---

Claim. For every partition of the perfect squares greater than $1$ into two non-empty parts $X$ and $Y$ there are non-empty finite $X'\subseteq X$ and $Y'\subseteq Y$ with $\sum_{x\in X'}1/x=\sum_{y\in Y'}1/y$. With $X=f^{-1}(1)$ and $Y=f^{-1}(-1)$ for a non-constant $f$ on $A=\{n^2:n\ge2\}$, the set $S=X'\cup Y'$ is a finite non-empty subset of $A$ with $\sum_{n\in S}f(n)/n=0$, and conversely such an $S$ yields the two subsets; so the squares other than $1$ have property $P_1$, the affirmative answer to the third question of Problem 318. The result is Theorem 6 of the manuscript filed as larsen_2026_sufficiently_abundant_numbers_pseudoperfect, whose result page theorem_6 writes out both directions of the equivalence.

Covers. The third of the problem's three questions, the squares other than $1$. The arithmetic-progression and positive-density questions have their own claim pages.

Source. Daniel Larsen, Sufficiently abundant numbers are pseudoperfect, a nine-page manuscript posted as 318.pdf in the author's GitHub repository Larsen-Daniel/Erdos-318; the linked copy is the file at the commit of 1 February 2026, which replaced an upload of 31 January 2026 whose eight pages contained no Theorem 6. Theorem 6 is on p. 8 and its proof on pp. 8--9: a greedy adjustment of the target followed by the paper's circle-method Theorem 4, the tool of its main result that every integer with a large enough abundance index and no small prime factor is pseudoperfect, the question of Problem 825. The paper's closing line acknowledges the AI systems Claude Opus 4.5 and ChatGPT 5.2 Pro for proofreading. The author announced the note in the problem's thread on 1 February 2026 as an application of that technical result. The manuscript is unrefereed, is not on arXiv and has no journal record; the proof is unverified by this corpus.

Acceptance. The site's curator, Thomas Bloom, writes in the commentary of the problem page that Larsen has proved the squares case, and the problem carries the label SOLVED (last edited 1 April 2026); the curator is independent of the author, and that credit is the reviewed evidence. No independent review and no refereed version were found. The formal-conjectures file for the problem states the squares case (erdos_318.parts.ii) with the docstring crediting Larsen and a sorry body; a statement file is not a formalization and is not linked here. Sattler's two 1982 papers announced a proof of this case that never appeared.

Formalization link. Collin Yuanjie Ren's Lean package of 16 September 2026, linked above at a pinned commit, calls itself a formalization of Larsen's result, prepared with OpenAI Codex: it proves the partition statement above and the formal-conjectures declaration erdos_318.parts.ii, and its README reports that both endpoints rest on the axioms propext, Classical.choice and Quot.sound alone, with no sorry or native evaluation. The package reproduces, as credited prior work, the progression and density parts of the earlier file in Boris Alexeev's repository (see the Lean proof of the progression question). The community database records the problem's formal status as Lean through this package, as of that entry's last update on 16 September 2026. This corpus has not built or audited it, so the link gives no formalized evidence.