On 8/22/22 07:33, David A. Wheeler wrote:
This is really cool. I've alerted Freek & asked him to add a link to
this in:
https://www.cs.ru.nl/~freek/100#25
I have no idea how Freek will handle this. In this case we want *both* proofs to
be cited. Also, this is a proof of unprovability, not a proof in the usual
sense.
I'll let him figure out what he's going to do :-).
Yeah, he has a convention of putting constructive proofs in italics but
doesn't define what "constructive" means. For irrationality of the
square root of two the italicized proof is for the equivalent of
https://us.metamath.org/ileuni/sqrt2irr.html but I (and wikipedia)
interpret "constructive" in the context of this problem as meaning
something stronger - https://us.metamath.org/ileuni/sqrt2irrap.html .
I suppose the exmidsbth result may fall under the "does not keep track
of /all/ formalizations" disclaimer at the top of the page, but we can
let him worry about that sort of thing.
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.
--
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/893839b4-d9c2-05de-1dc8-b7798134c465%40panix.com.
