Talk:Four color theorem/Archive 1

Archive 1

Archive 2

Archive 3

→

Archive 5

Initial talk entries

please fix the doubling:

"n 2004, Benjamin Werner and Georges Gonthier from INRIA formalized a proof of the theorem inside the Coq theorem prover. This removes the need to trust the various computer programs used to verify particular cases — it is only sufficient to trust the Coq prover."

---

I removed the following:

It has been proved that maps with countries that cover two or more non-adjacent areas (such as countries with colonies) require a maximum of twelve colours.

Either I don't understand this statement properly, or it is wrong. Suppose country #1 contains colonies of countries #2, #3,...,#n within it. Similarly, country #2 contains colonies of #1, #3,...,#n. And so on. The resulting map will need n colors. AxelBoldt 23:57 Oct 6, 2002 (UTC)

But what happened to the m-pire? This is a legitimate term, see e.g. http://portal.acm.org/citation.cfm?id=355274.355299&coll=Portal&dl=ACM . -phma

I agree - m-pires are an interesting extension (although I also agree that the assertion Axel removed must be wrong).

I will try to make a couple of images here to make the concepts more readily available (picture is worth a thousand words, etc.). In particular, this seems like the kind of topic which mathematically "unsophisticated" types might be very interested in, so we should smooth the intro as much as possible.

Like Fermat's last theorem, the 4-color theorem is rife with amateur "proof" attempts; I know I've seen a summary of common errors somewhere... User:chas_zzz_brown 16:52 7 oct 02 (UTC)

Quick update: from a google search...

Heawood proposed a theorem, but could not prove it. The theorem stated that every m-pire map could be colored with 6m colors (Hartsfield and Ringel). It was not for another 94 years before Jackson and Ringel proved the theorem.

So perhaps the original statement refered to 2-pires... User:chas_zzz_brown 17:34 7 oct 02 (UTC)

3/17/04 I believe I have proved this theorem incorrect, however I need varification. I created adjacent areas on a plane, and have found that the least amount of colors that can be used is five. I am unsure whether the map must be an actual geographical map, or if it can be theoretical. If you could clairify this for me, i would be most appreciative. Thank you-- Laura

The four colour theorem is for theoretical maps, which include all real maps. However remember that, if you are using a real map, bits of the same country which are not joined can be different colours. Also areas joined by a corner can have the same colour. Can you put an image of your map on this site? DJ Clayworth 18:06, 17 Mar 2004 (UTC)

Just to add to the amateurs...

There's a thing I don't really get... what was the difficulty in proving the theorem basically ?
Was it about showing that every map can be mapped to a planar graph ?

Intuitively, I thought that the Four color theorem could be equivalently expressed as

K₅ and K_3,3 are not planar

The complete graph K₅ means that all 5 vertices are adjacent, thus requiring 5 different colors to allow coloring without two adjacent vertices having the same color.

The same applies to K_3,3, where each vertex is connected to not more than 3 other vertices.

Both K₅ and K_3,3 can be made planar by just taking away one single edge in each. Thus, 4 colors suffice to color the modified K₅, while the K_3,3 is even 2-colorable.

Thus, it would be proved by Kuratowski's theorem - No planar graph contains a K₅ nor a K_3,3.
Then, the biggest group of fully connected vertices would be 4 as in the modified K₅.

It would be nice if someone could add to the Wikipedia article and explain why the above-mentioned condition is necessary but not sufficient, as I can imagine many people wondering about it just as well.

Obvious answer: There are nonplanar graphs which do not contain either K₅ or K_3,3 as subgraphs. And there are non-four-colorable graphs which do not contain K₅ or K_3,3. So Kuratowski's theorem has no relevance to the coloring problem. As you yourself point out, non-planarity and four-colorability aren't directly related, in that K_3,3 is actually two-colorable and nonplanar! So, even without the preceding rebuttal of your "argument," I don't see why you'd expect a result involving K_3,3 to be related to the four color theorem at all. --ajo, 23 Mar 2005

