PeopleofSuperintelligence

Researcher

Anatole Dedecker

Anatole Dedecker is a mathematician who helps maintain Mathlib, Lean’s mathematical library for formalized mathematics. As a first-year mathematics and computer-science undergraduate at Université Paris-Saclay, he began learning Lean in 2020 and worked on Mathlib with Heather Macbeth during a Carnegie Mellon visit in 2022. He coauthored a 2022 paper on robust bivariate tests and worked with Jireh Loreaux to formalize the continuous functional calculus in Lean. In May 2026, he presented joint Mathlib work on classical distributions; as of October 2026, he is a PhD student in operator algebras at Université Paris Cité.

Works
3
Citations
0
h-index
0

Publication numbers from OpenAlex, as of 18 October 2026.

Timeline

  1. 2020

    Learning Lean

    In 2020, he is a first-year undergraduate in mathematics and computer science at Université Paris-Saclay and begins learning Lean.

  2. 2022

    A Mathlib visit

    In 2022, Carnegie Mellon’s Hoskinson Center supports his US visit to work on Mathlib with Heather Macbeth while he is an undergraduate at Paris-Saclay.

  3. 2022

    Robust bivariate tests

    In 2022, he coauthors a paper describing robusTest, an R package that offers corrected versions of common tests in bivariate statistics.

  4. May 2024

    Non-unital functional calculus

    In May 2024, he and Jireh Loreaux complete the development of Mathlib’s non-unital continuous functional calculus.

  5. January 2025

    Continuous functional calculus

    In January 2025, he and Jireh Loreaux submit a paper describing their Lean formalization of the continuous functional calculus, which is already merged into Mathlib.

  6. May 2026

    Classical distributions in Mathlib

    In May 2026, he presents joint work with Luigi Massaci that defines vector-valued classical distributions in Mathlib and proves continuity of differentiation of distributions.

  7. As of October 2026

    PhD and Mathlib roles

    As of October 2026, he is a PhD student in operator algebras at Université Paris Cité and a Mathlib maintainer. He has formalized mathematics in Lean since 2020.

Career

  1. 2022Carnegie Mellon UniversityMathlib visitor

Education

  1. From 2020Université Paris-SaclayUndergraduate student in mathematics and computer science
  2. Université Paris CitéPhD student in operator algebras

From the biography.

Most-cited works

  1. The continuous functional calculus in Lean2025 · 0 citations
  2. The robusTest package: two-sample tests revisited2022 · 0 citations

From OpenAlex, as of 18 October 2026.

  1. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes Carnegie Mellon University. Our estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.
  2. Google has the highest combined h-index among AI organizationsIncludes Carnegie Mellon University. Our estimates of combined and median h-index at AI organizations, using current affiliations and OpenAlex records.
  3. The median h-index is 54 at universities and 20 at frontier AI labsIncludes Carnegie Mellon University. The median h-index is 54 at universities and 20 at frontier AI labs. We compare publishing careers, citations and moves to estimate how universities and frontier labs contribute to AI research.
  4. Stanford University trained or employed 27 of the 111 AI major-prize winners, more than any other universityIncludes Carnegie Mellon University. Stanford University trained or employed 27 of the 111 AI major-prize winners, more than any other university. We compare doctorate and employment links for major-prize and best-paper winners.

Colleagues

People with dated positions at the same organization in the same years.

Sources and credits

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

  1. Anatole Dedecker (introduction) leanprover-community.github.io. Checked 18 October 2026.
  2. Past Events — Hoskinson Center for Formal Mathematics cmu.edu. Checked 18 October 2026.
  3. The robusTest package: two-sample tests revisited arxiv.org. Checked 18 October 2026.
  4. This month in Mathlib (May 2024) leanprover-community.github.io. Checked 18 October 2026.
  5. The continuous functional calculus in Lean arxiv.org. Checked 18 October 2026.
  6. Spaces of classical distributions and locally convex spaces in Mathlib mathinstitutes.org. Checked 18 October 2026.
  7. Mathlib maintainers leanprover-community.github.io. Checked 18 October 2026.