Save 3cubes in set-mbox-ii.

[expln]

This PR adds 3cubes and all its lemmas.

Along with usual “Contributed by”, a new statement is used in comments - “The assertion statement was formalized by”. I am not sure if this wording is clear and correct, so please feel free to suggest a better one.

[savask]

First of all, congratulations! Nice to see this theorem formalized.

Along with usual “Contributed by”, a new statement is used in comments - “The assertion statement was formalized by”.

I suggest you remove these additional comments about formalization completely. I don't need any credit, and it is quite often that someone suggests a theorem to formalize in metamath, and I think usually people don't mention that in the comments.

Also, about theorems themselves: I remember that I suggested combining individual proofs into one large proof, but the proof of 3cubeslem3 is too large in my opinion, sorry! I'm in fact baffled by how large it is, it is just a series of simple algebraic manipulations, it shouldn't take that long.

One thing you can do (and should) is minimize your proofs with metamath-exe, see this page for further directions. For example, the proof of 3cubeslem2 can be shortened from 2032 to 1898 steps automatically.

The 3cubeslem3 itself probably can't be minimized automatically due to its size, so probably it's better to split it into several parts. Doing left hand side and right hand site separately is probably a good idea, maybe individual cubes can be expanded in separate lemmata as well. It would be interesting to see what other members of the community say, maybe the proof is so large for some technical reasons?

Finally, maybe the comment in 3cubes could have a bibliographic reference to the paper of Ryley himself (it.s S. Ryley, The Ladies' Diary 122 (1825), 35). I hope more experienced members could comment if that's desirable.

[tirix]

Yes, congratulations, it's impressive!
(and I often come out with very long proofs myself...)

The 3cubeslem3 itself probably can't be minimized automatically due to its size

I'm thinking a minimizer tool based on metamath-knife would probably be much faster than the current tool based on the metamath C executable, and maybe it would be able to handle such large inputs, but that's a project that has not been even started yet.

[savask]

I'm thinking a minimizer tool based on metamath-knife would probably be much faster than the current tool based on the metamath C executable, and maybe it would be able to handle such large inputs, but that's a project that has not been even started yet.

Yes, I agree, in my opinion such a tool is long overdue :-) The big downside of metamath-exe is that it decompresses the proof before minimizing it, so naturally the minimizer has a very hard time doing anything. If metamath-knife operated on the compressed proof itself, that would be a huge speed improvement alone.

That being said, I don't think it would make the proof of 3cubeslem3 two times shorter or anything on that scale of magnitude, so it is best that it's split into at least two parts.

[expln]

maybe the proof is so large for some technical reasons?

I think intermediate variables contribute to the length of the proof (as you supposed). I was sure they don't affect the length of the proof. But after your post in this PR I reviewed my proof for 3cubeslem3 and found some suspicious statements which look redundant and most probably they remained after the intermediate variables. Hopefully this should be easy to fix.

That being said, I don't think it would make the proof of 3cubeslem3 two times shorter or anything on that scale of magnitude, so it is best that it's split into at least two parts.

I will think on how to split it. But why do you think it is better to split it? Because then metamath.exe will be able to minimize shorter proofs?

[savask]

But why do you think it is better to split it? Because then metamath.exe will be able to minimize shorter proofs?

Yes, one reason is that metamath-exe can process proofs of moderate size more quickly (we used to run a full set.mm minimization run once in a while, and large proofs posed a problem). Also your theorems will have respective html pages on the metamath website with all the proof steps outlined, and I think it becomes pretty hard to read if the proof is too long.

I will think on how to split it.

One very logical idea for a split is, expand the left hand side in one lemma and the right hand side in another. If you find out that after the intermediate variables fix the proof shrinks in size a lot, then maybe this small split will be enough.

[expln]

Yes, congratulations, it's impressive!
(and I often come out with very long proofs myself...)

The 3cubeslem3 itself probably can't be minimized automatically due to its size

I'm thinking a minimizer tool based on metamath-knife would probably be much faster than the current tool based on the metamath C executable, and maybe it would be able to handle such large inputs, but that's a project that has not been even started yet.

Thank you, Thierry! Such a fast minimizer which can work with long proofs is definitely a needed tool.

[expln]

