The Incredible Proof Machine (pdf) is a visual means of doing proofs.

The Incredible Proof Machine can also be extended to do custom logics (Section 2.7 Custom logics).

Metamath has thousands of axioms and proven theorems. (set.mm)

It appears that Metamath and Incredible Proof Machine can coexist (ref) when the axiom (blocks) are created by hand.

enter image description here

Could the Incredible Proof Machine work automatically with Metamath if rules of Metamath can be automatically translated into Incredible Proof Machine custom logic blocks?

What an acceptable answer would need to address.

This seems like a term rewriting problem where the input term is a Metamath proof and the output term is a custom logic block.

The reason for the questions is that there may be something like free and bound variables that causes problems when rewriting the term that can not be solved with a one way rewrite of the term.

If that is the case then would a bidirectional interface (translator) work where Metamath updates knowledge to the translator?

This question is not asking for am implementation but something that explains why this can not be done or gives a high level overview of what would be needed.

I am aware that the Incredible Proof Machine has unification built-in. Since I work with Prolog daily that would not be an issue if needed.

Note I have not used Metamath yet but this introduction video (ref) is pretty clear and have only use the Incredible Proof Machine to do some of the examples.

A comment question expand to help clarify the question.

If I understand correctly, you mean to ask how an interactive GUI can be added to Metamath? Trebor

I like IPM because

  • it is easy to use (mouse vs memorizing exact syntax)

    • Metamath syntax (ref) - Has to be exact. Some of the editors make this nearly inconsequential. (YouTube)
    • With IPM it is a visual WSIWYG. If you like Visio you will feel right at home. IMO there is room for a bit of improvement but the essentials are there.

      Therefore we built an interactive theorem prover that allows the students to start conducting proofs immediately and without learning syntax first. With The Incredible Proof Machine (http://incredible.pm/) the student just drags blocks – which represent assumptions, proof rules and conclusions – onto a canvas and wires them up, using only the mouse or a touch interface.

  • Errors

    • Metamath - Error messages. (YouTube)
    • IPM shows errors

enter image description here

enter image description here

  • Customized with logics

    • See paper Section 2.7 Custom Logics
  • Indication of introduction or discharge

    • Notice in the image ∀ is on the left or right.

    enter image description here

  • Indication of local hypotheses

    • Notice that certain ports are not on the left or right but above.

      enter image description here

      • These blocks can be extended.

      enter image description here

Potential issues with IPM

  • Searching for proofs
    • Metamath has a nice search feature. (YouTube)
    • AFAIK there is no built-in means for searching for proofs. There are custom blocks (paper Section 2.6)
  • $\begingroup$ As the question is currently written, I view it as a question combining X and Y where X and Y don't interact in a useful way. Could you explain how this question is more than asking about Metamath and the Incredible Proof Machine separately? $\endgroup$
    – Trebor
    Commented Feb 19, 2022 at 14:26
  • $\begingroup$ If I understand correctly, you mean to ask how an interactive GUI can be added to Metamath? $\endgroup$
    – Trebor
    Commented Feb 19, 2022 at 14:45
  • $\begingroup$ Putting these in the question (instead of a comment) improves your question :-) $\endgroup$
    – Trebor
    Commented Feb 19, 2022 at 14:52
  • 1
    $\begingroup$ That's a long question! It seems that the IPM does handle free/bound variables, as in session 6. It seems that the IPM assumes all variables to be distinct. So my feeling is that it might be possible to use the IPM with a custom logic to encode set.mm. $\endgroup$ Commented Feb 19, 2022 at 16:08
  • 1
    $\begingroup$ In the IPM source, there are YAML files encoding the logic blocks and YAML files encoding the challenges. The former would have to be generated from the theorem statements in the database, and the latter, for a given proof, with the hypothesis and final statement, maybe allowing only theorems available/required for the proof. Might be a fun project :-) $\endgroup$ Commented Feb 19, 2022 at 16:09


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.