On November 26, 2019 12:36:56 PM EST, vvs <[email protected]> wrote: >So, to be >competitive Metamath's proofs should be detailed and clear at the same time.
I think that clarity of proofs is important. I think part of the problem is a pair of stylistic conventions, not necessarily weaknesses of Metamath itself. First, by convention we generally avoid creating new definitions, and I think we currently go a little too far in the direction of avoiding new definitions. There are disadvantages to new definitions, of course. For example, you typically have to have a number of theorems for each new definition so that the definition is useful, and in many cases you still have to expand a definition. Historically another problem was that definitions are really $a statements, which were not checked, but I don't consider that a problem any more (we now have a verifier checking them and I suspect we will have more soon). But new definitions can make more complicated concepts much clearer. If nothing else, new definitions generally shorten expressions and make it clear what the expressions are all about. I think we should seriously consider allowing or even encouraging more definitions so that more complex concepts are clearer. I think everyone agrees that some definitions are important, it's a matter of figuring out where to draw the line. Second, by convention we often have really long proofs instead of splitting them up into more lemmas and sub lemmas. Splitting them up into logical chunks turn off and really help. I think in at least some cases there are smaller theorems that are both reusable and crying to be made separate. In the longer term, I'd love to see the work completed to permit portions of proofs to be expanded and hidden while staying on an individual proof. I thought that work was really promising; I don't know what its current status is; I'd love to see that work completed. There's no getting around the fact that Metamath proofs are going to be much more detailed than many other systems, especially when compared to informal human proofs (such as those in the published math literature). And I can certainly imagine future systems that improve on Metamath. But I think we can use the mechanisms *already* available to make our proofs clearer. Where that makes sense, we should try to do it. --- David A.Wheeler -- 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/42E20803-3C99-4026-B9D8-612E81CD4C06%40dwheeler.com.
