---

Claim. The answer to Problem 469 is yes: $\sum_{n\in A}1/n$ converges, where $A$ is the set of primitive pseudoperfect numbers, the integers that are sums of distinct proper divisors of themselves while no proper divisor is. The manuscript, Zachary J. Lewis, Convergence of the Reciprocal Sum of Primitive Semiperfect Numbers, preprint revision 1.2.1 of 2026-07-13 in the repository linked above at its pinned commit, uses "semiperfect" for pseudoperfect. Its argument attaches to each weird number $n$ (abundant but not pseudoperfect) a gap $g(n)$ and the state parameter $\sigma(n)/g(n)$, proves exact formulas for how both change when $n$ is multiplied by a new prime $p$, and organizes these coprime prime extensions into a tree whose edges are either candidate primes, controlled by a Kraft-type potential, or forced primes, controlled by an exponentially damped potential; a finite bootstrap disposes of the remaining bounded states. The outcome is a uniform bound on the reciprocal mass of any prefix-free family of extensions that first become pseudoperfect. Every primitive pseudoperfect number is then reduced either to a primitive nondeficient number or to a decorated weird root that is itself primitive nondeficient, and the tree bound together with Avidon's count of primitive nondeficient numbers makes the sum over roots converge. The problem's source, Benkoski and Erdős 1974, conjectured the convergence through a count $O(x/(\log x)^k)$ of primitive pseudoperfect numbers up to $x$; the manuscript proves the convergence of the sum, not that count.

Submission note. Posted to erdosproblems.com as a proof claim by Zachary J. Lewis (account ZachL111) on 14 July 2026, giving "GPT-5.6 Sol Ultra (OpenAI Codex) and Anthropic Claude Fable 5" as the AI used, which the site marks as accepted as correct:

The manuscript claims that the reciprocal sum of primitive semiperfect numbers converges. For a weird integer n, it introduces a gap $g(n)$ and state parameter $\tau(n)=\sigma(n)/g(n)$, then proves exact transition formulas for coprime prime extensions np. These extensions are organized into a candidate/forced prime tree. A Kraft-type potential controls candidate edges, while an exponentially damped potential controls forced excursions. A finite bootstrap handles the remaining bounded states, giving a uniform reciprocal-mass bound for prefix-free families of first-semiperfect extensions. Every primitive semiperfect number is then reduced either to the primitive nondeficient case or to a decorated weird primitive-nondeficient root. The tree bound and Avidon's counting estimate make the resulting root sum convergent. The accompanying Lean 4 development contains an unconditional kernel-checked theorem and a literal formalization of the problem statement. Notes: The manuscript was submitted to arXiv in math.NT on July 14, 2026 and is currently awaiting moderation and public announcement. The Lean theorem is kernel checked, but independent human review of the manuscript, the formal definitions, and the correspondence between the manuscript and formalization remains pending. Computational assistance is disclosed in the manuscript. I am submitting this as a claimed proof and am not attempting to represent it here as peer reviewed or independently certified.

Formal verification by the author. The repository's formal/ folder, linked above at the same commit, holds a Lean 4 development pinned to Lean 4.31.0 and Mathlib, whose theorem Erdos469.erdos469 states that the reciprocals of the primitive semiperfect numbers are summable, with no hypotheses, and whose Erdos469.erdos469_problem_statement restates the result for a membership predicate written directly from the problem's words (positive integers, proper divisors, finite sets of distinct divisors, finite sums) and proved equivalent to the development's definition. The author's audit reports the axioms propext, Classical.choice and Quot.sound only, with no sorry, project axiom or native decision shortcut, over 2,413 public theorems.

Claimant. Zachary J. Lewis, an independent researcher posting under the forum account ZachL111, published the manuscript and its Lean development in Lewis's repository on 2026-07-13, the date the page carries, submitted the claim to the site's proof-claims tab on 2026-07-14 and takes responsibility for the mathematics. Lewis's disclosure names GPT-5.6 Sol Ultra, accessed through OpenAI Codex, for proof exploration, checking of intermediate arguments, exposition, finite diagnostic computations and the development and review of the Lean formalization, and Anthropic Claude Fable 5 for a separate model-based audit; the site credits the result to Lewis using GPT 5.6 and Claude Fable 5. The claim's notes say the manuscript was submitted to arXiv on 2026-07-14 and was awaiting moderation; no arXiv or journal record of it was found on 2026-10-07. At submission the author stated that independent human review of the manuscript and of its correspondence with the Lean definitions was still to come.

Acceptance. Thomas Bloom, the site's curator, marks the problem proved with a Lean qualification and credits Lewis on the problem page (edited 2026-09-01). In the problem's discussion thread, Boris Alexeev reported on 2026-07-21 that Alexeev had verified the formalization of the claim, and the same day the development entered Alexeev's repository of formalized Erdős problems; on 2026-07-22 Alexeev appended the density result below, and on 2026-07-27 Alexeev added the repository's index page, linked above at a pinned commit, and announced the density result in the thread. Its Erdos469 file names Lewis and the two systems as informal authors, GPT-5.6 Sol Ultra and Lewis as formal authors, restates the theorem for the problem's set $A$, and also proves that the pseudoperfect numbers have a natural density strictly between $0$ and $1$, trapped between $1/6$ and $\pi^2/6-1$, the density result of Erdős's 1970 paper that a thread comment of 2026-07-21 said the convergence could simplify. A single-file Lean version of the proof, which declares itself a formalization of Lewis's preprint obtained by Aristotle of Harmonic and was posted in the Woett repository on 2026-07-14, is linked above at its commit. This corpus has built and audited none of these developments, so no formalized evidence is listed, and the problem's own statement file in formal-conjectures is not a proof. The claim is accepted on the curator's documented acceptance and Alexeev's independent check of the formalization.