PeopleofSuperintelligence

Researcher

Riccardo Brasca

Riccardo Brasca is a mathematician who works on number theory and on formalizing mathematics in the Lean proof assistant, a field that AI tools are now entering. He completed a PhD at the Università degli Studi di Milano in 2012, held postdoctoral positions at ENS Lyon and the Max Planck Institute for Mathematics, and became a maître de conférences at Université Paris Cité in 2013. He began working in formalization in 2020, contributed to the Liquid Tensor Experiment, completed in 2022, and coordinated the Lean formalization of Fermat's Last Theorem for regular primes, with papers in 2023 and 2024. In 2026, he and Chris Birkbeck formalized Kummer's criterion for regularity using LLMs, and mathlib received the 2026 Demailly Prize. He is a maître de conférences at Université Paris Cité, a maintainer of mathlib and a scientific coordinator of the ANR project FALSE.

Works
14
Citations
49
h-index
4

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. 2012

    A PhD in Milan

    He completes his PhD in March 2012 at the Università degli Studi di Milano under Fabrizio Andreatta. His thesis concerns p-adic modular forms.

  2. Since 2013

    Associate professor at Paris Cité

    After postdoctoral positions at ENS Lyon, where Vincent Pilloni supervises him, and at the Max Planck Institute for Mathematics in Bonn, he becomes a maître de conférences (tenured associate professor) at Université Paris Cité in 2013. He is a member of the Institut de Mathématiques de Jussieu–Paris Rive Gauche.

  3. Since 2020

    A mathlib maintainer

    In 2020, he begins working in the formalization of mathematics. He serves as a maintainer of mathlib, the Lean mathematical library, whose maintainers hold the power to give final approval to proposed changes.

  4. 2022

    The Liquid Tensor Experiment

    In July 2022, the Lean community completes the Liquid Tensor Experiment, a formal verification of the main theorem of liquid vector spaces posed as a challenge by Peter Scholze. He is among the contributors to the project, which Johan Commelin leads.

  5. 2023–2024

    Fermat's Last Theorem in Lean

    He coordinates the Lean project to formalize Fermat's Last Theorem for regular primes. In 2023, he and three coauthors post a formalization of the first case in Lean and mathlib. In 2024, he and five coauthors post a complete formalization that includes a proof of Kummer's lemma.

  6. March 2026

    Synthetic differential geometry in Lean

    In March 2026, he and Gabriella Clemente post "Synthetic Differential Geometry in Lean" on arXiv. They formalize a Taylor theorem for functions of several variables in Lean and mathlib, and point to the possibility of using mathlib for constructive mathematics.

  7. 2026

    A Demailly Prize for mathlib

    In 2026, mathlib, the Lean library he maintains, is awarded the Demailly Prize.

  8. As of October 2026

    Kummer's criterion with LLMs

    He is a maître de conférences at Université Paris Cité whose research covers number theory and the formalization of mathematics, and a scientific coordinator of the ANR project FALSE. In May 2026, he gives a Colloquia Patavina talk in Padua, "Around Formalization: Why and How to Explain Mathematics to a Computer", that also covers how AI is beginning to transform formalization. In June 2026, he and Chris Birkbeck formalize Kummer's criterion for regularity, using LLMs.

Career

  1. Since 2013Université Paris CitéMaître de conférences
  2. 2015–2026Université Paris 8
  3. 2012–2013École Normale Supérieure de LyonPostdoctoral Researcher
  4. Max Planck SocietyPostdoctoral Researcher

Education

  1. 2012University of MilanPhD

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Most-cited works

  1. p -adic modular forms of non-integral weight over Shimura curves2012 · Compositio Mathematica · 22 citations
  2. Eigenvarieties for Cuspforms Over PEL Type Shimura Varieties With Dense Ordinary Locus2015 · Canadian Journal of Mathematics · 11 citations
  3. Hida theory over some unitary Shimura varieties without ordinary locus2021 · American Journal of Mathematics · 6 citations
  4. Eigenvarieties for non-cuspidal modular forms over certain PEL Shimura varieties2016 · 4 citations
  5. A complete formalization of Fermat's Last Theorem for regular primes in Lean2025 · Annals of Formalized Mathematics · 2 citations

From OpenAlex, as of 21 October 2026.

  1. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Université Paris Cité. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.
  2. Google has the highest combined h-index among AI organizationsIncludes Max Planck Society. We estimate that Google holds the highest combined h-index at 8,016, while universities account for 73% of the deduplicated total across AI organizations.
  3. People shaping AI work at a median of 3 organizations over a career: 3 for university starters and institute and lab starters, versus 2 for company startersIncludes Max Planck Society. Across 6,853 people shaping AI with a dated work role, we estimate a median of 3 parent organizations over a career (mean 3.6), comparing role groups, starting sectors and starting decades from the 1950s to 2020–2026.
  4. The United States employs an estimated 48% of people shaping AIIncludes Max Planck Society. We estimate where the people shaping AI work today, how universities, companies and research institutes split across countries, and how country shares have changed since the 1960s.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Riccardo Brasca yet. Send us a free-licensed photo.

  1. Riccardo Brasca riccardobrasca.github.io. Checked 20 October 2026.
  2. Progrès récents dans la formalisation de la théorie des nombres | Collège de France college-de-france.fr. Checked 20 October 2026.
  3. Colloquia Patavina for Students: Around Formalization: Why and How to Explain Mathematics to a Computer math.unipd.it. Checked 20 October 2026.
  4. Mathlib maintainers | Lean Community leanprover-community.github.io. Checked 20 October 2026.
  5. Completion of the Liquid Tensor Experiment | Lean community blog leanprover-community.github.io. Checked 20 October 2026.
  6. [2305.08955] Fermat's Last Theorem for regular primes arxiv.org. Checked 20 October 2026.
  7. [2410.01466] A complete formalization of Fermat's Last Theorem for regular primes in Lean arxiv.org. Checked 20 October 2026.
  8. [2603.17457] Synthetic Differential Geometry in Lean arxiv.org. Checked 20 October 2026.