---

Larsen proves that for every $\varepsilon>0$ there is an integer $L$ such that every integer $n$ with $\sigma(n)/n>2+\varepsilon$ and no prime factor below $L$ is a sum of distinct proper divisors of itself (the paper's Theorem 1), and deduces an absolute constant $C$ such that every positive integer $n$ with $\sigma(n)\ge Cn$ is such a sum (its Corollary 5). The deduction fixes $\varepsilon=1/10$, passes to the part $m$ of $n$ free of primes below $L$, and notes that if $m$ is not such a sum then $\sigma(n)/n$ is at most $(\sigma(m)/m)\prod_{p<L}p/(p-1)$, a bounded quantity; a multiple of a pseudoperfect number is pseudoperfect. The corollary is the problem's statement, so the answer is yes. The proof recasts the question as writing $1$ as a sum of reciprocals of divisors of $n$, groups the prime factors of $n$ into dyadic blocks, approaches $1$ greedily with controlled slack, and closes the gap with a circle-method count of subset sums of reciprocals. The site's commentary records that $C>2$ is necessary, since $70$ is abundant and not such a sum. The manuscript, its versions and its statements are described on the source card Larsen 2026. The first link is the eight-page manuscript uploaded to the Erdos-825 repository on 2026-01-31; the repository's commit of 2026-02-01 added only its TeX source, with typo fixes. The second link is the nine-page version in the Erdos-318 repository, which also carries the squares result for Problem 318; it replaced on 2026-02-01 a first upload of 2026-01-31 that presented Theorem 6 tentatively and left its check of Hypothesis 3 undone, and the replacement rewrites the proof of Theorem 6, fixes typos and states the range of $h$ in the proof of Theorem 1.

Formalization. The third link is a Lean 4 proof of the argument whose theorem erdos_825 states that there is a real $C>0$ such that every natural number $n$ with $\sigma(n)>Cn$ equals the sum of some set of its proper divisors; the statement is the one the formal-conjectures project wrote for the problem in its statement file, with $\sigma$ Mathlib's ArithmeticFunction.sigma 1 and the divisor set Nat.properDivisors. The file's header declares it a formalization of a solution to the problem, names Larsen as the author of the informal proof, the formal-conjectures authors as the authors of the statement, and OpenAI's Codex and GPT-5.6 Sol as the formal authors; it builds against Lean 4.33.0 and Mathlib v4.33.0, runs to 5,911 lines, and follows Larsen's argument through a rough-number reduction, a controlled greedy construction and a weighted unit-fraction circle method, importing the repository's Fourier-analytic unit-fraction modules. The commit adding the file is dated 2026-08-15 by its author and 2026-08-16 by its committer; the link carries the author date. The pinned file contains no sorry, axiom or native_decide; this corpus has not built or audited it, so its axiom closure is unverified and formalized is not listed as evidence.

Acceptance. Reviewed: the site's curator, Thomas F. Bloom, affirmed the argument on the discussion thread on 2026-01-31, noting that it also answers Erdős's further question of using only divisors at most $\varepsilon n$, and the problem page records the problem solved in the affirmative by Larsen (last edited 2026-02-01); the community database records the informal status proved as of 2026-01-31. No refereed version of the manuscript is recorded. Both versions of the manuscript, the eight-page file and the nine-page file, close with the sentence "We acknowledge the assistance of Claude Opus 4.5 and ChatGPT 5.2 Pro for proofreading." After the formalization, the site labels the problem PROVED (LEAN) (page last edited 1 February 2026), the community database records the formal status Lean as of 2026-08-23, and the formal-conjectures statement file, at the commit linked above, marks erdos_825 research solved with its formal-proof attribute pointing at the pinned Lean file. The problem page is Problem 825.