Time：14:00-16:00, Wednesday, March 25 2026
Venue：E14-116
Speaker：Christian Merten, Utrecht University
Title：Formalizing the ℓ-adic cohomology of a scheme in mathlib
Abstract: Formalization of mathematics is the process of digitizing definitions and theorems using a proof assistant. Lean is such a proof assistant and mathlib is its community maintained mathematical library covering most material encountered in an undergraduate mathematics degree, extending to graduate level and beyond in some areas. Very recently, mathlib has obtained definition of the ℓ-adic cohomology groups of a scheme. These groups are a central object of study in arithmetic geometry and were for example used in the proof of the Weil conjectures. The formalization of this definition is part of a larger effort to formalize the theory of pro-étale cohomology in a project joint with Jiedong Jiang from Westlake University. In this talk I will explain the process of formalizing such a definition and highlight some of the difficulties encountered on the way. I will also discuss how methods of auto-formalization are changing this process and explain how we use it to accelerate progress.
