{"id":"palomar/PALOMAR-2026-09-25-000018","url":"https://github.com/realazthat/zeta5-lean2/tree/2fa4e829816e1d4a4f61249cb758e67195d46806","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000018-v1.json","repo":"https://github.com/realazthat/zeta5-lean2","tags":["math.NT","msc:11J72","msc:11M06","irrationality","zeta-function","lean-formalization"],"score":0,"title":"Irrationality of the Riemann zeta value at five","trust":"high","domain":"math.NT","source":"palomar","authors":["Azriel Fasten"],"reviews":0,"subject":"math.NT","summary":"Formalization of the irrationality claim for the real value of the Riemann zeta function at five in Aabir Fauzan's September 2026 preprint. The two compared statements assert irrationality of this zeta value and of the sum of reciprocal fifth powers. The development constructs integer polynomials using normalized Hankel determinants, proves positivity and decay estimates, and derives irrationality. The paper's quantitative irrationality-measure claim is not part of this submission.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"ζ(5) is irrational","identifier":"doi:10.5281/zenodo.22826419","relationship":"formalizes"}]}