That's a real achievement, congratulations to Jim ! As for Wiedijk's list, I think the first principle would be to find a method that minimizes his work. He's maintaining the list out of goodwill and we do not want him to associate Metamath with extra work nor the Metamath community with lobbyists who try to overpublicize their work (I know it's not the case: I'm only speaking of the impression that this might give, and I may very well be misguided).
There are probably other formal systems with some top-100 theorems proved in multiple databases(?), so I do not know if we can ask for a special treatment for Metamath and have both versions linked. (This is not rhetorical: I really "do not know" if this is justified or not.) In any case, it would be nice to have cross-links between the comments in https://us.metamath.org/mpeuni/sbth.html and https://us.metamath.org/ileuni/exmidsbth.html, so that if only one version is referenced from the outside, the visitor can be informed of both versions by visiting any one of them. Benoît On Tuesday, August 23, 2022 at 4:52:37 PM UTC+2 David A. Wheeler wrote: > > > > On Aug 23, 2022, at 12:41 AM, Jim Kingdon <[email protected]> wrote: > > If the goal for iset.mm (supposing it were tracked separately from > set.mm) is to get above the lowest-ranked prover on the list, we need > three more proofs (iset.mm is at 6 and the lowest prover on the list is > at 8). Fortunately, after a dry spell I am finally starting to make some > progress on https://github.com/metamath/set.mm/issues/2575 which is a > blocker for most of the Metamath 100 theorems (because they rely on > summation one way or another). > > > > On a personal note I won't rest until I have > https://us.metamath.org/mpeuni/taupi.html in iset.mm. > > Which also relies on summation. > > We could ask him to track "Metamath (intuitionistic)" separately from > "Metamath". > and use the former for entries in set.mm. It's up to him if he does that. > > Should we ask? > > --- David A. Wheeler > > -- 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/bfc3b633-f7e5-46e5-abca-82c9ce3878dan%40googlegroups.com.
