{"id":"palomar/PALOMAR-2026-10-12-000001","url":"https://github.com/tokengr1nder/Erdos252/tree/575f822540523120bcfc9e0d59fcbf731fa8b7b9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000001-v1.json","repo":"https://github.com/tokengr1nder/Erdos252","tags":["math.NT","msc:11J72","number-theory","irrationality","lean-formalization"],"score":0,"title":"Erdős 252: irrationality of the factorial divisor-sum series","trust":"high","domain":"math.NT","source":"palomar","authors":["Tokengrinder"],"reviews":0,"subject":"math.NT","summary":"For every natural number k, the series whose nth term is the sum of the kth powers of the positive divisors of n, divided by n factorial, is irrational. This gives the positive-exponent statement of Erdős problem 252 and also includes exponent zero. The proof combines factorial-tail integrality, a finite coprime dilation grid with exact finite-difference cancellation, and incompatible progression means obtained by a fresh-prime refinement. It has no prime-pattern conjecture or unproved number-theoretic hypothesis. The Lean development also proves convergence and the equivalence of its…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true}