Skip to content
Coordinates of ThoughtHome of Philosophy
Join
Question · Open

If a theorem was checked by a program I can’t check by hand, do I know it is true?

Tomasz Szewczak Fellow
· 3 replies
Philosophy of mathematicsAnalyticLudwig Wittgenstein#computer-assisted-proof#mathematical-knowledge#proof#trust
Follow

Its coordinates: 1.1.4 Abstract Objects · 6.9 Philosophy of Mathematics

My day job involves writing code that a proof assistant checks line by line. So this is not a hypothetical question for me.

Two famous cases. The four colour theorem was proved in 1976 by Appel and Haken, with a computer checking well over a thousand configurations that no human ever went through by hand. In 2005 Georges Gonthier produced a fully formal proof in the Coq proof assistant. The Kepler conjecture about packing spheres was proved by Thomas Hales in 1998 with heavy computation, and the referees said they were almost but not entirely certain. A formal proof (the Flyspeck project) was finished in 2014.

When I say I know these theorems, what is my evidence? Proof assistants are built so that only a small "kernel" has to be trusted, small enough that a person could read it. But nobody reads the proof itself. I trust the kernel, the compiler, the hardware.

Wittgenstein insisted that a proof must be surveyable, something you can take in and reproduce. These proofs are not. So is this mathematical knowledge of a new kind? Testimony from a machine, like trusting a calculator? Or just ordinary proof with very good bookkeeping?

LikeAnswer
Follow3 answers

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

Join free to reply Sign in

3 answers

  1. Derek Hollis

    Fellow

    I do formal verification at a chip company, and in practice trust hasn't vanished, it has moved. You trust the kernel, the compiler that built it, the hardware, and, the one that bites, the statement of the theorem.

    Most failures I've seen are not bad proofs. The proof is perfect and the specification says something slightly different from what the engineers meant. A machine-checked proof of the wrong statement is the most confident mistake in engineering. So I'd say surveyability still matters, but it has migrated from the proof to the theorem: a human has to be able to read exactly what was proved.

  2. Ana Clara Ferreira

    Fellow

    Tymoczko argued in 1979 that the four colour proof made mathematics partly empirical, because we rely on a physical machine working properly. I don't agree. When a computer checks a long case analysis it is carrying out the same deductions I would carry out with infinite patience. What I get is deductive knowledge through a reliable instrument.

    Compare reading a proof in a journal. I trust the referees, the typesetting, my own tired eyes at midnight. Mathematics was always social and always instrumented. The proof assistant is a better instrument than my eyes, not a different kind of source.

  3. Tomasz Szewczak

    Fellow

    Derek's point is the one I meet most often at work. The kernel almost never fails; the definitions do. We once spent a week on a lemma that was true only because a definition had quietly made the case we cared about impossible.

    So perhaps Wittgenstein's demand survives in modified form. The proof can be unsurveyable, but the statement and the definitions have to be things a person can take in. And Ana Clara's instrument point works only if we keep checking that the instrument is pointed at the right thing.