I don't know but I was thinking of making such a request, if any, after we have 9 theorems for iset.mm (above the lowest ranking prover currently on the list). Currently we are at 6.
Now it is up to him how to categorize and the field is a bit of a wild west in terms of what axioms/libraries/etc each of the proofs on the list depend on, so that's why I'm at least as worried about our own tracking as I am about how we are able to present it on that list. On August 23, 2022 7:52:08 AM PDT, "David A. Wheeler" <[email protected]> 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/E366880F-C1ED-4D0A-916C-BF634AB43CE6%40panix.com.
