Riccardo Brasca


Contact Information



Work Experience

Maître de conférences (associate professor)

Université Paris Cité

Institut de Mathématiques de Jussieu-Paris Rive Gauche


Post-Doc

École Normale Supérieure de Lyon


Post-Doc

Max Planck Institute for Mathematics, Bonn


Publications and preprints

  • Fermat's Last Theorem for regular primes in Lean. Joint work with Alex Best, Chris Birkbeck, and Eric Rodriguez. 14th International Conference on Interactive Theorem Proving, no. 36, 2023.
  • The Liquid Tensor Experiment, 2023. Joint with the mathlib community.
  • p-adic powers of the Gauss–Manin connection for Siegel modular forms. Joint work with Giovanni Rosso. In preparation.
  • p-adic families of modular forms for Hodge type Shimura varieties. Submitted for publication.
  • Overconvergent Eichler-Shimura isomorphisms for certain unitary groups. Joint work with Daniel Barrera Salazar. In preparation.
  • Hida theory over some unitary Shimura varieties without ordinary locus. Joint work with Giovanni Rosso. arXiv:1711.05546. Amer. J. Math. 143 (2021), no. 3, 715–751 .
  • Eigenvarieties for non-cuspidal modular forms over certain PEL Shimura varieties. Joint work with Giovanni Rosso. arXiv:1605.05065. Submitted for publication.
  • An Introduction to Perfectoid Spaces. Joint work with Fabrizio Andreatta, Olivier Brinon, Bruno Chiarellotto, Nicola Mazzari, Simone Panozzo, and Marco Seveso. Panorama et Synthéses, no. 54, 2019.
  • Eigenvarieties for cuspforms over PEL type Shimura varieties with dense ordinary locus. Canadian Journal of Mathematics 68 (2016), no.6, 1227-1256. doi.org/10.4153/CJM-2015-052-2.
  • Quaternionic modular forms of any weight. Int. J. Number Theory 10 (2014), no. 31, 31-53. doi:10.1142/S1793042113500796.
  • p-adic modular forms of non-integral weight over Shimura curves. Compos. Math. 149 (2012), no. 1, 32–62. doi:10.1112/S0010437X12000449.

  • Scientific activities

  • Maintainer of Mathlib
  • Organizer of the Lean for the Curious Mathematician 2024 conference, CIRM
  • Organizer of the Atelier Lean of the seventh mini symposium of the Roman Number Theory Association, Università Roma Tre
  • Member of the ANR project COLOSS
  • Member of the ANR project PerCoLaTor
  • Organizer of the seminar Groupes Réductifs et Formes Automorphes, Institute de Mathématiques de Jussieu-Paris Rive Gauche
  • Organizer of the conference Solstice 2014, Université Paris 7
  • Referee for the Canadian Journal of Mathematics, International Journal of Number Theory, and Algebra & Number Theory
  • Reviewer for MathSciNet
  • Organizer of the workshop Almost Xmas seminar, Università degli Studi di Milano, Milan

  • Seminars and Talks

  • An introduction to proof assistants: a mini course about mathematical formalization

    Universidad de Santiago de Chile

  • Maintenance of Lean’s mathlib and the Liquid tensor experiment

    EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs

    Tbilisi State University - Tbilisi

  • Fermat's Last Theorem for regular primes in Lean

    Conference Lean in Lyon

    Institut Camille Jordan - Lyon

  • How to explain advanced mathematics to a computer

    Workshop Luxembourg Number Theory Day 2021

    University of Luxembourg

  • p-adic families of modular forms over Shimura varieties of Hodge type

    Workshop Jornada de Teoría de Números y Representaciones

    Universidad de Santiago de Chile

  • p-adic families of modular forms over Shimura varieties of Hodge type

    Conference p-adic modular forms and p-adic L-functions

    Fondazione Alessandro Volta, Como - Italy

  • Hida theory over some Shimura varieties without ordinary locus

    Fourth one-day workshop in Cardedeu: p-adic arithmetic geometry

    Universitat de Barcelona - Spain

  • Mini-course Katz p-adic modular forms

    Summer School on Modular Forms

    Università di Padova - Italy

  • Eigenvarieties for non-cuspidal Siegel modular forms

    Summer School on Modular Forms

    Università di Padova - Italy

  • Eigenvarieties for non-cuspidal Siegel modular forms

    Conference p-adic methods for Galois representations and modular forms

    Universitat de Barcelona - Spain

  • Hida theory over some Shimura varieties without ordinary locus

    Number Theory Seminar

    Cambridge University - UK

  • Hida theory over some Shimura varieties without ordinary locus

    Arithmetic and Algebraic Geometry Seminar

    University of Amsterdam - The Netherlands

  • Eigenvarieties for non-cuspidal Siegel modular forms

    Québec-Vermont Number Theory Seminar

    McGill University - Montreal, Canada

  • Variété de Hecke pour formes de Siegel non cuspidales

    Séminaire d'Arithmetique

    Université de Lille - France

  • Famiglie p-adiche di forme modulari non cuspidali

    Conference of the UMI, the Italian Mathematical Society

    University of Siena - Italy

  • Almost mathematics

    Summer schoolPerfectoid spaces

    Organized by the University of Padova - Brixen, Italy

  • Eigenvarieties for non-cuspidal Siegel modular forms

    Conference Journées arithmétiques à Lyon

    ENS-Lyon - France

  • About the notion of p-adic family of modular forms

    SeminarNumber Theory and Algebraic Geometry

    KU Leuven - Belgium

  • Hida theory over some Shimura varieties without ordinary locus

    Number Theory Seminar at Johns Hopkins University

    Johns Hopkins University - Baltimore, USA

  • Hida theory over some Shimura varieties without ordinary locus

    Seminar Automorphic Forms and Arithmetic

    Columbia University - New York City, USA

  • Théorie de Hida pour certaines variétés de Shimura sans lieu ordinaire

    Séminaire de théorie des nombres de l'IMJ-PRG

    Institut de Mathématiques de Jussieu-Paris Rive Gauche - France

  • Hida theory over Shimura varieties without ordinary locus

    Conference p-adic methods in number theory

    Università degli Studi di Milano - Italy

  • Families of overconvergent modular forms over Shimura varieties without ordinary locus

    Conference p-adic aspects of modular forms

    IISER - Pune, India

  • Familles des formes modulaires p-adiques et variétés de Hecke

    Séminaire MathJeunes

    ENS Ulm - Paris, France

  • Autour d'une construction géométrique des variétés de Hecke

    Séminaire groupes réductifs et formes automorphes

    Institut de Mathématiques de Jussieu-Paris Rive Gauche - France

  • About a geometric construction of eigenvarieties for Shimura variety of PEL type

    Summer number theory in Milan

    Università degli Studi di Milano - Italy

  • Variétés de Hecke pour certaines formes modulaires de type PEL

    Séminaire de théorie des nombres de Caen

    Université de Caen Basse-Normandie - France

  • Hecke varieties for Shimura varieties with ordinary locus

    Conference Variétés de Shimura et formes modulaires p-adiques

    Université Paris 13 - France

  • Strict O-modules and p-adic modular forms

    Oberseminar

    University of Zürich - Switzerland

  • Strict O-modules and p-adic modular forms

    Séminaire de théorie des nombres

    Institut de Mathématiques de Bordeaux - France

  • p-adic modular forms of non-integral weight over Shimura curves

    London number theory seminar

    Kings College - London, UK

  • p-adic modular forms of non-integral weight over Shimura curves

    Oberseminar

    Max Planck Institute for Mathematics - Bonn, Germany

  • p-adic modular forms of non-integral weight

    Workshop Algebraic Geometry and related topics

    Centro di Ricerca Matematica Ennio De Giorgi - Pisa, Italy

  • Perfectoid fields and algebras

    Almost Xmas Seminar

    Università degli Studi di Milano - Italy

  • p-adic modular forms of non-integral weight

    Christmas Seminar

    Università degli Studi di Milano - Italy

  • p-adic modular forms of non-integral weight over Shimura curves

    Seminario di teoria dei numeri

    Università degli Studi di Milano - Italy


  • Education

    Ph.D. in Mathematics

    Università degli Studi di Milano

    Thesis: p-adic families of modular forms over Shimura curves

    Advisor: Fabrizio Andreatta


    M.Sc. in Mathematics

    Università degli Studi di Milano

    Thesis: Galois cohomology via almost-́etale extensions

    Advisor: Fabrizio Andreatta


    B.Sc. in Mathematics

    Università degli Studi di Milano

    Spazi di Banach e propriet`a di Radon-Nikodym

    Advisor: Clemente Zanco


    Teaching Experience

    Université Paris Cité

  • Teaching various courses as maître de conférences

  • Università degli Studi di Milano, Italy

  • Teaching assistant, Calculus III course
  • Teaching assistant, Algebra II course