A computer-checked proof of the Four Color Theorem - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2023

A computer-checked proof of the Four Color Theorem

Résumé

This report gives an account of a successful formalization of the proof of the Four Color Theorem, which was fully checked by the Coq v7.3.1 proof assistant [13]. This proof is largely based on the mixed mathematics/computer proof [26] of Robertson et al., but contains original contributions as well. This document is organized as follows: section 1 gives a historical introduction to the problem and positions our work in this setting; section 2 defines more precisely what was proved; section 3 explains the broad outline of the proof; section 4 explains how we exploited the features of the Coq assistant to conduct the proof, and gives a brief description of the tactic shell that we used to write our proof scripts; section 5 is a detailed account of the formal proof (for even more details the actual scripts can be consulted); section 6 is a chronological account of how the formal proof was developed; finally, we draw some general conclusions in section 7.
Fichier principal
Vignette du fichier
FINALA computer-checked proof of the four color theorem - HAL.pdf (1.58 Mo) Télécharger le fichier
Origine : Accord explicite pour ce dépôt

Dates et versions

hal-04034866 , version 1 (17-03-2023)

Identifiants

  • HAL Id : hal-04034866 , version 1

Citer

Georges Gonthier. A computer-checked proof of the Four Color Theorem. Inria. 2023. ⟨hal-04034866⟩

Collections

INSMI LARA
162 Consultations
815 Téléchargements

Partager

Gmail Facebook X LinkedIn More