Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
I also suggest that if "visualization toggle" tries to reveal a hidden visualization, automatically invoke unification if there isn't a green checkmark. After all, if the user requested it, the user presumably thinks it's possible & we should try to achieve it.
Copied from https://github.com/expln/metamath-lamp/issues/83#issuecomment-1586236073