Four Colours?

Richard Zach reports that Georges Gonthier has a paper verifying the four colour map theorem. I found this odd, since I thought that Hud Hudson had shown that the theorem is not actually true, at least not as typically stated. Hudson’s proof is here though that link may not be accessible to everyone.

6 Replies to “Four Colours?”

1. Mike says:

Might be worth mentioning that Melvin Fitting—pretty well-known logician—also claims that the four color theorem has been proven. Anyway here is the link/address: http://comet.lehman.cuny.edu/fitting/

2. Richard Zach says:

Well, what they prove is the theorem that every planar graph can be 4-colored. Hudson shows that it depends on how you define “simple planar map”, “adjacent” etc. whether this is equivalent to “every simple planar map can be colored by 4 colors so that no two adjacent regions are colored by the same color.” Hudson’s example, for instance, corresponds not to a planar graph but to the complete graph on 6 vertices. The paper by Gonthier gives some explanation of how you have to understand “simple” and “adjacent” so that the correspondence holds (and these definitions exclude, I assume, the example Hudson constructs).

3. Jonas! says:

from what i understand, four color theorem is a theorem in graph theory, rather than concerning any real graphs. the graphs that hudson uses in his “disproof” cannot be translated into graph theory.

4. Quale says:

As a grad student in math I find this weird not because the theorem is false (yes this is a counter example but it involves maps with infinitly long borders which are normally understand to be excluded. It is not a ‘map’ in the normal everyday sense of the word) but because it has already been proved.

There is a famous computer assisted proof which pretty much everyone in the math community has heard of. Perhaps this is a proof that doesn’t need computer assistance which would be a big deal, though it would be providing another proof of an already proved theorem.

5. Quale says:

Opps my bad, should have followed the link before I said anything.

The problem with the original computer assisted proof is that many mathematicians have been somewhat skeptical of proofs that rely on computer checking. They worry that there might be an error in the computer work, despite the fact that a fair number of normal proofs published have errors. This is a big deal since it has formalized the proof in a way which can be formally checked for correctness as opposed to just relying on the authors to ‘get it right’ when they translate the problem to source code.

6. Richard Zach says:

Jonas— I only glanced at Hudson’s paper yesterday, but IIRC the map can be translated into a graph, just not into a planar graph.