La machine peut-elle démontrer ? Sans humain qui la dirige, sans doute non, mais l'ordinateur est de plus en plus utile pour l'assister, par exemple pour transformer une preuve humaine en preuve formelle. Des développements et applications spectaculaires sont actuellement en cours.

 Kurt Gödel (1906–1978).

La Machine peut-elle démontrer ? est le titre d’un article du numéro 8 de Tangente, paru voici trente ans. Il montrait sur des exemples élémentaires que, si un raisonnement permettait de réduire une question à l’analyse d’un nombre fini (et restreint) de cas vérifiables par ordinateur, alors la question relevait d’une démonstration par ordinateur. À l’époque, nombre de mathématiciens rejetaient encore ce principe, arguant (en toute rigueur, à juste titre) qu’il faudrait alors démontrer que le système d’exploitation utilisé était lui-même exempt d’erreurs.

 

Qu’est-ce qu’une démonstration ?

Pour aller plus loin, il faut préciser ce qu’est une démonstration. Malgré leurs différences de conception, les mathématiciens en ont tous la même idée. Chaque théorème mathématique se situe dans une théorie particulière, comme l’arithmétique ou la géométrie euclidienne. Ainsi, le théorème de Pythagore est un théorème de géométrie et celui concernant la factorisation des nombres un théorème d’arithmétique. À la base de chaque théorie se trouvent des définitions, qui donnent le sens des termes utilisés, et les axiomes, qui donnent les propriétés essentielles, mais indémontrables, des objets introduits. Ce sont les premières briques, qui vont permettre de démontrer tous les théorèmes, des vérités « primitives », que ... Lire la suite