This is already happening, by the way, and some Lean projects are being written in this way. Not only for the reader, but the proof writers themselves tend to need this to navigate their own code. Also check Lean 4 Blueprint, which is a component in this direction.