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 generate proofs which are byte identical because they also implement a specific sorting / packing strategy taking advantage of some flexibility in the specification to produce more compact proofs. If you want to implement this you will have to read the code of one of these systems.) On Sun, Feb 11, 2024 at 9:42 PM Jorge Agra <[email protected]> wrote: > 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, even if informally? > > Best regards. > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/e3b5b65e-1c4c-4f88-9ae1-a69e74b0ca0cn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/e3b5b65e-1c4c-4f88-9ae1-a69e74b0ca0cn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsGJbyDc208%2B4OgCf8Eci0DrqJMbD0aMWsa%3D%2B3WOHWyOw%40mail.gmail.com.
