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), 2024, 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.