Timeline for Can one measure the infeasibility of four color proofs?
Current License: CC BY-SA 3.0
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 |