PeopleofSuperintelligence

Researcher

Johan Commelin

Johan Commelin is a mathematician whose work brings research mathematics into Lean and helps maintain Mathlib. He wrote mathematics theses in 2011 and 2013, completed a PhD in Nijmegen in 2017, and held postdoctoral posts in Utrecht and Freiburg. With collaborators, he formalised perfectoid spaces in 2019, led the Liquid Tensor Experiment from 2021 to 2022, and coauthored award-winning Lean work on Witt vectors in 2021. Microsoft Research awarded him its Lean Award for the 2023 academic year; he coauthored a paper on Mathlib maintenance in 2025 and a paper on AI and mathematics in 2026. As of October 2026, he directs the Mathlib Initiative and works part-time as an assistant professor at Utrecht University.

Timeline

  1. 2011–2023

    Degrees and postdoctoral posts

    He writes his bachelor's thesis, Tannaka Duality for Finite Groups, under Lenny Taelman in 2011, and his master's thesis, Algebraic cycles, Chow motives, and L-functions, under Robin de Jong in 2013. He completes a PhD in Nijmegen under Ben Moonen in 2017, then works as a postdoc with Carel Faber in Utrecht from 2017 to 2018 and in Stefan Kebekus's group in Freiburg from 2018 to 2023.

  2. 2019

    Formalising perfectoid spaces

    In 2019, he joins Kevin Buzzard and Patrick Massot to formalise enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover.

  3. 2021–2022

    Leading the Liquid Tensor Experiment

    In 2021–2022, he leads the Liquid Tensor Experiment with a team of mathematicians, taking up Peter Scholze's challenge to verify a theorem in Lean.

  4. 2021

    Formalising Witt vectors in Lean

    In 2021, he and Robert Y. Lewis formalise Witt vectors and their ring operations in Lean. They prove that, for prime p, Witt vectors over Z/pZ are isomorphic to the p-adic integers, and their CPP 2021 paper receives a Distinguished Paper Award.

  5. 2023

    A Microsoft Research Lean Award

    In 2023, Microsoft Research names him a recipient of its Lean Award for the academic year. The award lets him hire a postdoc to improve how isomorphism-invariance is handled in formal mathematics using Lean.

  6. 2025

    Maintaining Mathlib as it grows

    In 2025, he coauthors Growing Mathlib, which describes ways to manage the library's growth through deprecations, linters, faster compilation, library redesign, technical-debt work and custom tools for reviewing and triaging contributions.

  7. 2026

    Mathematics in the age of AI

    In 2026, he coauthors Shaping the Future of Mathematics in the Age of AI, which examines values, mathematical practice, teaching, technology and ethics and offers recommendations to the mathematical community.

  8. As of October 2026

    Directing the Mathlib Initiative

    As of October 2026, he directs the Mathlib Initiative and works part-time as an assistant professor in Utrecht University's Faculty of Science. He maintains Mathlib, Lean's mathematical library.

Career

  1. NowMathlib InitiativeDirector
  2. NowUtrecht UniversityAssistant Professor

From the biography.

  1. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes Utrecht University. We estimate where the people shaping AI studied and where their careers led. Massachusetts Institute of Technology leads with 467 former students, including 291 recorded doctorates.
  2. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Utrecht University. 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.
  3. Google has the highest combined h-index among AI organizationsIncludes Utrecht University. 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.
  4. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes Utrecht University. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.

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 Johan Commelin yet. Send us a free-licensed photo.

  1. Johan Commelin math.commelin.net. Checked 21 October 2026.
  2. Formalising perfectoid spaces arxiv.org. Checked 21 October 2026.
  3. Liquid Tensor Experiment indico.math.cnrs.fr. Checked 21 October 2026.
  4. Formalizing the ring of witt vectors research.vu.nl. Checked 21 October 2026.
  5. Microsoft Research Lean Award Program microsoft.com. Checked 21 October 2026.
  6. Growing Mathlib: maintenance of a large scale mathematical library arxiv.org. Checked 21 October 2026.
  7. Shaping the Future of Mathematics in the Age of AI arxiv.org. Checked 21 October 2026.
  8. Team — Mathlib Initiative mathlib-initiative.org. Checked 21 October 2026.
  9. Johan Commelin - Utrecht University research-portal.uu.nl. Checked 21 October 2026.