---

Claim. Let $A\subseteq\mathbb N$ be infinite with exactly one even element $x$, and put $f(x)=-1$ and $f(n)=1$ for $n\in A\setminus\{x\}$; $f$ is non-constant. No finite non-empty $S\subset A$ has $\sum_{n\in S}f(n)/n=0$: such an $S$ would contain $x$ (otherwise the sum is positive) and would give $1/x=\sum_{n\in S\setminus\{x\}}1/n$, a fraction with an even denominator in lowest terms equal to a sum of fractions with odd denominators, whose lowest-terms denominator is odd. The odd numbers together with $2$ form such a set of density $1/2$, so the second question of Problem 318, whether every set of positive density has property $P_1$, is answered in the negative.

Covers. The second of the problem's three questions, sets of positive density. The arithmetic-progression and squares questions have their own claim pages.

Source and acceptance. The observation is published on the opening page of R. Sattler, On Erdös property $P_1$ for the sequence of squarefree numbers, Indagationes Mathematicae (Proceedings) 85 (1982), no. 3, 341--346, DOI 10.1016/1385-7258(82)90025-7, a refereed article that credits it to Erdős; the page is filed under Erdős as the result's author and dated by the article, whose Crossref record gives the year 1982 and, as its only day, the start of its first license, 1 January 1982. The site's curator, Thomas Bloom, records the failure for every set with exactly one even number in the commentary of the problem page (label SOLVED, last edited 1 April 2026) and attributes it through Sattler to Erdős; the curator is independent of the authors, and that record is the reviewed evidence. The article is not held in the library; the attribution rests on the site and on a thread comment of 17 August 2025 that reports it. The argument above is elementary and is written out in full on the problem page. A thread comment of 15 August 2025 gives the same argument and generalizes it to sets $A$ with an element $x$ such that $A\setminus\{x\}$ lies in a multiplicatively closed set containing no multiple of $x$; the comment is recorded here and has no page of its own.

Formalization link. The Lean file in Boris Alexeev's repository of formalized Erdős problems, added on 16 August 2026 and linked above at a pinned commit, calls itself a formalization of a solution to Problem 318 with Erdős as its informal author and Codex and GPT-5.6 Sol as its formal authors. Its theorem not_erdos_318 exhibits the odd numbers together with $2$ (densityCounterexample) as a set of density $1/2$ without property $P_1$ (densityCounterexample_hasDensity, densityCounterexample_not_P₁), the argument above, and so proves the formal-conjectures declaration erdos_318.parts.i, which carries no formal_proof attribute. The same file's proof for arithmetic progressions has its own page, the Lean proof of the progression question, and Collin Yuanjie Ren's package of 16 September 2026, linked on Larsen's page, reproduces the density part as credited prior work. This corpus has built and audited neither development, so the link gives no formalized evidence.