Feedback from metakunt, a recent contributor

[ookami]

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 at 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:

• Add deduction form variant to many missing lemmas in sections for complex numbers.
• Deprecate closed form theorems in favour of deduction form theorem over a long period of time. (New usage is discouraged)
• Port existing theorems that use above deprecated closed form to use deduction form.
• Delete those closed form variants after 1 year of being deprecated and ported.

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.

[samiro.d...@rwth-aachen.de]

While I am not (yet) a contributor to any databases in .mm format, your praise on "theorem(s) in deduction form" sparked my interest. Especially since I'm dealing with some rather terrible systems outside of Metamath (for example the one with only ψ→((φ→(ψ→χ))→((¬χ→((¬ξ→τ)→φ))→(ξ→χ))) as an axiom, where even finding a proof for  (ψ→φ)→((φ→χ)→(ψ→χ)) — that is, https://us.metamath.org/mpeuni/luk-1.html — is an open problem, see https://xamidi.github.io/pmGenerator/data/w2.txt or http://fitelson.org/walsh.pdf).

Looking at which "theorems" in your math box are declared as "deduction version", I came to the conclusion that you are actually not talking about special kinds of theorems but about rules of inference that take premises such that the theorem it originates from is stated in metalanguage. A theorem has zero premises, so these are technically not theorems (but metatheorems), despite called such by Metamath Proof Explorer.

From my experience, it is definitely easier to prove things via metalanguage due to the increased abstraction. Whether it should be done for ease of use whenever applicable is probably more of a policy/design choice, because it introduces redundancy. Especially since it should be kept in mind that these are not actually theorems, and results (in contrast to solutions as paths) should be theorems.

PS:

Based on my experience, you need a Google Account to join a Google Group, but then an admin can change your address. I have done this (David A. Wheeler changed it for me), but I cannot guarantee whether everything keeps working when you then again delete your Google Account (since I have kept mine). My two accounts are now definitely connected, whenever I do something in this list with my Google Account, it just acts like I'm using my other address, and when I'm using my other address, it also sends it to my Google Mail.

But maybe I am wrong about my first guess, and David could just invite/add a non-Google address? You should probably ask him directly.

[Jim Kingdon]

On 5/16/24 04:02, 'ookami' via Metamath wrote:

> I hope it is as simple as writing an E-mail to metamath at
> googlegroups.com.
>

As far as I know that works.

> Converting a theorem into deduction form with 5 or more conjuncts will
> amortize after 1 or 2 usages.

Once you get up to 5 or more conjuncts I don't think there is much
controversy on this point, and I don't think there would be much
argument about adding deductions (or replacing existing theorems with
deductions) when there are that many.

Oh and in case anyone isn't familiar, the terms being discussed here are
described at "theorem forms" on
https://us.metamath.org/mpeuni/conventions.html

> 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.
>

At least to my eyes this would seem like a case where we just need the
deduction form. Thanks for posting the counts on usages of each form.

> I would also for consistency sake reformulate inference form theorems

> as deduction form. . . . And should you ever need the form without the

> antecedent you can easily use mptru.

There might be a little less agreement about a statement which is this
global. The T. antecedents don't especially bother me but at least at
some times in the history of metamath having them around has not been
loved. And of course beyond a certain quantity of them, it might start
running up against some of our other desires, like shorter proofs.

> 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.

We do this where the resulting deduction theorem would be frequently
used, like https://us.metamath.org/mpeuni/0red.html . As far as I've
noticed in cases like this (where the antecedent really is just to save
an a1i, not because there are any hypotheses) the deduction form would
be in addition to the closed form, not instead of.

In a case of an equality, like this one, we have a bunch of theorems
like https://us.metamath.org/mpeuni/eqbrtrid.html which should help one
to combine deduction form with closed form.

> 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.
>

That's going to be a bit section-by-section or theorem-by-theorem, but
the d suffix is used where it is needed to distinguish different
theorems, not globally for all deduction form theorems.

> 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.

Pretty sure most of the tooling could use some love. Personally, I'm
most excited about the testsuites we have started to add to some of the
tools, but I suppose this isn't the place to go too deep into what would
be the best tooling-related things to work on.