6 ms·

Metamath Zero, a bootstrapping theorem prover

125 points by giomasce 7y ago

jkingdon2000 7y ago
For those who don't know much about computer-verified proofs, the way I'd sum it up is that there's a complexity crisis going on (similar to the "software crisis" which might not be completely solved but which has seen significant progress). And that Metamath Zero is one of the more promising projects out there aimed at this problem.
- lliiffee 7y ago
  Would you mind elaborating? I'd love to hear more.
  - digama0 7y ago
    Software gets more complicated, and so bugs become more common. Hardware gets faster, so speed pressures are reduced on software, so it gets more layered and hence slower; and also more complicated. More layers of abstraction means more things to get wrong, so correctness becomes a serious problem. The world is increasingly reliant on software, so correctness becomes a serious concern. That sums up the "software crisis" as it relates to correctness. Most theorem provers have been swept up in this. They are written in high level languages and frameworks made by people who paid no thought to verification and only slightly more than most to correctness. What's more, even some theorem prover languages have dubious correctness or semantics; Rust and Dafny are both languages that make a big deal about formal correctness but have no formal spec. (Rust is working on it.) Coq is not known to be consistent (the literature is full of "here is a proof that some subsystem of Coq has this and that property" but no one can handle the whole thing), not to mention that it has had a few soundness bugs in its history, one of which (Reals violate EM) wasn't even clearly a bug because no one knew what the model was supposed to be. Agda is a free for all as far as I can tell, and Isabelle has some strange thing with axiomatic typeclasses that takes them out of the HOL world. HOL Light is pretty decent metatheory-wise, and the logic at least was formalized inside itself, but the implementation has not, and OCaml's Obj.magic is still there, ready to cause inconsistency if you feel like using it. Lean has not had any soundness bugs to date, and the theory is well understood, but it is a massive C++ application and there are doubtless dozens of implementation bugs in there waiting to be found. None of the big theorem provers are really appropriate for trying to prove correct, because either it is not known what this even means or it's trivially false and we all try to pretend otherwise, or it's an intractable open question. These are the paragons of correctness in our world. Can we do better? What does it even mean to do better? This paper aims to find out.
    - stouset 7y ago
      Do we even know if it's possible to prove correctness of a theorem-prover, in a very general sense? At some point, that would imply that some theorem-prover would have to prove its own correctness (either by proving itself directly or by proving itself through a loop of theorem-provers). This seems intuitively like it start to run up against Gödel-style incompleteness problems.
      - im3w1l 7y ago
        Seems like the ideal would be a number of theorem provers each capable of verifying the next. And the first one simple enough to be verified with pen and paper
      - AgentOrange1234 7y ago
        Provers in the LCF tradition have tiny cores that avoid having to trust lots of code. There are also reflective provers that can admit self-verified extensions. One project, called Milawa, had several layers of this.
      - digama0 7y ago
        It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can define what a computer is, how it executes, what PA is, what a verifier is, and what it means for a program to verify theorems of PA. Then you can have a sequence of bytes (verifier B), and prove that they represent a program that verifies theorems of PA. 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.
dwheeler 7y ago
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 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 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 http://us.metamath.org/mpeuni/mmset.html
- h91wka 7y ago
  > Most verification systems work in terms of hours or days. What kind of verification does usually take hours? Just checked how long it takes to verify Raft using Coq and Verdi (pretty sizeable proof), and complete pipeline takes around 25 minutes (with Docker container creation, fetching dependencies, and what not). Verification of proof terms is a relatively easy task for a computer, as easy as type checking. Coming up with the proofs, on the other hand, that is hard.
  - digama0 7y ago
    The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4 and CakeML. You are right, verification is much faster than coming up with proofs, and that explains the majority of the disparity. But then why are we reinventing proofs so much? This is clearly needless work, and there are a thousand ways to solve the problem but even recognizing that it is a problem is difficult in certain circles.
