I think we need to update the "main" pages of the metamath website,
e.g., the main <https://us.metamath.org/>.
Implementing this will primarily involve changes to the repo:
https://github.com/metamath/metamath-website-seed especially:
https://github.com/metamath/metamath-website-seed/blob/main/index.html
For example, I'd like to update its information & make changes to
further welcome potential new contributors.
To do that, at the top of the page (before the table) I'd like to have ONE
sentence
that says "what Metamath is" along with a link to more info. Here's my proposed
text:
Metamath is a simple, robust, and flexible computer-processable language for
archiving, presenting, and rigorously verifying mathematical proofs. See the
FAQ for more details.
We'd then update the FAQ. Early in the FAQ I'd like to have updated text
that explains in more detail what Metamath is, along what is
*distinct* about Metamath.
The goal is to help newcomers understand what Metamath is, in today's context.
Below is an attempt at those initial entries,
based on the text of the website & the Metamath book.
I'm sure it needs work. I'd love to hear suggestions.
--- David A. Wheeler
=====
Q: What is Metamath, with a little more detail?
A:
Metamath is a simple, robust, and flexible computer-processable language for
archiving, studying, and rigorously verifying mathematical proofs.
Metamath allows you to state your axioms (assumptions), then state theorems and
their associated proofs.
A collection of axioms and proofs depending on them is called a "database", and
we support several databases
for various axiomatic systems.
While simple, Metamath is also powerful; the Metamath Proof Explorer (MPE) database
has over 23,000 proven theorems and is one of the top systems in the “Formalizing 100
Theorems” challenge. <https://www.cs.ru.nl/~freek/100/>
Metamath supports rigorously archiving mathematical knowledge in a computer
database, providing precision,
certainty, and the elimination of human error.
Q: What is distinctive about Metamath?
A:
Metamath is probably unlike anything you have encountered before
Here are distinctive traits of Metamath compared to other top systems for
formalizing mathematics:
* The Metamath language is simple and robust, with an almost total absence of
hard-wired syntax. We believe that it provides about the simplest possible
framework that allows essentially all of mathematics to be expressed with
absolute rigor.
* Metamath is not tied to any particular set of axioms, instead, axioms are
defined in a database.
* Metamath final proofs show every step, no exceptions, where each step
is *only* an application of an axiom or a previously-proved statement.
Most other proof systems allow statements (like "simp", "auto", or "blast")
which only assert that a proof could be found instead of
showing every step. Metamath's approach makes it possible for anyone to
follow backwards every
step of every proof. This also makes verification fast, because
the system does not need to rediscover proof steps.
* Many tools support Metamath, instead of one "canonical" tool that in practice
everyone uses.
Metamath was originally implemented by the "metamath-exe" tool, but today
you can use Metamath without using the original tool.
* The Metamath verifier has been re-implemented in many different
programming languages, so verification can be done by multiple
independent implementations. This greatly reduces the risk of accepting an
invalid
proof due to an error in the verifier.
* Substitutions (the fundamental operation in Metamath)
are easy to understand, even by those who are not
professional mathematicians. Anyone can look at a proof, then click on any
step
to see why that step is justified, and repeatedly follow that process back
to axioms.
* Proofs stay proven. In some systems, changes to the system's
syntax or how a tactic works causes proofs to fail in later versions,
causing older work to become essentially lost.
Metamath's language is
extremely small and fixed, so once a proof is added to a database,
the database can be rechecked with later versions of the Metamath program
and with other verifiers of Metamath databases.
If an axiom or key definition needs to be changed, it is easy to
manipulate the database as a whole to handle the change
without touching the underlying verifier.
Since re-verification of an entire database takes seconds, there
is never a reason to delay complete verification.
The set.mm began development in 1992 and proofs from that year
are still in use.
This aspect is especially compelling if your
goal is to have a long-term database of proofs.
Of course, other systems may have advantages over Metamath
that are more compelling to you, depending on what you value.
Some users of Metamath also use or develop other systems, and
we're always delighted to cooperate with other systems.
We hope this helps you understand Metamath
within a wider context.
Q: What tools exist for Metamath?
Many tools support Metamath. There are three main sorts of Metamath tools (some
tools belong to more than one sort):
* Proof assistants help you create proofs; these include mmj2, metamath-lamp,
metamath-exe, and yamma.
All proof assistants include some capabilities to automatically develop
proofs of some steps.
* Verifiers verify that a database is correct (in particular, that the proofs
in a database are correct).
There are over a dozen verifiers available.
Note that Metamath verifiers do not make logical inferences; they just make
a series of symbol
substitutions according to instructions given to it in a proof
and verifies that the result matches the expected theorem.
* Support. These kinds of tools perform other tasks such as generate HTML pages,
provide data about proofs, and so on.
See the links for more information.
Originally the first tool to support Metamath (the language) was also called
Metamath. This became confusing, so today we call that tool "metamath-exe".
Q: What verifiers are used to verify set.mm (the biggest database)?
A:
After every proposed change the *entire* updated set.mm database
must pass 5 different verifiers before being accepted.
These verifiers were written
in different programming languages by different people in different programming
languages.
These verifiers are:
* metamath-exe (in C by Norman Megill),
* smetamath-rs (in Rust by Stefan O'Rear),
* checkmm (in C++ by Eric Schmidt),
* mmj2 (in Java by Mel L. O'Cat and Mario Carneiro),
* mmverifier.py (in Python by Raph Levien)
This process provides exceptional confidence that its entire collection of
proofs is correct.
Q: What does this site provide?
This site (the Metamath Home Page) has a collection of web pages generated from
those proofs (in various axiomatic systems) and lets you see mathematics
developed in complete detail from first principles, with absolute rigor.
Hopefully it will amuse you, amaze you, and possibly enlighten you in its own
special way.
<More updated FAQ entries would follow.>
======== Past Sample texts, so you can compare them. =========
The current FAQ says the following, below:
"Q: What is Metamath?
A: Metamath is a tiny language that can express theorems in abstract mathematics,
accompanied by proofs that can be verified by a computer program. This site has a
collection of web pages generated from those proofs and lets you see mathematics
developed in complete detail from first principles, with absolute rigor. Hopefully
it will amuse you, amaze you, and possibly enlighten you in its own special
way."
The Metamath book abstract:
"Metamath is a computer language and an associated computer program for archiving,
verifying, and studying mathematical proofs. The Metamath language is simple and robust,
with an almost total absence of hard-wired syntax, and we believe that it provides about
the simplest possible framework that allows essentially all of mathematics to be
expressed with absolute rigor. While simple, it is also powerful; the Metamath Proof
Explorer (MPE) database has over 23,000 proven theorems and is one of the top systems in
the “Formalizing 100 Theorems” challenge. This book explains the Metamath language and
program, with specific emphasis on the fundamentals of the MPE database."
Metamath book preface:
Metamath\index{Metamath} is a computer language and an associated computer
program for archiving, verifying, and studying mathematical proofs at a very
detailed level. The Metamath language incorporates no mathematics per se but
treats all mathematical statements as mere sequences of symbols. You provide
Metamath with certain special sequences (axioms) that tell it what rules
of inference are allowed. Metamath is not limited to any specific field of
mathematics. The Metamath language is simple and robust, with an
almost total absence of hard-wired syntax, and we
believe that it
provides about the simplest possible framework that allows essentially all of
mathematics to be expressed with absolute rigor.
Using the Metamath language, you can build formal or mathematical
systems\index{formal system}\footnote{A formal or mathematical system consists
of a collection of symbols (such as $2$, $4$, $+$ and $=$), syntax rules that
describe how symbols may be combined to form a legal expression (called a
well-formed formula or {\em wff}, pronounced ``whiff''), some starting wffs
called axioms, and inference rules that describe how theorems may be derived
(proved) from the axioms. A theorem is a mathematical fact such as $2+2=4$.
Strictly speaking, even an obvious fact such as this must be proved from
axioms to be formally acceptable to a mathematician.}\index{theorem}
\index{axiom}\index{rule}\index{well-formed formula (wff)} that involve
inferences from axioms. Although a database is provided
that includes a recommended set of axioms for standard mathematics, if you
wish you can supply your own symbols, syntax, axioms, rules, and definitions.
The name ``Metamath'' was chosen to suggest that the language provides a
means for {\em describing} mathematics rather than {\em being} the
mathematics itself. Actually in some sense any mathematical language is
metamathematical. Symbols written on paper, or stored in a computer,
are not mathematics itself but rather a way of expressing mathematics.
For example ``7'' and ``VII'' are symbols for denoting the number seven
in Arabic and Roman numerals; neither {\em is} the number seven.
Some older text:
* Proofs *must* be a rigorously stated sequence of *only* axioms and previously-proved statements. Most other
proof systems allow proof statements like "simp", "auto", or "blast", which
aren't previously-proven statements but are instead requests to rediscover a proof. All Metamath proof
assistants *do* support automatically finding proofs of statements, but in Metamath what's important is
producing the final steps of the proof, not merely an assertion that it could be rediscovered.
