I am Alex, I'm a researcher interested in (formalization of) mathematics, computer science and machine learning.
Previously I was a Heilbronn Research Fellow at King's College London.
Before that I worked at VU Amsterdam, in the group of Sander Dahmen.
I got my PhD from Boston University (working with Jennifer Balakrishnan), and before that I worked at TU Kaiserslautern (on the MPIR Library), and studied at the Universities of Cambridge and Warwick.
Here is a picture of me.
And below are some things you might actually have come here looking for.
If you want to send me an email, go ahead! Just replace the .github.io part of this web address with @gmail.com.
A User's Guide to the Local Arithmetic of Hyperelliptic Curvesabove.
Square root time Coleman integration on superelliptic curvesabove.
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)