There are not nonplanar graphs which do not contain (a subdivision of) K₅ or K_3,3 as subgraphs. This is the amazing part of Kuratowski's Theorem. Planarity is certainly relevent to the Four Color Theorem, since it's the hypothesis. You have noted that the converse is false: that is, that a graph is 4-colorable does not prove that it is planar. This is true. If nothing else, Kuratowski's Theorem does provide an alternate way of stating the theorem: that if a graph contains no subdivision of K₅ or K_3,3, it can be 4-colored.

However, proving the theorem in this form is not intuitive, because all it immediately tells you is that you can locally 4-color every 5-vertex subgraph. But this forces several vertices to have a particular colour, which could make 4-colouring other subgraphs impossible. Deco 06:18, 23 Mar 2005 (UTC)

Update
Oh, and one more thing I found to wonder about: About the K₅ being a subgraph

Let's say that we have an arbitrary set of arbitrary numbers but that satisfies the following condition: Picking any 5 numbers out of the set always yields not more than 4 different ones.

Question: How many different numbers are there in the set ?
- The answer is 4.

True, but why should we care? --ajo

Hoang

Stuff from Wolfgang Haken entry

I was editing the Haken entry, when I realized there were a couple paragraphs about the controversy and impact of the 4-color theorem. That should properly be in the 4-color theorem entry. So here it is (with some additions by me):

At the time, the proof was considered very controversial because of its heavy dependence on computer "number-crunching" to sort through possibilities. Even Appel has agreed, in numerous interviews, that it lacks elegance and provided no new insight that has guided future mathematical research.

Others, however, have pointed to this work as the start of a sea-change in mathematicians' attitudes toward computers - which they had largely disdained as a tool for engineers rather than for theoreticians - leading to the creation of what is sometimes called "experimental mathematics."

Since then, there have been a number of computer-aided proofs, e.g. see the Kepler Conjecture, and the prestigious Annals of Mathematics, for the first time, accepted such a proof by D. Gabai, R. Meyerhoff, & N. Thurston of the geometric and topological rigidity of hyperbolic 3-manifolds.

I'm not sure how to fit this in; anybody want to try?--C S 02:41, Sep 8, 2004 (UTC)

Is the Four Color Theorem an example of Experimental Mathematics?

I don't believe so. I've never heard the term used to refer to a computer-aided proof, so I believe the use of the term in this context is wrong. The Experimental Mathematics entry should also be changed to reflect this. Can someone provide a reference to show the use of the term "experimental mathematics" to refer to a computer-aided proof? --C S 07:05, Sep 21, 2004 (UTC)

I've changed the definition of experimental mathematics to accurately reflect common usage. So I am removing the link to Experimental mathematics from the article. --C S 23:08, Oct 8, 2004 (UTC)

The Four Colour Theorem is absolutely not an example of Experimental Mathematics. A program was used to help prove it; Experimental Mathematics don't prove anything, they're used to find viable hypotheses. Whether a computer is used or not is irrelevent — either can be done with or without one. Deco 06:25, 23 Mar 2005 (UTC)

Link to another 2-D Theorem?

My intuition tells me that this has something in common with the mathematical proof of how many points on a 2D map can be connected to every other without allowing line-crossing. That was much easier. Don't remember the name though. 217.81.65.193 21:50, 2 Oct 2004 (UTC)

Uh, need a reference

I added this: "... and 1891 that Tait's proof was shown incorrect by Peterson ..." but I couldn't find good reference. There are only a handful of pages on Google that mention it. I've also found some bad misinformation out there, like a paper from the University of Auckland by Andreea Calude that comes up pretty high on Google claiming incorrectly that Tait disproved Kempe's false proof in 1880 - which makes me wish I could find more references. Anyway, if someone can find a book which settles this it would be good. A5 07:04, 16 Jan 2005 (UTC)

It is in the Notices of AMS article referenced at the end. -- Jitse Niesen 19:49, 18 Jan 2005 (UTC)

Hyphenation

I'm pretty sure the title should be "four-color theorem", not "four color theorem". I don't want to move and cause some weird double triple re-un-directs though. --Menchi 02:06, 27 Jan 2005 (UTC)