loganfrederick 7y ago
The author, Mario Carniero, is both one of the top three smartest and nicest people I know (and many other Ohio State students where he did his undergrad would agree). Glad to see his research getting Hacker News recognition.
- alexgartrell 7y ago
  I went to high school with Logan and with Mario. Mario was in my AP Comp Sci class with Mrs. White. I remember being proud of my forays into encryption, concurrency, and network programming. And then I looked over and Mario had implemented a graphing calculator (as in, take "y = x^2 + 4x -10" and emit a graph) in the windows command prompt. Then, when that was boring, he started researching and implementing the graphics algorithms for drawing lines at various slopes with minimal distortion. And then, when that was boring, he made his graphing calculator support polar coordinates (something I understood only as "oops, my graphing calculator is misconfigured"). Also, he was ~12 years old (IIRC) having skipped a few grades. I've met a lot of smart people between Carnegie Mellon, Facebook Infrastructure, and the Linux Kernel community, but Mario's one of two or maybe three at the absolute top in terms of intellectual horsepower.
xvilka 7y ago
I recently learned about some limitations in both Coq and Lean theorem prover after watching the video by Kevin Buzzard on formalization of math in Lean. He did some claims about quotient support in Coq, so I just asked[1] Coq developers straightly. I recommend to read their discussion and explanations. [1] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871
raphlinus 7y ago
This is very cool work, and I'm happy to see it. I've been fascinated with Metamath for a very long time, finding its simplicity extremely appealing, and have also made a number of attempts (under the Ghilbert name) to fix the problems Mario so eloquently identifies. But I never quite got it to gel. It's clear Mario has the technical chops, and I hope this publication gets the MM family a little more academic respectability and notice.
dwheeler 7y ago
FYI, the current publicly-available code for Metamath Zero is here: https://github.com/digama0/mm0 https://github.com/digama0/mm0
digama0 7y ago
For those who are more into watching talks on YouTube than reading papers, and are interested in the low level hardware formalization aspect of this project, there is a recording of the ITP 2019 presentation here: "x86 verification from scratch" https://www.youtube.com/watch?v=7hAShC6K_vA https://www.youtube.com/watch?v=7hAShC6K_vA
dwheeler 7y ago
If you're interested in the main book on Metamath, it is "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler. You can get the hardcover here: http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/metamath-a-computer-language-for-mathematical-proofs/hardcover/product-24129769.html http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/m... Full disclosure: I'm one of the co-authors.
ncmncm 7y ago
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.
infogulch 7y ago
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.

125 points by giomasce 7y ago

jkingdon2000 7y ago

For those who don't know much about computer-verified proofs, the way I'd sum it up is that there's a complexity crisis going on (similar to the "software crisis" which might not be completely solved but which has seen significant progress). And that Metamath Zero is one of the more promising projects out there aimed at this problem.

lliiffee 7y ago
Would you mind elaborating? I'd love to hear more.
- digama0 7y ago
  Software gets more complicated, and so bugs become more common. Hardware gets faster, so speed pressures are reduced on software, so it gets more layered and hence slower; and also more complicated. More layers of abstraction means more things to get wrong, so correctness becomes a serious problem. The world is increasingly reliant on software, so correctness becomes a serious concern. That sums up the "software crisis" as it relates to correctness. Most theorem provers have been swept up in this. They are written in high level languages and frameworks made by people who paid no thought to verification and only slightly more than most to correctness. What's more, even some theorem prover languages have dubious correctness or semantics; Rust and Dafny are both languages that make a big deal about formal correctness but have no formal spec. (Rust is working on it.) Coq is not known to be consistent (the literature is full of "here is a proof that some subsystem of Coq has this and that property" but no one can handle the whole thing), not to mention that it has had a few soundness bugs in its history, one of which (Reals violate EM) wasn't even clearly a bug because no one knew what the model was supposed to be. Agda is a free for all as far as I can tell, and Isabelle has some strange thing with axiomatic typeclasses that takes them out of the HOL world. HOL Light is pretty decent metatheory-wise, and the logic at least was formalized inside itself, but the implementation has not, and OCaml's Obj.magic is still there, ready to cause inconsistency if you feel like using it. Lean has not had any soundness bugs to date, and the theory is well understood, but it is a massive C++ application and there are doubtless dozens of implementation bugs in there waiting to be found. None of the big theorem provers are really appropriate for trying to prove correct, because either it is not known what this even means or it's trivially false and we all try to pretend otherwise, or it's an intractable open question. These are the paragons of correctness in our world. Can we do better? What does it even mean to do better? This paper aims to find out.
  - stouset 7y ago
    Do we even know if it's possible to prove correctness of a theorem-prover, in a very general sense? At some point, that would imply that some theorem-prover would have to prove its own correctness (either by proving itself directly or by proving itself through a loop of theorem-provers). This seems intuitively like it start to run up against Gödel-style incompleteness problems.
    - im3w1l 7y ago
      Seems like the ideal would be a number of theorem provers each capable of verifying the next. And the first one simple enough to be verified with pen and paper
    - AgentOrange1234 7y ago
      Provers in the LCF tradition have tiny cores that avoid having to trust lots of code. There are also reflective provers that can admit self-verified extensions. One project, called Milawa, had several layers of this.
    - digama0 7y ago
      It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can define what a computer is, how it executes, what PA is, what a verifier is, and what it means for a program to verify theorems of PA. Then you can have a sequence of bytes (verifier B), and prove that they represent a program that verifies theorems of PA. 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.

