Assistant de preuve
En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques.
Conception
[modifier | modifier le code]Beaucoup de projets ont été lancés pour formaliser les mathématiques, en 1966, Nicolaas de Bruijn lance le projet Automath, suivi par d'autres projets. Les projets les plus avancés sont le projet Mizar en Pologne, le projet HOL (en)-Isabelle en Grande-Bretagne et aux États-Unis et le projet Coq en France[1].
Ces logiciels permettent à un humain de transcrire les étapes d'une démonstration mathématique dans un processus appelé formalisation. Grâce à elle, le logiciel peut ensuite vérifier la validité de la démonstration[2].
Le but de ces projets est de mettre à la disposition du mathématicien des outils informatiques pour l’aider à élaborer une version formelle du résultat auquel il s’intéresse. Le logiciel stocke aussi les résultats démontrés auparavant.
L'écriture de preuves entièrement formelles est une activité extrêmement fastidieuse ; de nombreuses étapes qui seraient sautées, car considérées comme évidentes pour le lecteur familier des mathématiques, doivent être décortiquées dans les plus grands détails. Cependant, l'assistant de preuve peut fournir plus ou moins d'automatisation pour limiter le travail de l'utilisateur humain.
Certains assistants de preuve, tels que PVS, possèdent des procédures de décision dans des domaines souvent utilisés et décidables (tels que l'arithmétique de Presburger) ; souvent, on leur ajoute des procédures de semi-décision (qui ne se terminent pas forcément avec succès).
Succès
[modifier | modifier le code]Selon une étude de Freek Wiedijk évoquée en 2011 dans le magazine Pour la Science[1] mais réactualisée depuis[3], sur la liste des « 100 théorèmes mathématiques les plus importants » — liste attribuée à Paul et Jack Abad[4] — 91 des 100 théorèmes ont été formalisés.
Avec les assistants de preuve actuels, le travail de formalisation est rendu fastidieux par un langage complexe[1].
Théorèmes vérifiés avec des assistants de preuve
[modifier | modifier le code]
Une réorganisation et une clarification du contenu sont nécessaires.
- Puissance 4, en 1988.
- La non-existence de plan projectif fini d’ordre 10, en 1989.
- Le théorème des quatre couleurs, en 2005.
- La conjecture de Kepler, en 1999, dont la preuve est vérifiée par l'assistant HOL Light le 10 août 2014 après douze ans de travaux[5],[6],[2].
- Le théorème de Feit-Thompson, un théorème important de théorie des groupes, en 2012[7].
Utilisation
[modifier | modifier le code]Les assistants de preuve sont utiles pour vérifier la démonstration des problèmes très complexes, et aident à produire une démonstration formelle. Le célèbre problème des quatre couleurs est l'un des problèmes dont la démonstration a été vérifiée avec cet outil.
Une objection à l'usage d'assistants de preuve est que, de toute façon, la sécurité des preuves obtenues repose sur le bon fonctionnement de l'assistant. En effet, les assistants de preuves sont de gros logiciels complexes, dont on peut soupçonner qu'ils soient eux-mêmes bugués. Un assistant de preuve bugué peut permettre de démontrer l'absurde. Certains assistants de preuve, comme Coq, produisent un terme de preuve dont la vérification peut être déléguée à un logiciel beaucoup plus simple qu'un assistant complet ; ainsi, Coq produit des termes du calcul des constructions (inductives, à présent), un lambda-calcul typé d'ordre supérieur, dont on peut relativement facilement vérifier s'ils sont correctement typés. Coq, de plus, a lui-même été prouvé dans Coq par son vérificateur de démonstrations, ce qui rend la confiance que l'on peut avoir dans ce logiciel un peu plus légitime[8].
Les assistants de preuve pourraient devenir des outils pour expliquer une preuve aux humains, avec un niveau de détails adaptable à la demande. Ils sont une démonstration sous forme interactive, le premier niveau étant un texte simple ; un utilisateur pourra demander plus de rigueur sur n'importe quel passage précis, pouvant accéder au niveau ultime de la démonstration. Ces logiciels peuvent devenir un outil d'enseignement[2].
Assistants de preuve
[modifier | modifier le code]Références
[modifier | modifier le code]- Jean-Paul Delahaye, « Du rêve à la réalité des preuves », Pour la Science, , p. 90-95 (lire en ligne).
- Patrick Massot, « Pourquoi raconter des maths à un ordinateur », sur www.larecherche.fr (consulté le )
- (en) Freek Wiedijk, Formalizing 100 Theorems, mai 2015.
- (en) « The Hundred Greatest Theorems ».
- « Kepler avait-il raison ? » (consulté le )
- Sean Bailly, « La conjecture de Kepler formellement démontrée », sur pourlascience.fr, (consulté le ).
- (en) « Feit-Thompson theorem has been totally checked in Coq » (consulté le )
- Bruno Barras, « Coq en Coq », Rapport INRIA, INRIA, vol. RR-3026, (lire en ligne)
