Les Newsletters Interstices
    Niveau intermédiaire
    Niveau 2 : Intermédiaire

    Preuves formelles, preuves calculatoires

    Cet article est devenu obsolète, de par son contenu ou sa forme, il est donc archivé.

    Sécurité & Vie privée
    Langages, programmation & logiciel
    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.

    Newsletter

    Recevez chaque mois une sélection d'articles

    Niveau de lecture

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

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

    Votre choix a été pris en compte. Merci d'avoir estimé le niveau de ce document !

    Benjamin Werner

    Chercheur Inria, responsable de l'équipe TYPICAL, enseignant à l'École Polytechnique.
    Voir le profil