3 ms·

A computer-generated proof that nobody understands – Xena

• eesmith 7y ago
  > If 20 years ago we had raised the possibility that a computer could come up with a 1000 page proof of a statement which humans had formulated, however “easy” the objects in question were, I think that it would not have been hard to find people who would have been very skeptical. Isn't that pretty much what happened with the 1970s computer-based proof of the four color theorem?
  • ColinWright 7y ago
    This is a common mis-conception, but the answer is no. The 1976 Haken-Appel proof of the 4CC, now 4CT, proved that provided there was a collection of graphs that satisfied a certain criterion, the conjecture was true. In essence, they need a collection such that every graph had one (or more) of them as a sub-graph (the collection is unavoidable), and such that each of them was "reducible". Finding such a collection was tedious and error-prone, and then checking that each had the required property was also tedious and error-prone, so they programmed computers to construct the collection and verify the properties. The computer did not prove anything, and the structure of the proof is fairly easy to understand.