wlammen
commented
5 months ago One incentive of this database was having short proofs. So if a closed, or immediate form of a theorem has 7 or more applications, then it pays for having it around as a convenience. The number was disclosed to me by Norman Megill, the founder of this project. He would accept a proposal by me, if I could point out at least that many applications. Deduction is not always superior. See for example https://us.metamath.org/mpeuni/syl.html vs https://us.metamath.org/mpeuni/syld.html. Much of your critics is directed towards automation in proof design. There are more, like creating modules for better layering and separation of topics, that were suggested, or even discussed, in the past. We see little to no progress here, I think mostly due to lack of time. One can observe these phenomena in a project like metamath-knife, that still does not replace metamath.exe to full scale.
metakunt
tirix
glacode
david-a-wheeler
digama0
I don't have a google account and I don't know if it is possible to use the mailing list without one. If it is, please let me know the steps so that I can post it on the mailing list. Otherwise I would be happy if one of you could open a issue on the metamath mailing list on my behalf. I hope it is as simple as writing an E-mail to metamath@googlegroups.com.
Hey guys, I have been working for a few weeks on the project and as a new user I wish to share some feedback I have. I want to start this discussion to overall improve the state of metamath and make sure that it is easy and straightforward to use.
Many of you are either maintainers and/or are on the project for a long time. Also I will only be listing things that can be improved from my perspective, things that are positive/working are not listed. Those things include the helpful community and the fact that metamath is pretty fun to work on.
Here are the things that I had issues with and that I wish to improve in some way, listed in order of severity (most severe issues are listed first.)
-Lack of theorems in deduction form. Oh my goodness, I can't explain how much that one annoyed me. Once I have learned how deduction proofs work I fell in love with, it is simple, fast and has a great developer experience. The reason is once you have a theorem in deduction form the unifier will do most work for you, completing substeps automatically which I'd have to painstakingly find myself. It is just great and speeds up the development by one or two orders of magnitude per step. This adds up, my generous estimate would be that using theorems in deduction form is at least twice as fast as theorems in closed form, just by the virtue of autocompleting. But this is not all. The best thing about deduction proof (similar to an inference proof) is that it absorbs and scopes everything in context. That means that antecedents are all small, with some exceptions being conjunctions that eliminate themself eventually (classical case elimination). But this issue maps to closed form proofs so it is irrelevant. Point being it is easier for me to recreate a theorem in deduction form to use it, as I did in my mathbox, because it will save me time after just a few usages. Converting a theorem into deduction form with 5 or more conjuncts will amortize after 1 or 2 usages. Some lemmas which have lots of conditions are gcd lemmas, deduction forms are in my mathbox. I'd like to move them to main as they are way easier to use.
I have multiple suggestions here, my most preferred would be to rewrite simple results on complex numbers from closed form to deduction form and deprecate those closed form results and eventually delete them. (Section 5.2 and Section 5.3) I have the opinion that deduction form is superior to closed form in almost every other way and the benefits for moving in that direction would make proof development much faster. Since this is something I might be wrong with I would like to know if there are any downsides that would make this a bad idea.
I have checked randomly some theorems that have both a deduction and a closed form and I have found out that many theorems are referencing the deduction and not the closed form. If you consequently use deduction form you will get mmj2 autocomplete which in some cases autocompletes 20 steps. I really don't want to prove results that autocomplete can prove for me, this is a waste of time at best.
Here is one example https://us.metamath.org/mpeuni/add12.html 3 usages, 2 of which are proving inference and deduction version https://us.metamath.org/mpeuni/add12d.html 13 usages.
https://us.metamath.org/mpeuni/addcomd.html referenced theorems are 15 lines in my browser. Proof is done exclusively with theorems in deduction form while it's closed form only has 7 lines of usages
ltle 11 lines vs 21 lines for ltled addsub <1 line vs 5 lines for addsubd
The trend continues, there were even some theorems where the deduction form hat 100+ usages and the closed form not even 10.
I would also for consistency sake reformulate inference form theorems as deduction form. The decbld* theorems use those and if you rewrite those from base up you don't get the downside of always adding a1i to proofs. And should you ever need the form without the antecedent you can easily use mptru. Proof length should be around equal if it done consequently and the benefit is that future proofs in deduction forms don't need to use a1i on any hypotheses that are for future use.
Here are my suggestion as a bullet list:
Eventually: Rename deduction form without suffix, once inference and closed form are gone, see https://us.metamath.org/mpeuni/isumshft.html it is in deduction form without closed or inference form existing. My goal is to get there so that we have consistent theorems only in deduction form. My goal isn't to get rid of all inference and closed form theorems, just for some sections which I think benefit it the most.
The same I would also do for inference lemmas like 2+2=4 would become ph -> 2+2=4, so that future lemmas could directly use it if they ever need the fact that 2+2=4. Introduce new naming convention for those theorems in the section that would have no d suffix. Since there are only deduction form theorems it would not be necessary to suffix it anymore for a particular section.
I would like to research if a mass rewrite could be done automatically, I assume some of you have some experience in the necessary tools, in doubt I could do it by hand for each theorem. It shouldn't take that long if you work theorem for theorem (maybe several hundreds of hours)
But that is only if there is some consensus that it is wished. Maybe noone had this proposal but many implicitly wished for the same things as I did. Maybe you have a different workflow that does not have the same issues that I do. I would like to hear about it and have a discussion and bundle it in a RFC of some sorts where we can share opinions.
Another point is that useful theorems are either hidden in mathboxes or just nonexistent. The fact that lemmas are in its most general form without an ergonomic form existing makes several lemmas way harder to prove than it should be. An example is the fundamental theorem of calculus. It is nice that a general theorem exists but this leaks topological results, and it shouldn't. Also it is necessary that you prove that a function is real-differentiable, but either I'm completely stupid and missed how to use real derivative builders (which would be my fault), or that some ergonomic lemmas are missing. I've moved one theorem from Glauco's @glacode (I hope that's him) mathbox which was a godsend, and it still was way too difficult to prove. It should have easy to satisfy hypotheses where you only really need to check that the derivative matches and to eventually calculate the values at the boundaries. The fact that topology and (real/complex) differentiability leaks is not very helpful as everyone who wants to use the fundamental theorem to calculate an integral will have to reprove those statements that should be encapsulated in an easier to use theorem.
It is not understandable to me that there isn't a easy to use version of a theorem of such a fundamental fact that anyone knows and that a simpler version could exist. I love the fact that theorems are proven in its most general form. But a simpler use would be very much appreciated. Even better would be if those would be useful for most of us and not restricted to mathboxes. I get that there are theorems in mathboxes for experimental content. But some things really are so useful that they could be moved directly to main so that other people can use it.
As far as I can tell. @digama0 you have done some converting of theorems of closed to deduction form. I would like to gain that insight how you did it. An example is https://us.metamath.org/mpeuni/isumshft.html this theorem was written in 2007 and you have revised it to use deduction form. I would be interested in continuing your work.
Also I had some issues with tooling, I couldn't get yamma to run and mmj2 was extremely hard to set up (issue with java version and deceiving runtime params), also mmj2 crashes and gives some unexpected NPE when I wanted to search something. I could help to improve the tooling, that is fine. This is also a minor point.
Overall I am quite happy to work on the project. Metamath is fun, it would be even better if some/all of my suggestions would be implemented. I think the database doubled in the last few years, and I have added 1400+ lines which total just a bit over 75KB to my mathbox, which will be much more. I want the project to be scalable with simpler use. Because there are a few issues that new contributors will face as of now. Ancient/arcane tooling, documentationless proofs, difficulty understanding how to formulate proofs. Those improvements are all aimed for mathematicians who all know the theorems but don't know how to formulate them in a formal language. I am also especially thankful to @tirix , you took a lot of time to explain to me some basic concepts. Without that help I could't move forward.
I would love to hear your feedback and I hope that my future contributions will be helpful for future contributors, as I want this project to grow. This is partially motivated by @GinoGiotto ax-13 deprecation, my goal is to have consistent deduction form throughout the whole database.