> I'm *very* supportive of automation for Metamath, and I think everyone else is too. That's great! I am going to assume we can get >=5 people pitching in ideas/design and >=3 working on implementation (>10 hrs/week). In a couple of days, I will post a small questionnaire to understand what kind of features folks are looking for in the automation. Following that, I will help organize a design discussion.
> In Metamath, automated tools are used to find the proof, but what is stored as the proof is the *actual* exact sequence of axioms & previously-proven theorems... not just "hints" to an automation system to let it rediscover the proof. My goal is to make every proof/argument available and scrutinize-able by my users. So, Metamath's property of storing actual proof along with the fact that the proofs can be read by casual readers (with some Math background) are the main reasons I was attracted to Metamath instead of other systems in the first place. > I think Metamath has advantages, and there's no reason more can't be automated. Let's automate more then! -- 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/0836273d-94df-4d66-9554-ed029cc7a601n%40googlegroups.com.
