proof objects for mizar: already available?

There are two senses in which mizar already has proof objects, despite
appearances to the contrary.  However, both senses are unsatisfactory.

(a) One could argue that there's no difference between "proof object"
     and "mizar article", because the proof is contained right there in
     a mizar text.  That is, of course, correct.  But this is
     unsatisfactory because one must have the mizar infrastructure to
     work with the proof object.  Of course, with some mathematical and
     logical background one can read a mizar text in the same sense
     that one reads a book, but doing anything interesting requires the
     mizar tools.  (Moreover, as we all know, in general, owing to the
     evolving syntax and library, an article might even require a
     specific *version* of the mizar toolset.)  But proof objects
     shouldn't really depend on the version of mizar that was used to
     generate them.  They shouldn't even depend on mizar itself.  One
     should be able to inspect and work with a mizar object, in
     principle, independently of mizar.

(b) Proofs objects are already available, in some sense, for mizar
     proofs.  They do not give precisely what is wanted from the
     concept of proof object, though:

     * They are not always available.  With the current transformation
       into a vanilla first-order format, and with current ATPs, for
       less than half of mizar theorems from the library do we have
       deductions.  This is clearly an important result for the
       community, but not having deductions is a serious shortcoming.
       We want proof objects for all mizar proofs.

     * The calculi of the proofs that are found this way depend on the
       theorem prover employed.  One finds proofs in the superposition
       calculi, resolution calculi... The plurality of proof calculi is
       welcome -- we want to view mizar proof objects through various
       formal lenses -- but none of these is satisfactory because none
       is a natural deduction proof in the style of mizar.  (To some
       extent this problem can be overcome: an ATP could either do
       search in a natural deduction setting, or emit natural
       deductions by translating whatever calculus it uses into natural
       deduction.  But proof search in natural deduction is generally
       not as efficient as search in other calculi.  And the
       translation from other calculi to a natural deduction is not
       always clear.)  What is wanted from proof objects for mizar is a
       sort of natural deduction proof that adheres more or less to the
       mizar format, but which brings out all logical details.  It is
       unpleasant and awkward to switch from natural deduction-style
       mizar proofs to unnatural resolution deductions.

     * There is no assurance that the proofs discovered by an ATP
       thanks to Josef's translations are the same as the mizar proofs
       with which one started.  Genuinely new proofs can be (and are)
       discovered.  An ATP might exploit a premise or combination of
       premises in an unusual way that diverges from the input mizar
       proof.  An even when the ATP-discovered proof is more or less
       congruent to the mizar proof from which it came, because it is
       expressed in a different formal calculus there might be some
       uncertainty about whether we are looking at the same proof.

     * By diverging from mizar's natural deduction format, one loses
       the ability to carry out experiments and investigations that
       require that one works with natural deductions.  Thus, one might
       wish to investigate the notion of obviousness.  One might ask,
       for example, what instances of which universal formulas were
       used to carry out a particular by step.  One might wish to carry
       out certain transformations of the the deduction (e.g., rewrite
       a natural deduction by represent applications of definitions as
       rules of inference, rather than as applications of the rule of
       modus ponens).

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/