On Tuesday, July 23, 2019 at 3:03:28 PM UTC+3, Mario Carneiro wrote: > > In the right hands you can go very far with automation style proofs. > Unfortunately I don't think those hands are mine, since I seem to have > inherited a DIY attitude from metamath and don't make much essential use of > tactics even when they are available. >
I would argue that conventionally there could be actually two kinds of potential users: "programmers" and "mathematicians". "Programmers" feel comfortable when they constantly adjust their tools to better suit their personal requirements. And "mathematicians" (or "students" if you prefer) are just here to see proofs, they are not interested in writing the tools themselves. Depending on a particular audience you might get a different side of the opinion. -- 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/2eecc214-1a5d-47f4-ab81-647747bd5745%40googlegroups.com.
