It is weird to be honest. I first learned Coq and then started taking upper level maths classes. My group theory proofs were panned by my TAs as overly verbose, very precise, and I was specializing on H_1 and H_2s everywhere and having IHns flying around like crazy because I could not fathom how one proves things without formally connecting things up.

Then my profs told me I was not “wrong”, but proofs or expositions are to most mathematicians not programs (ha! How did I not know. You teach me natural deduction and expect me not to program?), more like convincing arguments/prose. At some point one abstracts.