A Spectral Reformulation of Birch-Swinnerton-Dyer: Formalized Prototype and Open Directions
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
We record a spectral reformulation of the Birch-Swinnerton-Dyer conjecture and its formalization in the Lean 4 kernel.
Length
1,920 words
Claims
3 theorems
Status
Sketch
Target
(internal research sketch — not yet submission-ready)