Some thoughts on automation and mathematical research

I discuss how mathematicians come to a shared notion of what is important, and how automated reasoning might affect that process. The deeper one digs the spade, the harder the digging gets; maybe it has become too hard for us unless we are given some outside help, be it even by such devilish devices as high-speed computing machines. (Weyl, [6])