Re: [mizar] Size of Mizar/MML

[Fabian Huch <huch@in.tum.de>]

Hi Artur and Adam,

On 6/5/25 21:14, Artur Kornilowicz arturk _AT_ math.uwb.edu.pl wrote:
> Hello,
>
>
> Fabian, if you are interested in more detailed statistics of MML, I 
> suggest using some XML files generated during the work of the Mizar 
> verifier.
> If you like, I can give you the files and teach you what information 
> is in the files.
> Having the files you can count, for example, how many times the given 
> notion is used or how many existential quantifier is used, or …
>
> You do not have to install the Mizar system; you can download the 
> files and prepare some simple software to process them.
>
>
> What do you think?
Thank you for the offer. For this overview, I want to apply a common 
methodology to many different ITP systems so I am restricting myself to 
simple analysis of the source code.

For this, counting tokens in .miz or .abs files is sufficient. I also do 
take into account the reported statistics from mmlquery.mizar.org (like 
Adam suggested as well).

In any case, for Mizar these statistics agree so I think this is sufficient.

This is not the case for some other provers (where e.g. automatically 
generated theorems would be counted as well in the "officially" reported 
statistics).


Best,

Fabian