Re: Rosetta Stone for Point-Set Topology Results in Mizar
Josef Urban josef.urban _AT_ gmail.com <[email protected]> Tue, 14 Nov 2023 07:23:32 +0100
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q16WymeNQLt9DSVUvCcAU+NFZS_sSiC32o8hbsLbV3nw1g@mail.gmail.com> |
--000000000000156991060a16d49f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Great! Perhaps the list of Proofwiki articles aligned with Mizar by Grzegorz Bancerek might be useful to such projects: https://proofwiki.org/wiki/Category:Mizar_Articles . Best, Josef On Tue, Nov 14, 2023 at 12:17=E2=80=AFAM Alex Nelson thmprover _AT_ gmail.c= om < [email protected]> wrote: > Hello, > > I spent the weekend assembling a "Rosetta Stone", organizing results as > found in Munkres's textbook on topology and their corresponding > formalization in Mizar: > https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/mizar/topol= ogy.html > > The Mizar formalization turned out to usually be better than Munkres. > > There are a few results which are not formalized in Mizar, like the > Urysohn metrization theorem, but it is entirely likely (highly probable) > that I have just been unable to find the formalization of various results > --- I have noted them in the Rosetta stone when there is no analogous > result in the MML. (If I have missed something, let me know, and I will > update my notes.) > > I think it might be useful for students learning Mizar who want to find > results in point-set topology, I hope you find it useful too :) > > Best, > Alex > --000000000000156991060a16d49f Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable <html><body><div dir=3D"ltr">Great!<div><br></div><div>Perhaps the list o= f Proofwiki articles aligned with Mizar by Grzegorz Bancerek might be use= ful to such projects: <a href=3D"https://proofwiki.org/wiki/Category= :Mizar_Articles">https://proofwiki.org/wiki/Category:Mizar_Articles</a> .= </div><div><br></div><div>Best,</div><div>Josef</div></div><br><div class= =3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Tue, Nov 14, 20= 23 at 12:17 AM Alex Nelson thmprover _AT_ <a href=3D"http://gmail.= com">gmail.com</a> <<a href=3D"mailto:[email protected].= pl">[email protected]</a>> wrote:<br></div><blockquot= e class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px= solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr">Hello,<br><br>= I spent the weekend assembling a "Rosetta Stone", organizing re= sults as found in Munkres's textbook on topology and their corre= sponding formalization in Mizar: <a href=3D"https://pqnelson.github.= io/org-notes/comp-sci/theorem-provers/mizar/topology.html">https://pqnels= on.github.io/org-notes/comp-sci/theorem-provers/mizar/topology.html</a><d= iv><br></div><div>The Mizar formalization turned out to usually be b= etter than Munkres.<br><br>There are a few results which are not formaliz= ed in Mizar, like the Urysohn metrization theorem, but it is entirely lik= ely (highly probable) that I have just been unable to find the formalizat= ion of various results --- I have noted them in the Rosetta stone when th= ere is no analogous result in the MML. (If I have missed something, let m= e know, and I will update my notes.)<br><br>I think it might be useful fo= r students learning Mizar who want to find results in point-set topology,= I hope you find it useful too :)<br><br>Best,<br>Alex</div></div> </blockquote></div></body></html> --000000000000156991060a16d49f--