Hello world!

• A complete formalization of Fermat's Last Theorem for regular primes in Lean (with Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Andrew Yang, and Ruben van de Velde), (abstract) (arXiv)
• Fermat’s Last Theorem for regular primes (with Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi), proceedings of Fourteenth Conference on Interactive Theorem Proving (ITP) 2023, (abstract) (arXiv) doi:10.4230/LIPIcs.ITP.2023.36
• Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves (with Anne Baanen, Nirvana Coppola, and Sander Dahmen), proceedings of Certified Programs and Proofs 2023, (abstract) (arXiv) doi:10.1145/3573105.3575682
• Automatically Generalizing Theorems Using Typeclasses , Workshop Papers at 12th Conference on Intelligent Computer Mathematics CICM 2021, CEUR-WS, (abstract) (pdf)
• Refined Selmer Equations for the Thrice-Punctured Line in depth two (with L. Alexander Betts, Theresa Kumpitsch, Martin Lüdtke, Angus McAndrew, Lie Qian, Elie Studnia, and Yujie Xu), Mathematics of Computation, 2023, (abstract) (arXiv) doi:10.1090/mcom/3898
• A User's Guide to the Local Arithmetic of Hyperelliptic Curves (with L. Alexander Betts, Matthew Bisatt, Raymond van Bommel, Vladimir Dokchitser, Omri Faraggi, Sabrina Kunzweiler, Céline Maistret, Adam Morgan, Simone Muselli, and Sarah Nowell), Bulletin of the London Mathematical Society, 2022, (abstract) (arXiv) doi:10.1112/blms.12604
• Square root time Coleman integration on superelliptic curves , Arithmetic geometry, number theory, and computation, Simons Symposia, 2021, (abstract) (preprint) doi:10.1007/978-3-030-80914-0_3
• Elliptic curves with good reduction outside of the first six primes (with Benjamin Matschke), Arithmetic geometry, number theory, and computation, Simons Symposia, 2021, (abstract) (arXiv) doi:10.1007/978-3-030-80914-0_5
• Computing classical modular forms (with Jonathan Bober, Andrew R. Booker, Edgar Costa, John Cremona, Maarten Derickx, David Lowry-Duda, Min Lee, David Roe, Andrew V. Sutherland, and John Voight), Arithmetic geometry, number theory, and computation, Simons Symposia, 2021, (abstract) (arXiv) doi:10.1007/978-3-030-80914-0_4 (errata)
• Two Recent p-adic Approaches Towards the (effective) Mordell Conjecture (with Jennifer Balakrishnan, Francesca Bianchi, Brian Lawrence, Steffen Müller, Nicholas Triantafillou, and Jan Vonk), Arithmetic L-Functions and Differential Geometric Methods, Regulators IV, May 2016, Paris, (abstract) (arXiv) doi:10.1007/978-3-030-65203-6_2
• Explicit Coleman Integration in Larger Characteristic , Proceedings of the Thirteenth Algorithmic Number Theory Symposium, 2018, (abstract) (arXiv) doi:10.2140/obs.2019.2.85
• Computing Zeta Functions of Cyclic Covers in Large Characteristic (with Vishal Arul, Edgar Costa, Richard Magner, and Nicholas Triantafillou), Proceedings of the Thirteenth Algorithmic Number Theory Symposium, 2018, (abstract) (arXiv) doi:10.2140/obs.2019.2.37

I organised the Heilbronn show and tell seminar in Spring 2023.
I ran the BUNTES learning seminar in Spring 2020: the topic was Abhyankar's conjecture.

• Notes from Céline Maistret's class, on Ranks and Parity of Ranks of Curves and Abelian Surfaces:
  Web notes on Ranks and Parity of Ranks of Curves and Abelian Surfaces
  Pdf notes on Ranks and Parity of Ranks of Curves and Abelian Surfaces
• Notes from Ali Altuğ's class, on Equidistribution in Number theory:
  Web notes on Equidistribution in Number theory
  Pdf notes on Equidistribution in Number theory
• Notes from Ali Altuğ's class on Automorphic forms and the Arthur-Selberg trace formula:
  Web notes on Automorphic forms and the Arthur-Selberg trace formula
  Pdf notes on Automorphic forms and the Arthur-Selberg trace formula
• My Part III Essay on Serre's conjecture; supervised by Jack Thorne (source on GitHub, comments welcome!)
• For (some old) lecture notes from my undergrad see Mjolnir.

• A SageMath package for computing local invariants of hyperelliptic curves via cluster pictures (with Raymond van Bommel) see A User's Guide to the Local Arithmetic of Hyperelliptic Curves above.
• A Julia package for computing Coleman integrals on superelliptic curves see Square root time Coleman integration on superelliptic curves above.

Past:

Modular Forms (Mastermath 2022) (TA and occasional lecturer)

Project course: Computer Assisted Proofs (VU 2022) (Lecturer)

Basic Concepts in Mathematics (VU 2021) (TA)

