(2026).
Synthetic Differential Geometry in Lean.
Preprint.
(2025).
A complete formalization of Fermat's Last Theorem for regular primes in Lean.
Annals of Formalized Mathematics.
(2025).
Eigenvarieties for non-cuspidal modular forms.
Submitted for publication (major revision in progress).
(2024).
Categorical foundations of formalized condensed mathematics.
Journal of Symbolic Logic.
(2023).
Fermat's Last Theorem for regular primes.
14th International Conference on Interactive Theorem Proving (ITP 2023).
(2021).
Hida theory over some unitary Shimura varieties without ordinary locus.
American Journal of Mathematics.
(2020).
p-adic families of modular forms for Hodge type Shimura varieties with non-empty ordinary locus.
Preprint.
(2019).
An introduction to perfectoid spaces.
Panoramas et Syntheses.
(2016).
Eigenvarieties for cuspforms over PEL type Shimura varieties with dense ordinary locus.
Canadian Journal of Mathematics.
(2014).
Quaternionic modular forms of any weight.
International Journal of Number Theory.