A mathematician looks at a line in a proof and asks herself 'is that a correct application of logical inference rules?' She either spots a violation or gets a feeling that it's in fact correct. There's a very high chance she got it right but no mystical state of pure logic that guarantees it.

In this scene, does an automated proof verifier count as a mathematician? I'd agree that there's still neither a 100% chance of correctness nor a mystical state of pure logic at work here, but calling the process "intuition" still strikes me as very misleading.