Re: Size of Mizar/MML
Alex Nelson thmprover _AT_ gmail.com <[email protected]> Thu, 5 Jun 2025 09:53:21 -0700
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAA+9CX0FC31tDYSBjEQwo0jP8uwXEMiXT-epoqf1p1cAtHBY3w@mail.gmail.com> |
--00000000000022f36a0636d5f4b1 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hello, I am not sure what you mean by "autogenerated theorems", I do not think Mizar has such a feature. Two bits of advice spring to mind: *Advice 1: Use the abstract files.* If you use the latest MML, the $MIZFILES/abstr/ directory will number the theorems and definitions automatically for you. After thinking about it for a bit, I think this is "the right way to go". These are the local files corresponding to what's available online (https://mizar.uwb.edu.pl/version/current/html/). You can simply "grep -r theorem $MIZFILES/abstr/ | wc -l" to get the number of theorems (for me, 75571) and "grep -r ":: .+:sch " $MIZFILES/abstr/ | wc -l" counts the number of schemes (for me, 914). Note that this will not count "lemmas" which are local to files, but "egrep -nr "Lm[0-9]+:" $MIZFILES/mml/ | wc -l" suggests there are 7345 lemma; I would not count them, personally, because they are often made into theorems later in the article (or they prove half of an "iff" statement, or...). Definitions are a bit trickier, since multiple definitions may appear within a single "definition block". One crude estimate may be give by looking at the number of times ":: ARTICLE:def " appears (running "grep -nr ":: .+:def " $MIZFILES abstr/ | wc -l" produces 14134). A similar grep may be done for synonyms (495) and antonyms (138), which are "abbreviations" of sorts. These numbers are for mizar-8.1.15_5.94.1493 which is the latest version of the MML. I should stress, these numbers are approximate. In particular, the theorem count will also include comments like ":: Binomial theorem" (the command "egrep -nr "::.+theorem" $MIZFILES/abstr/ | wc -l" tells me there are only 432 instances of this, which means there are 75139 theorems in the MML). I am certain there is a cleverer way to do a more accurate count of these things. *Advice 2: About axioms.* Also, the articles (files) TARSKI_0 and TARSKI_A contain the axioms to the underlying set theory, so presumably you'd want to exclude them? These are merely 6 axioms and 1 scheme. Best, Alex On Thu, Jun 5, 2025 at 8:56=E2=80=AFAM Fabian Huch huch _AT_ in.tum.de < [email protected]> wrote: > Dear Mizar Community, > > I am currently creating a comparison of large libraries of ITPs. I am > only considering libraries with more than 1M (nonempty) LOC, of which I > know (in alphabetical order): ACL2, HOL4, Isabelle, Lean, Metamath, > Mizar, PVS, Rocq. > To that end, I want to approximate the number of definitions (incl. > axioms / excl. abbreviations, instances, fixed values/constants, > examples) and proven proper theorems (excl. automatically generated > ones) by simple analysis of the sources, without running the system. > > For Mizar/MML, my approach would be to look at tokens in .miz files and > count: > > For definitions: "definition" > > For theorems: "theorem" and "scheme" > > > Does this sound reasonable? I am missing something? Any hints are > appreciated. > > > Best, > > Fabian Huch > > --00000000000022f36a0636d5f4b1 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr">Hello,<br><br>I am not sure what you mean by "autogen= erated theorems", I do not think Mizar has such a feature.<br><br>Two = bits of advice spring to mind:<br><br><b>Advice 1: Use the abstract files.<= /b>=C2=A0If you use the latest MML, the $MIZFILES/abstr/ directory will num= ber the theorems and definitions automatically for you. After thinking abou= t it for a bit, I think this is "the right way to go". These are = the local files corresponding to what's available online (<a href=3D"ht= tps://mizar.uwb.edu.pl/version/current/html/">https://mizar.uwb.edu.pl/vers= ion/current/html/</a>).<br><br>You can simply "grep -r theorem $MIZFIL= ES/abstr/ | wc -l" to get the number of theorems (for me, 75571) and= =C2=A0 "grep -r ":: .+:sch " $MIZFILES/abstr/ | wc -l" counts = the number of schemes (for me, 914). Note that this will not count "le= mmas" which are local to files, but "egrep -nr "Lm[0-9]+:&qu= ot; $MIZFILES/mml/ | wc -l" suggests there are 7345 lemma; I would not= count them, personally, because they are often made into theorems later in= the article (or they prove half of an "iff" statement, or...).<b= r><br>Definitions are a bit trickier, since multiple definitions may appear= within a single "definition block". One crude estimate may be gi= ve by looking at the number of times ":: ARTICLE:def " appears (r= unning "grep -nr ":: .+:def "=C2=A0 $MIZFILES=C2=A0 abstr/ | wc -l" produces=C2=A014134). A similar grep m= ay be done for synonyms (495) and antonyms (138), which are "abbreviat= ions" of sorts.<br><br>These numbers are for=C2=A0mizar-8.1.15_5.94.14= 93 which is the latest version of the MML.=C2=A0<br><br>I should stress, th= ese numbers are approximate. In particular, the theorem count will also inc= lude comments like ":: Binomial theorem" (the command "egrep= -nr "::.+theorem" $MIZFILES/abstr/ | wc -l" tells me there = are only 432 instances of this, which means there are 75139 theorems in the= MML). <br><br>I am certain there is a cleverer way to do a more accurate c= ount of these things.<br><div><div><br><b>Advice 2: About axioms.</b>=C2=A0= Also, the articles (files) TARSKI_0 and TARSKI_A contain the axioms to the = underlying set theory, so presumably you'd want to exclude them? These = are merely 6 axioms and 1 scheme.<br><br>Best,<br>Alex</div></div></div><br= ><div class=3D"gmail_quote gmail_quote_container"><div dir=3D"ltr" class=3D= "gmail_attr">On Thu, Jun 5, 2025 at 8:56=E2=80=AFAM Fabian Huch huch _AT_ = <a href=3D"http://in.tum.de">in.tum.de</a> <<a href=3D"mailto:owner-miza= [email protected]">[email protected]</a>> wrote:= <br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8= ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear Mizar Comm= unity,<br> <br> I am currently creating a comparison of large libraries of ITPs. I am <br> only considering libraries with more than 1M (nonempty) LOC, of which I <br= > know (in alphabetical order): ACL2, HOL4, Isabelle, Lean, Metamath, <br> Mizar, PVS, Rocq.<br> To that end, I want to approximate the number of definitions (incl. <br> axioms / excl. abbreviations, instances, fixed values/constants, <br> examples) and proven proper theorems (excl. automatically generated <br> ones) by simple analysis of the sources, without running the system.<br> <br> For Mizar/MML, my approach would be to look at tokens in .miz files and <br= > count:<br> <br> For definitions: "definition"<br> <br> For theorems: "theorem" and "scheme"<br> <br> <br> Does this sound reasonable? I am missing something? Any hints are <br> appreciated.<br> <br> <br> Best,<br> <br> Fabian Huch<br> <br> </blockquote></div> --00000000000022f36a0636d5f4b1--