This quote sums it up pretty well: > Voevodsky himself is careful to distinguish the various ways computers should or shouldn’t be put to use. “Lots of people

This quote sums it up pretty well: > Voevodsky himself is careful to distinguish the various ways computers should or shouldn’t be put to use. “Lots of people don’t understand the difference between using computers for calculation, for computer-generated proofs, and for computer-assisted proofs,” he says. “The computer-generated proofs are the proofs which teach us very little. And there is a correct perception that if we go toward computer-generated proofs then we lose all the good that there is in mathematics—mathematics as a spiritual discipline, mathematics as something which helps to form a pure mind.”