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).
Adding a new line to the disjoints box currently requires pressing shift+enter, but this doesn't work on mobile devices. Pressing enter on a smartphone/tablet should insert a new line instead of exiting the text area.
Adding a new line to the disjoints box currently requires pressing shift+enter, but this doesn't work on mobile devices. Pressing enter on a smartphone/tablet should insert a new line instead of exiting the text area.