A machine-checked solution to the Jacobians challenge

 A machine-checked solution to the Jacobians challenge🔗

This site documents a complete, machine-checked solution to Kevin Buzzard's Jacobians challenge — an API for the Jacobian of a compact Riemann surface, formalized in Lean 4 on top of Mathlib. The mathematics (genus, the genus-0 sphere theorem, Riemann–Roch, Abel's theorem, the Jacobian as a complex torus) is written by AI agents under human direction; nothing is taken on trust — every statement is checked by the Lean kernel.

Contents

  1. 1. How to validate this solution
  2. 2. Conformance: Buzzard’s spec vs. this formalization
  3. 3. holomorphic forms
  4. 4. local multiplicity
  5. 5. surfaces and charts
  6. 6. mapping degree
  7. 7. paths and integrals
  8. 8. residue calculus
  9. 9. jacobian construction
  10. 10. projective line
  11. 11. meromorphic and divisors
  12. 12. meromorphic trace
  13. 13. sphere topology
  14. 14. cech cohomology
  15. 15. form trace tower
  16. 16. dbar solvability
  17. 17. dolbeault comparison
  18. 18. planar stokes atoms
  19. 19. finiteness and chi
  20. 20. canonical forms
  21. 21. laurent tails
  22. 22. monodromy
  23. 23. residue theorem
  24. 24. serre duality cech
  25. 25. abel weak solutions
  26. 26. proper map degree
  27. 27. serre duality tails
  28. 28. cech h1 genus
  29. 29. riemann roch
  30. 30. abel theorem
  31. 31. genus zero headline
  32. 32. period lattice rank