Johan Commelin

I am director of the Mathlib Initiative, and work part-time as universitair docent (assistant professor) at Utrecht University. My main interests lie in arithmetic geometry and formalization of mathematics.

From 2018 till 2023 I was a postdoc in the group of Stefan Kebekus in Freiburg (DE). From 2017 till 2018 I was a postdoc of Carel Faber in Utrecht (NL). From 2013 till 2017 I was a PhD student in Nijmegen (NL), supervised by Ben Moonen.

Current research topics include: formalization of algebraic geometry, homological algebra, and condensed mathematics; categorical logic and applications of o-minimality to algebraic geometry/topology; in particular, applications of o-minimality to the theory of periods and motives. I am actively involved in the Lean community. In 2021-2022, I have lead the Liquid Tensor Experiment following up on a challenge by Peter Scholze.

If you want to learn more about Lean, here's a great place to find guides/resources/tutorials/chat/etc.

I greatly appreciate (anonymous) feedback on my lectures, talks, and other activities.

Students

I am currently supervising 3 PhD students:

News & Olds

Contact details

@: j.m.commelin@uu.nl
johan@lean-fro.org
A: Room HFG4.17
Utrecht University
Mathematisch Instituut
Budapestlaan 6
3584CD Utrecht
Nederland

Preprints

Publications

  1. With Adam Topaz. Abstraction boundaries and spec driven development in pure mathematics. Bull. Amer. Math. Soc. DOI: https://doi.org/10.1090/bull/1831 Published electronically: February 15, 2024 [PDF]
  2. With Victoria Cantoral Farfán. The Mumford–Tate conjecture implies the algebraic Sato–Tate conjecture of Banaszak and Kedlaya. Indiana Univ. Math. J. 71 (2022), no. 6, 2595--2603. [arXiv:1905.04086]
  3. With Robert Y. Lewis. Formalizing the Ring of Witt Vectors. Certified Programs and Proofs 2021, 264–277. [arXiv:2010.02595] [project webpage] This paper was accepted with a Distinguished Paper Award.
  4. With Kevin Buzzard and Patrick Massot. Formalising perfectoid spaces Certified Programs and Proofs 2020, 299–312. [offprint] [arXiv:1910.12320] [project webpage]
  5. With Matteo Penegini. On the cohomology of surfaces with pg = q = 2 and maximal Albanese dimension. Trans. Amer. Math. Soc. 373 (2020) 1749-1773. [arXiv:1901.00193]
  6. On compatibility of the ℓ-adic realisations of an abelian motive. Annales de l’Institut Fourier. Volume 69 (2019) no. 5, p. 2089–2120. [link]
  7. The Mumford–Tate conjecture for products of abelian varieties. Algebraic Geometry (6) 6 (2019) 650–677. [link]
  8. The Mumford–Tate Conjecture for the Product of an Abelian Surface and a K3 Surface. Documenta Math. 21 (2016) 1691–1713. [link]

Past teaching

CourseSemester
Grondslagen van de WiskundePeriod 2 - 24/25
Bewijzen in de WiskundePeriod 1 - 24/25
Calculus and Linear AlgebraSemester 2 - 23/24
Bewijzen in de WiskundePeriod 1 - 23/24
Assistent for FunktionentheorieSummer 2021
Teaching: Coxeter Groups and Lie AlgebrasWinter 20/21
Assistent for Introduction to Algebraic CurvesSummer 2020
Assistent for Mathematics for Natural Scientists IISummer 2020
Assistent for Cohomology of Algebraic VarietiesWinter 19/20
Assistent for Mathematics for Natural Scientists IWinter 19/20
Seminar Local FieldsSummer 2019
Linear Algebra 2Summer 2019

Other writing

MacLane's Q'-construction and Breen–Deligne resolutions (draft). An unpublished note written as part of the Liquid Tensor Experiment.

My PhD thesis: On ℓ-adic compatibility for abelian motives & the Mumford–Tate conjecture for products of K3 surfaces [Erratum]. Completed in the summer of 2017 under the supervision of Ben Moonen.

I wrote my master's thesis, titled Algebraic cycles, Chow motives, and L-functions, in the spring of 2013 under the supervision of Robin de Jong.

I wrote my bachelor's thesis, titled Tannaka Duality for Finite Groups, in the spring of 2011 under the supervision of Lenny Taelman.

Side projects