After graduating with a CS degree and a repetitive strain injury, I decided to teach myself mathematics properly (so I could do technical/creative things without a computer). I took the project very seriously, working part-time at a grocery store with no other obligations on my time than learning.
I would say the two biggest difficulties were 1) Undoing all the very bad math education I'd received earlier in life, and associated repulsion that came from it 2) Figuring out that when I ran into walls understanding certain things it could always be reduced to gaps in my knowledge that were implicitly assumed to not be there. I often ran into that reading proofs in the early days and wanted nothing more than 'very explicit' proofs as you describe (I used to always write mine that way too! In part because it's what I wished the authors were doing).
I'd like to build something in software that automatically associates expandable annotations to mathematical notation, e.g.: http://images.slideplayer.com/34/10244075/slides/slide_5.jpg —It would be super annoying if all the text were always revealed, but with a little cleverness and imagination I think a good scheme could be developed which would satisfy both beginners and experts. I would want a standard library of annotations which would automatically get associated just by using certain standard notational elements.
Here's another demo I put together to try out the same concept for natural language documents: http://symbolflux.com/lodessay/