Mémoire sur les nombres premiers
A Lean 4 proof, with no unproved steps and no hypotheses, of explicit two-sided bounds for Chebyshev's function psi from P. L. Chebyshev, Mémoire sur les nombres premiers, 1852, with Chebyshev's constant A = log 2/2 + log 3/3 + log 5/5 - log 30/30 = 0.92129.... For every natural number n at least 30, psi of n is at least A n - 5 log n + 2 log 30 - 1; for every natural number n, psi of n is at most 6A/5 n + 2 log^2 n + 160. The proof uses Chebyshev's combination of log n!, log of the factorials of n/2, n/3 and n/5, and log of the factorial of n/30, as in the paper, with error terms weaker…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000029
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000029/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-11-01-000029/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'