LaTeX rendering

Skip to first unread message


Feb 12, 2022, 6:26:04 AMFeb 12
to Metamath

my first post to this list.

I am trying Metamath.  I have a couple of questions about basic whereabouts.

1.  is there a way to customize the .tex file you get with a command like :
show proof tfr2 /all /lemmon /tex .
I am getting a .tex file which gives a number of errors when I try to pdflatex it (mostly missing labels)

2. is there a way to output proof in a tree like display (say,  sequent calculi / natural deduction style)?

3. is there  some kind of IDE for Metamath?

Sorry if I am asking questions which have been already asked and answered.

Thierry Arnoux

Feb 12, 2022, 10:42:05 AMFeb 12
to, mario

Hi Mario,

Welcome to the list!

The proofs on the Metamath web page are actually displayed in a tree like way, if you look at the identation:

Take for example:

You'll notice the final statement (step 7) has an indentation of "1". The statements it refers to (steps 5 and 6) both have an indentation of "2", and so on. It's not strictly a tree, as some tree leafs may be referred to from different branches (here, step 1 is used both in steps 2 and 6)

You've already asked about MMJ2, that's the IDE of choice.

I've built a Metamath plug-in for Eclipse, but I've also had feedback it's not easy to install.

I'm sorry I've not used the Latex output, I can't help with that question..


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
To view this discussion on the web visit


Feb 15, 2022, 12:10:11 PMFeb 15
to Metamath
I have been able to install MMJ2.
Thanks Best wishes
Reply all
Reply to author
0 new messages