Archives

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.

acces au film

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 en cours à la date de l'exposé, 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.

Une mise en forme en XML/SMIL a été réalisée par Pierre Jancène. Pour visionner ces documents, RealPlayer était utilisé à l'origine, les évolutions logicielles ne permettent malheureusement plus de les lire.

Il reste possible d'accéder aux différentes parties de la vidéo, au format Real, lisibles avec RealPlayer ou VLC.

Niveau de lecture

Aidez-nous à évaluer le niveau de lecture de ce document.

Il vous semble :

Si vous souhaitez expliquer votre choix, vous pouvez ajouter un commentaire (qui ne sera pas publié).