First of all, congratulations! Nice to see this theorem formalized.

Thanks Saveliy!

I suggest you remove these additional comments about formalization completely.
Finally, maybe the comment in 3cubes could have a bibliographic reference to the paper of Ryley himself

Done.

One thing you can do (and should) is minimize your proofs with metamath-exe

Done for all theorems except 3cubeslem3l and 3cubeslem3r - they are still too long.

One very logical idea for a split is, expand the left hand side in one lemma and the right hand side in another. If you find out that after the intermediate variables fix the proof shrinks in size a lot, then maybe this small split will be enough.

I extracted the left hand side and the right hand side as 3cubeslem3l and 3cubeslem3r, but they are still too long. The fix for intermediate variables removed some small amount of redundant steps but it didn’t improve the situation significantly. Theoretically I can keep splitting proofs further. But it will take some time. On the one hand, I am not sure if this is a good idea because it will add additional lemmas to the global namespace but such lemmas will be hardly reusable. It would be nice if Metamath had a keyword “local” which prevented supplementary assertions from being placed in the global namespace :) On the other hand, if the issue with long proofs is a blocker for running minimizations on the entire set.mm then of course such long proofs must not appear in set.mm.

[savask]

Since this is mathbox only, in my opinion it's good to merge.

On the one hand, I am not sure if this is a good idea because it will add additional lemmas to the global namespace but such lemmas will be hardly reusable.

I think additional lemmata are fine, metamath uses cryptic names for theorems so a collision between labels is unlikely.

On the other hand, if the issue with long proofs is a blocker for running minimizations on the entire set.mm then of course such long proofs must not appear in set.mm.

I don't think we had a full set.mm minimization run since Norm passed away, and it looks like nothing like that is planned in the near future, so this is probably not a very big issue right now. I wonder how readable the proof will be once it appears on html pages, but that we will find out later :-)

Such a fast minimizer which can work with long proofs is definitely a needed tool.

Since metamath-lamp can work with proofs of this length, you could try making a minimizer yourself. The idea is as follows. Suppose you have a proof, and step 100 proves some statement S using steps 50,60,70 and theorem X. The minimizer tries proving statement S using some other theorem Y from the database, referencing, for example, steps 2, 40, 50, 99. It may happen that, for instance, step 60 is no longer used in the proof, hence you can delete it (and recursively all other steps which are not used anymore) shortening the whole proof.

Of course the tricky part is that you introduced a new theorem Y to the list of used theorems (and some no longer used theorems may have disappeared), and also some step numbers in the compressed proof got smaller. In order to tell if this indeed shortened the proof, one has to generate the full compressed proof once again, but often one can just use some heuristic.

Done for all theorems except 3cubeslem3l and 3cubeslem3r - they are still too long.

One other thing. Try running the command save proof 3cubeslem3l /compressed in metamath-exe, it will take a bit of time, but not too long. You'll notice that the proof will be smaller (it shank from 266 to 240 lines), the reason being a different arrangement of used theorems, compare:

In your version:

      ( wcel a1i expcld mulcld oveq2d addcld adddid oveq1d eqtrd addassd eqcomd
      co eqtr4d mulcomd mulassd expp1d wceq c3 cexp c2 caddc c7 c6 c9 c5 c8 3cn

after recompression:

      ( c3 cexp co c2 cmul caddc c6 mulcld oveq2d addcld oveq1d eqtrd eqtr4d c1
      a1i mulcomd mulassd c7 c9 c5 c8 c4 cc wcel 3cn cn0 3nn0 expcld cq qcn syl

The secret here is that theorems which are used more often should be placed first in the theorem list.

[avekens]

According lemmas, see our conventions:

   A proof with the sole purpose of supporting a final proof is a lemma;
   the naming convention for a lemma is the final proof label followed by
   "lem", and a number if there is more than one.  E.g., ~ sbthlem1 is the
   first lemma for ~ sbth .  The comment should begin with "Lemma for",
   followed by the final proof label, so that it can be suppressed in
   theorem lists (see the Metamath program "MM> WRITE THEOREM_LIST"
   command).

So maybe the comments of your lemmas should be revised accordingly (the labels are already OK - they contain at least the fragment "lem").

[expln]

Since metamath-lamp can work with proofs of this length, you could try making a minimizer yourself.

Thanks for sharing the algorithm. This sounds feasible to implement in metamath-lamp. I added it to my to-do list.

One other thing. Try running the command save proof 3cubeslem3l /compressed in metamath-exe

Done for all the theorems added in this PR.

The secret here is that theorems which are used more often should be placed first in the theorem list.

I think this also could be implemented in metamath-lamp. Added to my to-do list :)

[expln]

So maybe the comments of your lemmas should be revised accordingly (the labels are already OK - they contain at least the fragment "lem").

This is done. Thanks!

[avekens]

Ready to be merged (from my point of view).

[benjub]

There are still several statements that could use fewer lines and remain readable (which is a different practice than our current one), but I think it's ok, especially since this is in a mathbox.

[expln]

There are still several statements that could use fewer lines and remain readable

Do you mean the below statements? Would the below be a good formatting?

    3cubeslem3l $p |- ( ph -> ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) )
        + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) )
      =
        ( ( ( A ^ 7 ) x. ( 3 ^ 9 ) ) + ( ( ( A ^ 6 ) x. ( 3 ^ 9 ) )
        + ( ( ( A ^ 5 ) x. ( ( 3 ^ 8 ) + ( 3 ^ 8 ) ) )
        + ( ( ( A ^ 4 ) x. ( ( ( 3 ^ 7 ) x. 2 ) + ( 3 ^ 6 ) ) )
        + ( ( ( A ^ 3 ) x. ( ( 3 ^ 6 ) + ( 3 ^ 6 ) ) )
        + ( ( ( A ^ 2 ) x. ( 3 ^ 5 ) )
        + ( A x. ( 3 ^ 3 ) ) ) ) ) ) ) ) ) $=

    3cubeslem3r $p |- ( ph -> ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 )
        + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) )
        + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) )
        + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) )
      =
        ( ( ( A ^ 7 ) x. ( 3 ^ 9 ) ) + ( ( ( A ^ 6 ) x. ( 3 ^ 9 ) )
        + ( ( ( A ^ 5 ) x. ( ( 3 ^ 8 ) + ( 3 ^ 8 ) ) )
        + ( ( ( A ^ 4 ) x. ( ( ( 3 ^ 7 ) x. 2 ) + ( 3 ^ 6 ) ) )
        + ( ( ( A ^ 3 ) x. ( ( 3 ^ 6 ) + ( 3 ^ 6 ) ) )
        + ( ( ( A ^ 2 ) x. ( 3 ^ 5 ) )
        + ( A x. ( 3 ^ 3 ) ) ) ) ) ) ) ) ) $=

    3cubeslem3 $p |- ( ph -> ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) )
        + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) )
      = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 )
        + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) )
        + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) )
        + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) ) $=

    3cubes $p |- ( A e. QQ <-> E. a e. QQ E. b e. QQ E. c e. QQ
      A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) ) $=

[avekens]

At least 3cubes should be reformatted as proposed:

3cubes $p |- ( A e. QQ <-> E. a e. QQ E. b e. QQ E. c e. QQ
                           A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) ) $=

[benjub]

The one that @avekens proposed, yes. There are also two "equal" signs that are alone on their lines and that could go to the line right before or right after (I prefer when "=" is at the end of the line, since it tells the reader they should expect a next line, but others prefer to begin a line with "=").

For the moment, there are no strict rules, because there is no automatic wrapping of statement lines, so respecting and enforcing the rules would be a nightmare. Therefore, try to find a balance between compactness and readability, but don't worry too much.

[expln]

At least 3cubes should be reformatted as proposed

There are also two "equal" signs that are alone on their lines and that could go to the line right before or right after

Thanks for the clarifications. This is done.

I could not put the A constant right below the E. because of the line length restriction. So I put it as much to the right as possible.

I chose to put the equal sign at the beginning of the line because Thierry previously mentioned "The idea is to have the equal sign = and the top level operations stand out a bit more.".

[avekens]

I think this PR is ready to be merged (3 approvals, no objection).

[GinoGiotto]

Looks like one of the checks failed during merge? https://github.com/metamath/set.mm/actions/runs/7732471647/job/21082474245

[tirix]

It worked after I re-run the failed tests.