metamathProofAssistantMetadata

NOTE: This is proposed.

Here is my latest conception, a format for "batch" proof assistant input that would be input inside a .mm file!

The idea takes advantage of the "<MM>" metadata comment content used with "<MODULE>", as implemented recently:

    $( <MM> <MODULE> <ID>LOGICB</ID> <PREREQ> </PREREQ> </MODULE> </MM> $)

The idea would look like this in practice in the optimal case where the user has entered all information necessary to specify a proof – all step labels and hypothesis references:

    ${
      a1i.1 $e |- ph $.
      a1i   $p |- ( ps -> ph ) 
            $=
        wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.
        $( [?] $) $( [24-Sep-05] $)
      $( <MM> <PROOF>
         1:     a1i.1  |- ph                       $.
         2:     ax-1   |- ( ph -> ( ps -> ph ) )   $.
         3:1,2  ax-mp  |- ( ps -> ph )             $.
         </PROOF> </MM>
      $)
    $}

Each step begins with a number delimited by a ":", with hypothesis references (perhaps optional?, depending on the skill of the proof assistant), followed by a label (also perhaps, optional), followed by a formula, followed by "$.".

The way I see it working is that a student wishing to do proofs would enter just a "?" proof step in the "$=" section of a theorem, and then follow the theorem statement with a "$( <MM> <PROOF> …" comment. Then, when either proof assistant or verify proof is called upon AND the proof is incomplete BUT is followed by a PROOF metadata comment, the enhanced proof assistant would attempt to construct a real Metamath proof.

In theory the student might not know the step labels to input, but the proof assistant might be able to derive them, assuming the formulas are correct. That would be the primary benefit of using this format – not having to memorize 6000 different labels, as we have in set.mm alone. It would be a tremendous programming challenge also. But in mmj2, given that each statement is parsed, the top level syntax label is known, and that limits the search (if top level syntax label is "wi" then we're looking for a label which also has a "wi" at the top level, or has just a variable of the same type, (i.e. as with ax-mp.)

The experiment above demonstates the concept and shows how Metamath.exe stored the real proof, leaving the metadata proof comment intact. Of course, I had to enter the proof the old way…

Obviously, this is nothing fancy or especially brilliant. But it is a first step towards a friendlier GUI proof assistant. Once a batch interface and algorithm has been tested, the way would be clear to running a proof assistant program in server mode and responding to input.

The nice thing also, is that now that the "<MM>" comment tag has been staked out – a precedent set – the way is open to using that same idea for Proof Assistant, as well as other things that may not presently fit into the scheme for metamath.exe but may be add-ons used elsewhere, thus enhancing Metamath's usefulness.

--ocat 24-Sep-2005