Mon lemme de topologie est vrai dans les espaces métriques, les espaces compacts ou même les groupes topologiques, mais je ne souhaite pas le démontrer plusieurs fois.

Je souhaite travailler avec des fonctions méromorphes, et pourtant, j’ai encore du mal à écrire rigoureusement toutes les conditions de la définition.

Derrière ces exemples se cache une dure réalité :
– Nos preuves sont très vulnérables à une légère modification anodine des pages précédentes.
– Nous devons souvent refaire des preuves très similaires en raison d’hypothèses légèrement différentes.
– Nos preuves doivent tenir compte de la manière dont nous avons démontré certains lemmes (et pas seulement des lemmes).

Ce sont précisément les problèmes que certains paradigmes de programmation nous permettent d’éviter. Cela est particulièrement utile pour expliquer les mathématiques à un assistant de preuve, mais nous verrons que la mise en œuvre de ces paradigmes sur nos trois exemples peut changer la façon dont nous faisons des mathématiques « sur papier ».