A Lean 4 Formalization of the Birch and Swinnerton-Dyer Conjecture and Its Surrounding Theory

The Birch and Swinnerton-Dyer conjecture predicts that for an elliptic curve \(E/\mathbb{Q}\) the Mordell-Weil rank equals the order of vanishing of the Hasse-Weil \(L\)-function at \(s = 1\), and that the leading Taylor coefficient is expressed by an explicit formula involving the real period, regulator, Shafarevich-Tate group, Tamagawa numbers, and torsion. It remains an open Millennium Prize problem.

This paper presents a Lean 4 formalization of the mathematical infrastructure surrounding BSD: the classical partial results, the modern refinements, explicit narrowings at rank \(\leq 1\) and at every rank with a certified Mordell-Weil lower bound, a structural reduction of the rank half of the conjecture to the finiteness of the Shafarevich-Tate group, a Perrin-Riou-based narrowing of the leading-term formula at rank \(1\), and eight concrete worked curves spanning ranks \(0\) to \(3\). We formalize \(231\) theorems across \(32\) thematic phases covering the Mordell-Weil theorem, modularity, the Gross-Zagier formula, Kolyvagin's theorem on Heegner points, Selmer-group bounds, the parity conjecture, \(p\)-adic BSD in the sense of Mazur-Tate-Teitelbaum, the Iwasawa main conjecture of Kato-Skinner-Urban, the generalization to abelian varieties and motives (Bloch-Kato), equivariant BSD for Galois representations, modularity lifting (Wiles, Taylor-Wiles, Khare-Wintenberger), Euler systems (Kato, Rubin, Kolyvagin), visibility of Shafarevich-Tate (Cremona-Mazur), algorithmic BSD via two-descent, the average-rank results of Bhargava-Shankar and Bhargava-Skinner-Zhang, a GRH-effective rank identity for \(\mathrm{an\_rank} \leq 1\) (Goldfeld, Hoffstein-Lieman, Gross-Zagier-Kolyvagin-effective), the unconditional rank-\(0\) theorem of Coates and Wiles for elliptic curves with complex multiplication, Rubin's unconditional main conjecture for CM curves, the Iwasawa-main-conjecture route to the BSD leading-term formula at rank \(0\), a GRH-effective LMFDB database anchoring six per-curve closures (including one CM closure for \(E_{27a1}\) via \(\mathbb{Z}[\omega]\)), Kato's unconditional rank upper bound combined with Cremona mwrank lower bounds to give unconditional rank identities at ranks \(2\) and \(3\) (\(E_{389a1}\) and \(E_{5077a1}\)), the congruent-number family \(E_n : y^2 = x^3 - n^2 x\) with its universal CM structure and Tian's unconditional rank-\(\geq 1\) theorem, a prototype latent-spectral reformulation, a Cassels-Mazur-descent derivation of the rank identity from the finiteness of the \(p\)-primary Shafarevich-Tate group combined with the Iwasawa-theoretic identification of the Selmer rank with the analytic rank, and the Perrin-Riou \(p\)-adic Gross-Zagier framework (Perrin-Riou 1993, Nekovář 1995, Kobayashi 2013) composed with the Skinner-Urban Iwasawa main conjecture to reduce the BSD leading-term formula at rank \(1\) to a single cited fact. The elliptic curves \(E_0 : y^2 = x^3 - x\) (Cremona