Disclaimer: I’m just learning about proof verification systems. Bear with me on this journey :)
Recently, I’ve stumbled over Metamath. Metamath is a proof verification system. It allows you to formalize mathematical proofs and checks that everything is sound and consistent. Proof verification systems are related to automated proof solvers that try to go one step further. They want to automate the holy grail of the mother of all sciences. There are many interesting systems like Isabelle and Coq. However, they are quite complex. Metamath’s formal language, on the other hand, is quite simple, and there even is even a Python verifier for Metamath proofs with just 300 LoC.
The freely available Metamath book both introduces the languages as well as explains the basics behind it in a very understandable way. I can highly recommend it, especially chapter 4, which explains the details for the language and how it works.
The Metamath language
Here is an example from the book that establishes the well-known modus ponens:
If “A implies B” and A holds, then B holds. In Metamath, it looks like this (taken and abridged from the Metamath book):
$( Declare the constant symbols we will use $)
$c -> ( ) wff |- $.
$( Declare the metavariables we will use $)
$v P Q $.
$( Specify properties of the metavariables $)
wp $f wff P $.
wq $f wff Q $.
$( Define composite "wff"$)
wim $a wff ( P -> Q ) $.
$( Define the modus ponens inference rule $)
min $e |- P $.
maj $e |- ( P -> Q ) $.
mp $a |- Q $.
What happens here?
We define a couple of constants:
wfffor a well-formed formula;
|-for the turnstile symbol, which is used to say that something is true. For example,
I know A is true.
->for a logical implication. For example,
A implies B.
)are needed for building composite formulas.
Then, we define two variables
Q that we use to establish the modus pones rule.
$f wff P $. and
$f wff Q $., we declare that these variables both have to be well-formed formulas. We also want to allow composite expressions like
(P -> Q) to be well-formed when
Q are, so we specify
$a wff ( P -> Q ) $.. Now we are ready to establish the modus ponens:
$e |- P $.is the minor premise that has to be true already.
$e |- ( P -> Q ) $.is the logical implication that Q follows from P.
$a |- Q $.is the assertion that then Q has to be true.
Now this is true to us and obvious. However, for Metamath, this is just a new substitution rule: if it finds
|- A and
|- (A -> B) in its set of hypotheses, it can apply the modus ponens rule and it can infer P:=A and Q:=B, substitute and add
|- B to the set of hypotheses. There is no understanding of what this actually means.
The acute reader will notice that the composite wff
(P -> Q) is also introduced as such assertion. Indeed, it is no different for Metamath, only for us interpreting it: modus ponens is about an axiom of logic, whereas the composite wff is “just” a definition of the allowed syntax.
Fascination spawns curiosity
I’ve left out an actual proof written in Metamath. Have a look at the book if you’re in interested in learning more about it! I hope what you have seen is sufficient for the main insight:
The fascinating bit about proof verification systems is that they don’t actually understand proofs, maths or the logic behind them. You could express the simplest or most complex idea in them, and they would verify either by simply applying repeated substitutions on symbols that are inherently devoid of meaning. As with every piece of information that is stored and processed in a computer, the users provide meaning to it by interpreting it using external devices. It is particularly blatant in this case though. This leads to one interesting conclusion: “Out of nothingness, we can create everything”. If we only give it the right meaning.
Most proof solvers and verification systems use custom formal languages. I wonder:
Q.1: Can we use a normal programming language to create domain-specific languages or frameworks that describes and verifies proofs in itself?
I think the answer to this is yes. There are probably different ways of using programming languages for this. I’m not referring to writing a parser for a formal language in a programming language, but rather to using the language and its compiler/interpreter directly to verify proofs. Regular proof verifiers with external formal language lie outside the boundary of this question. It is about how we can reinterpret a regular programming language (think Python or Dart) to embed a metalanguage in it (think Metamath).
If we can use a web language as “proof carrier”, we could maybe create an intuitive editor for proofs and mathematical theories.
Q.2: Can proof verification become a UX problem? Can we make it truly fun and intuitive to use?
Proof verification and automation tools could provide important value to education if they were accessible enough. On the one hand, they allow one to easily check one’s understanding. On the other hand, a more formal representation could make it possible to store, search and reuse mathematical knowledge more easily.
Q.3: Can we help people self-educate by providing tools that help understanding through rigor?
Last but not least, what is logic? Is it self-evident, do we understand it?, or is it just a consequence of the environment we perceive? If so, what if our environment was logic?
Q.4: Can we use Metamath to bootstrap reasoning for AIs and better understand logic itself?
I cannot provide answers to any of these questions yet, but it’s fun to ask them nonetheless.