Proving a theorem by checking every case

The reduction was human work, and so was the idea that a finite set of configurations would settle an infinite question. The case checking was not, and no reader could redo it by hand in a lifetime. Mathematicians objected that a proof nobody can verify is not a proof, and over the following thirty years they stopped objecting, as the method spread and a cleaner version was published in 1997 that still needed the machine. What was ceded is the exhaustive part of an argument, the bookkeeping that establishes a result without explaining it. What was not is the choice of what to prove and the design of the reduction, which is where the mathematics went on living.