Coq proved four colour theorem

Coq Proof Assistant

Coq means rooster in French. But it has been named after the name of its inventor, Thierry Coquand. It is an interactive theorem prover. It is not an automated theorem prover but includes automatic theorem proving tactics. It mechanically checks proofs of mathematical assertions. Vladimir Vocvodsky (Fields Medalist) is a big supporter of such proof verification computer programs.

World map with four colours (By Fibonacci [CC BY-SA 3.0], via Wikimedia Commons)

In 1852, Francis Guthrie, a graduate student at University College in London, wrote a letter to his younger brother, containing what he thought would be a simple little puzzle. He wrote

Can every map drawn on the plane be coloured with four colours so that no two regions having a common border have the same colour?

In 1879, Alfred Kempe demonstrated that five colours suffice. Kempe’s proof was an elegant attempt to solve four colour problem, you should read this article by Timothy Sipak (Alma College). In 1922 Philip Franklin proved that all maps with 26 or fewer regions can be 4-coloured. This wasn’t terribly edifying in itself, but Franklin’s method paved the way for the eventual solution by introducing the idea of a reducible configuration.

In 1950, Heinrich Heesch, who had invented a clever method for proving that many configurations are reducible, said that he believed the four-colour theorem could be proved by finding an unavoidable set of reducible configurations. The only difficulty was to find one –and it wouldn’t be easy, because some rule-of-thumb calculations suggested that such a set would have to include about 10,000 configurations. With the computers then available, it would have taken about a century to deal with an unavoidable set of 10,000 configurations. Though modern computers can do the job in a few hours!

In 1976, Kenneth Appel and Wolfgang Haken managed to reduce the number of configurations to be tested to 1,936 cases and went through all of them with aid of a computer program. After running the program for two months they concluded that four colours will always suffice. This proof was controversial because the majority of the cases were checked by a computer program, not by hand.

In 2008, George Gonthier and Benjamin Werner, proved four colour theorem using Coq. Unlike the programs used by Appel and Haken, Coq automatically generates a proof on the basis of the algorithm that has been selected. So we have is a proof of which 0.2% was done by a human being (that matters and must be gotten right) and other 99.8% by a machine (since Coq is certified to be bug free, we can be sure that rest is correct). The shortest known proof of the four colour theorem today still has over 600 cases and is a proof by exhaustion.

For further information, see: http://mathoverflow.net/q/164947

To know more about “automatic theorem proving” see: http://hardmath123.github.io/meet-the-robinson.html

Advertisement