Hi, I think I can come up with shorter (and more readable) versions for some of the proofs I saw on the MPE explorer. I will never know until I try it. I would like to try out mmj2 to experiment with some proofs.
I watched the "Introduction to Metamath & mmj2" <https://www.youtube.com/watch?v=Rst2hZpWUbU> video mentioned at " http://us.metamath.org/index.html#faq";. I looked for the "http://us.metamath.org/index.html#downloads"; section and I found: mmj2.zip <http://us2.metamath.org:88/ocat/mmj2/mmj2.zip> (7.2 MB) (latest version, 2.4.1 26-Jan-2016, maintained by Mario Carneiro) mmj2-orig.zip <http://us2.metamath.org:88/downloads/mmj2-orig.zip> (Mel O'Cat's last official version, 11-Oct-2011) However, a google search for "mmj2 download" came up with something that looks like a later version at: https://groups.google.com/forum/#!topic/metamath/3kN15fc2MdY >From watching the video, I noticed that mmj2 is a text based editor. I do not mind ASCII, I even prefer it in some cases. At the same time, I find the HTML version much easier to read, follow and present to newcomers who never heard of Metamath. Are there any HTML or Lyx based editors that incorporate the mmj2 features which I could help beta test? Thanks, Noam Tene -- 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/ee2b8ff7-c648-44b9-96ce-df6066f63cf3%40googlegroups.com.
