Birch and Swinnerton-Dyer Conjecture

[ishaanxgupta]

What is the conjecture

The Birch and Swinnerton-Dyer Conjecture (BSD) is a central open problem in number theory and arithmetic geometry. It concerns an elliptic curve (E) defined over the rational numbers (E(Q).

Informally, the conjecture states that the number of independent rational points on (E) (the algebraic rank of (E(Q) is equal to the number of times the associated (L)-function (L(E,s)) vanishes at the special value (s = 1) (the analytic rank).

Equivalently:

the arithmetic complexity of an elliptic curve is exactly reflected by the behavior of its (L)-function at (s = 1).

References:

• Wikipedia: https://en.wikipedia.org/wiki/Birch_and_Swinnerton-Dyer_conjecture
• Clay Mathematics Institute (Millennium Prize Problems): https://www.claymath.org/millennium/birch-and-swinnerton-dyer-conjecture/

Prerequisites needed

To formalize the Birch and Swinnerton-Dyer conjecture in Lean, the following mathematical context is required:

• A formal definition of elliptic curves over (E(Q) (or more generally, global fields)
• The Mordell–Weil group (E(Q) and a notion of its rank
• A formal definition of the (L)-function of an elliptic curve, including analytic continuation to (s=1)
• A notion of order of vanishing of a complex function at a point

Some of these components are partially available in Mathlib, but others (notably elliptic curve (L)-functions and analytic rank) may require new definitions or additions under ForMathlib.

AMS categories

• ams-11G05 (Elliptic curves over global fields)
• ams-11G40 (L-functions of elliptic curves, BSD conjecture)

Choose either option

• I plan on adding this conjecture to the repository
• This issue is up for grabs: I would like to see this conjecture added by somebody else