"It doesn't have to be as big of a deal as this."
Agree. The truthfulness of the four-colour theorem is good to know, although there is not yet any human-readable proof.
Agree. The truthfulness of the four-colour theorem is good to know, although there is not yet any human-readable proof.
For a general theorem prover, reading the code doesn't explain anything insightful about why the theorem is true. For the 4 color theorem, the code that proved it actually gives insight in how the proof works.