Revue philosophique

De l'entretien avec Thierry Coquand, publié sous le titre Langages des maths, langages de l'informatique, nous ne retiendrons qu'un aspect, celui de la difficulté des démonstrations en mathématiques.

Cette affirmation est étonnante, car la formalisation des mathématiques donne l'impression que les démonstrations sont faciles à établir ou à réfuter. Et pourtant non, car les établir complètement, sans divers sauts intuitifs, est très long et demande des notations bien adaptées.

Ecoutons Thierry Coquand

Avant la rencontre avec l’informatique, les mathématiciens, notamment Bourbaki, étaient déjà allés très loin sur le chemin de la formalisation des démonstrations, mais ils voyaient bien les limites de cette démarche. Si on donne tous les détails dans une démonstration, si on la formalise totalement, elle devient vite trop longue et illisible pour les humains.
En revanche, un ordinateur a besoin de tous ces détails et ne s’effraie pas de la longueur des démonstrations. L’arrivée de l’informatique changeait donc tout.

L'informatique utilisant un langage approprié (un type particulier de langage de programmation, dit "fonctionnel", comme les langages Lisp ou ML) permettrait d'avoir des démonstrations complètes, suivies et vérifiées pas à pas.

Thierry Coquand poursuit :

... nous avons découvert, depuis cinquante ans, qu’écrire des démonstrations absolument correctes est impossible sans ordinateur. Chaque étape du développement des mathématiques nous a cependant apporté de nouvelles notations qui nous ont rapproché de cet idéal. C’est pour cela qu’il y a une histoire des langages d’expression des démonstrations.

Par exemple :

Georges Gonthier et son équipe ont formalisé une démonstration du théorème de Feit-Thompson. La démonstration de ce théorème était connue depuis les années 1960, mais il leur a fallu six ans pour construire cette démonstration formelle, c’est bien le signe que tout n’était pas dit dans la démonstration originale.


Thierry Coquand, informaticien et mathématicien français, professeur à l’Université de Göteborg en Suède, est l’auteur de travaux en théorie de la démonstration et sur les mathématiques constructives.

 

Article complet : https://theconversation.com/langages-des-maths-langages-de-linformatique-120777 ou https://www.lemonde.fr/blog/binaire/2019/07/26/demonstrations-mathematiques-et-programmes-informatiques/