dwheeler 7y ago

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 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 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 http://us.metamath.org/mpeuni/mmset.html

h91wka 7y ago
> Most verification systems work in terms of hours or days. What kind of verification does usually take hours? Just checked how long it takes to verify Raft using Coq and Verdi (pretty sizeable proof), and complete pipeline takes around 25 minutes (with Docker container creation, fetching dependencies, and what not). Verification of proof terms is a relatively easy task for a computer, as easy as type checking. Coming up with the proofs, on the other hand, that is hard.
- digama0 7y ago
  The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4 and CakeML. You are right, verification is much faster than coming up with proofs, and that explains the majority of the disparity. But then why are we reinventing proofs so much? This is clearly needless work, and there are a thousand ways to solve the problem but even recognizing that it is a problem is difficult in certain circles.

loganfrederick 7y ago

The author, Mario Carniero, is both one of the top three smartest and nicest people I know (and many other Ohio State students where he did his undergrad would agree). Glad to see his research getting Hacker News recognition.

alexgartrell 7y ago
I went to high school with Logan and with Mario. Mario was in my AP Comp Sci class with Mrs. White. I remember being proud of my forays into encryption, concurrency, and network programming. And then I looked over and Mario had implemented a graphing calculator (as in, take "y = x^2 + 4x -10" and emit a graph) in the windows command prompt. Then, when that was boring, he started researching and implementing the graphics algorithms for drawing lines at various slopes with minimal distortion. And then, when that was boring, he made his graphing calculator support polar coordinates (something I understood only as "oops, my graphing calculator is misconfigured"). Also, he was ~12 years old (IIRC) having skipped a few grades. I've met a lot of smart people between Carnegie Mellon, Facebook Infrastructure, and the Linux Kernel community, but Mario's one of two or maybe three at the absolute top in terms of intellectual horsepower.

xvilka 7y ago

I recently learned about some limitations in both Coq and Lean theorem prover after watching the video by Kevin Buzzard on formalization of math in Lean. He did some claims about quotient support in Coq, so I just asked[1] Coq developers straightly. I recommend to read their discussion and explanations. [1] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871

raphlinus 7y ago

This is very cool work, and I'm happy to see it. I've been fascinated with Metamath for a very long time, finding its simplicity extremely appealing, and have also made a number of attempts (under the Ghilbert name) to fix the problems Mario so eloquently identifies. But I never quite got it to gel. It's clear Mario has the technical chops, and I hope this publication gets the MM family a little more academic respectability and notice.

dwheeler 7y ago

FYI, the current publicly-available code for Metamath Zero is here: https://github.com/digama0/mm0 https://github.com/digama0/mm0

digama0 7y ago

For those who are more into watching talks on YouTube than reading papers, and are interested in the low level hardware formalization aspect of this project, there is a recording of the ITP 2019 presentation here: "x86 verification from scratch" https://www.youtube.com/watch?v=7hAShC6K_vA https://www.youtube.com/watch?v=7hAShC6K_vA

dwheeler 7y ago

If you're interested in the main book on Metamath, it is "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler. You can get the hardcover here: http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/metamath-a-computer-language-for-mathematical-proofs/hardcover/product-24129769.html http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/m... Full disclosure: I'm one of the co-authors.

ncmncm 7y ago

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.

infogulch 7y ago

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.