Li's criterion for the Riemann Hypothesis
Li's criterion for the Riemann zeta function, formalized in Lean 4 over Mathlib: Mathlib's `RiemannHypothesis` holds if and only if every Li-Keiper coefficient of the completed xi function has nonnegative real part. The zero-indexed analytic coefficient at n is Li's classical lambda_(n+1), the n-th Taylor coefficient at 0 of the logarithmic derivative of s |-> xi(1/(1-s)). A second compared theorem identifies this analytic coefficient with Li's arithmetic coefficient, the symmetrized sum over the nontrivial zeros counted with multiplicity, and proves that symmetrized family summable so the…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-05-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-05-000005/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-05-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'