 There is also a project by William Hale to add a graphical user interface to Metamath called "Mmide".Paul Chapman in its turn is working on a new proof browser, which has highlighting that allows you to see the referenced theorem before and after the substitution was made.Milpgame is a proof assistant and a checker (it shows a message only something gone wrong) with a graphic user interface for the Metamath language(set.mm),written by Filip Cernatescu, it is an open source(MIT License) Java application (cross-platform application