PeopleofSuperintelligence

Researcher

Floris van Doorn

Floris van Doorn is a mathematician whose work makes advanced mathematics easier to check with Lean, a theorem prover he coauthored a system paper about in 2015. He earned a doctorate at Carnegie Mellon in 2018, then held postdoctoral roles in Pittsburgh and Paris-Saclay before joining Bonn as a professor in 2023. His work includes tools for mathlib, a shared library of formal mathematics, and a Lean proof of Smale’s sphere eversion theorem. In 2025, he shared the Thoralf Skolem Award for Lean’s system-description paper and received an ERC Synergy Grant with Christoph Thiele for HALF. He leads Bonn’s Formalized Mathematics workgroup and maintains mathlib; in August 2026, he coauthored a blueprint for a Lean formalization that used large language models.

Links
Website

Timeline

  1. 2015

    The Lean theorem prover

    He coauthors “The Lean Theorem Prover (System Description)” with Leonardo de Moura, Soonho Kong, Jeremy Avigad and Jakob von Raumer in 2015. Lean aims to bridge interactive and automated theorem proving.

  2. 2018

    A Carnegie Mellon doctorate

    He earns a doctorate in Pure and Applied Logic at Carnegie Mellon in 2018. His dissertation is titled “On the formalization of higher inductive types and synthetic homotopy theory.”

  3. 2020

    Maintaining mathlib

    He coauthors a 2020 paper with Gabriel Ebner and Robert Y. Lewis about maintaining mathlib, a community-developed library of formal mathematics. The paper describes tools that check proof developments for subtle mistakes and generate documentation for contributors.

  4. By 2023

    Postdocs and a Bonn professorship

    After his doctorate, he works as a postdoc at the University of Pittsburgh’s Department of Mathematics with Tom Hales and at Paris-Saclay’s Laboratoire de Mathématiques d'Orsay with Patrick Massot. In 2023, he joins Bonn’s Mathematical Institute as a professor.

  5. 2023

    Formalizing sphere eversion

    With Patrick Massot and Oliver Nash, he formalizes the local h-principle in Lean in 2023, reproving Smale’s sphere eversion theorem.

  6. 2025

    A Skolem Award and ERC grant

    In 2025, he shares the Thoralf Skolem Award with four coauthors for the 2015 paper “The Lean Theorem Prover (System Description).” He and Christoph Thiele receive a six-year ERC Synergy Grant for HALF, funded at 6.4 million euros to formalize harmonic analysis with Lean and help mathematicians verify proofs.

  7. As of October 2026

    Professor and mathlib maintainer

    He is a professor at the University of Bonn’s Mathematical Institute and leads its Formalized Mathematics workgroup. Mathlib lists him among its maintainers. In August 2026, he coauthors a blueprint for a Lean 4 formalization of norm-variation estimates for multiple ergodic averages; the formalization was completed largely automatically with frontier large language models.

  1. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI from 1961 to 2025, with a year-by-year chart.
  2. The United States employs an estimated 53% of people in our data with a known employment countryOur estimates of where AI careers are concentrated now and how countries’ shares of dated positions changed over time.
  3. 46% of living people in our data with known birth and employment countries work outside their birth countryOur estimate of cross-border careers in AI, from country of birth and the country of each current organization.
  4. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionOur estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.

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 Floris van Doorn yet. Send us a free-licensed photo.

  1. The Lean Theorem Prover (System Description) - Microsoft Research microsoft.com. Checked 19 October 2026.
  2. Jeremy Avigad's Home Page andrew.cmu.edu. Checked 19 October 2026.
  3. Maintaining a Library of Formal Mathematics arxiv.org. Checked 19 October 2026.
  4. Skolem Award for Floris van Doorn — Bonn Mathematics mathematics.uni-bonn.de. Checked 19 October 2026.
  5. CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs sigplan.org. Checked 19 October 2026.
  6. Skolem Award für Floris van Doorn — Bonner Mathematik mathematics.uni-bonn.de. Checked 19 October 2026.
  7. Will mathematical research results be verified by computers in the future? — Bonn Mathematics mathematics.uni-bonn.de. Checked 19 October 2026.
  8. Floris van Doorn's Home Page florisvandoorn.com. Checked 19 October 2026.
  9. Mathlib maintainers leanprover-community.github.io. Checked 19 October 2026.
  10. A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations arxiv.org. Checked 19 October 2026.