Hey Thierry Thanks for those rules. I am planning to export human proofs to TeX (and let mathJax do the translation to mathML), so I might not be able to use your rules as is but, following their lead, they might speed up writing TeX rules. I'll open source the rules for translating metamath to TeX, once/when/if I write them
You are right about the symplifying the formula part and about the showcasing part too. By selecting the root of a formula and applying reduce, it can be simplified in one go. When formulas are too complicated for Mephistolus to handle, it will require some human gently guiding it's software hands (like with students) (much) later, I hope to be able to handle commutativity, associativity, moving things around in a user/mouse/touch friendly way. Best regards, Olivier Le dimanche 1 décembre 2019 04:55:19 UTC+1, Thierry Arnoux a écrit : > > > Hi Olivier, > > Very interesting! > Mathjax is also what I’m using for the rendering of the “structured” > pages, like: > > > http://metamath.tirix.org/esum.html > > > http://metamath.tirix.org/areacirc.html > > > I’m maintaining the rules for translating any set.mm statement into > MathJax here: > > https://github.com/metamath/set.mm/blob/develop/set-mathml.mmts > > Feel free to reuse it! > > It looks like for simplifying a formula, one would start at the lowest > level, and then continuously work ones way up: > If I’m looking for a proof assistant, I would probably like to have this > automated, and the whole formula simplified in one step. > > But I suppose for educational purposes, you want to expose each of these > steps. > BR, > _ > Thierry > > > -- 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/7a62d3e0-40a4-4bc6-8e94-6cc73e3322ca%40googlegroups.com.
