> *Thank you, Igor, it is a really interesting video.*
Thanks, Glauco! Yamma’s feature of proposing a list of theorems is also very useful. I want to add such a feature to mm-lamp in the future. > *there's potential for improving the search maybe by adding special tactics for set.mm which narrow down the search with specific theorems banned/allowed.* Thanks for the feedback! Current implementation of the bottom-up prover allows to provide a list of theorems to use. Also it is possible to narrow down usage of some theorems to some specific scenarios. For example, to allow usage of syl only when the first hypothesis is of the form of |- ( ph -> X e. A ) and the conclusion is |- ( ph -> Y = ( X ^ N ) ). With appropriately collected list of theorems to use and such rules for narrowing down usage of some theorems, the bottom-up prover becomes very fast, so I don’t even need to specify statement length restriction. But all of these are available in macros only. I also have a few more ideas to try, for example, making bottom-up prover parameters dynamic, so they depend on what is needed to prove. Currently I am working on a few other improvements which will affect macros API. After that I will start documenting the macros feature. On Saturday, December 7, 2024 at 8:09:48 AM UTC+1 savask wrote: > > Here is my video ... > > It was very interesting, thanks. For me the highlight of the video was the > "proving bottom-up" dialog, which can search for proofs of large depth > automatically. Metamath.exe also has one (the "improve" command), and mmj2 > doesn't, as far as I'm aware, so in a sense metamath-lamp has partly > surpassed mmj2 in functionality. > > There was an interesting part near the end where the proof search couldn't > figure out that A e. CC is implied by A e. RR, since the latter statement > has the same length and hence isn't picked up by the "Less" search > heuristic. I think mmj2's transformation script > <https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js> > > can circumvent such issues in special cases, so there's potential for > improving the search maybe by adding special tactics for set.mm which > narrow down the search with specific theorems banned/allowed. > > > I proved the fifth theorem. Again, apparently one hypothesis is not > needed, the set B is not required to be not empty. > > Nice! You shouldn't require nonemptyness until lemma 7, which postulates > the existence of unity. I think it's a bit unfortunate that we allow empty > magmas, since algebraic structures are usually assumed to be based on > nonempty sets; this makes the theory more uniform. > -- 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 visit https://groups.google.com/d/msgid/metamath/9d3bff4e-c615-41f8-b75b-e96e4a0b910bn%40googlegroups.com.
