{"id":"palomar/PALOMAR-2026-10-05-000005","url":"https://github.com/linrock/math-proofs/tree/0917cd01090b52088aa82b09c8c84689047b8171/erdos-1054","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-05-000005-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.NT","msc:11A25","msc:11N36","msc:11P32","number-theory","divisors","erdos-problems","lean-formalization"],"score":0,"title":"Erdős 1054: sums of smallest divisors","trust":"high","domain":"math.NT","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.NT","summary":"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 0}…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-05","reactions":{},"formalized":true,"formalizes":[{"title":"Principia Erdős 1054 proof and almost-all Goldbach master","identifier":"https://github.com/antoshashakov/Principia-Math-Solutions/tree/c9910942522fbd3a07c034ac57947f56df6f0f6d/erdos1054","relationship":"adapts"}]}