Formalising the (pro-)étale topology of a scheme - C. Merten

Oct 6, 2025  ·   In Kyoto Japan  ·   Event ``AHGT Seminar''

Abstract

Formalising mathematics is the process of teaching mathematics to a proof assistant such as Lean. While sometimes this is a mechanical translation process, most often it requires mathematical insights on how to encode the mathematical objects efficiently in a formal language. Lean's mathematical library mathlib aims to provide unified foundations and definitions for all of mathematics. This objective requires every formalisation to fit in a bigger picture, often leading to a gap between pen-and-paper mathematics and its formal counterpart.

In my talk, after giving a brief demonstration of Lean, I will explain how we bridge this gap using the example of the formalisation of the étale fundamental group of a scheme highlighting some of the unforeseen difficulties encountered during the formalisation. I will close with reporting on the ongoing efforts of formalising the foundations of the (pro)étale cohomology of a scheme in mathlib.

1. C. Mathlib, The Lean mathematical library, 2019 [arXiv] [Git]
2. C. Merten et al. Formalisation of the étale fundamental group, Git Repository.
3. C. Merten et al. Formalisation of the (pro)étale cohomology of a scheme, Git Repository (following [BS13])