Preuves formelles, preuves calculatoires

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.

• Chapitre 1
• Chapitre 2
• Chapitre 3
• Chapitre 4
• Conclusion