An introduction to p-adic L-functions — Lean blueprint

 An introduction to p-adic L-functions — Lean blueprint🔗

Compiled2026-06-16T12:17:31ZProject76ed29adev/padic: bring code current to origin 4530701 + bump-align to d90090f; vendor blueprint sourceLeanleanprover/lean4:v4.31.0-rc2VersoBlueprintv4.30.0@fdccf1340444Mathlibd90090f647ca

This is the mathematical blueprint for a Lean 4 / Mathlib formalisation of Jacinto and Williams (2023), An introduction to p-adic L-functions.

The notes build, from the ground up, the cyclotomic Iwasawa theory of the Riemann zeta function. Starting from p-adic measures and the Iwasawa algebra \Lam \cong \Zp[[T]], they construct the Kubota–Leopoldt p-adic L-function \zeta_p, prove that it interpolates the special values \zeta(1-n) = -B_n/n of the Riemann zeta function against the Teichmüller character, and then develop the structure theory of \Lam-modules far enough to state and (for Vandiver primes) prove the Iwasawa Main Conjecture. A final part sketches the analogous picture for modular forms.

How to read this blueprint. Each node below is a definition, theorem or proposition with its mathematical statement and a paragraph-level proof sketch. The dependency graph records which results feed into which. A node is coloured green once the Lean declaration it references (lean := …) is fully proved, blue while it is stated but still contains sorry, and left uncoloured while it is roadmap-only. There is no manual status to maintain: Verso reads it from the Lean side directly.

Status. Roadmap stage. The chapters record the intended statements and proof strategies for the whole paper (§2–§15 of Jacinto and Williams (2023)); the Lean skeletons that the graph points at are being introduced incrementally, after which the corresponding nodes colour in.

Contents

  1. 1. Overview and roadmap
  2. 2. What a p-adic L-function should be
  3. 3. Measures and the Iwasawa algebra
  4. 4. The Kubota-Leopoldt p-adic L-function
  5. 5. Interpolation at Dirichlet characters
  6. 6. The value at s = 1
  7. 7. The residue at s = 1
  8. 8. The p-adic family of Eisenstein series
  9. 9. The Coleman map
  10. 10. Iwasawa theorem on the zeros of the p-adic zeta function
  11. 11. Proof of Iwasawa theorem
  12. 12. The Iwasawa Main Conjecture
  13. 13. Iwasawa mu-invariant
  14. 14. Iwasawa theory for modular forms
  15. 15. Dependency graph
  16. Dependency Graph
  17. 16. Progress summary
  18. Blueprint Summary
  19. 17. References
  20. Blueprint Bibliography