Metamath Zero, a bootstrapping theorem prover
This is really interesting work.<p>I like this quote: &quot;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.&quot;<p>Most verification systems work in terms of hours or days.  Changing the order of magnitude means that verification can happen constantly.<p>The paper mentions that it verifies Metamath set.mm, one of the largest bodies of formalized mathematics, in less than 1 second.  Here&#x27;s some more info for the curious:<p>* My Gource visualization of the development of set.mm over time: <a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=XC1g8FmFcUU" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=XC1g8FmFcUU</a><p>* My video &quot;Metamath Proof Explorer: A Modern Principia Mathematica&quot; (which gives overall background&#x2F;context of Metamath): <a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=8WH4Rd4UKGE" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=8WH4Rd4UKGE</a><p>* Metamath Proof Explorer (MPE) aka &quot;set.mm&quot; - the home page for this body of formalized mathematics: <a href="http:&#x2F;&#x2F;us.metamath.org&#x2F;mpeuni&#x2F;mmset.html" rel="nofollow">http:&#x2F;&#x2F;us.metamath.org&#x2F;mpeuni&#x2F;mmset.html</a>