data David = Research | Activities | Events | Talks | Miscellaneous | Lean-LMFDB

This page was generated by Haskell on 26.01.26 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 of global function fields
  Preprint submitted to the Seventeenth Algorithmic Number Theory Symposium
• 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