Re: Size of Mizar/MML
Fabian Huch huch _AT_ in.tum.de <[email protected]> Thu, 5 Jun 2025 19:22:52 +0200
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
This is a multi-part message in MIME format.
--------------P0XxsLkXHU5iuvJJcCMJwBO0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
On 6/5/25 18:53, Alex Nelson thmprover _AT_ gmail.com wrote:
> Hello,
>
> I am not sure what you mean by "autogenerated theorems", I do not
> think Mizar has such a feature.
Yes, this part of my project description applies to other ITPs.
>
> 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.
That is a great suggestion. Thank you!
>
> 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).
Certainly; my goal is merely an approximation. For uniformity, I will
count the comments -- for some ITPs it is not feasible to spearate them.
>
> 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.
I think it is reasonable to include them (but hardly matters for the
approximation).
Best,
Fabian
--------------P0XxsLkXHU5iuvJJcCMJwBO0
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: 8bit
<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">On 6/5/25 18:53, Alex Nelson thmprover
_AT_ gmail.com wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAA+9CX0FC31tDYSBjEQwo0jP8uwXEMiXT-epoqf1p1cAtHBY3w@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">Hello,<br>
<br>
I am not sure what you mean by "autogenerated theorems", I do
not think Mizar has such a feature.<br>
</div>
</blockquote>
Yes, this part of my project description applies to other ITPs.<br>
<blockquote type="cite"
cite="mid:CAA+9CX0FC31tDYSBjEQwo0jP8uwXEMiXT-epoqf1p1cAtHBY3w@mail.gmail.com">
<div dir="ltr"><br>
Two bits of advice spring to mind:<br>
<br>
<b>Advice 1: Use the abstract files.</b> 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 (<a
href="https://mizar.uwb.edu.pl/version/current/html/"
moz-do-not-send="true" class="moz-txt-link-freetext">https://mizar.uwb.edu.pl/version/current/html/</a>).<br>
<br>
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...).<br>
<br>
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.<br>
</div>
</blockquote>
That is a great suggestion. Thank you!<br>
<blockquote type="cite"
cite="mid:CAA+9CX0FC31tDYSBjEQwo0jP8uwXEMiXT-epoqf1p1cAtHBY3w@mail.gmail.com">
<div dir="ltr"><br>
These numbers are for mizar-8.1.15_5.94.1493 which is the latest
version of the MML. <br>
<br>
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).<br>
</div>
</blockquote>
Certainly; my goal is merely an approximation. For uniformity, I
will count the comments -- for some ITPs it is not feasible to
spearate them.<br>
<blockquote type="cite"
cite="mid:CAA+9CX0FC31tDYSBjEQwo0jP8uwXEMiXT-epoqf1p1cAtHBY3w@mail.gmail.com">
<div dir="ltr"><br>
I am certain there is a cleverer way to do a more accurate count
of these things.<br>
<div>
<div><br>
<b>Advice 2: About axioms.</b> 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>
</div>
</div>
</div>
</blockquote>
<p>I think it is reasonable to include them (but hardly matters for
the approximation).</p>
<p><br>
</p>
<p>Best,</p>
<p>Fabian</p>
</body>
</html>
--------------P0XxsLkXHU5iuvJJcCMJwBO0--