I've thought a bit about a web editor and I really like the idea. It makes distribution of the tool effortless. Here's a few things.
Firstly for me I think the most enduring challenge of metamath is finding theorems in the database to use them in proofs. I had a go at making a search engine but that didn't go so well. I like how Milpgame is laid out with all the theorems down the left hand side. I think in my imaginary ideal tool that would be something which was central, easy ways to search the database with common theorems in a palette maybe and even suggested theorems to use next if that is possible. Secondly I had a look at making a frontend and came across Quill <https://quilljs.com/>, you can see how in maybe 10 lines <https://quilljs.com/playground/> you can add a text editor to a webpage so I think the frontend would be relatively easy. Thirdly I recently came across literate programming <https://en.wikipedia.org/wiki/Literate_programming> for the first time. I think it's a really interesting idea and immediately made me think of metamath. If it were possible to write proofs in natural language and then have macros replace the natural language with mm steps I think that could be a really powerful way of bridging the gap between beginners and experienced users. It's also interesting how it only uses substitutions which is very in line with how metamath works. It might also really help with constructing a proof, that's generally how I try to do things, to write down the ideas first and then fill in the details after. I even had some crazy thought about trying to auto generate natural language explanations of proofs from existing proofs, however that was probably just a flight of fancy. Jon -- 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/1275742c-ec72-48c1-b728-a184edb21da0%40googlegroups.com.
