---

Claim. Let $A\subseteq\mathbb N$ be an infinite arithmetic progression and let $f:A\to\{-1,1\}$ be non-constant. Then some finite non-empty $S\subset A$ has $\sum_{n\in S}f(n)/n=0$: every infinite arithmetic progression has property $P_1$, the first question of Problem 318. The proof is the Lean development in Boris Alexeev's repository of formalized Erdős problems, added on 16 August 2026 and linked above at a pinned commit. Its theorem erdos_318.variants.infinite_AP states the result with the P₁ predicate of the formal-conjectures statement file, for a set A with A.IsAPOfLength ⊤, and its proof normalizes the progression to $\{a+id\}$ and builds the zero-sum from two elements of opposite sign through a density lemma for two-colorings of the progression. The same file proves not_erdos_318, that the odd numbers together with $2$ form a set of density $1/2$ without $P_1$ (the second question, recorded as a formalization link on the Erdős page), the variants univ and odd (the cases $A=\mathbb N$ and the odd numbers), and the trivial failure squares with $1$ included; it also records that the statement file's auxiliary contain_single_even variant is false as stated, since $\{2\}$ has exactly one even member and $P_1$ vacuously. The file declares no axiom and contains no sorry.

Covers. The first of the problem's three questions, infinite arithmetic progressions, the part that Sattler's accepted theorem settles from the literature; this page records the independent machine proof of the same statement. The squares question is settled on Larsen's page.

Depends on. No page of this wiki.

Claimant and standing. The file's header calls it a Lean formalization of a solution to Problem 318, names Paul Erdős as its informal author and Codex and GPT-5.6 Sol as its formal authors, and cites only the problem's thread and the statement file; it does not mention Sattler's 1982 paper, so the progression proof is recorded as the repository's own result rather than as a formalization of Sattler's theorem, with the repository's owner as the claimant. On 18 September 2026 the formal-conjectures repository attached formal_proof attributes pointing at this file to its declarations erdos_318.variants.infinite_AP, variants.univ and variants.odd; the community database records the problem's formal status as Lean, as of that entry's last update on 16 September 2026, through Collin Yuanjie Ren's package for the squares, which reproduces this file's progression and density parts as credited prior work. The site's page does not mention the development, no outside reviewer has examined it, and this corpus has not built or audited it, so the claim is pending and the link gives no formalized evidence.