Johan Commelin

I work part-time as universitair docent (assistant professor) at Utrecht University, and part time at the Lean FRO. 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