Metamath Zero, a bootstrapping theorem prover

This is really interesting work.

I like this quote: "sometimes, performance is about more than just getting work done a little faster. When something takes a lot less time, it changes the way you interact with the computer. A process that takes hours goes on the nightly build server; a process that takes minutes might be a compile that runs on your local machine; a process that takes seconds is a progress bar; and a process that takes milliseconds might happen in an editor between keystrokes."

Most verification systems work in terms of hours or days. Changing the order of magnitude means that verification can happen constantly.

The paper mentions that it verifies Metamath set.mm, one of the largest bodies of formalized mathematics, in less than 1 second. Here's some more info for the curious:

* My Gource visualization of the development of set.mm over time: https://www.youtube.com/watch?v=XC1g8FmFcUU ↗

* My video "Metamath Proof Explorer: A Modern Principia Mathematica" (which gives overall background/context of Metamath): https://www.youtube.com/watch?v=8WH4Rd4UKGE ↗

* Metamath Proof Explorer (MPE) aka "set.mm" - the home page for this body of formalized mathematics: http://us.metamath.org/mpeuni/mmset.html ↗

There is something about the process of getting optimal performance in a system that tells you whether you are moving in the right direction.

The universe speaks to you directly, in the count of cycles consumed, albeit somewhat garbled by incidentals of the CPU implementation and, particularly, caching. But the implementers of the CPU are chasing correctness and optimal performance too, so are always working toward the same goal, at their level. Even the caching, when you get down to counting cycles, reveals truths about your computation.

So, a proof system that is several orders of magnitude faster than another is that much closer to ultimate truth, because there is simply less room for significant errors of comprehension to hide in.

This is the reason that efficient languages and runtime systems are, and will always be, important. Garbage collection is an evil because it muddies the water, corrupting the connection between what your program says and what actually happens in the machine.

It seems that metamath's representation is a basic primitive for encoding maths at a syntactic level. It uses simple rules to recursively apply syntactical substitution transformations in order to build up a kind of complete, ostensibly true statement. A statement that is encoded in a way that a small proven-true statement checker can ~linearly (!) follow along the statement of the proof and find it logically sound. It seems weird to me that it's even possible to cross the boundary from syntactic representation to semantic meaning so seamlessly.