{"id":"palomar/PALOMAR-2026-10-22-000039","url":"https://github.com/wcook04/plectis-erdos-lean/tree/8d47efd230e041b76b8233a49164ca798977053c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000039-v1.json","repo":"https://github.com/wcook04/plectis-erdos-lean","tags":["math.NT","msc:11J72","msc:11J82","msc:33D15","irrationality","lambert-series","hypergeometric-series","number-theory"],"score":0,"title":"An explicit rational-base irrationality region for Zudilin's Lambert series","trust":"high","domain":"math.NT","source":"palomar","authors":["Will Cook"],"reviews":0,"subject":"math.NT","summary":"For coprime integers a > b >= 1 satisfying b^μ < a, equivalently log b / log a < θ*, the selected Lean theorems prove irrationality of F(a/b). They include the base 31/4 and every positive integer power, plus associated irrationality-measure bounds. The region excludes 3/2. This configuration does not select the paper's later sharp fixed-base asymptotic or all-rank Hankel results.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Zudilin's forms at rational bases and exact normalised Hankel order","identifier":"https://github.com/wcook04/plectis-erdos/blob/147f3f1da400a84dcb3013ea6cef75dc8f382b09/paper/1049/erdos-1049-rational-base-lambert.pdf","relationship":"formalizes"},{"title":"Complete reasoning record for Erdős problem 1049","identifier":"https://github.com/wcook04/plectis-erdos/blob/147f3f1da400a84dcb3013ea6cef75dc8f382b09/paper/1049/erdos1049-rational-base-lambert-reasoning-surface.pdf","relationship":"formalizes"},{"title":"Heine's basic transform and a permutation group for q-harmonic series","identifier":"doi:10.4064/aa111-2-4","relationship":"adapts"}]}