Hello world!

I am Alex, I'm a researcher interested in (formalization of) mathematics, computer science and machine learning.
I currently work at Harmonic, applying machine learning and formal methods to develop and scale AI systems that can reason and learn without depending on human generated data. 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.

Picture of me in action, credit to Barinder Banwait

Publications

Seminars

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.

Code

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)

Research talks

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)

Selected expository talks (some with notes in the link)

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)

Find me on the web