The specification for metamath checking in general is given in the Metamath
Book: https://us.metamath.org/downloads/metamath.pdf
The proof blocks are written in "compressed proof format", which is
specified in Appendix B of the metamath book. (Although, metamath-exe, mmj2
and metamath-knife
Greetings,
tried to find a definition for proof generation from a list of
statements/expressions+justifications+dependencies.
mmj2, metamath.exe, yamma, metamath-lamp, all generate valid proof
statements, but could not find a spec on the requirements that they
implement.
Is a spec available,
