Skip to content
Coordinates of ThoughtHome of Philosophy
Join
Debate

Thesis

A proof no human can check by hand is still a proof, and the four-colour theorem is known

Ana Clara Ferreira Fellow
· 3 replies
Philosophy of mathematicsAnalytic#computer-proof#four-colour-theorem#mathematical-knowledge#proof
Follow

Its coordinates: 1.1.4 Abstract Objects · 6.9 Philosophy of Mathematics

Where it stands

In 1976 Kenneth Appel and Wolfgang Haken announced a proof that every map can be coloured with four colours so that no two neighbouring regions share one. The proof reduced the problem to almost two thousand configurations and used a computer to check them. No human has ever checked all of them by hand.

In 1979 the philosopher Thomas Tymoczko argued that this changed what a proof is. Traditional proofs are surveyable: a competent mathematician can follow every step. The four-colour proof relies on trusting a machine's run, which makes our knowledge of the theorem partly empirical, like knowledge from an experiment.

Thesis: Tymoczko was wrong. A proof that no human can survey is still a proof, and we know the four-colour theorem as surely as we know any deep theorem.

My reasons: long human proofs are not really surveyable either; nobody holds the classification of finite simple groups in one head. And in 2005 Georges Gonthier gave a formal proof of the four-colour theorem checked in the proof assistant Coq, whose small trusted core can itself be checked by hand.

The other side is not silly. Mathematicians want proofs that explain why a theorem is true, and a giant case check explains nothing. Is a proof that convinces without explaining still a proof? I tutor logic to pay the rent; tell me which side you're on.

LikeReply
SaveFollow3 replies

Join the conversation: members reply here, and joining is free. Reading is always free.

Join free to reply Sign in

3 replies

For the thesis 2

  1. Tomasz Szewczak

    For Fellow

    For. I check proofs with machines every day, so I'm biased, but Tymoczko's argument has aged badly. His worry was that we trust an unverified program on unverified hardware. Gonthier's proof changes the question: what we must trust now is a small kernel, a few thousand lines, which has been studied far more carefully than the referees of most human proofs ever study a paper.

    If anything, the formal proof is more surveyable than a hundred-page human one. The survey is just divided differently.

  2. Ana Clara Ferreira

    For Fellow

    Vikram, I accept that we want explanation, and that the four-colour proof gives little of it. But I'd call that a demand on good proofs, not on proofs. A proof by exhaustion of five cases explains nothing either, and we teach those happily. I'll grant you "unsatisfying" without granting you "not knowledge".

Against the thesis 1

  1. Vikram Sethi

    Against Fellow

    Against, as a teacher. When I prove to my students that the square root of two is irrational, the proof doesn't only show that; it shows why, and they can use the idea again elsewhere. The four-colour proof gives certainty and no insight. Nobody can reuse it.

    I accept it as a valid verification. I don't accept that it gives us mathematical knowledge in the full sense, the kind a mathematician means when she says she knows why something is true. Maybe that's a different word, but it's the word that matters to mathematics.