---

Claim. Linmiao Xu's Lean 4 development Erdős #1054: sums of smallest divisors, registered in the Palomar registry as PALOMAR-2026-10-05-000005 on 5 October 2026, proves the three formal-conjectures statements of the problem with the answers (i) no, (ii) no and (iii) yes: $f(n)$ is not $o(n)$; it is not $o(n)$ on any set of natural density one; and $\limsup f(n)/n=\infty$ along every set of density one. Its README adds a lower density at least $c/(A^3(1+\log A)^4)$ for the odd $n$ with $f(n)>An$, a small-ratio bound $\#\{n\le X: 0<f(n)\le\delta n\}\le C\delta^3X$, and $f(2)=f(5)=0$ in the formal-conjectures convention for unrepresented values.

It is an independent proof, not a formalization of a named claimant's manuscript. It adapts the divisor-prefix sieve and the almost-all binary Goldbach modules of the Principia Math development (an earlier revision of the repository linked from [[problems/divisors/E1054/claims/2026_06_22_principia_math|Principia Math's claim page]]) and modules of the PrimeNumberTheoremAnd project, under their licenses. The README reports that none of its modules uses sorry and that the exported theorems depend only on propext, Classical.choice and Quot.sound.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-05-000005:

A complete Lean 4 proof of all three parts of Erdős problem 1054. For the least integer f(n) whose k smallest divisors sum to n, we prove that f(n) is not o(n), is not o(n) on any density-one set, and satisfies limsup f(n)/n = ∞ on every density-one subtype. Building on the qualitative divisor-prefix sieve and almost-all binary Goldbach proof from Principia-Math-Solutions, this formalization proves the Formal Conjectures statements along with a sharp second-moment lower-density bound c / [A^3 (1 + log A)^4] for odd n with f(n) > A n, the Tao–Kovač small-ratio upper bound #{n ≤ X : 0 < f(n) ≤ δ n} ≤ C δ^3 X, liminf_{f(n)>0} f(n)/n = 0, and the asymptotic density equivalence between {s(2d)} and even aliquot values.

Depends on. [[problems/divisors/E1054/claims/2026_06_22_principia_math|Principia Math's limsup theorem]], whose Lean modules the development adapts.

Standing. Claimed. The registry replays the proof in Lean kernels and records a model review by GPT-6 Sol through Codex with a neutral outcome, which is not an independent review; no refereed publication is recorded, and the site labels the problem OPEN. It is third-party Lean that this corpus has not built or audited, so no formalized evidence is listed. Nothing here is independently reviewed by this project.