Turn proofs into some other format

[nomeata]

possible outputs that would be nice are:

• human readable text (in the style of EasyProve)
• proof trees (using LaTeX and inference rules)
• Isabelle theories
• Coq theories

[gattschardo]

If we consider Isabelle or Coq theories, OpenTheory should be worth a look, since it's developed as a proof exchange tool (only between the HOL family of provers, for now). Isabelle/HOL does have "read" support though, so we would get that for free!

[gattschardo]

So, OpenTheory works by putting assumption terms in a stack-based custom VM (specs are here) and then writing a program for that VM that turns them into the conclusion terms, i.e. that program is the proof. Regardless of how useful having that format is, this sounds

• quite similar to our own approach
• like a fun thing to implement

I consider doing this when I'm done with the rule export!