{"id":"palomar/PALOMAR-2026-10-11-000021","url":"https://github.com/daizisheng/erdos-824/tree/b4b7099bb8ab9c1c7fc61dae18a73cdbe503fe5a/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000021-v1.json","repo":"https://github.com/daizisheng/erdos-824","tags":["math.NT","msc:11N25","msc:11A25","analytic-number-theory","shifted-primes","lean-formalization"],"score":0,"title":"Erdős Problem #824 under a smooth shifted-prime hypothesis","trust":"high","domain":"math.NT","source":"palomar","authors":["Shisheng Li","Zhong Zhuang"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of the conditional lower bound for the number h(x) of pairs of coprime positive integers a 0 and all sufficiently large natural x. The argument adapts Pollack and Pomerance's finite counting method. A⁺ itself, the squarefree strengthening, and the accompanying paper's argument relying on the WD preprint are not formalized here.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Coprime pairs with equal sum of divisors, assuming smooth shifted primes","identifier":"","relationship":"formalizes"},{"title":"Some problems of Erdős on the sum-of-divisors function","identifier":"","relationship":"adapts"}]}