New proof of the four color theorem uses 8202 configurations reduced in parallel
Researchers developed a new proof of the four color theorem after almost a decade of work and a faster graph coloring method, which also helps in studying planar graphs.
Researchers have developed a new proof of the four color theorem, chip.pl reports. The work began in 2015 and took almost a decade. The proof relies on 8202 configurations, and the authors also devised a considerably more efficient graph coloring method chip.pl
chip.plchip.plOpen source ↗.
The four color theorem and earlier proofs
The theorem states that any map divided into disjoint regions can be colored with at most four colors, so that no two regions sharing a border have the same color. The question dates to 1852. British mathematician Francis Guthrie, coloring a map of English counties, noticed that four colors were enough to distinguish all neighboring regions, and he wondered whether this held for every possible map.
Alfred Bray Kempe presented the first attempted proof in 1879. It was regarded as correct for eleven years, until Percy John Heawood found an error in it. Some of Kempe's ideas nevertheless became a foundation for later research.
In 1976 Kenneth Appel and Wolfgang Haken presented a proof that for the first time used a computer to check a huge number of mathematical configurations. They reduced the problem to 1482 cases, which were verified by computers at the University of Illinois. The result caused controversy, because some mathematicians questioned whether a computer-assisted proof could be considered complete. A refined version appeared in 1997 and required checking 633 configurations chip.pl
chip.plchip.plOpen source ↗.
Parallel reduction and planar graphs
The new proof again confirms the theorem. It uses 8202 configurations that can be reduced in parallel instead of being analyzed one at a time. As a result, the procedure is considerably faster than earlier solutions.
The tools developed in the work may matter beyond map coloring. They help to better understand the structure of planar graphs, which are mathematical models made of points connected by lines that do not cross except at shared vertices. Such graphs are used in computer science, network analysis and the modeling of various phenomena.
