data
David
=
Research
|
Activities
|
Events
|
Talks
|
Miscellaneous
|
Lean-LMFDB
Research
This page was generated by
Haskell
on 25.12.25 with theme inspired by
GHCi.
*David> print projects
Here are some of my research interests.
The
Birch and Swinnerton-Dyer conjecture
over
global fields
Local-global obstructions
to
rational points
on varieties
Computational aspects
of
L-functions
of
global function fields
The
formalisation
of
elliptic curves
in the
Lean theorem prover
Pedagogical aspects
of undergraduate
mathematics education
Here are some of my ongoing projects.
With Chris Birkbeck, I am organising the workshop
Bridging Lean and the LMFDB
in the summer of 2026
With Mentzelos Melistas, I am investigating the divisibility of Tamagawa numbers of elliptic curves over global function fields
With Peiran Wu and Junyan Xu, I am formalising the structure of the Tate module of an elliptic curve in Lean
With Chris Birkbeck and Bhavik Mehta, I am verifying regulators of number fields and elliptic curves in Lean
I am developing
an extensible Magma interface for motivic L-functions over global function fields
I am generating a database of L-functions of λ-adic representations over the rational function field
*David> print papers
Here are my publications so far.
L-values of elliptic curves twisted by cubic characters
Accepted in the
Canadian Journal of Mathematics
An elementary formal proof of the group law on Weierstrass elliptic curves in any characteristic
(with Junyan Xu)
Published in the
14th International Conference on Interactive Theorem Proving (ITP 2023),
volume 268 of Leibniz International Proceedings in Informatics, pages 6:1–6:19. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Wadern, Germany, 2023
Here are some of my unpublished work.
Computing L-functions of λ-adic representations over global function fields
Preprint in preparation
Algebraic proofs for elliptic divisibility sequences and division polynomials (with Junyan Xu)
Preprint in preparation
Algebraicity of Artin–Hasse–Weil L-series over global function fields
Preprint submitted to the
Bulletin of the London Mathematical Society
L-functions of Dirichlet twists of elliptic curves: computations and congruences
PhD thesis supervised by
Vladimir Dokchitser
The Mordell–Weil theorem in Lean
with
source code
LSGNT mini project supervised by
Kevin Buzzard
The Euler system of Heegner points
LSGNT group mini project supervised by
Vladimir Dokchitser
Arithmetic statistics for elliptic curves
Master's thesis supervised by
Toby Gee