41 citations · 54 across the 13 of their papers we have counts for
15 papers
The Educational Proof Assistant Waterproof in an Introductory Proof Course: Proof Construction and Learning Processes
Pim Otte, Rogier Bos, Johan Commelin +1
We study the use of an educational proof assistant in an introductory proof course through a quasi-experiment in a varied setting: multiple teachers, students with different study…
Shaping the Future of Mathematics in the Age of AI
Johan Commelin, Mateja Jamnik, Rodrigo Ochigame +2
Artificial intelligence is transforming mathematics at a speed and scale that demand active engagement from the mathematical community. We examine five areas where this transformat…
Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin +3
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for ch…
Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth +1
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a compu…
Abstraction boundaries and spec driven development in pure mathematics
Johan Commelin, Adam Topaz
In this article we discuss how abstraction boundaries can help tame complexity in mathematical research, with the help of an interactive theorem prover. While many of the ideas we…
Model categories for o-minimal geometry
Reid Barton, Johan Commelin
We introduce a model category of spaces based on the definable sets of an o-minimal expansion of a real closed field. As a model category, it resembles the category of topological…
Formalizing the Ring of Witt Vectors
Johan Commelin, Robert Y. Lewis
The ring of Witt vectors over a base ring is an important tool in algebraic number theory and lies at the foundations of modern -adic Hodge theory. $\mathbb{W…
Exponential periods and o-minimality II
Johan Commelin, Annette Huber
This paper is a sequel to "Exponential periods and o-minimality I" that the authors wrote together with Philipp Habegger. We complete the comparison between different definitions o…
Exponential periods and o-minimality
Johan Commelin, Philipp Habegger, Annette Huber
Let be an exponential period. We show that the real and imaginary part of are up to signs volumes of sets definable in the o-minimal structure generated by $\…
Formalising perfectoid spaces
Kevin Buzzard, Johan Commelin, Patrick Massot
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geome…
The Mumford-Tate conjecture implies the algebraic Sato-Tate conjecture of Banaszak and Kedlaya
Victoria Cantoral Farfán, Johan Commelin
The algebraic Sato-Tate conjecture was initially introduced by Serre and then discussed by Banaszak and Kedlaya. This note shows that the Mumford-Tate conjecture for an abelian var…
On the cohomology of surfaces with and maximal Albanese dimension
Johan Commelin, Matteo Penegini
In this paper we study the cohomology of smooth projective complex surfaces of general type with invariants and surjective Albanese morphism. We show that on a Ho…
The Mumford--Tate conjecture for products of abelian varieties
Johan Commelin
Let be a smooth projective variety over a finitely generated field of characteristic~ and fix an embedding . The Mumford--Tate conjecture is a prec…
On compatibility of the -adic realisations of an abelian motive
Johan Commelin
In this article we introduce the notion of a quasi-compatible system of Galois representations. The quasi-compatibility condition is a slight relaxation of the classical compatibil…
The Mumford-Tate conjecture for the product of an abelian surface and a K3 surface
Johan Commelin
In this paper we prove the Mumford-Tate conjecture in degree 2 for the product of an abelian surface and a K3 surface over a finitely generated field …