Unconditional Birch-Swinnerton-Dyer for CM Elliptic Curves at Rank 0: A Formally Verified Proof
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
For every elliptic curve $E / \mathbb{Q}$ with complex multiplication by the ring of integers of an imaginary quadratic field, if $L(E, 1) > 0$ then the full Birch-Swinnerton-Dyer leading-term formula
$$L_{\mathrm{lead}}(E) \;=\; \frac{\Omega_E \cdo
Length
3,148 words
Claims
6 theorems
Status
Draft
Target
Experimental Mathematics