Easier Typesetting of Proof Trees

A Frontend to the LaTeX Bussproofs package with accompanying VIM Plugin

Recently I wanted to typeset a quite large proof tree in LaTeX using the Bussproofs package. As usual, I didn’t do this by hand editing text files, but by using the convenient LyXproofs library for doing this in a what-you-see-is-what-you-mean manner within LyX. Still, I didn’t quite like the experience; the nice math support of LyX came at the cost of the tree no longer fitting into the window; also, I didn’t want to go the step back to plain LaTeX editing.

The solution I came up with is a new, lisp-like syntax for specifying proof trees along with a rendering engine translating trees specified in this syntax to LaTeX, either for including into existing files or for outputting a standalone file suitable for direct compilation.