A Lean 4 formalization of the Connes--Consani Arithmetic Site and selected analytic ingredients surrounding its connection to the Riemann zeta function.
The project now enforces a sharp distinction between:
- declarations proved by Lean;
- published mathematical results described as formalization targets; and
- genuinely open steps toward the Riemann Hypothesis.
In particular, the repository does not claim a proof of RH. The current formal core includes the tropical structure sheaf, concrete finite-adèle orbit quotient, the elementary characterization of flat positive-integer actions, tensor-square Frobenius maps, and the von-Mangoldt/completed logarithmic-derivative identities. See FRONTIER.md for the trust boundary, literature map, and prioritized research milestones.
Build the Lean library with:
lake buildThe project blueprint and API documentation are available at https://jonbannon.github.io/ArithmeticSite/.