What's the most confusing thing for a mathematician when they start using a proof assistant, speaking from your personal experience? (Computer scientists, plese do not answer this one.)