Contrasting metamath

[David A. Wheeler]

I am trying to find a short way of contrasting metamath with other math formalization tools like HOL light, Coq, Mizar, and so on, focusing on how explicit the steps are.

My try:
Most other math fomalization tools (such as HOL and Coq) have users explain to a computer how to re-discover the individual formal steps of a proof. In contrast, Metamath records and verifies every actual step.

Plausible? How could that be improved? It's difficult to capture the contrast in just a few words. I'm not trying to say that the other tools are awful, I am just trying to contrast their approaches.

--- David A.Wheeler

[fl]

My try:
Most other math fomalization tools (such as HOL and Coq) have users explain to a computer how to re-discover the individual formal steps of a proof. In contrast, Metamath records and verifies every actual step.

Plausible? How could that be improved? It's difficult to capture the contrast in just a few words. I'm not trying to say that the other tools are awful, I am just trying to contrast their approaches.

The other systems have algorithms to try several plausible inference rules and simply return that one of them

matches your goal formula but not which one. Metamath checks that the inference rules proposed by the user

matches the formula.

--

FL

 

[Norman Megill]

I tried to capture the idea graphically in the 4th slide of my talk
http://us.metamath.org/downloads/ihp2014mm.pdf (although in the past
couple of years the sophistication coordinate for the Metamath point has
been increasing, making the contrast less dramatic). The idea for this
slide is not completely original: in an early version of Freek's "The
Seventeen Provers of the World" he had a visually similar figure that
labeled the points, and I was amused at how Metamath stood out in sharp
contrast to the others. Unfortunately he decided to leave this out of
the published version - I think he replaced it with a feature chart on
p. 11 - and I don't remember how he labeled the abscissa and ordinate.

The first few slides of some of Mario's slide presentations that
introduce Metamath may also suggest ideas. These are linked at
http://us2.metamath.org:88/other.html

Norm

[David A. Wheeler]

On August 5, 2016 8:29:45 AM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>I tried to capture the idea graphically in the 4th slide of my talk
>http://us.metamath.org/downloads/ihp2014mm.pdf (although in the past
>couple of years the sophistication coordinate for the Metamath point
>has
>been increasing, making the contrast less dramatic).

Yes, I know about that chart. I don't think it's *wrong*, but I think that chart provides limited help for people unused to these tools. In particular, it doesn't explain understand why that is so... or why you might want one or the other. And as you noted, there are increasingly automated tools, which makes understanding the chart even trickier.

I like FL's summary... that's kind of where I was going. Metamath/Ghilbert/etc really take a different approach from HOL/Coq/etc., and I am trying to very briefly explain the difference in mindset. It really is different, and I think it's a little hard to explain to someone who's never seen the difference.

>The first few slides of some of Mario's slide presentations that
>introduce Metamath may also suggest ideas. These are linked at
>http://us2.metamath.org:88/other.html

Excellent. I will definitely take a look. Thank you.


--- David A.Wheeler

[Mario Carneiro]

On Fri, Aug 5, 2016 at 2:34 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On August 5, 2016 8:29:45 AM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>I tried to capture the idea graphically in the 4th slide of my talk
>http://us.metamath.org/downloads/ihp2014mm.pdf (although in the past
>couple of years the sophistication coordinate for the Metamath point
>has
>been increasing, making the contrast less dramatic).

Yes, I know about that chart.  I don't think it's *wrong*, but I think that chart provides limited help for people unused to these tools. In particular, it doesn't explain understand why that is so... or why you might want one or the other.  And as you noted, there are increasingly automated tools, which makes understanding the chart even trickier.

I will point out that unlike many (but not all) of "the others", Metamath has basically set its original specification in stone, and the increasing sophistication is not with respect to the language itself, but rather the tooling environment that surrounds it. For example, a proof script for today's Mizar will not work with yesterday's Mizar or tomorrow's Mizar, and there are no mechanisms for extracting "the proof" from the script (they don't even really have such a concept), so the trusted code base changes with each version. This is exactly what we want to avoid. (In fairness, HOL Light and maybe Isabelle has a similar approach to a static core, although Coq I think goes through periodic changes to the kernel and Lean is not stable.)

Mario

[David A. Wheeler]

Mario:

