Thanks for the interest in this subject. It's surely tempting to try mmpp at some point in the future.
As for UI I think that the most important thing is that it should be adaptive to users progress. That is it should give a list of possible theorems to use depending on the context and this list should be presented in some creative form. It's a vague description, but without some better real world examples it is best description I could imagine. Introducing some visual elements for stimulating geometric intuition and using mouse might be a good idea. I admit that I was impressed by incredible.pm interface and Jape's Fitch boxes in its UI. As Frederic pointed out earlier there is interesting http://proofs.openlogicproject.org/. There are other browser based proof editors as well. Sorry if this doesn't make much sense. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f68c5543-51cd-4c6d-92c7-6c84250cecdd%40googlegroups.com.
