 In particular Metamath sometimes hesitates between several formulas analyzes (most of them being meaningless) and asks the user to choose.In "Mmj2" this limitation no longer exists.There is also a project by William Hale to add a graphical user interface to Metamath called "Mmide".