> > Formalizing a proof with metamath is certainly a very good way > to understand an unformal proof. I don't know if you have alreay tried it. >
Yes, I did. I proved simple propositional calculus theorems in mmj2 using deductive form. But I'm at loss from a sheer amount of theorems in set.mm and the only help is their name conventions and rudimentary search facility. That's just too painful in comparison to e.g. Lean's tactics mode (or auto completion) which will infer many details without your consent. But the price is high: there is no detailed axiomatic proof which is understandable by humans. For example a simple arithmetic theorem when exported take dozens of megabytes of incomprehensible byte-code (compare to Metamath's proofs) which can't be rendered/pretty-printed and even type checking takes far too much time. Using #check or #print doesn't help either because it used dependent type theory as a foundation. People can get used to it, mmj2 is not that bad after all. But it needs much more tedious training than necessary, even though it's secondary to my goals. I will do it eventually but only after I'm already proficient enough with Lean (MM0 is not ready yet). Looks like I'm more used to tactics workflow even before I knew that it used tactics behind the scene. I have some previous beginner's experience with other proof assistants with a more user friendly UI but I didn't learn their tactics language before. Good tutorial is a key to become familiar with database and workflow. And a good interactive goal driven UI helps a lot. I'm just don't feel confident without much background in mathematics so I will try to get that confidence before diving into set.mm. Or if Mario's suggestion to create a curated database will be implemented then I could try it sooner. -- 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/84494ffb-6779-4d8d-ad44-aa701b29d155%40googlegroups.com.
