Zeta23 — more than two thirds of the zeta zeros are simple and on the critical line
A complete, sorry-free Lean 4 / Mathlib formalization of the headline theorems of Alpöge–Furman, "More than two thirds of the zeta zeros are simple and on the critical line" (arXiv:2608.13637). Writing N(T) for the number of nontrivial zeros ρ of the Riemann zeta function with 0 1. The statements are made against Mathlib's `riemannZeta` and `DirichletCharacter.LFunction`, with multiplicity via `analyticOrderAt`; nothing is assumed — every analytic input (Weil's explicit formula for ζ and for L(s,χ), the Riemann–von Mangoldt formula, Stirling-type estimates for Γ′/Γ, Chebyshev–Mertens bounds,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/lean/anthropics__formal-math__zeta23
curl -X POST /api/v1/records/lean/anthropics__formal-math__zeta23/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/lean/anthropics__formal-math__zeta23/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'