[Hol-info] useful HOL statistics to show the amount of proof work?

[Lu Z. <lu...@cs...>]

Hi,

First, please forgive me if this question is too silly. I had this 
question when I talked to a colleague, who has no idea about theorem 
proving at all, about the amount of proof work that can be involved in 
solving a problem. How to evaluate the amount of proof work that HOL 
does? What are the statistics that I can use, and how to get them in HOL?

Before I speak of HOL, an example I think can help illustrate my 
question is that SMT solvers often say "the number of clauses" that can 
be solved. When someone who does not know an SMT solver hear that a 
solver could solve 200 clauses 15 years ago but now can solve 2,000,000 
clauses, she knows that there is big difference, because there is a huge 
gap between these two numbers: 200 vs 2,000,000. The numbers make her 
feel there is a difference.

Now, come to HOL. What number should I use to convey the amount of work 
in a proof? Or something else if not a number. Some examples popping out 
in my mind are: the number of tactics used (may be silly), the number of 
rewriting steps, or ...

Thanks.
Lu