A truly great tool might as well generalize to the axiomatic method in general. When I've gone through math texts (Euclid's Elements, calculus, topology, etc.) I find it annoying to flip back so much when they are constantly referencing past figures. Even if you write the often used axioms and definitions down, there will still be some that are a pain to access.
I think there's a big opportunity to figure out a way to display these systems in a way no one has done well yet. I'm surprised that if I want to go through Euclid's elements in 2021, it's probably going to be in a pdf or a really basic static webpage. How is there not a super slick app that reveals all kinds of connections in a way only possible with interactive media?
I so happened to have spent yesterday afternoon figuring out mu4e on Emacs, which I'm new to. Figured out IMAP but not sending yet. Worked with gmail with a very simple config file.