Bridging Lean and the LMFDB
As of July 2025, together with Andrew Sutherland and David Roe, we are leading a project to create links between Lean and the LMFDB. This is a two-year project is funded by Renaissance Philanthropy. The project is hosted here.
​
Publications/Preprints
-
Formalising modular forms, Eisenstein series and the statement of the modularity conjecture. Preprint
-
A complete formalization of Fermat's Last Theorem for regular primes in Lean (joint with Alex Best, Riccardo Brasca, Eric Rodriguez, Reuben van de Velde and Andrew Yang), Annals of Formalized Mathematics, 2025, published version, arxiv
-
Fermat's Last Theorem for regular primes (joint with Alex Best, Riccardo Brasca and Eric Rodriguez). 14th International Conference on Interactive Theorem Proving
-
Overconvergent Hilbert modular forms via perfectoid modular varieties (joint with Ben Heuer and Chris Williams), Ann. Inst. Fourier, 2023, published version, arxiv
-
2-adic slopes of modular forms over Q(sqrt{5}), Bull. London Math. Soc., published version, arxiv version.
-
Extensions of vector bundles on the Fargues-Fontaine curve (joint with Tony Feng, David Hansen, Serin Hong, Qirui Li, Anthony Wang, Lynnelle Ye), J. Inst. Math. Jussieu, published version, arxiv version.
-
Slopes of overconvergent Hilbert modular forms, Experimental Mathematics, published version ,arxiv version.
-
The Jacquet-Langlands correspondence for overconvergent Hilbert modular forms, Int. J. Number Theory, published version ,arxiv version.
-
Masters project: On the p-adic Langlands correspondence for algebraic tori, J. Th. Nombres Bordeaux, published version, arxiv version.