Preuves formelles, preuves calculatoires
Si elle est complètement détaillée, une preuve se ramène à l'utilisation de règles logiques, dont la correction est précisément définie de manière syntaxique : c'est là une des caractéristiques du raisonnement mathématique. Réussir cette opération en pratique demande de faire appel à l'informatique, et plus précisément à sa branche dite des méthodes formelles.
 |
Dans cet exposé, structuré en quatre chapitres, Benjamin Werner distingue tout d'abord les deux rôles de l'ordinateur, son rôle de vérificateur formel étant bien distinct de son rôle de calculateur.
À travers plusieurs exemples, il s'attache ensuite à montrer comment les systèmes de preuves modernes, comme Coq, permettent de s'attaquer à des preuves nécessitant des calculs importants, et de répondre à des interrogations quant à la validité de certains résultats spectaculaires. Il montre ainsi comment Coq sert à prouver qu'un grand nombre est premier, puis comment ce système a permis de valider la démonstration du théorème des quatre couleurs
. Il présente enfin un chantier toujours en cours, la validation de la démonstration de la conjecture de Kepler.
Cet exposé de Benjamin Werner a été enregistré le 11 décembre 2006, à l'INRIA Rocquencourt.
- la présentation de 1 h 20 min en XML/SMIL : les transparents synchronisés avec la vidéo de l'orateur (haut débit).
- la présentation de 1 h 20 min en XML/SMIL : les transparents synchronisés avec la voix de l'orateur, sans sa vidéo (modem).
- l'ensemble des transparents synchronisés avec la voix accessibles individuellement (modem).
La mise en forme en XML/SMIL a été réalisée par Pierre Jancène. Pour visionner ces documents, utiliser RealPlayer.