{"id":"palomar/PALOMAR-2026-09-30-000030","url":"https://github.com/dtq1997/zeta2-zeta3-linear-independence/tree/669c92bf7a3728e0de9ad80c373bc29fb5ca3d58","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000030-v1.json","repo":"https://github.com/dtq1997/zeta2-zeta3-linear-independence","tags":["math.NT","msc:11J72","msc:11M06","number-theory","zeta-values","irrationality","lean-formalization"],"score":0,"title":"Linear independence of 1, ζ(2), ζ(3) over ℚ","trust":"high","domain":"math.NT","source":"palomar","authors":["Qian Tang"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of the linear independence of 1, ζ(2) and ζ(3) over ℚ. The proof is inspired by A. Fauzan's work on the irrationality of ζ(5) and builds on the Lean formalization of the irrationality of Li₂(1/2), registered in Palomar as PALOMAR-2026-09-30-000013. It shows that the method of that proof can be pushed further. The main difference from the Li₂(1/2) proof is that the rational functions appearing here are allowed to have poles of order two. The remaining details are similar, with some minor modifications. The compared theorems depend on propext, Classical.choice and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true}