I want to point to a former discussion https://groups.google.com/g/metamath/c/mnkBQV1_cXc (starting with an impressive essay written by Norm), in which the question what and how to move definitions/theorems to main set.mm is discussed. Especially my proposal to introduce an additional layer betwen main set.mm and the mathboxes (see https://groups.google.com/g/metamath/c/mnkBQV1_cXc/m/A5OEsTk7AQAJ) could be helpful here: Such an "incubator layer" could be a place for definitions/theorems which are not experimental anymore, but not mature enough to be moved to main set.mm. This could also support the review process described by Benoît.
Alternatively, we could create a "Mathbox for Christian Goldbach" where we could place Thierry's and my material about Goldbach's conjecture. On Friday, January 14, 2022 at 1:51:53 PM UTC+1 Benoit wrote: > 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/76e6d845-1746-4850-87ee-3d8db28829e1n%40googlegroups.com.
