More broadly it seems that he's oblivious to the field of automated theorem proving altogether. Why would people devote their lives to ATP if it weren't useful

More broadly it seems that he's oblivious to the field of automated theorem proving altogether. Why would people devote their lives to ATP if it weren't useful? Of course humans need to derive insight from proofs, but it's also important for them not to have mistakes.