“Our system of refereeing was designed in an age before computers. Our system is poorly adapted for a proof that relies on 40,000 lines of computer code. There is a better way, and this prize today fills me with a new level of energy and enthusiasm. I am channeling that energy into a system that offers greater reliability than a human referee. Computer proofs should be checked by computers.”