> Here are a few videos which show the automation I used to prove some parts of 3cubes (all videos are speechless)
That's impressive! In all fairness, it's pretty hard to understand what's going on in the videos, but it looks like your tactics use a lot of intermediate variables in the process (which get eliminated in the end, I guess). I think any intermediate variables can be avoided whatsoever. Also I was expecting a lot less manual interaction for comparing two polynomials, but I probably don't understand some details. You might know about this already, but mmj2 also has some macros, see https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js Maybe this can serve as inspiration for future work. -- 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/6d48a4de-4b22-46ad-b267-f496c3495e5bn%40googlegroups.com.
