四色定理的一个形式证明
A formal proof of the four color theorem
摘要：
自从1852年Francis Guthrie首次提出四色定理以来，一直没有找到四色定理的正式证明。为什么？为什么？我们认为，一个坏主意把人们引向了一条崎岖的道路。利用与五色定理的形式证明相似的方法，本文给出了四色定理的一个形式证明，即每个平面图都是四色图。形式证明也可以看作是一个算法，使用四种颜色的平面图，使没有两个相邻的顶点接收相同的颜色。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
