What Vampire and similar “automated theorem provers” are doing is searching for a proof of some logical statement (that you specify). That proof search is a rea

What Vampire and similar “automated theorem provers” are doing is searching for a proof of some logical statement (that you specify). That proof search is a really tough problem, so there’s a ton of research that goes into finding ways of speeding up the search e.g. through novel data structures. Proof verification —- the process of verifying the correctness of some claimed proof —- is much faster.