[HN Gopher] A non-constructive proof of the Four Colour Theorem
___________________________________________________________________
A non-constructive proof of the Four Colour Theorem
Author : ColinWright
Score : 122 points
Date : 2022-12-21 15:36 UTC (7 hours ago)
(HTM) web link (arxiv.org)
(TXT) w3m dump (arxiv.org)
| scythe wrote:
| 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.
| bodhiandphysics wrote:
| This is in fact a very common proof strategy in combinatorics,
| often known as the probabalistic method. Naturally it was
| invented by Paul Erdos
| sweezyjeezy wrote:
| 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.
| zeroonetwothree wrote:
| I haven't read this carefully yet but I'm initially skeptical
| that it's that easy.
| naasking wrote:
| 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...
| burnished wrote:
| That quote is so dense with words that individually are old
| friends, but paired up that way are as strangers to me.
| mkaic wrote:
| That was a surprisingly prosaic way to communicate this
| feeling, are you by chance a writer? If not, you should
| write more!
| ectopod wrote:
| Of writing, prosaic means unpoetic, i.e. dull.
| thombat wrote:
| He might just be Buster Scruggs' less melodious & more
| bookish brother.
| lairv wrote:
| So until now every proofs of this theorem were still computer-
| assisted right ?
| gentle wrote:
| Yes, that's right.
| NelsonMinar wrote:
| 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.)
| Dove wrote:
| 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. ;)
| Dove wrote:
| AMS has a good summary:
| https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem
| anonymousDan wrote:
| How did the errors arise, some bug in the theorem prover?
| Dove wrote:
| 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.
| puzzledobserver wrote:
| 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
| SilasX wrote:
| 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.
| OJFord wrote:
| 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?
| nicky0 wrote:
| 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.
| OJFord wrote:
| 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?
| ColinWright wrote:
| 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?
| sebzim4500 wrote:
| 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.
| ColinWright wrote:
| That's cool.
| OJFord wrote:
| 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'?
| ColinWright wrote:
| >> _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/FactoringViaGraphThree
| Colouri...
|
| [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.
| ColinWright wrote:
| 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.
| siftrics wrote:
| 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?
| lmm wrote:
| 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).
| ColinWright wrote:
| 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.
| siftrics wrote:
| 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.
| Someone wrote:
| 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)
| OJFord wrote:
| If you don't have such a blob then you don't even need four?
| ColinWright wrote:
| 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
| bodhiandphysics wrote:
| 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.
| Phemist wrote:
| 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...
| bodhiandphysics wrote:
| 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.
| blevin wrote:
| 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.
| Phemist wrote:
| 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.
| Phemist wrote:
| 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.
| NotYourLawyer wrote:
| Meeting at a point doesn't count, so for example, blue could be
| recolored to be red.
| Phemist wrote:
| 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.
| klyrs wrote:
| 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.
| drbacon wrote:
| The "countries" are supposed to share an edge. An edge, no
| matter how small, breaks the cross.
| Phemist wrote:
| 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.
| bell-cot wrote:
| 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.)
| ColinWright wrote:
| "... 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.
| pfortuny wrote:
| The thing is: those four regions can be recoloured (change
| green by orange).
| qsort wrote:
| 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 ;)
| onos wrote:
| Agree on the first part. If correct, it is a wonderful
| achievement, apparently built upon the work of at least two
| others.
| EGreg wrote:
| Hardly I doubt HN is that place
|
| Can this also prove the more general Hadwiger's conjecture?
| feet wrote:
| 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
| notafraudster wrote:
| Waterloo has a Department of Combinatorics and Optimization?
| Amazing.
| mwnorman2 wrote:
| 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
| bodhiandphysics wrote:
| Tutte's are the central results in this work
| Syzygies wrote:
| 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.
| ruuda wrote:
| > In a prediction market, I'd bet on this proof being right.
|
| Let's create a question on Metaculus!
| spekcular wrote:
| 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?
| [deleted]
| ogogmad wrote:
| 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?
| spekcular wrote:
| 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.
| ogogmad wrote:
| > 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
| spekcular wrote:
| Yes. How does it bear on what I wrote?
| eganist wrote:
| 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.
| spekcular wrote:
| See above clarification about the bad writing.
| adgjlsfhk1 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.
| adgjlsfhk1 wrote:
| 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.
| spekcular wrote:
| 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.)
| ColinWright wrote:
| 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.
| ngvrnd wrote:
| well put.
| Sniffnoy wrote:
| 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?
| sebzim4500 wrote:
| 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.
| spekcular wrote:
| You're not missing anything.
| Strilanc wrote:
| 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.)
| civilized wrote:
| 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.
| krsrhe wrote:
___________________________________________________________________
(page generated 2022-12-21 23:00 UTC)