Even though I already reacted on github, I'll extend my congratulations to Jim here, and also to Mario for the informal proof. As important as Bézout's identity is the extended Euclidean algorithm, and having formalized it completely constructively is an achievement. I hope you'll update the Metamath 100 page. I think one can say without too much of a stretch that the proof is in Heyting arithmetic (Peano's axioms do not appear as axioms in iset.mm, but if one traces back your proofs, one can probably convince oneself that this is the case) so there are no questions about its constructive nature (I mean: there is no issue about predicativity or IZF versus CZF).
Benoît On Monday, January 10, 2022 at 8:50:51 AM UTC+1 [email protected] wrote: > 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/50b11628-fb12-4a56-bf29-547bd452d269n%40googlegroups.com.
