> 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/e49b7f21-471a-473b-8c3f-838acff8ca09n%40googlegroups.com.
