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