I'm a math professor who has lost years to this question. I've met various authors involved in successful proofs. My 1976 grad school application from the University of Illinois came postmarked "Four Colors Suffice" (Appel, Haken). I've also been inundated with well-intended crank proofs of every tar pit like this. One can tell the difference without focusing one's eyes.
These authors have long, established careers, with 2,000 MathSciNet citations between them. Waterloo is a hotbed of combinatorics; I doubt that they posted this before passing the paper around a bit.
Graph theory as a branch of mathematics is like photography as an art form: Anyone can point a camera, and one sees a lot of incredibly weak graph theory if one digs deep enough into the regional conference circuit.
This work is deep, relying on an understanding of generating functions that many casual practitioners don't possess. If the proof has a flaw, the issue will be technical and difficult to uncover. I love how people take the obvious bet that this is likely wrong because so many proof attempts have failed. In a prediction market, I'd bet on this proof being right.
I caught a rumour of this paper about 6 months ago, so I'm pretty sure that in the meantime it's been evaluated and assessed by colleagues. So I'm pretty sure it's going to be right, with only small fixable things that need tidying up.
Just as the incorrect proof by the amateur mathematician or crank is likely to be in a predictable form - a bunch of drawings of graphs with increasingly obtuse notation, reference to special cases within special cases, etc., isn't the incorrect proof by working combinatorialists likely to look exactly like this paper? An argument from complex analysis relating to either generating functions, Tutte polynomials, or some similar concept, together with some difficult arguments about how the asymptotics should be correctly used?
The fact that this includes arguments which casual practitioners would not be able to confidently use in a crank proof does not evidence its correctness. It just shows us that it's from a different type of person, susceptible to making a different type of error.
Your post feels like a dispatch from bizarro-world.
There is a good amount of second-order evidence that the proof is wrong. Further, I skimmed the introduction, and it seems the indicated approach cannot possibly work. My guess is that both authors are senile. (They're quite old.)
If you give me decent odds, I'd be happy to bet against you regarding the proof's correctness. Would you take 1:1?
Hey, could you please make your substantive points without swipes and personal attacks? If you know more than others, that's great, but then share some of what you know (without putdowns) so the rest of us can learn. If you don't want to do that, not posting is also a fine option.
I have no idea whether the proof is right or wrong, and I'm not so sentimental as to believe that the harsher person is more likely to be wrong. (Besides, naysayers are usually right, just like they are when predicting that any given startup will fail.) However, the HN guidelines (https://news.ycombinator.com/newsguidelines.html) ask you not to post like this and that's important too. Other users are making their case against the OP while following the guidelines just fine. Please be more like them.
There's no personal attack here. I'm sorry if that comment comes across as curt, but the post I responded is (in my opinion) grossly misleading and deserves pushback. For example, consider the statement: "If the proof has a flaw, the issue will be technical and difficult to uncover," made by someone claiming years of experience as a math professor thinking about this question. This is easily identifiable as wrong, because the purported proof is just 7 pages (actually less than that due to extraneous material) and does not use any particularly technical mathematics (a strong undergraduate major probably knows enough to comprehend what's going on). Indeed, people found the error in (less than) 12 hours after that comment was made.
The comment about senility is not a "swipe." It is a very real problem in the mathematics community. Mathematicians get old and are sometimes afflicted by dementia, and this unfortunately can manifest as hopeless attempts at famous problems. Atiyah's "proof" of the Riemann Hypothesis right before his death is perhaps the most well known example, but there are others that (thankfully) aren't disseminated publicly. In the pre-internet age, journal editors were able to make such things quietly disappear. But now we have the arxiv. This is valuable context for understanding why two mathematicians with distinguished publication histories might be posting an incorrect proof, which had not been provided by other comments.
That being said, I will endeavor to phrase such comments more carefully in the future. Thank you for your message.
I am going to finetune a content moderation model based only on the principle that it should, at all times, ask itself: “what would dang do?” and then do that
The tone of your comment is pretty harsh. What kind of 2nd-order evidence do you see? And why did you learn from the introduction that makes you so sure? It's only an introduction, which might only give you an oversimplified summary of their ideas.
Yeah, my guess is that both are senile if they're putting this on the arxiv.
Second-order evidence: Old mathematicians (~80). Famous problem. Weird, imprecise writing style. No mention of the proof by mainstream mathematical news sources (breakthroughs are usually accompanied by excited blogging/tweeting). No acknowledgements directed at other mathematicians who have checked or commented on the proof.
[deleted argument here; replaced by more precise comment below]
My tone is harsh because I think the best thing to do is to quietly ignore it, similar to how the community treated Atiyah's claims of a RH proof at the end of his life.
Some counterpoints: 2 mathematicians greatly increases chances of senility. Blogs/twitter also correlate much stronger with author age than truth of statement.
>The argument looks like it's based on large n asymptotics, so even assuming everything works correctly the strongest statement they can hope to show is that the theorem is true for all n > n_0, where n_0 is some large constant. But there is no mention of this fact. The theorem is claimed for all n.
This is completely wrong. A proof for all n>n_0 is a proof for all n, since any counter-examples have to exist as subgraphs of arbitrarily large graphs.
I don't think asymptotic estimates of that form suffice to treat this problem. (Where else in combinatorics has an argument of this form succeeded? What intuitive reason is there to expect it to succeed here?)
Specifically I think section 4 is basically nonsense. (I see Sniffnoy has already pointed this out below.)
(Re: your comment, Theorem 7 is going to fail below the smallest counterexample, right? This is bad, imprecise writing - a red flag.)
> The argument looks like it's based on large n asymptotics, so even assuming everything works correctly the strongest statement they can hope to show is that the theorem is true for all n > n_0, where n_0 is some large constant. But there is no mention of this fact. The theorem is claimed for all n.
The point is that if there were a small graph that was a counter-example, then there would be large graph counter-examples (and the percentage of them would increase with graph size), so proving that the 4 color theorem is true for large graphs implies that it is true for all graph sizes.
> the argument looks like it's based on large n asymptotics, so even assuming everything works correctly the strongest statement they can hope to show is that the theorem is true for all n > n_0, where n_0 is some large constant. but there is no mention of this fact. the theorem is claimed for all n.
They're claiming:
> Theorem 7. If there is a map L which cannot be 4-coloured then only an exponentially small fraction of the maps with n edges can be 4-coloured.
It's not bizarre at all. The math community has unfortunately been down this road many times before. When an 80-year-old announces a 7 page proof of a famous problem, the smart money is on the proof being wrong. As the comments elsewhere on this story indicate, this heuristic turned out to be correct. The only new twist is that we have two 80-year-olds this time, not one.
To be clear, I don't like this state of affairs. As suggested above, the best course of action seems to be to ignore the posting.
>It's so inappropriate that in the field that's actually trained for this, they're disallowed by compact, even with extensive evidence.
The field trained for this is not refraining from this because it's hard to get right, but because it undermines the privacy promise they give their clients! not an argument applicable to people who do not have that professional reputation to uphold.
Of course you should speculate about mental health of people when it's relevant to the topic - it's a factor heavily shaping many people's behaviour!
OK, section 4.2 makes no sense to me. So they have this set Q, right? Which is the set of plane graphs that can be written G=A*B*C*D, where * denotes joining at a cut vertex. Their goal is to show that every G∈Q can be 4-colored, and then use that to argue that a nonzero fraction of plane graphs can be 4-colored, and then argue (via the generating functions and asymptotics) that this means that they all can be.
Except... if they can show that every G∈Q can be 4-colored, then all of this argument with generating functions and asymptotics is unnecessary, right? Because surely G can be 4-colored iff A, B, C, and D all can; and since A, B, C, and D can be any plane graph, that would be the end of it -- if you have a plane graph A and you want to 4-color it, all you'd have to do is stick a 3-path hanging off the end of it to put it in Q (indeed, in the subset they call \overline{Q}), and then 4-color that. The rest of the argument would appear to be unnecessary!
Meanwhile, their argument for why graphs in Q can be 4-colored doesn't seem to make any sense to me. It's inductive, but they haven't written it in a clear manner that makes it exactly apparent how they inductive hypothesis is used. I honestly do not see how they are justifying the statement "It follows from the Induction Hypothesis that S_1 is 4-colorable" -- it doesn't look like any work is being done, it all looks circular to me!
An inductive hypothesis mentioning some independent variable like n needs to look like a conditional, e.g.: "If all maps in Q with at most n-1 edges are 4-colorable, then all maps with at most Q(n) is 4-colored, all maps in Q with at most n edges can be 4-colored" and then it has to be shown.
From my reading, it looks like can't make up their mind about whether Q = {X . Y: X, Y graphs} or Q = {X . Y : X, Y in Q}. Neither definitions seems to work everywhere.
This definition fails because Q-bar needs to be a subset of Q, but in Q-bar, the graphs T1, S2, and T2 are specified to be the single-edge graphs e1, e2, e3. But single-edge graphs are not in Q.
My memory is that the Four Colour Theorem was one of the first computer search-assisted proofs which caused all sorts of epistemological questions. Specifically how to know whether the software had no bugs and ran correctly, and how re-running to get the same result only lowered the probability and did not yield absolute certainty. Seems sort of a quaint concern now.
(Apologies for no reference. I hope I'm not misremembering.)
You're remembering entirely correctly! I gave a talk on the Four Color Theorem as part of my master's degree in 2001, and it was a somewhat active epistemic debate among mathematicians at the time. I took the position that examining code was no different than examining a proof, that running it through a computer was no different than running it through your brain, and that mathematicians are not shy at all about "automating" processes over uncountable infinities in proofs, so why should we be shy about automating them over thousands mechanically?
There is a fun faith-shaking element to the story, though. The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them. And IIRC, he found about a dozen errors! They weren't fatal -- he was able to repair them -- but that whole process didn't really reassure people. ;)
The original computer assisted proof of the four colour theorem was written in IBM 370 assembler [0]. This was naturally susceptible to programming errors such as those discussed above. Gonthier's subsequent certified proof requires trust in a much smaller body of code and hardware [1].
That's a really good question. I may have known the answer to it twenty years ago, but I don't now. XD
What I can tell you is that it wouldn't have been so straightforward as that. We're not talking about an axiom-to-result symbolic proof piece of software like you might attempt to write now. It wasn't a computer proof so much as a computer-assisted proof. Lots of human analysis to describe specific properties, and then a computer program to check that a long list of geometric configurations had those properties.
I don't know exactly what the program output as its proof, but I can only imagine the problems would have been small assumptions built into its design failing in corner cases. The theorem is notoriously difficult to reason about rigorously, and there have been a number of accepted proofs over the years that turned out to be false. It really doesn't help the whole situation that not only is it the first major computer-assisted theorem, it just happens to deal with a result that people are already wary of.
>The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them
I don't feel this is fundamentally different from the categorization of finite simple groups, which is also combining many small theorems and proofs, yet more widely accepted.
The same issues come up with interactive zero-knowledge proofs[A], where someone proves that they possess certain private information without leaking said information.
The proofs have the form:
1) Give the prover a challenge that they only have a 50% chance[B] of passing if they don't possess the private info.
2) Repeat as necessary with new, independent challenges.
3) If they keep passing, hooray! The probability that it's a faker decays exponentially. You can get really high confidence, very quickly!
Doing more rounds is just like re-running the computer proof.
[A] I first learned about the issue from reading the Scott Aaronson lectures that became Quantum Computing Since Democritus
[B] Doesn't have to be 50%, any figure will give the exponential decay and only require a linear increase in the number of rounds, so long as the probability stays the same between all rounds.
I fail to see the connection - new runs of the compuuter proof isn't going to randomize the code (like it does in zkp), so its not going to reduce the probability of error (excepting cosmic ray induced errors of course)
Yes it is — the fact that the later computations got the same result is evidence that the earlier ones weren’t flukes.
My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent. Randomization is one way to achieve that but not a hard requirement.
Even so, it seems you do see the connection, you just dispute one element that you think is critical.
> My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent.
But they are obviously not independent.
This is like flipping a coin once, looking at the result 20 times in a row (without flipping it again), concluding you have magic luck powers since you got heads twenty times in a row, and that would be really unusual in the analgous system where you flipped a coin 20 times instead of just looking at it.
> Randomization is one way to achieve that but not a hard requirement.
This is besides the point, but pray tell. How do you reduce the probability of an algorithm being incorrectly programmed by means of running it multiple times without changing the input or introducing some randomness somewhere? I don't think that's possible. Really the ZKP case isn't even checking the algorithm but checking a specific user input is consistent.
I think this would be equivalent to denying that BPP without coin flips is P, which afaik it is.
> Even so, it seems you do see the connection, you just dispute one element that you think is critical.
I mean, i guess you could say that if you modify the system to add the connection you are trying to establish, then yes the connection becomes obvious.
Yes, independent with respect to the variable you're testing. In the ZKP, the independence is between the challenges given to the prover. In the computational proof, independence is between the probability of computational error affecting the calculation. (To be sure, you'd want to run the proof on different hardware!)
>> Randomization is one way to achieve that but not a hard requirement.
>This is besides the point, but pray tell.
Wait, what? Your original comment[1] was specific alleging that the absence of a randomizer completely broke the analogy:
>I fail to see the connection - new runs of the compuuter proof isn't going to randomize the code.
How would this be "beside the point" when it's the point you introduced? Did you forget the point you were trying to make?
>How do you reduce the probability of an algorithm being incorrectly programmed by means of running it multiple times without changing the input or introducing some randomness somewhere?
Even doing the same run on the same hardware would provide evidence against against the earlier result being a fluke (e.g. from cosmic rays), as I said before. But yes, as above, to round out the possibilities, you'd want different people to translate the proof into different languages and hardware and run it there -- that would likewise increase your confidence in the result, just like running different rounds of the interactive ZKP would.
>I mean, i guess you could say that if you modify the system to add the connection you are trying to establish, then yes the connection becomes obvious.
Sorry, are you really saying that you see no parallel whatsoever between:
a) Run the 4-color computer proof multiple times to increase your confidence that the result wasn't just luck, and
b) Run additional rounds of an interactive ZKP to increase your confidence that the prover wasn't just lucky?
If so, that feels like more of a you-problem.
If you were disputing that additional runs of the 4-color computer proof could increase your epistemic confidence in it, then you should have raised that in response to the original comment[2], not one (like mine) that accepted it and pointed out an analogous situation.
> In the computational proof, independence is between the probability of computational error affecting the calculation. (To be sure, you'd want to run the proof on different hardware!)
But i don't think that is the concern at hand. Yes, re-running can reduce probability of failures due to soft-memory errors and such. But does nothing against logic errors (or non-transient hardware errors). My understanding is the main concern with the proof is not that a cosmic ray hits RAM and flips a bit, but that either the logic may be wrong or a general epistimitic unease that no human directly inspected the cases of the proof.
In any case i said as much in my original comment. To quote: "excepting cosmic ray induced errors of course"
> Wait, what? Your original comment[1] was specific alleging that the absence of a randomizer completely broke the analogy:
Yes, i stand by that (although accept your point that independence not randomization is the salient property). I also maintain that whether or not it is theoretically possible to do independent tests without a randomness is irrelavent to the matter at hand. What matters is if rerunning the code was an independent experiment, not what could theoretically be possible. Even if there exists some non-random way to do that, its irrelavent to whether or not any method was used.
> Sorry, are you really saying that you see no parallel whatsoever between:
>
>a) Run the 4-color computer proof multiple times to increase your confidence that the result wasn't just luck, and
>
>b) Run additional rounds of an interactive ZKP to increase your confidence that the prover wasn't just lucky?
Yes.
Although for greater clarity, i would clarify (a) to say i don't see the connection to non-negligibly increasing your confidence the result of the 4 colour is correct. I agree (and said this in my very first comment) that it would increase your confidence that you didn't get an incorrect result due to a soft-memory error. I would say that relative to all the possible reasons why you might get an incorrect answer, transient hardware failure is very low, so the increase in confidence from rerunning is negligible because the meat of the question is programming error.
In the analagous situation, re-running the zkp gives an extremely high increase in confidence the answer is correct, usually at least halving the possibility of error.
> If you were disputing that additional runs of the 4-color computer proof could increase your epistemic confidence in it
Sure, although the original comment was a bit vauge as to exactly what they meant.
Most of this proof is very dense. But Theorem 7 seems like an interesting tactic that allows the authors to infer nonexistence from rarity:
>Theorem 7. If there is a map L which cannot be 4-coloured then only an exponentially small fraction of the maps with n edges can be 4-coloured.
It's one of those things that seems obvious in retrospect — of course large random graphs should be likely to contain any particular graph! But it hadn't occurred to me in my own (very amateur) considerations of the problem.
Will be interesting to see if it's correct. We've gone from an argument too long for a human to read to one in just seven pages.
I think that's a bit different - in the probabilistic method you show that if you randomly sample a graph (say) then the probability of it having some property is > 0 - therefore there must exist some graph having the property.
Theorem 7 in their paper is trying to count the number of graphs that contain a hypothetical 4-color counterexample if it exists. It's done by hitting a suitable generating function with a big analysis hammer to bound its coefficients, not by probabilistic means.
I'm not a mathematician, but when I was in school I read a lot of 'pop math', and fancied myself a lot better at it than I was (or am). I was fascinated by things like the FCT, and recall writing a document ...I don't think I kidded myself proving it, but at least 'understanding' it.
The rough sketch was to show that it was not possible to construct a map that required five colours: that if you take a blob of one colour, wrap it in three others, all four are touching the others, but you can't possibly add a fifth since it either only touches the outer three, or it has to prevent two of them touching to get to the inner one (then the non-touching ones could be recoloured the same).
To this day, although I of course realise I was having no groundbreaking thoughts and it did not constitute a proof, I do not understand why the actual proofs are so complex, or require so much computation? It eluded far greater minds for over a century - what am I missing that makes it so problematic?
It's (relatively) easy to prove that you can't have five regions that all touch each other. If you could then that would mean that a map requires (at least) five colours, but that's not the only way a map could require five colours. Even so, it's certainly the first thing to try.
But colours-at-distance can be forced, so proximity isn't needed to create the need for another colour.
The theorem is difficult for two meta-reasons. One is that there are arbitrarily many planar configurations, and you need to prove that they are all four-colourable. The other is that whether or not a planar graph is three colourable is NP-Complete, and showing a planar graph is five-colourable is fairly easy, so it's on the boundary between fairly easy and really hard.
The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example. This is easily done by hand.
Appel and Haken's proof of the four-colour theorem proceeded the same way, but the unavoidable set was large. The computation was to confirm that the set was unavoidable, and that each element was reducable. This involved a huge amount of tedious bookkeeping, best done by machine, but it was really just "doing the sums". The real work was creating a finite amount of bookkeeping that would then constitute a proof.
>The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example. This is easily done by hand.
Isn't this missing a crucial point? You seem to be saying:
1. There is some (small) set S of graphs, all of which are 5-colorable
2. Every planar graph has at least 1 sub-graph in S
3. Therefore, all planar graphs are 5-colorable
But, from statements 1 and 2, one can only conclude that every planar graph _has a sub-graph_ that is 5-colorable, not that the entire graph is 5-colorable.
Don't you also need to prove that the complement of the sub-graphs is 5-colorable?
> The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example.
You said:
> Isn't this missing a crucial point? You seem to be saying:
> 1. There is some (small) set S of graphs, all of which are 5-colorable
This is not what it's saying. It's saying that these graphs cannot be in a minimal counter-example. That's different from simply saying that they are 5-colourable.
> 2. Every planar graph has at least 1 sub-graph in S
> 3. Therefore, all planar graphs are 5-colorable
No, you've missed a bit of my comment. I said:
> showing for each of those that it cannot be in a minimal counter example.
So we have an unavoidable set U. So for every graph G there is an element S of U that is a sub-graph of G.
But we have also shown for every element S of G that any graph containing S cannot be a minimal counter-example. We're not showing that these elements S of U are themselves 5-colourable, we are showing that any G containing S is not a counter-example to the theorem.
So now suppose the theorem is false. That means there is a graph that requires 6 colours. From among those choose a minimal one, so M is a minimal counter-example. But the set U is unavoidable, so there is a S in U that is a subgraph of M. But any graph containing S cannot be a minimal counter-example, and we have our contradiction.
Hence there are no counter-examples, and the theorem is true.
For the Five Colour Theorem the unavoidable set U has only four graphs, so it's easy to check by hand. For the Four Colour Theorem in the original proof there were around 2000 elements of U, so it was infeasible to check by hand. That has been reduced to 633 graphs in U, but it's still tough to check by hand.
The paper in the original submission here takes a different approach.
> I read "those" as "those subgraphs" rather than "those graphs".
That is the correct reading; your mistake must be elsewhere?
>> [the proof] proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example.
No minimal counterexample to the claim [that a planar graph is 5-colorable] can contain any of these subgraphs. All planar graphs contain at least one of these subgraphs. Therefore, all planar graphs fail to satisfy the predicate "this graph is a minimal counterexample to the claim that all planar graphs are 5-colorable".
The elaboration is very explicit that the theorem is "for every subgraph S in the unavoidable set U, that subgraph (S) cannot be contained in any minimal counterexample":
>> we have also shown for every element S of G that any graph containing S cannot be a minimal counter-example.
As the sibling comment to this says, you must still be confused about something here. Let me expand.
The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds as follows.
Cleverly produce a set U of small graphs S that have the following properties:
1: For every graph G, there is an S in U such that S is a sub-graph of G;
2: If G is a counter-example to the theorem, and S from U is a sub-graph of G, then there is a smaller graph H that is also a counter-example.
This is enough, because now let M be a minimal counter-example. By (1) there is an S from U that is a sub-graph of M. But by (2) there is then a smaller counter-example, contradicting the minimality of M. So there can be no counter examples.
With that now in mind, here is the original statement:
We proceed by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example. This is easily done by hand.
You don't just show that the graphs in S are 5-colourable. You show that they couldn't possibly be part of a minimal non-colourable graph (e.g. if a graph containing this subgraph is not 5-colourable, you can replace this subgraph with this simpler subgraph, and the larger graph will still be non-5-colourable).
That shows (loosely) that there is no map with five countries that cannot be four-colored. It says nothing about maps with six, seven, etc. countries. An actual map may have billions of countries and need not even contain “a blob of one colour, wrapped in three others”.
Loosely because
a) it only shows it for such maps that contain such a blob. Who says other maps with five countries are easier to four-color?
b) it doesn’t rigorously show it. That you (and me, and everybody who looked at it) can’t find a way to draw that fifth area that touches all others doesn’t say much. what are your arguments for showing you looked hard enough?
For a similar case, read about the Jordan curve theorem. In layman’s terms, it says closed curves on a plane have an inside and an outside part (https://en.wikipedia.org/wiki/Jordan_curve_theorem). Naive readers think it’s so trivial to not require a proof, and it took mathematicians a while to figure out that it needed one. I don’t know the details, but mathematicians may have observed that that theorem also is true on a sphere but isn’t true on a torus (a closed loop ‘around the hole’ in the torus doesn’t have an interior and an exterior). So, they needed an explanation as to why it’s true on a plane or a sphere but not on a torus (the answer essentially boils down to “because a torus has a hole in it”, but that requires a rigorous definition of what a hole is)
"An actual map may have billions of countries and need not even contain “a blob of one colour, wrapped in three others”."
In fact every map of interest will contain a blob wrapped in at least three others.
But they are right that the problem is showing that the theorem holds for maps with billions of regions, or more. Decisions you make early in the process of colouring the map can turn out to be wrong, but only much later as you are trying to colour the last few.
In short, you are saying "I can't see how it can go wrong", but that's not enough ... there are things that might happen that you weren't able to imagine, and that's part of why proofs like this are hard.
Also, the theorem is true, and that makes it hard to explain why it might go wrong. Because we now know that it doesn't.
The grand-parent comment also says:
"... the Jordan curve theorem ... is true on a sphere ..."
The stronger form is not true on a sphere. The stronger form says that every topological sphere in 3-space has an interior that's retractable to a point and an exterior that's retractable to a shell. But the Alexander Horned Sphere[0] is a counter example.
In short, weird things you didn't suspect can happen, so proofs are sometimes harder than you think, even for "obvious" things.
in some sense because there might be strongly non-local effects... an assignment of color in one part of the graph can have an effect on what colors are allowed in a very different part of the graph. Planarity assures some degree of "locality", you can't arbitrarily connect one point to another point.
But as a result there could never be an area of an infinitely large map that had five regions each needing a different colour. I understand people are saying but you take two such sub-maps, put them next to each other, and maybe the 'outside' colours are the same - but in that case you could always just recolour them individually before putting them together?
What you've said here might be a reasonable reply in your head, but for me, reading its parent, and this reply, I can't work out what you're trying to say.
You need to be really careful about things like "infinitely large map" ... if you want to talk about really large things then they are really large. But if you want to talk about infinite sized things then you need to be careful. There are traps in infinities, and this theorem is about finite maps (or equivalently, graphs).
Proving that a small, local sub-section doesn't require five colours is helpful, but no one has been able to extend that, because there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
You are saying the sorts of things I've seen many times before, but you need to try to make complete, precise statements about exactly what you propose. So far all you've said is that you can't arrange five regions that all touch each other, and that's true. Now, exactly how do you extend that to a map with billions of regions?
It was the comment I replied to that introduced infinitely large maps - but regardless I wasn't trying to be as clever as you might be trying to assume (and of course not finding it :)) - I would have said the same about 'really large' or indeed 'just a bit larger than the 4 or 5 regions I described initially'.
> there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
This is the bit I can't grasp - I honestly appreciate the responses and attempts to explain it, but it just (mistakenly, I can accept even if I don't understand) seems counter-intuitive to me. As in, intuitive that it extends, or that there's no such problem.
Maybe I just need to play with it on paper a bit, stumble into such a spooky action to get it.
> Now, exactly how do you extend that to a map with billions of regions?
I don't have the background for the precision you'd like I'm afraid (if I did, I'm sure I'd understand anyway!) but loosely - divide and conquer; a similar thing happens at the interface of all the 'sub-maps'?
>> there is a kind of "spooky action at a distance" that can happen
> This is the bit I can't grasp
OK. Let me give you a collection of statements, each of which I can expand on, but which might give you a sense of the problem.
* Instead of colouring regions in a map we can colour vertices of a graph;
(put a vertex in each region and connect vertices if their regions share a border)
* If a graph can be three-coloured then it can be four-coloured;
(Any three colouring is a four colouring, but with no vertices of the fourth colour)
* An instance of colouring an arbitrary graph can be converted into an instance of colouring a planar graph;
(There is a "widget" that uncrosses edges)
* Given a number to factor, we can construct a graph such that three-colouring the graph will produce a factorisation[0];
(Graph three-colouring is NP-Complete, so this is even easier than that)
Broadly, we can construct a graph that has exactly one (up to permutation of colours) valid three-colouring. As you start to colour it you find that you have to make choices, on average about $4/3$ choices per vertex[1]. But the wrong choice results in not being able to complete the colouring, and you don't know which choice or choices were wrong.
So you get this "spooky action at a distance" thing going on.
Sometimes a planar graph can't be coloured with three colours, and sometimes it can but a colouring is hard to find. When we allow the extra colour it turns out that it's always possible, but it's not obvious that that should be the case.
That's an #ISS-level view of the ideas ... hope it helps.
I'm sure I'm mistaken, but I believe the conversion to a graph loses exactly the information I'm trying to use: a vertex with three edges, where each of those vertices are also all interconnected, can have a fourth edge to a fifth vertex which also has an edge to each of the others; on the map this is not possible. Right?
From my napkin sketch to satisfy myself, I think you can show the same thing equivalently by saying 'and the edges are not allowed to cross' - but I don't know if that's something that exists in graph theory? (If so, it seems to me it should be used here? And if it is, well, finally we have a modicum of precision for what I'm trying to get at!)
If you have a map in which you want to colour the regions, you can convert to a graph by putting a capital city in each region, then putting a road between two capitals of countries that share a border. Colouring the capital cities vertices) so that any joined by roads (edges) get different colours is exactly the same problem.
The graph-colouring problem is more general now, but every planar graph is equivalent to a map and vice-versa ... there is a one-to-one correspondence between these problems.
Now we move to the NP-Completeness of the 3-colouring of general graphs. That shows that this sort of thing is hard for the reasons I gave in the grandparent post.
"But" I hear you say "That's for general graphs, and not for planar graphs!"
Yes, but there is a way to convert a graph-colouring problem on a non-planar graph into an equivalent graph-colouring problem on a planar graph, so we neither gain nor lose much by consider just planar graphs.
So 3-colouring planar graphs is NP-Complete.
Then you get into my comments about making bad choices and having to backtrack, and spooky action at a distance.
I have no idea what that guy is talking about, but your post reminded me of a fun trick. If you have a colouring of every finite subgraph then you can show the existence of a colouring of the whole graph by using Tychonoff's theorem.
What poset should we set up on which to invoke Zorn's lemma directly? Anything I can think of does seem to me more easily understood via compactness/the ultrafilter lemma, but that may just be a fact about my own psychology.
Yes, but invoking Zorn's lemma on that poset does nothing useful. This just proves the trivial fact that the big graph exists. How do you prove that a coloring of the big graph exists?
And if we take the poset to be partial colorings ordered by inclusion, it's not the case that a maximal partial coloring must color the entire graph. Some partial colorings have made choices which prevent them from being extended any further.
[To be clear, whenever I say "coloring", I mean from a fixed set of colors. E.g., a 4-coloring.]
Put another way, it actually is important here that the set of colors we are talking about is finite. It's NOT the case that just having every finite subgraph be C-colorable entails that the entire graph is C-colorable, when C is infinite. For example, if G is the complete graph on an uncountable set of nodes and C is a countably infinite set, then every finite subgraph of G is C-colorable, but G itself is not.
So somewhere in the argument, the finiteness of C must play a role. This is in ensuring compactness.
> there could never be an area of an infinitely large map that had five regions each needing a different colour
A more precise version (infinite -> finite, "...needing a different color looking only at that sub-map) is plausibly true. That doesn't help you though, because...
> maybe the 'outside' colours are the same - but in that case you could always just recolour them individually before putting them together
...this is false. Five patches of one sub-map might touch one patch of the other sub-map. So now you'd have to prove that the first sub-map can be colored with three colors to rescue your proof of the FCT. Further...
> you take two such sub-maps, put them next to each other [...]
...your argument here seems to boil down to "I can construct the full map by gluing together sub-maps". Depending on how you constrain the sub-maps to prove necessary properties (see above), this may not be true. But even if it were, your argument that it works seems to only consider gluing together two sub-maps of specifically size five, which obviously does not allow you to construct maps with more than ten patches.
This makes for two to three fully deal-breaking errors in your proof sketch.
As a followup, this proof has now been declared as fatally flawed by John Carlos Baez, with some additional analysis by Noam Zeilberger. The argument is beyond my personal mathematical knowledge, but I would consider this a pretty definitive verdict.
Not only does Waterloo have a world-class C-&-O department, they also had a hero
from Bletchley Park - Dr William Tutte, a kind gentle genius that never
bragged about his accomplishments (he didn't talk about it, even to his family!)
He broke the 'Lorenz' cipher (generally regarded as much more difficult than
Enigma) Almost all modern Graph-theory and Matroid analysis is built on
his work.
---
Mike Norman, B.Math UofW 1986
I have always wondered about this sample. Consider the possible 4-colours to be red, blue, green and orange, as in the image. We need to determine the colour of the black square. All 4 colours are joined in this inverted cross like formation and the center of the cross (a gray pixel atm) kind of indicates an infinity point. If the space in which these colours are drawn is not discrete, then they can all be said to join at the center of the cross.
Is this sample just not allowed by the rules of the "game"?
Your example adds more constraints than the original problem, by pre-assigning colors to regions and then asking how to solve for the black region.
In the original problem statement, you could solve by re-assigning your green region to be orange, your red region to be blue, your black region to green, and the white regions to red. Also note that regions that meet at a single point (as in your example) are not considered to be adjacent.
aha, so infinities are not allowed. Fair enough, in that case the gray pixel needs to be filled with one of the colours and the two colours connected to that specific one become interchangeable.
The four colour theorem does generalize to infinite planar graphs, in the sense that if an infinite graph can be embedded in the plane without overlaps, then a four-colouring is possible. It's a straightforward consequence of the compactness theorem for propositional logic, which I set as an exercise for my students when I teach the topic.
so in essence there is an additional constraint, that each touching edge has to be of a given minimal size. Each contiguous "blob" with a given circumference of N * this minimal size, can only connect to at most N other blobs.
No, there is no minimal size, just that we only consider two regions as being "in contact" and therefore requiring different colours) if they have a shared boundary, and that boundary is of non-zero length.
There is no limit to how many regions can surround and be in contact with a given region, it's just that the shared border that defines "in contact with" must be of non-zero length.
Note also: we are dealing with finite maps. That means that for any given map there will be a shortest boundary for that map, but it doesn't mean there is a minimum constraint.
Consider the gray pixel in the center a placeholder, much like Escher's place holder in the above image (because he couldn't think of how to realistically depict what turns out to be the infinite fractal nature of the center)
> An edge, no matter how small breaks the cross.
My very weak intuition says that an edge of infinite smallness would not.
"... an edge of infinite smallness ..." is not a well-defined concept, and is not allowed in the original formation of the problem. Otherwise take a circle and divide it into N segments "like a pizza". They all meet in the middle in an "edge of infinite smallness", so that would require N colours.
Now make N as large as you like.
So allowing this makes the problem uninteresting, and precluding it makes the problem interesting and hard.
(I don't recall details - but the preconditions of the Four Colour Theorem rule out all the fuzzy sets, infinitely crooked lines, "this region is all points with one rational and one irrational coordinate", and other trickery that folks who've had a bit of math might otherwise be tempted by.)
The graph has to be planar, which means no to edges intersect (or you can move the edges so that no two edges intersect). The complete graph with 5 or more vertices isn't planar.
This is btw equivalent to a graph with 5 nodes, where all nodes are connected to every other node, which would quite obviously be impossible to colour with just 4 colours.
It's not, though. If the four corners are sharp, blue & red are not adjacent, nor are green & orange. You can re-paint blue to red and orange to green, and you're left with a proper 3-coloring. Alternately, if the grey pixel takes another color (say, red) so that blue, green and orange are all adjacent to it, then green & orange are not adjacent -- re-paint orange to green, and you get a 4-coloring. Finally, if the grey pixel is its own region, you're effectively back in the first case and you can paint it black to obtain a 3-coloring.
I am sure this is wrong. You cannot use asymptotic analysis on this problem. The assumptions it makes in section 4 does not necessarily prove or is specific to the 4-color theorem. Just splitting vertices etc. does not suffice to prove it for 4 colors, it can also prove it for 5 etc.
> The approach uses a singularity analysis of generating functions for particular sets of maps, and Tutte's enumerative and asymptotic work on planar maps and their chromatic polynomials
Oh, my mistake! I've always (incorrectly) thought it meant "being prose-ful" or "reminiscent of poetic prose". My intention was to compliment @burnished's writing :P
Given the history of false proofs of the four color theorem surviving scrutiny for decades, I think I'll wait for this to be verified by a computer proof language such as Lean before trusting it.
(This is intended seriously, but I do love the ironic twist compared to historical hesitancy to accept the computer assisted proof.)
A short paper like this will almost certainly be either verified or refuted by the traditional method of mathematicians reading and analyzing the proof's logic. Computer-aided proof is pretty niche in mathematics.
HN is good to spot crackpots, linbait and other kinds of papers that are very bad. This was posted by ColinWright, so my guess is that it's not obviously bad. If it has an error, it will need like a month or a year to be discovered. Anyway, I hope to see in a month a new discussion when Tao (or someone) have enough time to understand it.
I'm a math professor who has lost years to this question. I've met various authors involved in successful proofs. My 1976 grad school application from the University of Illinois came postmarked "Four Colors Suffice" (Appel, Haken). I've also been inundated with well-intended crank proofs of every tar pit like this. One can tell the difference without focusing one's eyes.
These authors have long, established careers, with 2,000 MathSciNet citations between them. Waterloo is a hotbed of combinatorics; I doubt that they posted this before passing the paper around a bit.
Graph theory as a branch of mathematics is like photography as an art form: Anyone can point a camera, and one sees a lot of incredibly weak graph theory if one digs deep enough into the regional conference circuit.
This work is deep, relying on an understanding of generating functions that many casual practitioners don't possess. If the proof has a flaw, the issue will be technical and difficult to uncover. I love how people take the obvious bet that this is likely wrong because so many proof attempts have failed. In a prediction market, I'd bet on this proof being right.
I caught a rumour of this paper about 6 months ago, so I'm pretty sure that in the meantime it's been evaluated and assessed by colleagues. So I'm pretty sure it's going to be right, with only small fixable things that need tidying up.
Just as the incorrect proof by the amateur mathematician or crank is likely to be in a predictable form - a bunch of drawings of graphs with increasingly obtuse notation, reference to special cases within special cases, etc., isn't the incorrect proof by working combinatorialists likely to look exactly like this paper? An argument from complex analysis relating to either generating functions, Tutte polynomials, or some similar concept, together with some difficult arguments about how the asymptotics should be correctly used?
The fact that this includes arguments which casual practitioners would not be able to confidently use in a crank proof does not evidence its correctness. It just shows us that it's from a different type of person, susceptible to making a different type of error.
> In a prediction market, I'd bet on this proof being right.
Let's create a question on Metaculus!
How about Manifold? https://manifold.markets/ZviMowshowitz/will-the-new-nonconst...
well put.
Your post feels like a dispatch from bizarro-world.
There is a good amount of second-order evidence that the proof is wrong. Further, I skimmed the introduction, and it seems the indicated approach cannot possibly work. My guess is that both authors are senile. (They're quite old.)
If you give me decent odds, I'd be happy to bet against you regarding the proof's correctness. Would you take 1:1?
Hey, could you please make your substantive points without swipes and personal attacks? If you know more than others, that's great, but then share some of what you know (without putdowns) so the rest of us can learn. If you don't want to do that, not posting is also a fine option.
I have no idea whether the proof is right or wrong, and I'm not so sentimental as to believe that the harsher person is more likely to be wrong. (Besides, naysayers are usually right, just like they are when predicting that any given startup will fail.) However, the HN guidelines (https://news.ycombinator.com/newsguidelines.html) ask you not to post like this and that's important too. Other users are making their case against the OP while following the guidelines just fine. Please be more like them.
Hi Dang,
There's no personal attack here. I'm sorry if that comment comes across as curt, but the post I responded is (in my opinion) grossly misleading and deserves pushback. For example, consider the statement: "If the proof has a flaw, the issue will be technical and difficult to uncover," made by someone claiming years of experience as a math professor thinking about this question. This is easily identifiable as wrong, because the purported proof is just 7 pages (actually less than that due to extraneous material) and does not use any particularly technical mathematics (a strong undergraduate major probably knows enough to comprehend what's going on). Indeed, people found the error in (less than) 12 hours after that comment was made.
The comment about senility is not a "swipe." It is a very real problem in the mathematics community. Mathematicians get old and are sometimes afflicted by dementia, and this unfortunately can manifest as hopeless attempts at famous problems. Atiyah's "proof" of the Riemann Hypothesis right before his death is perhaps the most well known example, but there are others that (thankfully) aren't disseminated publicly. In the pre-internet age, journal editors were able to make such things quietly disappear. But now we have the arxiv. This is valuable context for understanding why two mathematicians with distinguished publication histories might be posting an incorrect proof, which had not been provided by other comments.
That being said, I will endeavor to phrase such comments more carefully in the future. Thank you for your message.
I believe that you're talking about something real, and when you provide the fuller description, it no longer feels like an attack.
I am going to finetune a content moderation model based only on the principle that it should, at all times, ask itself: “what would dang do?” and then do that
The tone of your comment is pretty harsh. What kind of 2nd-order evidence do you see? And why did you learn from the introduction that makes you so sure? It's only an introduction, which might only give you an oversimplified summary of their ideas.
Are both of them senile?
Yeah, my guess is that both are senile if they're putting this on the arxiv.
Second-order evidence: Old mathematicians (~80). Famous problem. Weird, imprecise writing style. No mention of the proof by mainstream mathematical news sources (breakthroughs are usually accompanied by excited blogging/tweeting). No acknowledgements directed at other mathematicians who have checked or commented on the proof.
[deleted argument here; replaced by more precise comment below]
My tone is harsh because I think the best thing to do is to quietly ignore it, similar to how the community treated Atiyah's claims of a RH proof at the end of his life.
Some counterpoints: 2 mathematicians greatly increases chances of senility. Blogs/twitter also correlate much stronger with author age than truth of statement.
>The argument looks like it's based on large n asymptotics, so even assuming everything works correctly the strongest statement they can hope to show is that the theorem is true for all n > n_0, where n_0 is some large constant. But there is no mention of this fact. The theorem is claimed for all n.
This is completely wrong. A proof for all n>n_0 is a proof for all n, since any counter-examples have to exist as subgraphs of arbitrarily large graphs.
I don't think asymptotic estimates of that form suffice to treat this problem. (Where else in combinatorics has an argument of this form succeeded? What intuitive reason is there to expect it to succeed here?)
Specifically I think section 4 is basically nonsense. (I see Sniffnoy has already pointed this out below.)
(Re: your comment, Theorem 7 is going to fail below the smallest counterexample, right? This is bad, imprecise writing - a red flag.)
> I think the best thing to do is to quietly ignore it
If you think that's the best thing to do then why not do it?
* No discussion of how these techniques were developed.
* No discussion of why they were not found by other people in the past.
* No discussion of how these techniques could be used on other problems.
* A lot of calculations which would be left out as trivial by most graph theory papers (for example, calculations about the edge counts of subgraphs)
> The argument looks like it's based on large n asymptotics, so even assuming everything works correctly the strongest statement they can hope to show is that the theorem is true for all n > n_0, where n_0 is some large constant. But there is no mention of this fact. The theorem is claimed for all n.
Have you seen this comment? https://news.ycombinator.com/item?id=34083099
Yes. How does it bear on what I wrote?
The point is that if there were a small graph that was a counter-example, then there would be large graph counter-examples (and the percentage of them would increase with graph size), so proving that the 4 color theorem is true for large graphs implies that it is true for all graph sizes.
You're claiming:
> the argument looks like it's based on large n asymptotics, so even assuming everything works correctly the strongest statement they can hope to show is that the theorem is true for all n > n_0, where n_0 is some large constant. but there is no mention of this fact. the theorem is claimed for all n.
They're claiming:
> Theorem 7. If there is a map L which cannot be 4-coloured then only an exponentially small fraction of the maps with n edges can be 4-coloured.
These claims appear mutually exclusive.
See above clarification about the bad writing.
This is a bizarrely hostile attitude to have. Critique their work, not their age.
It's not bizarre at all. The math community has unfortunately been down this road many times before. When an 80-year-old announces a 7 page proof of a famous problem, the smart money is on the proof being wrong. As the comments elsewhere on this story indicate, this heuristic turned out to be correct. The only new twist is that we have two 80-year-olds this time, not one.
To be clear, I don't like this state of affairs. As suggested above, the best course of action seems to be to ignore the posting.
It is not appropriate for you to speculate publicly about the mental health of people you've never met.
It's so inappropriate that in the field that's actually trained for this, they're disallowed by compact, even with extensive evidence.
Please stop.
>It's so inappropriate that in the field that's actually trained for this, they're disallowed by compact, even with extensive evidence.
The field trained for this is not refraining from this because it's hard to get right, but because it undermines the privacy promise they give their clients! not an argument applicable to people who do not have that professional reputation to uphold.
Of course you should speculate about mental health of people when it's relevant to the topic - it's a factor heavily shaping many people's behaviour!
Their LaTeX compiled, though.
Reposting my comment from /r/math:
OK, section 4.2 makes no sense to me. So they have this set Q, right? Which is the set of plane graphs that can be written G=A*B*C*D, where * denotes joining at a cut vertex. Their goal is to show that every G∈Q can be 4-colored, and then use that to argue that a nonzero fraction of plane graphs can be 4-colored, and then argue (via the generating functions and asymptotics) that this means that they all can be.
Except... if they can show that every G∈Q can be 4-colored, then all of this argument with generating functions and asymptotics is unnecessary, right? Because surely G can be 4-colored iff A, B, C, and D all can; and since A, B, C, and D can be any plane graph, that would be the end of it -- if you have a plane graph A and you want to 4-color it, all you'd have to do is stick a 3-path hanging off the end of it to put it in Q (indeed, in the subset they call \overline{Q}), and then 4-color that. The rest of the argument would appear to be unnecessary!
Meanwhile, their argument for why graphs in Q can be 4-colored doesn't seem to make any sense to me. It's inductive, but they haven't written it in a clear manner that makes it exactly apparent how they inductive hypothesis is used. I honestly do not see how they are justifying the statement "It follows from the Induction Hypothesis that S_1 is 4-colorable" -- it doesn't look like any work is being done, it all looks circular to me!
Am I missing something here?
Terence Tao is also concerned about that section: https://mathstodon.xyz/@tao/109554420101377184
An inductive hypothesis mentioning some independent variable like n needs to look like a conditional, e.g.: "If all maps in Q with at most n-1 edges are 4-colorable, then all maps with at most Q(n) is 4-colored, all maps in Q with at most n edges can be 4-colored" and then it has to be shown.
From my reading, it looks like can't make up their mind about whether Q = {X . Y: X, Y graphs} or Q = {X . Y : X, Y in Q}. Neither definitions seems to work everywhere.
Where does Q = { (S1 . T1) . (S2 . T2) : S1,S2,T1,T2 in Q } not work?
This definition fails because Q-bar needs to be a subset of Q, but in Q-bar, the graphs T1, S2, and T2 are specified to be the single-edge graphs e1, e2, e3. But single-edge graphs are not in Q.
You're not missing anything.
My memory is that the Four Colour Theorem was one of the first computer search-assisted proofs which caused all sorts of epistemological questions. Specifically how to know whether the software had no bugs and ran correctly, and how re-running to get the same result only lowered the probability and did not yield absolute certainty. Seems sort of a quaint concern now.
(Apologies for no reference. I hope I'm not misremembering.)
You're remembering entirely correctly! I gave a talk on the Four Color Theorem as part of my master's degree in 2001, and it was a somewhat active epistemic debate among mathematicians at the time. I took the position that examining code was no different than examining a proof, that running it through a computer was no different than running it through your brain, and that mathematicians are not shy at all about "automating" processes over uncountable infinities in proofs, so why should we be shy about automating them over thousands mechanically?
There is a fun faith-shaking element to the story, though. The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them. And IIRC, he found about a dozen errors! They weren't fatal -- he was able to repair them -- but that whole process didn't really reassure people. ;)
AMS has a good summary: https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem
To save others the effort of reading - this only discusses the proof and not the by-hand check or "about a dozen errors" mentioned in the parent post.
How did the errors arise, some bug in the theorem prover?
The original computer assisted proof of the four colour theorem was written in IBM 370 assembler [0]. This was naturally susceptible to programming errors such as those discussed above. Gonthier's subsequent certified proof requires trust in a much smaller body of code and hardware [1].
[0] https://projecteuclid.org/journals/illinois-journal-of-mathe...
[1] https://www.ams.org/notices/200811/tx081101382p.pdf
That's a really good question. I may have known the answer to it twenty years ago, but I don't now. XD
What I can tell you is that it wouldn't have been so straightforward as that. We're not talking about an axiom-to-result symbolic proof piece of software like you might attempt to write now. It wasn't a computer proof so much as a computer-assisted proof. Lots of human analysis to describe specific properties, and then a computer program to check that a long list of geometric configurations had those properties.
I don't know exactly what the program output as its proof, but I can only imagine the problems would have been small assumptions built into its design failing in corner cases. The theorem is notoriously difficult to reason about rigorously, and there have been a number of accepted proofs over the years that turned out to be false. It really doesn't help the whole situation that not only is it the first major computer-assisted theorem, it just happens to deal with a result that people are already wary of.
>The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them
I don't feel this is fundamentally different from the categorization of finite simple groups, which is also combining many small theorems and proofs, yet more widely accepted.
The same issues come up with interactive zero-knowledge proofs[A], where someone proves that they possess certain private information without leaking said information.
The proofs have the form:
1) Give the prover a challenge that they only have a 50% chance[B] of passing if they don't possess the private info.
2) Repeat as necessary with new, independent challenges.
3) If they keep passing, hooray! The probability that it's a faker decays exponentially. You can get really high confidence, very quickly!
Doing more rounds is just like re-running the computer proof.
[A] I first learned about the issue from reading the Scott Aaronson lectures that became Quantum Computing Since Democritus
[B] Doesn't have to be 50%, any figure will give the exponential decay and only require a linear increase in the number of rounds, so long as the probability stays the same between all rounds.
I fail to see the connection - new runs of the compuuter proof isn't going to randomize the code (like it does in zkp), so its not going to reduce the probability of error (excepting cosmic ray induced errors of course)
Yes it is — the fact that the later computations got the same result is evidence that the earlier ones weren’t flukes.
My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent. Randomization is one way to achieve that but not a hard requirement.
Even so, it seems you do see the connection, you just dispute one element that you think is critical.
> My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent.
But they are obviously not independent.
This is like flipping a coin once, looking at the result 20 times in a row (without flipping it again), concluding you have magic luck powers since you got heads twenty times in a row, and that would be really unusual in the analgous system where you flipped a coin 20 times instead of just looking at it.
> Randomization is one way to achieve that but not a hard requirement.
This is besides the point, but pray tell. How do you reduce the probability of an algorithm being incorrectly programmed by means of running it multiple times without changing the input or introducing some randomness somewhere? I don't think that's possible. Really the ZKP case isn't even checking the algorithm but checking a specific user input is consistent.
I think this would be equivalent to denying that BPP without coin flips is P, which afaik it is.
> Even so, it seems you do see the connection, you just dispute one element that you think is critical.
I mean, i guess you could say that if you modify the system to add the connection you are trying to establish, then yes the connection becomes obvious.
>But they are obviously not independent.
Yes, independent with respect to the variable you're testing. In the ZKP, the independence is between the challenges given to the prover. In the computational proof, independence is between the probability of computational error affecting the calculation. (To be sure, you'd want to run the proof on different hardware!)
>> Randomization is one way to achieve that but not a hard requirement.
>This is besides the point, but pray tell.
Wait, what? Your original comment[1] was specific alleging that the absence of a randomizer completely broke the analogy:
>I fail to see the connection - new runs of the compuuter proof isn't going to randomize the code.
How would this be "beside the point" when it's the point you introduced? Did you forget the point you were trying to make?
>How do you reduce the probability of an algorithm being incorrectly programmed by means of running it multiple times without changing the input or introducing some randomness somewhere?
Even doing the same run on the same hardware would provide evidence against against the earlier result being a fluke (e.g. from cosmic rays), as I said before. But yes, as above, to round out the possibilities, you'd want different people to translate the proof into different languages and hardware and run it there -- that would likewise increase your confidence in the result, just like running different rounds of the interactive ZKP would.
>I mean, i guess you could say that if you modify the system to add the connection you are trying to establish, then yes the connection becomes obvious.
Sorry, are you really saying that you see no parallel whatsoever between:
a) Run the 4-color computer proof multiple times to increase your confidence that the result wasn't just luck, and
b) Run additional rounds of an interactive ZKP to increase your confidence that the prover wasn't just lucky?
If so, that feels like more of a you-problem.
If you were disputing that additional runs of the 4-color computer proof could increase your epistemic confidence in it, then you should have raised that in response to the original comment[2], not one (like mine) that accepted it and pointed out an analogous situation.
[1] https://news.ycombinator.com/item?id=34088094
[2] https://news.ycombinator.com/item?id=34084448
> In the computational proof, independence is between the probability of computational error affecting the calculation. (To be sure, you'd want to run the proof on different hardware!)
But i don't think that is the concern at hand. Yes, re-running can reduce probability of failures due to soft-memory errors and such. But does nothing against logic errors (or non-transient hardware errors). My understanding is the main concern with the proof is not that a cosmic ray hits RAM and flips a bit, but that either the logic may be wrong or a general epistimitic unease that no human directly inspected the cases of the proof.
In any case i said as much in my original comment. To quote: "excepting cosmic ray induced errors of course"
> Wait, what? Your original comment[1] was specific alleging that the absence of a randomizer completely broke the analogy:
Yes, i stand by that (although accept your point that independence not randomization is the salient property). I also maintain that whether or not it is theoretically possible to do independent tests without a randomness is irrelavent to the matter at hand. What matters is if rerunning the code was an independent experiment, not what could theoretically be possible. Even if there exists some non-random way to do that, its irrelavent to whether or not any method was used.
> Sorry, are you really saying that you see no parallel whatsoever between: > >a) Run the 4-color computer proof multiple times to increase your confidence that the result wasn't just luck, and > >b) Run additional rounds of an interactive ZKP to increase your confidence that the prover wasn't just lucky?
Yes.
Although for greater clarity, i would clarify (a) to say i don't see the connection to non-negligibly increasing your confidence the result of the 4 colour is correct. I agree (and said this in my very first comment) that it would increase your confidence that you didn't get an incorrect result due to a soft-memory error. I would say that relative to all the possible reasons why you might get an incorrect answer, transient hardware failure is very low, so the increase in confidence from rerunning is negligible because the meat of the question is programming error.
In the analagous situation, re-running the zkp gives an extremely high increase in confidence the answer is correct, usually at least halving the possibility of error.
> If you were disputing that additional runs of the 4-color computer proof could increase your epistemic confidence in it
Sure, although the original comment was a bit vauge as to exactly what they meant.
Most of this proof is very dense. But Theorem 7 seems like an interesting tactic that allows the authors to infer nonexistence from rarity:
>Theorem 7. If there is a map L which cannot be 4-coloured then only an exponentially small fraction of the maps with n edges can be 4-coloured.
It's one of those things that seems obvious in retrospect — of course large random graphs should be likely to contain any particular graph! But it hadn't occurred to me in my own (very amateur) considerations of the problem.
Will be interesting to see if it's correct. We've gone from an argument too long for a human to read to one in just seven pages.
This is in fact a very common proof strategy in combinatorics, often known as the probabalistic method. Naturally it was invented by Paul Erdos
I think that's a bit different - in the probabilistic method you show that if you randomly sample a graph (say) then the probability of it having some property is > 0 - therefore there must exist some graph having the property.
Theorem 7 in their paper is trying to count the number of graphs that contain a hypothetical 4-color counterexample if it exists. It's done by hitting a suitable generating function with a big analysis hammer to bound its coefficients, not by probabilistic means.
So until now every proofs of this theorem were still computer-assisted right ?
Yes, that's right.
They still are.
I'm not a mathematician, but when I was in school I read a lot of 'pop math', and fancied myself a lot better at it than I was (or am). I was fascinated by things like the FCT, and recall writing a document ...I don't think I kidded myself proving it, but at least 'understanding' it.
The rough sketch was to show that it was not possible to construct a map that required five colours: that if you take a blob of one colour, wrap it in three others, all four are touching the others, but you can't possibly add a fifth since it either only touches the outer three, or it has to prevent two of them touching to get to the inner one (then the non-touching ones could be recoloured the same).
To this day, although I of course realise I was having no groundbreaking thoughts and it did not constitute a proof, I do not understand why the actual proofs are so complex, or require so much computation? It eluded far greater minds for over a century - what am I missing that makes it so problematic?
It's (relatively) easy to prove that you can't have five regions that all touch each other. If you could then that would mean that a map requires (at least) five colours, but that's not the only way a map could require five colours. Even so, it's certainly the first thing to try.
But colours-at-distance can be forced, so proximity isn't needed to create the need for another colour.
The theorem is difficult for two meta-reasons. One is that there are arbitrarily many planar configurations, and you need to prove that they are all four-colourable. The other is that whether or not a planar graph is three colourable is NP-Complete, and showing a planar graph is five-colourable is fairly easy, so it's on the boundary between fairly easy and really hard.
The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example. This is easily done by hand.
Appel and Haken's proof of the four-colour theorem proceeded the same way, but the unavoidable set was large. The computation was to confirm that the set was unavoidable, and that each element was reducable. This involved a huge amount of tedious bookkeeping, best done by machine, but it was really just "doing the sums". The real work was creating a finite amount of bookkeeping that would then constitute a proof.
Thanks for the insightful comment.
>The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example. This is easily done by hand.
Isn't this missing a crucial point? You seem to be saying:
1. There is some (small) set S of graphs, all of which are 5-colorable
2. Every planar graph has at least 1 sub-graph in S
3. Therefore, all planar graphs are 5-colorable
But, from statements 1 and 2, one can only conclude that every planar graph _has a sub-graph_ that is 5-colorable, not that the entire graph is 5-colorable.
Don't you also need to prove that the complement of the sub-graphs is 5-colorable?
My comment was:
> The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example.
You said:
> Isn't this missing a crucial point? You seem to be saying:
> 1. There is some (small) set S of graphs, all of which are 5-colorable
This is not what it's saying. It's saying that these graphs cannot be in a minimal counter-example. That's different from simply saying that they are 5-colourable.
> 2. Every planar graph has at least 1 sub-graph in S
> 3. Therefore, all planar graphs are 5-colorable
No, you've missed a bit of my comment. I said:
> showing for each of those that it cannot be in a minimal counter example.
So we have an unavoidable set U. So for every graph G there is an element S of U that is a sub-graph of G.
But we have also shown for every element S of G that any graph containing S cannot be a minimal counter-example. We're not showing that these elements S of U are themselves 5-colourable, we are showing that any G containing S is not a counter-example to the theorem.
So now suppose the theorem is false. That means there is a graph that requires 6 colours. From among those choose a minimal one, so M is a minimal counter-example. But the set U is unavoidable, so there is a S in U that is a subgraph of M. But any graph containing S cannot be a minimal counter-example, and we have our contradiction.
Hence there are no counter-examples, and the theorem is true.
For the Five Colour Theorem the unavoidable set U has only four graphs, so it's easy to check by hand. For the Four Colour Theorem in the original proof there were around 2000 elements of U, so it was infeasible to check by hand. That has been reduced to 633 graphs in U, but it's still tough to check by hand.
The paper in the original submission here takes a different approach.
Ah, thank you. The key to my misreading was this part:
> showing for each of those that it cannot be in a minimal counter example
I read "those" as "those subgraphs" rather than "those graphs".
Thanks.
> I read "those" as "those subgraphs" rather than "those graphs".
That is the correct reading; your mistake must be elsewhere?
>> [the proof] proceeds by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example.
No minimal counterexample to the claim [that a planar graph is 5-colorable] can contain any of these subgraphs. All planar graphs contain at least one of these subgraphs. Therefore, all planar graphs fail to satisfy the predicate "this graph is a minimal counterexample to the claim that all planar graphs are 5-colorable".
The elaboration is very explicit that the theorem is "for every subgraph S in the unavoidable set U, that subgraph (S) cannot be contained in any minimal counterexample":
>> we have also shown for every element S of G that any graph containing S cannot be a minimal counter-example.
As the sibling comment to this says, you must still be confused about something here. Let me expand.
The proof that every planar graph (equivalently every map on a plane) is five colourable proceeds as follows.
Cleverly produce a set U of small graphs S that have the following properties:
1: For every graph G, there is an S in U such that S is a sub-graph of G;
2: If G is a counter-example to the theorem, and S from U is a sub-graph of G, then there is a smaller graph H that is also a counter-example.
This is enough, because now let M be a minimal counter-example. By (1) there is an S from U that is a sub-graph of M. But by (2) there is then a smaller counter-example, contradicting the minimality of M. So there can be no counter examples.
With that now in mind, here is the original statement:
We proceed by showing that there is a small set of sub-graphs such that every graph must contain one (an unavoidable set), and then showing for each of those that it cannot be in a minimal counter example. This is easily done by hand.
I hope that helps.
You don't just show that the graphs in S are 5-colourable. You show that they couldn't possibly be part of a minimal non-colourable graph (e.g. if a graph containing this subgraph is not 5-colourable, you can replace this subgraph with this simpler subgraph, and the larger graph will still be non-5-colourable).
That shows (loosely) that there is no map with five countries that cannot be four-colored. It says nothing about maps with six, seven, etc. countries. An actual map may have billions of countries and need not even contain “a blob of one colour, wrapped in three others”.
Loosely because
a) it only shows it for such maps that contain such a blob. Who says other maps with five countries are easier to four-color?
b) it doesn’t rigorously show it. That you (and me, and everybody who looked at it) can’t find a way to draw that fifth area that touches all others doesn’t say much. what are your arguments for showing you looked hard enough?
For a similar case, read about the Jordan curve theorem. In layman’s terms, it says closed curves on a plane have an inside and an outside part (https://en.wikipedia.org/wiki/Jordan_curve_theorem). Naive readers think it’s so trivial to not require a proof, and it took mathematicians a while to figure out that it needed one. I don’t know the details, but mathematicians may have observed that that theorem also is true on a sphere but isn’t true on a torus (a closed loop ‘around the hole’ in the torus doesn’t have an interior and an exterior). So, they needed an explanation as to why it’s true on a plane or a sphere but not on a torus (the answer essentially boils down to “because a torus has a hole in it”, but that requires a rigorous definition of what a hole is)
If you don't have such a blob then you don't even need four?
This is in the grandparent comment:
"An actual map may have billions of countries and need not even contain “a blob of one colour, wrapped in three others”."
In fact every map of interest will contain a blob wrapped in at least three others.
But they are right that the problem is showing that the theorem holds for maps with billions of regions, or more. Decisions you make early in the process of colouring the map can turn out to be wrong, but only much later as you are trying to colour the last few.
In short, you are saying "I can't see how it can go wrong", but that's not enough ... there are things that might happen that you weren't able to imagine, and that's part of why proofs like this are hard.
Also, the theorem is true, and that makes it hard to explain why it might go wrong. Because we now know that it doesn't.
The grand-parent comment also says:
"... the Jordan curve theorem ... is true on a sphere ..."
The stronger form is not true on a sphere. The stronger form says that every topological sphere in 3-space has an interior that's retractable to a point and an exterior that's retractable to a shell. But the Alexander Horned Sphere[0] is a counter example.
In short, weird things you didn't suspect can happen, so proofs are sometimes harder than you think, even for "obvious" things.
0: https://en.wikipedia.org/wiki/Alexander_horned_sphere
in some sense because there might be strongly non-local effects... an assignment of color in one part of the graph can have an effect on what colors are allowed in a very different part of the graph. Planarity assures some degree of "locality", you can't arbitrarily connect one point to another point.
Your proof sketch actually suggested that it was not possible to construct a map with five regions that require five colours.
Now you need to generalise that to maps with infinitely many regions.
But as a result there could never be an area of an infinitely large map that had five regions each needing a different colour. I understand people are saying but you take two such sub-maps, put them next to each other, and maybe the 'outside' colours are the same - but in that case you could always just recolour them individually before putting them together?
What you've said here might be a reasonable reply in your head, but for me, reading its parent, and this reply, I can't work out what you're trying to say.
You need to be really careful about things like "infinitely large map" ... if you want to talk about really large things then they are really large. But if you want to talk about infinite sized things then you need to be careful. There are traps in infinities, and this theorem is about finite maps (or equivalently, graphs).
Proving that a small, local sub-section doesn't require five colours is helpful, but no one has been able to extend that, because there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
You are saying the sorts of things I've seen many times before, but you need to try to make complete, precise statements about exactly what you propose. So far all you've said is that you can't arrange five regions that all touch each other, and that's true. Now, exactly how do you extend that to a map with billions of regions?
It was the comment I replied to that introduced infinitely large maps - but regardless I wasn't trying to be as clever as you might be trying to assume (and of course not finding it :)) - I would have said the same about 'really large' or indeed 'just a bit larger than the 4 or 5 regions I described initially'.
> there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
This is the bit I can't grasp - I honestly appreciate the responses and attempts to explain it, but it just (mistakenly, I can accept even if I don't understand) seems counter-intuitive to me. As in, intuitive that it extends, or that there's no such problem.
Maybe I just need to play with it on paper a bit, stumble into such a spooky action to get it.
> Now, exactly how do you extend that to a map with billions of regions?
I don't have the background for the precision you'd like I'm afraid (if I did, I'm sure I'd understand anyway!) but loosely - divide and conquer; a similar thing happens at the interface of all the 'sub-maps'?
>> there is a kind of "spooky action at a distance" that can happen
> This is the bit I can't grasp
OK. Let me give you a collection of statements, each of which I can expand on, but which might give you a sense of the problem.
* Instead of colouring regions in a map we can colour vertices of a graph;
(put a vertex in each region and connect vertices if their regions share a border)
* If a graph can be three-coloured then it can be four-coloured;
(Any three colouring is a four colouring, but with no vertices of the fourth colour)
* An instance of colouring an arbitrary graph can be converted into an instance of colouring a planar graph;
(There is a "widget" that uncrosses edges)
* Given a number to factor, we can construct a graph such that three-colouring the graph will produce a factorisation[0];
(Graph three-colouring is NP-Complete, so this is even easier than that)
Broadly, we can construct a graph that has exactly one (up to permutation of colours) valid three-colouring. As you start to colour it you find that you have to make choices, on average about $4/3$ choices per vertex[1]. But the wrong choice results in not being able to complete the colouring, and you don't know which choice or choices were wrong.
So you get this "spooky action at a distance" thing going on.
Sometimes a planar graph can't be coloured with three colours, and sometimes it can but a colouring is hard to find. When we allow the extra colour it turns out that it's always possible, but it's not obvious that that should be the case.
That's an #ISS-level view of the ideas ... hope it helps.
[0] https://www.solipsys.co.uk/new/FactoringViaGraphThreeColouri...
[1] Beigel, R.; Eppstein, D. (2005), "3-coloring in time O(1.3289^n)"[2]
[2] https://en.wikipedia.org/wiki/Graph_coloring#cite_note-15
PS: I've upvoted you because I'm sure other people have the same questions, they're good questions, and they deserve answers.
I'm sure I'm mistaken, but I believe the conversion to a graph loses exactly the information I'm trying to use: a vertex with three edges, where each of those vertices are also all interconnected, can have a fourth edge to a fifth vertex which also has an edge to each of the others; on the map this is not possible. Right?
From my napkin sketch to satisfy myself, I think you can show the same thing equivalently by saying 'and the edges are not allowed to cross' - but I don't know if that's something that exists in graph theory? (If so, it seems to me it should be used here? And if it is, well, finally we have a modicum of precision for what I'm trying to get at!)
Edit: OK, sorry, that is a 'planar graph'.
So, to try to answer your questions:
If you have a map in which you want to colour the regions, you can convert to a graph by putting a capital city in each region, then putting a road between two capitals of countries that share a border. Colouring the capital cities vertices) so that any joined by roads (edges) get different colours is exactly the same problem.
The graph-colouring problem is more general now, but every planar graph is equivalent to a map and vice-versa ... there is a one-to-one correspondence between these problems.
Now we move to the NP-Completeness of the 3-colouring of general graphs. That shows that this sort of thing is hard for the reasons I gave in the grandparent post.
"But" I hear you say "That's for general graphs, and not for planar graphs!"
Yes, but there is a way to convert a graph-colouring problem on a non-planar graph into an equivalent graph-colouring problem on a planar graph, so we neither gain nor lose much by consider just planar graphs.
So 3-colouring planar graphs is NP-Complete.
Then you get into my comments about making bad choices and having to backtrack, and spooky action at a distance.
Hope that helps.
I have no idea what that guy is talking about, but your post reminded me of a fun trick. If you have a colouring of every finite subgraph then you can show the existence of a colouring of the whole graph by using Tychonoff's theorem.
Super cool, but Tychonoff would not have been my first stop here. This seems like a case where it's simplest just to invoke Zorn's lemma directly.
What poset should we set up on which to invoke Zorn's lemma directly? Anything I can think of does seem to me more easily understood via compactness/the ultrafilter lemma, but that may just be a fact about my own psychology.
Use the subgraph relation to define the poset. The big graph is then obviously an upper bound for every chain.
Yes, but invoking Zorn's lemma on that poset does nothing useful. This just proves the trivial fact that the big graph exists. How do you prove that a coloring of the big graph exists?
And if we take the poset to be partial colorings ordered by inclusion, it's not the case that a maximal partial coloring must color the entire graph. Some partial colorings have made choices which prevent them from being extended any further.
[To be clear, whenever I say "coloring", I mean from a fixed set of colors. E.g., a 4-coloring.]
Put another way, it actually is important here that the set of colors we are talking about is finite. It's NOT the case that just having every finite subgraph be C-colorable entails that the entire graph is C-colorable, when C is infinite. For example, if G is the complete graph on an uncountable set of nodes and C is a countably infinite set, then every finite subgraph of G is C-colorable, but G itself is not.
So somewhere in the argument, the finiteness of C must play a role. This is in ensuring compactness.
That's cool.
In short: No.
> there could never be an area of an infinitely large map that had five regions each needing a different colour
A more precise version (infinite -> finite, "...needing a different color looking only at that sub-map) is plausibly true. That doesn't help you though, because...
> maybe the 'outside' colours are the same - but in that case you could always just recolour them individually before putting them together
...this is false. Five patches of one sub-map might touch one patch of the other sub-map. So now you'd have to prove that the first sub-map can be colored with three colors to rescue your proof of the FCT. Further...
> you take two such sub-maps, put them next to each other [...]
...your argument here seems to boil down to "I can construct the full map by gluing together sub-maps". Depending on how you constrain the sub-maps to prove necessary properties (see above), this may not be true. But even if it were, your argument that it works seems to only consider gluing together two sub-maps of specifically size five, which obviously does not allow you to construct maps with more than ten patches.
This makes for two to three fully deal-breaking errors in your proof sketch.
As a followup, this proof has now been declared as fatally flawed by John Carlos Baez, with some additional analysis by Noam Zeilberger. The argument is beyond my personal mathematical knowledge, but I would consider this a pretty definitive verdict.
[1]: https://mathstodon.xyz/@noamzoam/109567981846531700
Waterloo has a Department of Combinatorics and Optimization? Amazing.
Not only does Waterloo have a world-class C-&-O department, they also had a hero from Bletchley Park - Dr William Tutte, a kind gentle genius that never bragged about his accomplishments (he didn't talk about it, even to his family!) He broke the 'Lorenz' cipher (generally regarded as much more difficult than Enigma) Almost all modern Graph-theory and Matroid analysis is built on his work. --- Mike Norman, B.Math UofW 1986
Tutte's are the central results in this work
Some comments on the math subreddit by some folks going through the proof in case anyone with a more formal background is interested:
https://old.reddit.com/r/math/comments/zruc58/221209835_a_no...
https://imgur.com/a/WJKb9fT
I have always wondered about this sample. Consider the possible 4-colours to be red, blue, green and orange, as in the image. We need to determine the colour of the black square. All 4 colours are joined in this inverted cross like formation and the center of the cross (a gray pixel atm) kind of indicates an infinity point. If the space in which these colours are drawn is not discrete, then they can all be said to join at the center of the cross.
Is this sample just not allowed by the rules of the "game"?
Consider it an extreme case of gerry-mandering...
Your example adds more constraints than the original problem, by pre-assigning colors to regions and then asking how to solve for the black region.
In the original problem statement, you could solve by re-assigning your green region to be orange, your red region to be blue, your black region to green, and the white regions to red. Also note that regions that meet at a single point (as in your example) are not considered to be adjacent.
aha, so infinities are not allowed. Fair enough, in that case the gray pixel needs to be filled with one of the colours and the two colours connected to that specific one become interchangeable.
The four colour theorem does generalize to infinite planar graphs, in the sense that if an infinite graph can be embedded in the plane without overlaps, then a four-colouring is possible. It's a straightforward consequence of the compactness theorem for propositional logic, which I set as an exercise for my students when I teach the topic.
so in essence there is an additional constraint, that each touching edge has to be of a given minimal size. Each contiguous "blob" with a given circumference of N * this minimal size, can only connect to at most N other blobs.
No, there is no minimal size, just that we only consider two regions as being "in contact" and therefore requiring different colours) if they have a shared boundary, and that boundary is of non-zero length.
There is no limit to how many regions can surround and be in contact with a given region, it's just that the shared border that defines "in contact with" must be of non-zero length.
Note also: we are dealing with finite maps. That means that for any given map there will be a shortest boundary for that map, but it doesn't mean there is a minimum constraint.
The "countries" are supposed to share an edge. An edge, no matter how small, breaks the cross.
https://blog.artsper.com/wp-content/uploads/2022/08/escher-2...
Consider the gray pixel in the center a placeholder, much like Escher's place holder in the above image (because he couldn't think of how to realistically depict what turns out to be the infinite fractal nature of the center)
> An edge, no matter how small breaks the cross.
My very weak intuition says that an edge of infinite smallness would not.
"... an edge of infinite smallness ..." is not a well-defined concept, and is not allowed in the original formation of the problem. Otherwise take a circle and divide it into N segments "like a pizza". They all meet in the middle in an "edge of infinite smallness", so that would require N colours.
Now make N as large as you like.
So allowing this makes the problem uninteresting, and precluding it makes the problem interesting and hard.
An "edge of infinite smallness" is a point.
(I don't recall details - but the preconditions of the Four Colour Theorem rule out all the fuzzy sets, infinitely crooked lines, "this region is all points with one rational and one irrational coordinate", and other trickery that folks who've had a bit of math might otherwise be tempted by.)
Meeting at a point doesn’t count, so for example, blue could be recolored to be red.
The graph has to be planar, which means no to edges intersect (or you can move the edges so that no two edges intersect). The complete graph with 5 or more vertices isn't planar.
This is btw equivalent to a graph with 5 nodes, where all nodes are connected to every other node, which would quite obviously be impossible to colour with just 4 colours.
It's not, though. If the four corners are sharp, blue & red are not adjacent, nor are green & orange. You can re-paint blue to red and orange to green, and you're left with a proper 3-coloring. Alternately, if the grey pixel takes another color (say, red) so that blue, green and orange are all adjacent to it, then green & orange are not adjacent -- re-paint orange to green, and you get a 4-coloring. Finally, if the grey pixel is its own region, you're effectively back in the first case and you can paint it black to obtain a 3-coloring.
The thing is: those four regions can be recoloured (change green by orange).
I am sure this is wrong. You cannot use asymptotic analysis on this problem. The assumptions it makes in section 4 does not necessarily prove or is specific to the 4-color theorem. Just splitting vertices etc. does not suffice to prove it for 4 colors, it can also prove it for 5 etc.
I haven’t read this carefully yet but I’m initially skeptical that it’s that easy.
From the abstract:
> The approach uses a singularity analysis of generating functions for particular sets of maps, and Tutte's enumerative and asymptotic work on planar maps and their chromatic polynomials
Err yeah, so easy...
That quote is so dense with words that individually are old friends, but paired up that way are as strangers to me.
That was a surprisingly prosaic way to communicate this feeling, are you by chance a writer? If not, you should write more!
Of writing, prosaic means unpoetic, i.e. dull.
Oh, my mistake! I've always (incorrectly) thought it meant "being prose-ful" or "reminiscent of poetic prose". My intention was to compliment @burnished's writing :P
He might just be Buster Scruggs' less melodious & more bookish brother.
Flajolet and Sedgewick have a nice book on Analytic Combinatorics that covers this
I highly recommend that book; it can be dense, but it is a treasure trove of information.
Given the history of false proofs of the four color theorem surviving scrutiny for decades, I think I'll wait for this to be verified by a computer proof language such as Lean before trusting it.
(This is intended seriously, but I do love the ironic twist compared to historical hesitancy to accept the computer assisted proof.)
A short paper like this will almost certainly be either verified or refuted by the traditional method of mathematicians reading and analyzing the proof's logic. Computer-aided proof is pretty niche in mathematics.
If it's correct, then it's a wonderful approach.
If it's not correct, then HN is the place to find where's the error.
By elimination of disjunction, upvote ;)
HN is good to spot crackpots, linbait and other kinds of papers that are very bad. This was posted by ColinWright, so my guess is that it's not obviously bad. If it has an error, it will need like a month or a year to be discovered. Anyway, I hope to see in a month a new discussion when Tao (or someone) have enough time to understand it.
Edit: Quoting a comment by bakkoting:
> Terence Tao is also concerned about that section: https://mathstodon.xyz/@tao/109554420101377184 .
That's not a good sign.
Agree on the first part. If correct, it is a wonderful achievement, apparently built upon the work of at least two others.
Hardly I doubt HN is that place
Can this also prove the more general Hadwiger's conjecture?
With the amount of incorrect comments I see on HN, definitely not. I'm not saying that I'm not included in that group, but I think we all are