Preuves formelles, preuves calculatoires

Benjamin Werner (1)

1 TYPICAL - Types, Logic and computing

Dans cet exposé, Benjamin Werner présente les méthodes formelles appliquées à la validation de résultats spectaculaires comme la démonstration du théorème des quatre couleurs, ou encore de la conjecture de Kepler.

Mots clés: théorème des quatre couleurs; coloration de graphe; conjoncture de Kepler; Coq; méthode formelle

Domaines: Mathématiques [math]

Benjamin Werner. Preuves formelles, preuves calculatoires. Interstices, 2007. ⟨hal-01350254⟩