I disagree. The term "four color theorem" is common enough, in my (limited) experience. --ajo, 23 March 2005

    4CT is also acceptable.  --Jillbones 01:24, 16 December 2005 (UTC)

In response to Shadowraven

...and his 'disproof':

You way want to look at this.

Another victory for Mathematics! :) --TACD 21:52, 23 Mar 2005 (UTC)

Since the "disproof" is clearly incorrect but seems to frequently recur (here and in the article), perhaps it can be reworked into a "Common Misconceptions" section? It certainly helps to clearly explain the theorum when shown a 'wrong' counter-example and the 'right' way to color the map.

Kutulu 13:34, 22 Apr 2005 (UTC)

2004 or 2002?

The article has two copies of the same statement, only with different years:

In 2004, Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq theorem prover. This removes the need to trust the various computer programs used to verify particular cases — it is only sufficient to trust the Coq prover.

In 2002, Benjamin Werner and Georges Gonthier from INRIA formalized a proof of the theorem inside the Coq theorem prover. This removes the need to trust the various computer programs used to verify particular cases — it is only sufficient to trust the Coq prover.

Which is the right one?

--cesarb 12:05, 14 Apr 2005 (UTC)

This was annouced at a conference in France on Dec. 2004, and at a March 2005 meeting of Automated Reasoning Group the proof was referenced as being made 'last fall', so I'm confident than 2002 was just a mistake.

Kutulu 13:13, 22 Apr 2005 (UTC)

Thanks. --cesarb 13:45, 22 Apr 2005 (UTC)

Needs to be updated?

Just reading this: http://www.theregister.com/2005/04/18/four_colour_self_checking/

Perhaps this page needs to be updated (not sure enough to do it myself :) --Blinken 03:46, 19 Apr 2005 (UTC)

What needs to be updated? The work of Werner and Gonthier is already mentioned (twice in fact, but with different dates, see the above section on this talk page). -- Jitse Niesen 10:41, 19 Apr 2005 (UTC)

---

At any rate this article needs a bit of cleaning up, in that the History and Theorem Proved sections need merging. Ben Finn 18:15, 1 May 2005 (UTC)

Newby, sorry for possible sloppiness. I don't get why there are so many permutations that a computer must run through them. A "country" is an area on a surface with a continous border. Around that area are neighboring countries. There are only 2 possibilities,an odd or even number of countries. If even you need three colors, if odd 4.

Colouring just one country and its neighbouring countries is easy. This is called a locally correct colouring. It only becomes complicated when you have a whole map full of countries, like a map of the countries in Europe or the states in the United States. You can colour each country individually, but when you try and put all those colourings together you may find they're inconsistent. Good question, though. Deco 00:06, 7 May 2005 (UTC)

Date of Appel-Haken proof

Do we have any references for that they proved the four color theorem in 1976, as Viritidas' edit states? Both references are published in 1977, and one usually takes the date of publication. -- Jitse Niesen 09:49, 10 May 2005 (UTC)

NP-complete?

Can someone please clarify the statement in the introduction about four-colouring of maps being NP-complete? This is incorrect/misleading/confused for several reasons:

• There exist quadratic time algorithms for colouring a planar map with four colours. The existence of a quartic-time algorithm has been known since the work of Appel/Haken; the quadratic time algorithm has been known since the mid 90s with the work of Robertson et al.
• The problem of determining whether an arbitrary graph is THREE colourable is NP-complete. This is in fact one of the standard examples of an NP-complete problem. I guess it's probably true for four colours too but is completely irrelevant to this article, because this article is about planar graphs only.

So what was that sentence really trying to say? Dmharvey File:User dmharvey sig.png Talk 12:54, 6 Jun 2005 (UTC)

The person who said this was right, but quite misleading. I can vouch for your statements and have updated the article accordingly. Actually, 3-colouring remains NP-complete when restricted to planar graphs, which is curious (on a planar graph, k-coloring is in P for all k ≠ 3, and NP-complete for k=3). This is another one of those areas where the small differences between P problems and NP-complete problems emerge. Deco 03:31, 7 Jun 2005 (UTC)