MA225 Multivariable Calculus (BU Fall 2017) (TA)

MA123 Calculus 1 Section A2 (BU Summer 1 2017) (Lecturer)

EK102 Linear Algebra (BU Spring 2017) (TA)

MA121 Calculus I for Life and Social Scientists (BU Fall 2016) (TA)

CS137 Discrete Maths and its Applications 2 (Warwick 2014) (TA)

Formalization and Arithmetic Geometry; past, present, and future, VaNTAGe a virtual math seminar on open conjectures in number theory and arithmetic geometry, (slides) (video)

Leaff, a Lean diff tool, Lean Together 2024, (video)

Integral solutions of Generalized Fermat equations, University of Exeter, Algebra and Number Theory Seminar, November 22nd 2023

Lean for the curious arithmetic geometer, Rational Points 2023, Scheny, July 28th 2023 (slides)

Formalizing algebraic number theory, recent progress and future challenges, Formalisation of mathematics with interactive theorem provers, Cambridge, June 8th 2023 (slides)

p-adic integration and points on curves, Heilbronn show and tell seminar, March 2023

Coleman integration and its Uses in Number Theory, King's internal research seminar, March 2023 (slides)

COleman integration and its Uses in Number Theory, COUNT, COmputations and their Uses in Number Theory, Luminy, February 2023 (slides)

Solving Diophantine equations via the class group, London Learning Lean seminar, February 2023 (slides) (video)

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves, Certified Programs and Proofs, Boston, January 2023 (slides) (video)

The $S$-unit equation and non-abelian Chabauty in depth 2, Oberseminar Zahlentheorie und Arithmetische Geometrie, Leibniz Universität Hannover, 2022 (slides)

Metaprogramming for Automation of Library Maintenance, EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs, CLAS, Tbilisi Georgia, 2022 (slides)

Formalization in number theory, past, present and future, Dutch Intercity Number Theory Seminar, 2022 (slides)

Mathematical results as structured data, Big Data in Pure Mathematics, 2022 (slides)

The $S$-unit equation and non-abelian Chabauty in depth 2, London Number Theory Seminar, 2022 (slides)

A guided tour of Chabauty methods, Binghamton University Arithmetic Seminar, 2021 (slides)

Elliptic curves with good reduction outside of the first six primes, DIAMANT Symposium Autumn 2021, (slides)

Automatically Generalizing Theorems Using Typeclasses, FMM 2021, part of CICM 2021, (slides) (video)

The $S$-unit equation and non-abelian Chabauty in depth 2, Bristol Linfoot seminar, 2021

The $S$-unit equation and non-abelian Chabauty in depth 2, UGA Arithmetic Geometry/Number Theory Seminar, 2021

The $S$-unit equation and non-abelian Chabauty in depth 2, Freiburg Freitagsseminar, 2021

Generalising typeclass assumptions in Lean, Lean Together 2021, (slides) (video)

Computations with $p$-adic polylogarithms in SageMath, Global Virtual SageDays 109, 27/5/20 (slides)

Explicit computation with Coleman integrals, Journées Arithmétiques XXXI, University of Istanbul, 2019, 2/7/19 (slides)

Explicit computation with Coleman integrals, Boston University - Keio University workshop, 2019, 27/6/19 (slides)

Computing Coleman integrals on superelliptic curves (Lightning Talk), Arithmetic of Low Dimensional Abelian Varieties, ICERM, 2019 (slides)

Zeta functions and $p$-adic integrals; computations and applications, AMS Graduate Student Conference in Algebra/Number Theory, Brown, 2019 (slides)

(Explicit) Coleman Integration in Larger Characteristic, ANTS XIII 2018 UW-Madison, 17/7/18 (slides)

Rebuilding a topological hierarchy (in the Lean proof assistant), LFTCM 2020 (video)
The Kodaira-Parshin construction, STAGE Fall 2018
Quaternion Algebras, and Descent and Canonical Models BUNTES Fall 2018
The (inescapable) p-adics, a lightning talk at the BU Math retreat (slides)
A Smörgåsbord of Dessins d'Enfants, and Dessins, integer points on elliptic curves and a proof of the ABC conjecture BUNTES Spring 2018
The Tannakian formalism cannot hurt you STAGE Spring 2018
Various in BUNTES 2017 (Abelian varieties: Complex theory, Étale cohomology, the Rosati involution)
Ribet's converse to Herbrand's theorem: Cuspstruction, at STAGE Spring 2017, (notes on my blog: part I, part II)
Serre's Conjecture, at Ulm University Oberseminar (based on part III essay)
Singular Moduli, at Warwick Imperial Autumn Meeting 2014 & Cambridge Part III seminar series (slides)
Riemann Hypotheses, at Warwick Mathematics Society talks (slides)
Geometric approaches to solving Diophantine equations, at Tomorrow's Mathematicians Today 2013, (slides)

Twitter Github Stackexchange