Comment by dwheeler | Hacker News Reader

Comment by dwheeler | Hacker News Reader

Parent Full thread

Metamath contributor here! Each proving tool has its pros and cons, but always happy to see Metamath noted :-).

One thing that's cool about Metamath is that the axioms are not built-in. It's true that the most-used system is based on classical logic and ZFC set theory https://us.metamath.org/mpeuni/mmset.html ... but you don't have to use that system. There's a well-maintained database using intuitionistic logic: https://us.metamath.org/ileuni/mmil.html ; on the so-called "New Foundations" (a many-sorted system): https://us.metamath.org/nfeuni/mmnf.html ; on HOL https://us.metamath.org/holuni/mmhol.html ; and you can make your own if you want to.

In Metamath the proofs hide absolutely nothing. There's no hand-waving "it's obvious that". Every step in a proof must be rigorously and directly proven by some axiom or a previously-proven theorem with absolutely no exceptions. This also means that while finding proofs can be hard, verifying proofs is fast. I just ran a proof verification run of over 47,000 theorems in 6.35 seconds. In the Metamath Proof Explorer / set.mm database (the one with classical logic and ZFC), we routinely run multiple provers by different people on every proposed change. So not only is the kernel small, it's implemented by multiple different programs, making it extremely unlikely we'll accept an invalid proof.

This video I made years ago summarizes Metamath: https://www.youtube.com/watch?v=8WH4Rd4UKGE

Metamath is interesting for education in the principles of formal proofs, because:

1. The Metamath Book is self-contained well written, simple introduction.

2. Everything is explicit, nothing is hidden.

3. Because of extremely simple syntax and semantics it's easy write own proof verifier.

The drawbacks are:

1. Non-standard approach to free and bound variables.

2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.

3. Almost no proof automation. No tactics. Long, hard to read proofs.

I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.

What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL

Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm

Reading `hol.mm` made me grateful for Lean 4's general purpose programming.

I get the string substitution focus, and respect what metamath has achieved, but the bridge Lean 4 makes wrt systems programming has left quite an impression.

I wonder how many people mostly see mathlib4 & think that's the one prescribed route (ala Rust) when one of Lean 4's under-documented super powers is the ease with which you can roll your own light-weight low to zero overhead domain-specialized constructs that are also trivial to prove because of the dependent type system.

(Perhaps more for verified functional systems than deep math.)

There are other forms of logic? is intuitionistic logic as rigorous? fascinating

edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!

> if it is weakened, how can you prove the same stuff?

Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.

This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.

Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.

Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).

Having a weaker base system means you can distinguish more fine grained between statements.

For example, in an intuitionistic setting there is a difference between a set being non-empty and a set having an element.

Reply on news.ycombinator.com