Skip to main content
10 events
when toggle format what by license comment
Jul 17, 2021 at 2:21 history edited Tony Huynh
edited tags
Nov 17, 2020 at 7:11 comment added Andrej Bauer I thought you were asking about the number of cases, sorry. Is there any particular reason why you're interested in humans?
Nov 17, 2020 at 1:45 comment added Colin McLarty @AndrejBauer I would be surprised if it can say how long a human would take to find, or complete, the requisite cases.
Oct 30, 2020 at 16:24 comment added Andrej Bauer I am pretty sure the formalization of the four-color theorem by Gonthier et al. can produce the exact number of examples, or whatever statistics you are interested in. There is no need to do any guesswork. Is that what you're interested in?
Sep 17, 2013 at 10:22 vote accept Colin McLarty
Sep 16, 2013 at 22:50 comment added Terry Tao If you allow probabilistically checkable proofs as acceptable, it may be possible to first use a computer to convert the computational component of the 4CT into a PCP format, and then any human armed with a couple of dice could verify the proof with, say, 99% confidence in a very short amount of time (maybe even minutes). I'm not sure what the state of the art is though on actually implementing a PCP.
Sep 16, 2013 at 15:06 answer added Noah Snyder timeline score: 8
Sep 16, 2013 at 8:16 comment added Marc van Leeuwen I think a more realistic question would be how many graph theorists would be needed to verify the proof, given that human beings, after spending a certain amount of time (which depends on the individual) on a boring task start to suffer from demotivation, increasing error rate, or going mad. If a graph theorist can do one configuration without hitting this limit, that would be positive. Then compare with the number of graph theorists one is willing to spend on the problem.
Sep 16, 2013 at 0:34 answer added Tony Huynh timeline score: 36
Sep 15, 2013 at 21:35 history asked Colin McLarty CC BY-SA 3.0