I think we can separate both issues (the question of symbols for Even/Odd being discussed on github, and the question of mutual mathbox uses). Probably the best option is: if mathbox A uses the theorem xxx proved in mathbox B, then add to mathbox A the axiom ax-xxx with exactly the same statement as xxx and put a comment like "Duplicate of ~ xxx."
As for moving to Main, I think it is premature because both mathboxes show conditional proofs (actually, "very conditional", in the sense that the intermediate steps posited as axioms are not anecdotal, it seems, but correct me if I'm wrong). Conditional proofs are fine for works in progress, but Main is not for works in progress, and moving conditional proofs to Main could be seen from the outside as bragging about Metamath being able to prove this and that. Again, there may be exceptions and I haven't looked at the present case enough. A more general remark: we should strive to maintain the high review standards of Main, and I fear sometimes that the following may happen: when theorems are introduced in a mathbox, reviewer A thinks "it's in a mathbox, so a cursory review suffices and if/when it is moved to Main, a thorough review will be done anyway", and later when that part is moved to Main, reviewer B thinks "it's only a move of something already in set.mm so it has been already reviewed, so a cursory review suffices". I'm not worried about contributions from long-time contributors Thierry and Alexander (although everyone may make mistakes), but more about future contributions. Benoît On Friday, January 14, 2022 at 6:05:11 AM UTC+1 Alexander van der Vekens wrote: > On Friday, January 14, 2022 at 5:02:53 AM UTC+1 Thierry Arnoux wrote: > >> ... >> > Anyway, I'd also like to point out that technically, nothing prevents >> Alexander (sorry for the mix-up in my previous mail) to use theorems from >> my Mathbox; this rule is nowhere enforced. Maybe a short comment that this >> goes against the usage and why we chose to make an exception would also >> work! >> > >> Actually, it *is enforced* not to use theorems of other's mathboxes: on > running "verify markup", there will be warning, for example: > > ?Warning: The proof of "tgoldbachgtX" in the mathbox for Alexander van der > Vekens references "tgoldbachgt" in the mathbox for Thierry Arnoux. > > If it is not accepted to have a dedicated symbol "Odd" (and if we have > such a symbol, we also should have a symbol "Even" for symmetry reasons, > although it would not really be needed), I already though of using > Thierry's local `O`, but let's discuss this further in the github issue > #2433 opend by Jim. > -- 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/429297c3-6a75-44e4-bc6b-bbe957d3bdfcn%40googlegroups.com.
