Re: [mizar] Re: what's new in mizar?

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Fri, 14 Dec 2007, Jesse Alama wrote:
>
>> Excellent!  I'm glad to hear that the checker can now handle a wider
>> class of "obvious" inferences.  Are there cases in the MML where this
>> really arises?  In other words, if, say, trivdemo is run on the old MML,
>> do we find any cases where the text could be simplified?
>
> Indeed, there were quite a few such cases where 'trivdemo' detected
> proofs that could be simplified to a straightforward justification
> (see. RELAT_1:9 for example). But adjusting the library according to
> what 'relinfer' reports is even more important.

Do you have some numbers here?  It would be interesting to know, for
example, how many lines from the MML can now be safely deleted thanks to
the improved checker.

Jesse

-- 
Jesse Alama (alama@stanford.edu)