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).
The editor icon bar icons already overflow into 2 lines on Firefox on my Samsung Android phone. The undo/redo icon will make even more phones go multi-line. Smartphones are widely available, but they also have limited screen space.
I recommend "overflowing" icons into the hamburger; this is done in other applications. Then any icons that can't fit quietly move into the hamburger, so all capabilities are still available without using up limited screenspace.
The editor icon bar icons already overflow into 2 lines on Firefox on my Samsung Android phone. The undo/redo icon will make even more phones go multi-line. Smartphones are widely available, but they also have limited screen space.
I recommend "overflowing" icons into the hamburger; this is done in other applications. Then any icons that can't fit quietly move into the hamburger, so all capabilities are still available without using up limited screenspace.