as a non-mathematician, I would love to see mouseover hints for mathematical symbols. For example, the proof explorer has a symbol ∈ which means "is contained within". But I don't know that without consulting the "Metamath Proof Explorer Overview" page. Being able to put the definition into the proof would greatly improve accessibility to non- or novice mathematicians, IMO.