> 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/96D94F8F-B139-452A-B6BB-AE260D6DFC26%40dwheeler.com.
