Updating the metamath website - esp. "What is Metamath" & what's distinct about it
107 views
Skip to first unread message
David A. Wheeler
Jun 7, 2023, 10:54:53 PM6/7/23
to Metamath Mailing List
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.
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.
Jim Kingdon
Jun 8, 2023, 2:01:59 AM6/8/23
to meta...@googlegroups.com
I often discuss my math hobby with acquaintances and I usually lead with
something like "I write math proofs that can be checked by a computer".
Granted, that is as a conversation opener rather than a web site but
perhaps something as brief as that could be a candidate for the one
sentence intro.
I will admit to having a bit of a sentimental attachment to the current
mini-FAQ which makes it hard for me to single out which parts are worth
keeping. I'm especially looking at "What is Metamath?", "Will Metamath
help me learn abstract mathematics?", and "Who is the intended audience
for Metamath?" although I see that your proposed text below does keep
some of the text from those answers. Of course the answer to "Are there
other sites that formalize math from its foundations?" is thoroughly out
of date.
I do like most of the proposed text below for example calling out the
non-hard-wired axioms and that proofs are stored as steps not as recipes
for applying tactics.
Philosophically I'm all for less wordy a goal, rather than more detail.
But as you can see from my somewhat conflicted message here it is hard
to know what to cut. I am looking at things like
https://leanprover.github.io/about/ or
https://wiki.portal.chalmers.se/agda/pmwiki.php (both brief) but I can't
tell whether they are inspiring or fail to explain themselves enough in
terms that people new to those systems would understand.
I would like to call out one thing you said, "further welcome potential
new contributors". I'm not sure the exact best strategy to make the page
do that, but maybe something like talk about how many past contributors
there have been or "UNCLE NORM WANTS YOUR PROOF" or a discussion of
community and collaboration or something else that goes a little bit
beyond the mechanics of contributing.
Thank you for taking a look at this.
something like "I write math proofs that can be checked by a computer".
Granted, that is as a conversation opener rather than a web site but
perhaps something as brief as that could be a candidate for the one
sentence intro.
I will admit to having a bit of a sentimental attachment to the current
mini-FAQ which makes it hard for me to single out which parts are worth
keeping. I'm especially looking at "What is Metamath?", "Will Metamath
help me learn abstract mathematics?", and "Who is the intended audience
for Metamath?" although I see that your proposed text below does keep
some of the text from those answers. Of course the answer to "Are there
other sites that formalize math from its foundations?" is thoroughly out
of date.
I do like most of the proposed text below for example calling out the
non-hard-wired axioms and that proofs are stored as steps not as recipes
for applying tactics.
Philosophically I'm all for less wordy a goal, rather than more detail.
But as you can see from my somewhat conflicted message here it is hard
to know what to cut. I am looking at things like
https://leanprover.github.io/about/ or
https://wiki.portal.chalmers.se/agda/pmwiki.php (both brief) but I can't
tell whether they are inspiring or fail to explain themselves enough in
terms that people new to those systems would understand.
I would like to call out one thing you said, "further welcome potential
new contributors". I'm not sure the exact best strategy to make the page
do that, but maybe something like talk about how many past contributors
there have been or "UNCLE NORM WANTS YOUR PROOF" or a discussion of
community and collaboration or something else that goes a little bit
beyond the mechanics of contributing.
Thank you for taking a look at this.
Paul Chapman
Jun 8, 2023, 2:08:48 AM6/8/23
to meta...@googlegroups.com
On 08/06/2023 03:54, David A. Wheeler wrote:
> These verifiers were written
> in different programming languages by different people in different programming languages.
By different people. :)
> These verifiers were written
> in different programming languages by different people in different programming languages.
Cheers, Paul
David A. Wheeler
Jun 10, 2023, 9:48:49 PM6/10/23
to Metamath Mailing List
This pull request proposes an update to the early part of the us.metamath.org
website main page:
https://github.com/metamath/metamath-website-seed/pull/8
Comments welcome.
The rest of the page also needs updating, but it took me a little while just to get this far.
If we keep working on making improvements it'll be a *lot* easier for
newcomers to understand what this Metamath thing is all about.
--- David A. Wheeler
website main page:
https://github.com/metamath/metamath-website-seed/pull/8
Comments welcome.
The rest of the page also needs updating, but it took me a little while just to get this far.
If we keep working on making improvements it'll be a *lot* easier for
newcomers to understand what this Metamath thing is all about.
--- David A. Wheeler
David A. Wheeler
Jun 11, 2023, 10:00:38 PM6/11/23
to Metamath Mailing List
Here is my latest attempt to define Metamath - comments?
> Metamath is a simple and flexible computer-processable language that
> supports rigorously verifying, archiving, and presenting mathematical proofs.
This is in part a response to Jim Kingdom, who
noted that he emphasizes "checking with a computer". Fair enough,
so I thought putting "rigorously verifying" first would be sensible.
At first I was worried iif putting "rigorously" first would be confusing, but I think it's far;
Metamath really *does* provide added rigor for archiving and presenting.
Please post feedback and/or approval of this & related changes here:
https://github.com/metamath/metamath-website-seed/pull/8
I realize not everyone cares about the front page, and that's fine,
but I think it's important to update these pages to help potential newcomers.
--- David A. Wheeler
> Metamath is a simple and flexible computer-processable language that
> supports rigorously verifying, archiving, and presenting mathematical proofs.
This is in part a response to Jim Kingdom, who
noted that he emphasizes "checking with a computer". Fair enough,
so I thought putting "rigorously verifying" first would be sensible.
At first I was worried iif putting "rigorously" first would be confusing, but I think it's far;
Metamath really *does* provide added rigor for archiving and presenting.
Please post feedback and/or approval of this & related changes here:
https://github.com/metamath/metamath-website-seed/pull/8
I realize not everyone cares about the front page, and that's fine,
but I think it's important to update these pages to help potential newcomers.
--- David A. Wheeler
Reply all
Reply to author
Forward
0 new messages