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. -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7366C361-EE65-4B70-868A-81738BF5DEBA%40dwheeler.com.
