> Igor, congratulations! I hope you'll prepare a pull request to set.mm, in my opinion the result is interesting enough to have it, at least, in a mathbox.
> I looked over your proof file. I think some smaller lemmata (especially leading to the proofs of 3cubeslem1 and 3cubeslem2) can be joined into bigger chunks, that way proofs will be able to reuse same statements (for example, in syntax breakdown steps). Also I have a feeling that the metamath.exe minimization algo will be able to do more with bigger proofs. Similarly, many proofs share the same hypotheses (for instance, |- ( ph -> A e. RR ) ), and it can be reused if you put several statements into one block. Thank you! Sure, I will add it into my mathbox after some enhancement. > Also you seem to be jumping back and forth from the deduction style (like in _3cubeslem1_gtz_d) and "usual style" (like in _3cubeslem1_gtz_i). I don't know if that's necessary, but the idea is usually to carry the proof in deduction style where it's possible and maybe switch to the usual style near the end to state the main result. At the beginning I didn’t know what approach to use. That’s why there are theorems in different forms in the beginning. Initially I created all three forms (inference, deduction and closed) for each theorem because I didn’t know what form I would need further in the proof. But somewhere in the middle of the proof I realized that I need only deduction. Before creating a pull request I will remove all redundant theorems. > By the way, did you end up using some automation to finish the proof, or you did it all by hand after all? The parts where I needed to compare or transform polynomials have been proved in semi-automatic mode. Everything else has been done manually. I heavily used the bottom-up prover of mm-lamp, but I count it as “manual mode” because it is able to find only very simple proofs. By the semi-automatic mode I mean a new automation functionality which I added to mm-lamp while working on this proof. It is currently not available on the mm-lamp web site, but I will release it in one of the next versions (hopefully in the next one). - Igor On Tuesday, January 2, 2024 at 9:14:52 AM UTC+1 savask wrote: > > A proof for 3cubes is ready > > Igor, congratulations! I hope you'll prepare a pull request to set.mm, in > my opinion the result is interesting enough to have it, at least, in a > mathbox. > > I looked over your proof file. I think some smaller lemmata (especially > leading to the proofs of 3cubeslem1 and 3cubeslem2) can be joined into > bigger chunks, that way proofs will be able to reuse same statements (for > example, in syntax breakdown steps). Also I have a feeling that the > metamath.exe minimization algo will be able to do more with bigger proofs. > Similarly, many proofs share the same hypotheses (for instance, |- ( ph -> > A e. RR ) ), and it can be reused if you put several statements into one > block. > > Also you seem to be jumping back and forth from the deduction style (like > in _3cubeslem1_gtz_d) and "usual style" (like in _3cubeslem1_gtz_i). I > don't know if that's necessary, but the idea is usually to carry the proof > in deduction style where it's possible and maybe switch to the usual style > near the end to state the main result. > > If you prepare the set.mm pull request, more experienced metamath users > will surely give more comments on how to simplify the proof, what labels to > choose etc. I think it can be shortened quite a bit. > > By the way, did you end up using some automation to finish the proof, or > you did it all by hand after all? > -- 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/7dff569d-2100-4f13-a31a-fee8f6f58bedn%40googlegroups.com.
