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é.

    Non classé
    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.
    Benjamin Werner

    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.

    • 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).

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

    Newsletter

    Le responsable de ce traitement est Inria. En saisissant votre adresse mail, vous consentez à recevoir chaque mois une sélection d'articles et à ce que vos données soient collectées et stockées comme décrit dans notre politique de confidentialité

    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