A Lean formalization project accompanying the General Central Singularity Formula (GCSF), focusing on the structural setup and definitions around central singular behavior of L-functions.
This repository does not claim a full formal proof of the General Central Singularity Formula.
Instead, it provides a Lean formalization of the structural definitions and foundational framework introduced in the paper, intended as a verification-oriented companion and a step toward future formal development.
- Hakjun Kim
This project is licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0).
- License file:
LICENSE - License URL: https://creativecommons.org/licenses/by/4.0/
lake build
lake exe gcsflean