We're working on the infrastructure to make such a thing easier, but the project does not currently have a leader: https://github.com/treenotation/jtree/issues/83
https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...
When you combine this with the fact that these ML programs are not proofs but proof scripts, that perform a lot of "unnecessary" work like searching for a proof rather than just going straight for the answer, it suddenly begins to make sense why these systems take on the order of hours to days to check their whole libraries.
Coq and Lean are somewhere in the middle, because they have proof terms, but the logic itself still requires some unbounded computations. Checking a proof here is often fast, unless you make too much use of computation in the logic. But people often don't care about proof terms, and still store the proof scripts, which are as slow as ever.
Metamath is in this setting somewhat unique in eschewing proof scripts altogether, or more accurately, inlining proof scripts immediately on the author's machine. The resulting proofs are often comparatively long and verbose, but I would argue this is only a display matter, since all the other provers are doing the same thing, they just aren't showing it.
First, jtree is a bit orthogonal as that’s just an implementation. The github issue is there for convenience, it’s arbitrary.
The reason for tree notation is that it’s a level up from binary. Binary notation does not give you the ability to define new symbols. Tree notation is a 2d binary. You can define new abstractions. It is a bridge between human and machine languages.
Take any concept in mathematics, such as “derivative”. How would you define such a concept, starting only from 1s and 0s? Tree notation gives you a method to do that, in a way that’s not only efficient (noiseless), but also gives you practical tools, like complexity counting.