Irrationality of Li₂(1/2)
A Lean formalization of the irrationality of Li₂(1/2) = Σ_{n≥1} 2^(-n)/n². The proof is inspired by A. Fauzan's work on the irrationality of ζ(5) and builds on Moritz Firsching's Lean formalization in mo271/Zeta5. The central idea is to establish the irrationality of a real number r by constructing a sequence of integer polynomials P_n whose values P_n(r) decay rapidly as n tends to infinity, while for every rational q, P_n(q) ≠ 0 for infinitely many n. Analytic umbral calculus was used to find suitable polynomials Q_n with rational coefficients. Random matrix theory provides rapid decay of…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-30-000013
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000013/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-000013/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'