A formal proof of the four color theorem

TL;DR

This paper presents a formal proof of the four color theorem, establishing that every planar graph can be colored with four colors without adjacent vertices sharing the same color, and provides an algorithm for such coloring.

Contribution

It offers the first formal proof of the four color theorem and introduces an algorithm for four-coloring planar graphs, advancing mathematical rigor and practical coloring methods.

Findings

Formal proof of the four color theorem provided

Algorithm for four-coloring planar graphs developed

Proof extends methods used for the five 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.