Formalising the (pro)étale topology of a scheme

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.