For those who have been keeping score, set.mm is up to 74 theorems from
the Metamath 100 list.
iset.mm on the other hand has been stuck at one (which is induction over
natural numbers) for some time (despite much progress in constructing
real numbers, sequence convergence, existence of square roots, and other
topics, they didn't hit Metamath 100 theorems).
I am pleased to report that we can now report that we have a second
Metamath 100 theorem in iset.mm. This is "bezout" which is stated as in
http://us.metamath.org/mpeuni/bezout.html but proved using a
constructive proof (we cannot just assert the existence of an infimum of
nonnegative integers; instead we apply the Extended Euclidean Algorithm
to compute the greatest common divisor and also show that it satisfies
the Bézout property). For more details I suppose the informal proof at
https://github.com/metamath/set.mm/issues/2399 is probably the most
readable place to start (although the proof there is spread over several
comments and not quite written out with consistent notation and dead
ends removed), or browse through bezout and all its lemmas in iset.mm.
Although I did the mmj2 formalization, I want to also acknowledge Mario
Carneiro's essential contributions to this effort. I was very much
stumbling through "how do you even turn the Extended Euclidean Algorithm
into metamath proofs?" when his informal (but detailed) proofs paved the
way for a much simpler and clearer approach than anything I might have
eventually come up with. Most of his proofs in the github issue linked
above translated pretty directly into the formalization which was just
merged.
What's next? My own plan is to continue formalizing number theory
(working towards https://github.com/metamath/set.mm/issues/2298 -
another Metamath 100 theorem) (well or summation -
https://github.com/metamath/set.mm/issues/2167 - if I ever get back to
that). But other contributions are welcome! We've already seen some
great CZF work from Benoit and a few contributions from others, so
please do send in proofs, or open an issue or otherwise get in touch if
you want advice or help. iset.mm has gotten to the point where it is
both a treatment of how logic and set theory are affected by the absence
of excluded middle, but also covers other topics like complex numbers,
square roots, and absolute value, including issues which are different
without excluded middle such as sequence convergence, apartness, or
supremums. So there's plenty to work on if you don't want to have to
start from the beginning.
--
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/b8647f17-b85c-0f15-69c2-82b16349d910%40panix.com.
