It is becoming increasingly feasible to prove mathematical theorems in a computer program called a proof assistant and build large libraries with formally verified proofs.
Lean is one such program, which has the largest community of mathematicians collaboratively building a mathematical library with undergraduate and graduate level mathematics.
In this talk, I will show how to prove theorems inside Lean, and explain why this is useful. I will not assume any prior knowledge about proof assistants.

Diffusion simultanée sur:

 https://webconf.imo.universite-paris-saclay.fr/b/jer-7cp-7mk