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

This page was generated by Haskell on 26.07.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 Peiran Wu and Junyan Xu, I am formalising the structure of the Tate module of an elliptic curve in Lean
• With Chris Birkbeck, I am computing torsion subgroups of elliptic curves via the Lutz–Nagell theorem 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.
• ABC implies that Ramanujan's tau function misses almost all primes (with Evan Chen, Seewoo Lee, Ken Ono, and Jujian Zhang)
  Accepted in Indagationes Mathematicae
• 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.
• Tamagawa numbers and torsion of elliptic curves over function fields (with Mentzelos Melistas)
  Preprint in preparation
• On the paucity of lattice triangles (with Evan Chen, Ken Ono, Jiaxin Zhang, and Jujian Zhang)
  Preprint
• Computing L-functions of λ-adic representations of global function fields
  Preprint
• Algebraic proofs for division polynomials (with Junyan Xu)
  Preprint in preparation
• Algebraicity of Artin–Hasse–Weil L-series over global function fields
  Preprint
• 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