Follow up. > 5. He somehow got lost in the gory technical details of strict proof syntax > and verification. But the core idea of a Metamath proof is applying > patterns to symbol strings. He seems not always be aware of this 'road > map'. I remember when I first looked into Metamath I was not in the least > interested in details like how variables are defined. In fact, I was not > concerned with program details at all. I was satisfied to know how to > replay a proof by hand. Once I learned the top level formalism, I easily > could imagine a stack like structure for some automatic verification.
Not sure what we can do to help there. -- 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/ac188c41-0a50-4604-ab82-896093fa0c3e%40googlegroups.com.
