Linear independence of 1, ζ(2), ζ(3) over ℚ
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-30-000030
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000030/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000030/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'