Metamath Zero, a bootstrapping theorem prover

I think it's 100% valid, indeed, the Metamath and/or Metamath Zero verifiers are verifying much more. I'm measuring time to verify ALL proofs of an entire system, including every theorem and lemma. The Coq measure you're quoting is the time to verify just a single proof with its lemmas. Coq is slower at verifying "a single proof of a theorem including all its lemmas" (though a complex one) than Metamath is at verifying "proofs of all theorems including all lemmas". To be fair, Coq is not designed to do this quickly, so that should not be surprising.

> Also proofs in Coq are typically structured and are pretty complex because of all the automation, while metamath proofs look like core dumps :)

You're showing the "compressed" format. That's simply its internal storage format, which is normally optimized to reduce storage space. Humans do not need to work in that format (and usually don't). Normally for final display the proofs are shown in HTML, for example:

> http://us.metamath.org/mpeuni/f1o2ndf1.html

Note that in the HTML display every step is justified by a hyperlink; you can click on the hyperlink to see the justification (recursively). For example, step 3 uses the justification "syl"; if you click on "syl" you'll find that it says that if ⊢ (𝜑 → 𝜓) and ⊢ (𝜓 → 𝜒) then ⊢ (𝜑 → 𝜒). The theorem syl is itself proved, and you can click on its links to see how it derives all the way back to definitions and axioms.

If you want to see just simple text, you can see the proof in text format by installing "metamath" and running this:

> metamath 'read set.mm' 'show proof f1o2ndf1'

As far as "structured" goes, I think structuring proofs is necessary for any system. A complex proof in Metamath is typically built up from axioms, previous proofs, and lemmas as needed. I think that's necessary for any math verification system.

I agree that calling it "one proof" is a mischaracterization, but comparing all of Raft to all of set.mm is probably about right. I would guess set.mm is 10-100 times larger than Raft in terms of number and complexity of actual proof content, but it checks in a fraction of the time, in part because of that "core dump". You might think it ugly, but have you ever looked at a .vo file? The difference is metamath checks its 'cache' in to version control.

There's no RSI in working with Metamath. What I mean is that the workflow is largely dependent on me knowing what I want to prove and roughly how I want to prove it, rather than Metamath chewing CPU.

What have you proven? Well, verifier A (using PA) proves that "verifier B proves theorems of PA". That means that "if B says phi is true, PA |- phi". We would have a hard time actually running verifier B inside the logic of verifier A (that entails running all the steps of the computation B does as theorem applications inside verifier A), but even if we did, we would obtain a proof of "PA |- phi". If we assume A correctly implements PA, then that means PA |- "PA |- phi". In general, this is the best we can do. If we assume further that PA is a sound axiom system, i.e. when it proves facts about numbers then we won't find concrete counterexamples, then this strengthens to PA |- phi and then to phi itself, so we've learned that phi is true.

The plan is to prove inside verifier A (that is, MM0) the statement "Here is a sequence of bytes. It is an executable that when executed has the property that if it succeeds on input "T |- phi", then T |- phi." The bootstrapping part is that the sequence of bytes in question is in fact the code of verifier A. In order to support statements of the form "here is a sequence of bytes", the verifier also has the ability to output bytes as part of its operation (it's not just a yes/no oracle), and assert facts about the encoding of those bytes in the logic.

Regarding CakeML, I'm really impressed by the work they've done, and I think they more than anyone else are leading the charge on getting verification as pervasive as possible at every level (especially the low levels, where historically it has been difficult to get past the closed source barrier). That said, I think they are not doing an optimal job at being a bootstrap. They have a system that does that and so much more that if you just want a bootstrap it's way overkill. And you pay for that overkill - 14 hour compilation per target (see https://cakeml.org/regression.cgi).

There is a second proof checker for MM0 in mm0-hs: https://github.com/digama0/mm0/tree/master/mm0-hs , which has a few more features like the MM1 server mode to give interactive feedback, as well as a verifier that reads a text version of the proof file (not described in the paper, the .mmu format).

The footnotes are supposed to be links to the github repo but I got the versions mixed up and submitted a partially anonymized version to arXiv.