>I will point out that unlike many (but not all) of "the others",
>Metamath
>has basically set its original specification in stone, and the
>increasing
>sophistication is not with respect to the language itself, but rather
>the
>tooling environment that surrounds it. For example, a proof script for
>today's Mizar will not work with yesterday's Mizar or tomorrow's Mizar,
>and
>there are no mechanisms for extracting "the proof" from the script
>(they

>don't even really have such a concept)...

I think this is really important. It's true that MPE does change over time, and an externally maintained proof could in theory depend on a particular older version of MPE. But you could trivially verify an entire older proof, with that old version of MPE, with the current tool sets.



--- David A.Wheeler

[fl]

 

 For example, a proof script for today's Mizar will not work with yesterday's Mizar or tomorrow's Mizar,

I don't know why you say that because they definitely have a policy regarding proofs similar to Metamath's one:

They preserve *all* the proofs in their database when they upgrade their software. It's not the case of Isabelle

as you noticed it.

[Mario Carneiro]

On Sat, Aug 6, 2016 at 6:25 AM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

 

 For example, a proof script for today's Mizar will not work with yesterday's Mizar or tomorrow's Mizar,

I don't know why you say that because they definitely have a policy regarding proofs similar to Metamath's one:

They preserve *all* the proofs in their database when they upgrade their software. It's not the case of Isabelle

as you noticed it.

This is true, but doesn't contradict what I said. When the software is upgraded, many proofs can and must be correspondingly upgraded. Of course it is good that they upgrade the MML along with it, but there may be other scripts not in version control that will not be updated, and even if this were not the case the historical proofs themselves are no longer valid. This differs from Metamath's behavior in that the basic software is forwards and backwards compatible to older proofs. (Of course, this is not taking in to account the set.mm *library*, which of course has a similar policy to Mizar - library changes may cause proofs with today's set.mm to fail on tomorrow's and yesterday's set.mm. But given the right version of set.mm, the newer software will still be able to verify the old proof, and the old software will be able to verify the new proof.)

Mario

[Norman Megill]

One way to look at it is that many other systems can tell you that a
theorem is provable but do not show you an actual formal proof.

As a simple example, consider a program that verifies a (classical)
propositional calculus tautology by checking it against a 0-1 truth
table. Has it verified that the theorem is provable? Yes. Can the
program show you a proof from a set of axioms? No.

Norm

On 8/4/16 4:56 PM, David A. Wheeler wrote:

[fl]

 

One way to look at it is that many other systems can tell you that a
theorem is provable but do not show you an actual formal proof.

As a simple example, consider a program that verifies a (classical)
propositional calculus tautology by checking it against a 0-1 truth
table.  Has it verified that the theorem is provable?  Yes.  Can the
program show you a proof from a set of axioms?  No.

Those programs (all but Metamath) internally use semantic methods.

I agree with that. But since Metamath doesn't, I think to compare the systems

it is clearer to explain as if they were using syntactical ones only.

--

FL

[David A. Wheeler]

Here is a tweaked version of FL's summary that I like:
Many other formal math verification systems (such as HOL, Coq, and Mizar) have algorithms that try several plausible inference rules and return that one of them matches your goal formula - but not which one. Metamath checks that each inference rule proposed by the user exactly matches the formula.




--- David A.Wheeler

[Norman Megill]

I find this a little vague.

Metamath tools like "minimize" will try plausible inference rules and
change rules proposed by the user to more efficient ones.

Non-Metamath systems may rely on semantic methods like 0/1 truth tables
that just report valid or not valid. In this case, it is following an
unambiguous algorithm without "trying" anything, and there is no "which
one" to return.

The original proof of theorem "meredith" in set.mm was created
completely automatically by a program I wrote to create a 0/1 truth
table from a tautology then convert it to a Metamath proof. There was
no user involvement. (It has been replaced with a much shorter proof
found by Andrew Salmon and Wolf Lammen.)

The important difference as I see it is simply:

Metamath shows you complete formal proofs from axioms,
and none of the other ones do.

This is independent of how the proof was originally created -
semantically, or trying several plausible inference rules, or manually.
Formal proofs from axioms can in principle be generated from all of
these methods, but the other proof systems don't consider it important
enough to do so, particularly since algorithms to do may be nontrivial.

Norm

[Cris Perdue]

David,

You may be intentionally focusing on other issues, but if I were asked to contrast Metamath with other verification systems I would absolutely want to point out that Metamath is not just a verification system, but also what one might call a "proof exposition" system. I like very much some of the language at the top of page http://us.metamath.org/mpegif/mmset.html, such as:

Each proof is pieced together with razor-sharp precision using a simple substitution rule that practically anyone (with lots of patience) can follow, not just mathematicians. Every step can be drilled down deeper and deeper into the labyrinth until axioms of logic and set theory—the starting point for all of mathematics—will ultimately be found at the bottom.

. . .

Metamath's formal proofs . . . are broken down into the most explicit detail possible so that you can see exactly what is going on. Each proof step represents a microscopic increment towards the final goal. But each step is derived from previous ones with a very simple rule, and you can verify for yourself the correctness of any proof with very little skill. All you need is patience. With no prior knowledge of advanced mathematics or even any mathematics at all, you can jump into the middle of any proof, from the most elementary to the most advanced, and understand immediately how the symbols were mechanically manipulated to go from one proof step to another, even if you don't know what the symbols themselves mean.

Anyone using the metamath web site will also notice the commentary that accompanies many of the theorems, reflecting the philosophy behind Metamath and contributing to its unique value as an aid to exposition of the math.

-Cris

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Dan Connolly]

On Sat, Aug 6, 2016 at 6:18 PM, Norman Megill <n...@alum.mit.edu> wrote:
> The important difference as I see it is simply:
>
> Metamath shows you complete formal proofs from axioms,
> and none of the other ones do.

Perhaps other systems don't emphasize it to the same extent, but
Metamath is not unique in this sense.

McCune took a similar approach in 1996:

"Proofs found by programs are always questionable. Our approach to
this problem is to have the theorem prover construct a detailed proof
object and have a very simple program (written in a high-level
language) check that the proof object is correct. The proof checking
program is simple enough that it can be scrutinized by humans, and
formal verification is probably feasible."
-- https://www.cs.unm.edu/~mccune/papers/robbins/

Just like Metamath's checker is a few thousand lines of C, McCune's is
361 lines of lisp. Its specification isn't as thorough, but it's
simple enough:

; ... Otter proof objects have 6 kinds of step:
; 1. input input clause
; 2. resolve resolution on identical literals
; 3. merge merge identical literals
; 4. instantiate instantiate variables
; 5. paramod paramodulation on identical terms
; 6. flip flip an equality literal (positive or negative)

And the various constructive proof systems produce proof objects as a
matter of course, no?
http://www.cs.cornell.edu/~clarkson/courses/sjtu/2014su/terse/ProofObjects.html

--
Dan Connolly
http://www.madmode.com/

[Mario Carneiro]

On Sat, Aug 6, 2016 at 8:35 PM, Dan Connolly <dc...@madmode.com> wrote:

On Sat, Aug 6, 2016 at 6:18 PM, Norman Megill <n...@alum.mit.edu> wrote:
> The important difference as I see it is simply:
>
>   Metamath shows you complete formal proofs from axioms,
>   and none of the other ones do.

Perhaps other systems don't emphasize it to the same extent, but
Metamath is not unique in this sense.

McCune took a similar approach in 1996:

  "Proofs found by programs are always questionable. Our approach to
this problem is to have the theorem prover construct a detailed proof
object and have a very simple program (written in a high-level
language) check that the proof object is correct. The proof checking
program is simple enough that it can be scrutinized by humans, and
formal verification is probably feasible."
  -- https://www.cs.unm.edu/~mccune/papers/robbins/

This doesn't sound appreciably different from what HOL Light does. Nevertheless, HOL Light does not *display* these generated proof objects, even if it is constructing them at some level. Sure, that's just an "implementation detail", but it's surprisingly hard to get this right.
 

Just like Metamath's checker is a few thousand lines of C, McCune's is
361 lines of lisp. Its specification isn't as thorough, but it's
simple enough:

; ... Otter proof objects have 6 kinds of step:
;   1. input        input clause
;   2. resolve      resolution on identical literals
;   3. merge        merge identical literals
;   4. instantiate  instantiate variables
;   5. paramod      paramodulation on identical terms
;   6. flip         flip an equality literal (positive or negative)

And the various constructive proof systems produce proof objects as a
matter of course, no?
http://www.cs.cornell.edu/~clarkson/courses/sjtu/2014su/terse/ProofObjects.html

Same point. Coq produces proof objects (and in fact they are important data in a constructive setting), but facilities for displaying these proofs in anything approaching human readable status is completely lacking.

Mario

[Norman Megill]

I have used McCune's system and have found its proofs to be among the
most readable of the other systems.

But it does not provide a formal proof from a set of axioms. Its 6
rules are not "elementary" in the same sense as an instance of an axiom
scheme.

According to the definition of a formal proof that appears in most
mathematical logic textbooks, each step is an instance of an axiom
scheme or an instance of a rule scheme applied to previous steps. To
make formal proofs practical, Metamath extends this mildly by allowing
references to previous theorem schemes in addition to axiom and rule
schemes, and by treating instances of schemes to be schemes themselves.
It is trivial to convert them to strict textbook formal proofs if that
is desired, although for all but the simplest proofs the result would be
unmanageably long.

Norm

[fl]

> [It's vague]

Yes but it is easy to understand. It's just like the contract of an algorithm. It's not the way
the algorithm works actually, but it's all what one needs to know. And it allows to contrast Metamath
with other systems according to their essential difference that relies on their interfaces
not on the internal methods they use. Nothing prevents from adding extra explanations
later.

 

Metamath tools like "minimize" will try plausible inference rules and
change rules proposed by the user to more efficient ones.

The algorithm "minimize" is definitely not at the heat of Metamath. I would not use
"minimize" to describe Metamath.

--
FL

[David A. Wheeler]

On August 6, 2016 8:35:22 PM EDT, Dan Connolly <dc...@madmode.com> wrote:

>Perhaps other systems don't emphasize it to the same extent, but
>Metamath is not unique in this sense.
>

>McCune took a similar approach in 1996...

I used prover9 (the automatic proof finder that succeeded otter) and ivy (the verifier proved using ACL2) for my PhD dissertation. As an automated proof finder for first order logic it's really quite something.

Metamath is different.. but it can be a challenge to explain that difference to those who have never used it.



--- David A.Wheeler

[Norman Megill]

Prover9 is designed to prove stand-alone theorems rather than to build a
hierarchical body of knowledge. When I mentioned other systems, I
primarily had in mind those mentioned on the Freek 100 list.
Nonetheless, here is my take on it and its relatives.

McCune's EQP prover (a Prover9 relative optimized for equational
varieties such as the Robbins algebra) displays its proofs in a format
very close to a formal proof that can be easily translated (by hand at
least) to Metamath, and I have done this myself without difficulty.

In the case of the Prover9 proof objects, while they are a step in the
right direction, the issue is that the proofs do not justify that the 6
rules are valid FOL inferences, and we have to take them on faith.
While they are probably justified by informal proofs in a paper or
textbook, we can never be absolutely sure there is no subtle hidden flaw.

(It may be possible to devise a set of Metamath lemmas corresponding to
the various cases of each rule and use these to automate a translation
to Metamath. That's what I would first look at if I wanted to translate
Prover9 proofs.)

The situation is similar with other systems, to varying degrees. This
gap between the axioms of logic and the rules used by the proof language
is a key difference from Metamath.

Some mathematicians may say that it is obvious that the rules hold in
FOL and that this gap is therefore unimportant. However, it is unlikely
that a beginner could prove this gap from the axioms, perhaps not even
by consulting an informal proof. Metamath makes the complete derivation
accessible to everyone.

How important is it to provide complete proofs? Here is a 2013 email
(quoted with permission) from set.mm contributor Andrew Salmon, who by
chance came upon a link to Metamath in a gaming forum while in high school.

(begin quote)
"I would like to thank you for introducing me to pure mathematics. I am
now going into my senior year of high school, but I have resolved to
major in mathematics and my ultimate dream is to become a math
professor. I would not have even thought about this decision had it not
been for Metamath.

Really, Metamath was what I needed to overcome the discomfort that I had
with mathematics as I had been taught: intuitively grasping the concepts
while lacking any understanding of the underlying logic.

...PS: I've finished (most) of Rudin's Principles of Mathematical
Analysis and am now reading chapter 4 of Spivak's Calculus on Manifolds,
among other things. Also, I've taken a class on graph theory at a
university and am working with a professor on a research project in
graph theory. Maybe my goal of a publication before the end of high
school will come true!"
(end quote)

Norm