A first-year project at LSGNT, supervised by Kevin Buzzard.
The aim of this project was to use Lean to formalise some of the definitions around elliptic curves, specifically in order to state the BSD Conjecture.
The result for curves over the rationals is a lean file which, if every sorry were filled in with a proof, would be a full proof of BSD.
In the number field case, there are more definitions needed to give the analytic rank.
Along the way, it was necessary to define infinite products and prove that a quotient of a finitely-generated group is finitely generated. These are in separate files called tprod.lean and fg_quotient.lean.
More details and explanation about the project are in the directory pdf.
If you have Lean 3 installed, you can get this code by opening a command line, navigating to the correct directory, and typing
leanproject get jamiebell2805/BSD-conjecture
code BSD-conjecture
If you do not have Lean installed, instructions to do so are available at the leanprover community.