[tsimionescu]

I don't think writing proofs in Isabel is really comparable to regular programming. Note also that writing formal machine-verifiable proofs is a skill that few career mathematicians have. Writing regular proofs is a comparably much simpler skill, one that is universal among career mathematicians.

So, the fact that your practice of a very complex version of a skill also improved your ability to practice the simpler version of the skill isn't really surprising.

Coincidentally, my understanding is that many mathematicians find such deeply formal proofs hard to follow, compared to more informal ones. It would actually be interesting to know if your proofs have become more or less satisfying to a practicing mathematician after your experience with Isabel and HOL.