[6534278]

This is a bit out of my area but...

> still a huge gap between my skills and what is needed for real work

That's kind of inevitable, you've passed your driving test but that doesn't mean you're ready to compete in Formula One race.

> Note even that, you cannot even follow proofs of real theorems

This may not be relevant to your experience or it may, but decades ago I did a tool-guided transformation of a very simple specification into a very simple program. This was done as a study for teaching people. I carefully explained every step as best I could, but the interesting thing was as my memory of doing it faded, the explanations became mainly useless – why I did a particular transformational step became lost, and my prior written explanations just didn't help. It's not like commenting code!

Now, maybe with extra experience I could do better these days, but quite possibly not. There is a certain kind of 'zone' you go into which has no parallel with programming. It may be that theorem proving at that level may only be something you can do, and do with practice, but can't follow afterwards; a state of mind. I don't know. FYI anyway.