top of page

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 versionarxiv 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 versionarxiv version.

bottom of page