Johan Commelin
I am a postdoc in the group of Stefan Kebekus. My main interest lies in algebraic geometry and algebraic number theory.
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:
applications of ominimality to algebraic geometry/topology;
in particular, applications of ominimality to the theory of periods and motives.
At the same time, I am very actively involved in the Lean community.
Right now I'm leading the Liquid Tensor Experiment
following up on a challenge by Peter Scholze.
News & Olds
 Quanta Magazine published an
article
about the Liquid Tensor Experiment.
 Nature published a news story
about the Liquid Tensor Experiment.
 My grant proposal is accepted! It is a 2year DFG Walter Benjamin position
to work on LTE.
 The
Liquid Tensor Experiment has reached its first target!
See
this blogpost by Peter Scholze, for an account of his experiences the past half year.
 The 2022 edition of Lean for the Curious Mathematician
will take place at ICERM (Providence, USA).
I am coorganising this workshop with Jeremy Avigad, Kevin Buzzard, Yury Kudryashov,
Heather Macbeth, and Scott Morrison.
More details will follow. Stay tuned!
Contact details
Preprints
 With Reid Barton.
Model categories for ominimal geometry.
[arXiv:2108.11952]
 With Annette Huber.
Exponential periods and ominimality II.
[arXiv:2007.08290]
 With Annette Huber and Philipp Habegger.
Exponential periods and ominimality I.
[arXiv:2007.08280]
Publications

With Victoria Cantoral Farfán.
The Mumford–Tate conjecture implies the
algebraic Sato–Tate conjecture
of Banaszak and Kedlaya.
Accepted for publication in Indiana Math.
[arXiv:1905.04086]
 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.
 With Kevin Buzzard and Patrick Massot.
Formalising perfectoid spaces
Certified Programs and Proofs 2020, 299–312.
[offprint]
[arXiv:1910.12320]
[project webpage]

With Matteo Penegini.
On the cohomology of surfaces with
p_{g} = q = 2
and maximal Albanese dimension.
Trans. Amer. Math. Soc. 373 (2020) 17491773.
[arXiv:1901.00193]

On compatibility of the ℓadic realisations of an abelian motive.
Annales de l’Institut Fourier.
Volume 69 (2019) no. 5, p. 2089–2120.
[link]

The Mumford–Tate conjecture for products of abelian varieties.
Algebraic Geometry (6) 6 (2019) 650–677.
[link]

The Mumford–Tate Conjecture for the Product of an Abelian Surface and a K3 Surface.
Documenta Math. 21 (2016) 1691–1713.
[link]
Past teaching
Course  Semester 
Assistent for Funktionentheorie  Summer 2021 
Teaching: Coxeter Groups and Lie Algebras  Winter 20/21 
Assistent for Introduction to Algebraic Curves  Summer 2020 
Assistent for Mathematics for Natural Scientists II  Summer 2020 
Assistent for Cohomology of Algebraic Varieties  Winter 19/20 
Assistent for Mathematics for Natural Scientists I  Winter 19/20 
Seminar Local Fields  Summer 2019 
Linear Algebra 2  Summer 2019 
Other writing
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 Lfunctions, 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
 Lean and its mathematical library.
I am one of the maintainers of the mathematical library of the Lean theorem prover.
 Superficie algebriche. (Together with Pieter Belmans.) le superficie algebriche is a tool for studying numerical invariants of minimal algebraic surfaces over the complex numbers. We implemented it in order to better understand the Enriques–Kodaira classification, and to showcase how mathematics can be visualised on the web.
 Sloganerator. Together with Pieter Belmans I wrote a webapp that makes it easy to suggest slogans for tags (results) in the Stacks Project.