A formal proof of the four color theorem

Abstract

A formal proof has not been found for the four color theorem since 1852 when Francis Guthrie first conjectured the four color theorem. Why? A bad idea, we think, directed people to a rough road. Using a similar method to that for the formal proof of the five color theorem, a formal proof is proposed in this paper of the four color theorem, namely, every planar graph is four-colorable. The formal proof proposed can also be regarded as an algorithm to color a planar graph using four colors so that no two adjacent vertices receive the same color.

9 pages, 2 Figures

Cited by in corpus (19)

• The Simplicial Model of Univalent Foundations (after Voevodsky)
• A Deductive Verification Framework for Circuit-building Quantum Programs
• Machine Learning in Proof General: Interfacing Interfaces
• QED at Large: A Survey of Engineering of Formally Verified Software
• An introduction to univalent foundations for mathematicians
• Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
• Improving legibility of natural deduction proofs is not trivial
• A formal proof of Hensel's lemma over the p-adic integers
• An Existence Theorem of Nash Equilibrium in Coq and Isabelle
• Coloring Planar Graphs via Colored Paths in the Associahedra
• Generators and Relations for 2-Qubit Clifford+T Operators
• A Study of Continuous Vector Representationsfor Theorem Proving
• Proof Assistants for Teaching: a Survey
• A certified reduction strategy for homological image processing
• UTC Time, Formally Verified
• Proof Scores: A Survey (full version)
• On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
• Wheel Random Apollonian Graphs
• Mechanized semantics