Johan Commelin

Johan Commelin is an Assistant Professor in the Fundamental Mathematics group at the Mathematical Institute of Utrecht University. He works part-time (0.6FTE) at Utrecht University and part-time at Lean FRO, focusing on arithmetic geometry and formalization of mathematics.

His educational background includes:

• PhD in Nijmegen (2013-2017), supervised by Ben Moonen
• Master's degree with thesis on "Algebraic cycles, Chow motives, and L-functions" (2013), supervised by Robin de Jong
• Bachelor's degree with thesis on "Tannaka Duality for Finite Groups" (2011), supervised by Lenny Taelman

Commelin's research focuses on formalization of algebraic geometry, homological algebra, and condensed mathematics, as well as categorical logic and applications of o-minimality to algebraic geometry and topology. His work particularly examines applications of o-minimality to the theory of periods and motives. He is actively involved in the Lean community and led the Liquid Tensor Experiment following Peter Scholze's challenge.

His recent publications show a strong trend toward formalization of mathematics using the Lean theorem prover, with significant contributions to formalizing advanced mathematical concepts like perfectoid spaces and Witt vectors. His work bridges traditional mathematical research with computer-assisted proof verification.

Scientific awards include:

• Distinguished Paper Award for "Formalizing the Ring of Witt Vectors" at Certified Programs and Proofs 2021

Commelin supervises three PhD students: Raphael Douglas Giles, Christian Merten, and Pim Otte. He has received grants supporting his work in formalization of mathematics and is actively involved in organizing the group meeting on logic, formalization, and related topics at Utrecht University.

He is one of the maintainers of the mathematical library of the Lean theorem prover and has collaborated on projects like "Superficie algebriche" and "Sloganerator" with Pieter Belmans.