Séminaire Géométrie Topologie Dynamique
Teaching mathematics to computers
06
jan. 2022
jan. 2022
Intervenant : | Floris Van Doorn |
Institution : | LMO |
Heure : | 14h00 - 15h00 |
Lieu : | 2L8 et en ligne |
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