Donald MacKenzie’s book Mechanizing Proof: Computing, Risk, and Trust was published in 2001, when mathematicians and philosophers were still arguing over whether the Appel-Haken proof of the Four Color Theorem actually counted as a mathematical proof. That’s not to say the argument over the Appel-Haken proof has been settled since then; but now there is much more food for argument. Tim Gowers, Tom Hales, and Vladimir Voevodsky, all of whom enjoy impeccable credentials as pure mathematicians (and none of whom would ever be mistaken for a nerd), are actively working on automated proof-checking and theorem proving. Hales has worked on a variety of deep questions in geometry, number theory, and logic, but is best known for his computer-assisted proof, with Samuel P. Ferguson, of Kepler’s conjecture on sphere packing. The inability of the human referees to verify the program that made his proof work, and thus to certify the proof as valid, inspired Hales to launch a massive international project, called Flyspeck, to devise a completely formal version of his proof. The paper announcing the successful completion of this project was released this January. It is, by any measure, a landmark in the history of human mathematics. Does it also presage the end of that history?
Hales gave a talk last June at the Séminaire Bourbaki in Paris. Bourbaki didn’t used to go in for that kind of thing, but the hall was packed and the discussion session was unusually lively— you can watch it on YouTube. For once there were philosophical questions, including some big ones: “To formalize a proof, do you need to understand it?” (1:07:20) and “Do you think the job of mathematician is threatened?” (1:07:56). It’s worth listening to Hales’s answers.
Back in prehistoric times, philosophical reaction to the Appel-Haken proof presupposed that humans were still in charge. Thomas Tymoczko thought that accepting Appel-Haken proof committed us “to changing the sense of the underlying concept of ‘proof'” because, in contrast to the usual practice, “the proof of the four-color theorem was not ‘surveyable'” (here and in what follows I’m quoting MacKenzie; the word surveyable is from Wittgenstein). Paul Teller countered that
Surveyability is needed, not because without it a proof is in any sense not a proof… but because without surveyability we seem not to be able to verify that a proof is correct.
Perhaps, thought Teller, “mathematics is not an essentially human activity.” Stuart Shanker disagreed with both Tymoczko and Teller; he “drew upon the authority of Wittgenstein” to argue that a proof must be surveyable, and that therefore the Appel-Haken proof is not a proof.
Ian Hacking’s Why is There Philosophy of Mathematics at All? claims that this sort of talk is both a misreading of Wittgenstein and an unrealistic account of actual mathematical proofs, which are typically not surveyable. But this is moot if there aren’t any human mathematicians around to do the surveying.
Gregory Chaitin paraphrases William Byers in his review of the latter’s How Mathematicians Think:
if mathematicians think they are machines, they will behave like machines; if mathematicians think they are trivial, then they will be trivial.
We have computers now, so we don’t need to have people imitating machines. The 21st century is beginning: time to throw off our chains, and unleash the power of our imagination and creativity. We should be as unlike machines as possible.
Reassuring words to reread on a day when the New York Times published an article entitled “If an Algorithm Wrote This, How Would You Even Know?”