Un assistant de preuve (comme lean, coq ou isabelle) n'a pas le même but qu'un manuel de mathématiques.
Effectivement, dans un assistant de preuve il faut tout démontrer au moindre détail près. Je m'y suis essayé pour (tenter de) formaliser une preuve d'un calcul. Sans doute que je ne m'y suis pas pris de manière optimale (après tout, c'est la première fois que je manipulais un tel outil), mais j'ai vite abandonné après avoir passé plus de 800 lignes sur une partie triviale du calcul qui n'aurait pas méritée 10 lignes sur un article en papier.
Mais une des choses qu'un assistant de preuve ne fait pas, c'est expliquer une démonstration ; dire quelles étapes sont importantes, dire ce qui relève d'une méthode habituelle, à quel moment on a besoin d'adapter ladite méthode, etc. Alors que c'est justement le boulot d'un manuel de mathématiques.
Peut-être y-a-t'il des manières pertinentes d'inclure les assistants de preuve dans des manuels de mathématiques. Mais dans l'état actuel des choses, ça ne peut pas remplacer les démonstrations écrites de manières habituelles.
PS : Le rapport de 80 entre la taille de la démonstration formelle en assistant de preuve et la démonstration papier tiens sans doute au domaine dans lequel elle se plaçait (en plus de mon inexpérience avec l'assistant de preuve). Dans d'autre domaines, une il y aura plutôt un rapport de 2 entre la taille de la démonstration Coq et la démonstration papier.
[^] # Re: Typos, erreurs et preuves
Posté par danarmk . En réponse à la dépêche Sortie du Frido pour les Matheux. Évalué à 3. Dernière modification le 19 septembre 2023 à 13:42.
Un assistant de preuve (comme lean, coq ou isabelle) n'a pas le même but qu'un manuel de mathématiques.
Effectivement, dans un assistant de preuve il faut tout démontrer au moindre détail près. Je m'y suis essayé pour (tenter de) formaliser une preuve d'un calcul. Sans doute que je ne m'y suis pas pris de manière optimale (après tout, c'est la première fois que je manipulais un tel outil), mais j'ai vite abandonné après avoir passé plus de 800 lignes sur une partie triviale du calcul qui n'aurait pas méritée 10 lignes sur un article en papier.
Mais une des choses qu'un assistant de preuve ne fait pas, c'est expliquer une démonstration ; dire quelles étapes sont importantes, dire ce qui relève d'une méthode habituelle, à quel moment on a besoin d'adapter ladite méthode, etc. Alors que c'est justement le boulot d'un manuel de mathématiques.
Peut-être y-a-t'il des manières pertinentes d'inclure les assistants de preuve dans des manuels de mathématiques. Mais dans l'état actuel des choses, ça ne peut pas remplacer les démonstrations écrites de manières habituelles.
PS : Le rapport de 80 entre la taille de la démonstration formelle en assistant de preuve et la démonstration papier tiens sans doute au domaine dans lequel elle se plaçait (en plus de mon inexpérience avec l'assistant de preuve). Dans d'autre domaines, une il y aura plutôt un rapport de 2 entre la taille de la démonstration Coq et la démonstration papier.