On Sat, 25 Jan 2020 14:10:21 -0800 (PST), "'Alexander van der Vekens' via Metamath" <[email protected]> wrote: > the goal should be a > database in which "every published mathematical result is available" and > which has "essentially *all* mathematics formalized".
That's a big dream, and for the very long term, a worthy (and incredibly ambitious) goal. We'll need to find some smaller & shorter term goals. I've been championing filling in the Metamath 100, and I think it's been a useful example of that. I think other shorter-term goals could be useful For example, we could have the goal of fully formalizing certain works. An obvious example is to complete the formalization of elementary geometry based on Tarski's axioms, following [Schwabhauser]. Formalizing certain works will help us develop the key infrastructure needed to support many other works. I think in *reality* there will be multiple databases for different axiom sets. E.g., if you don't believe in classical logic, iset.mm (or its descendent) may be what you care about. But that's okay, it just means that there will really be a *collection* of such databases. [Desirable properties proposed are...] > Completeness (as far as possible)! ... I don't think it will ever *actually* be complete, but sure, it's a worthy long-term goal. > "Beauty" (see also section 1.1.4 in the metamath book): > Not only the proofs should be beautiful (being short, elegant, tricky, > etc.), but also the definitions and theorems [and] structure... That's a reasonable desire, though beauty is in the eye of the beholder. In any case, I think efforts to do that are useful, as long as we acknowledge that there will always be differences of opinions & imperfections. > "Simplicity" and "Rigor" ... Desirable, sure. But in the end, I think actually *having* proofs (leaning towards completeness) is the more important part. Without proofs, there's no point in it. > To conclude: To answer the question about the goals for set.mm, we have to > agree on the purposes (e.g. knowledge base/library vs. pedagocial textbook) > and the properties (completeness, beauty, simplicity, brevity, etc.) first. I don't really agree with that statement. Different people may have different goals and still work together. At a high level people will agree on those generic properties; the issue will be working them out in practice. As far as *purpose* goes, if it must be one, it should be knowledge base/library. But I think that's a false dichotomy: I don't think it should be just one or the other. A knowledge base has great pedagogical value. One problem with traditional pedagogical systems is that students *cannot* follow the "whole string" in any area that interests them. Indeed, some areas can be hard to understand *because* the full story is never told. Metamath can enable solutions to this. If I may, I have an computer science analogy. In the early 1970s people who wanted to study operating systems studied the code of Unix, because that was available to study. Then AT&T decided to make it hard to *legally* study Unix. So people created "toy" operating systems like Minux and Xinu, and there was a whole fad focused on microkernels, because these systems were the kind that academics could easily create themselves. But many academics quickly became completely disconnected from studying *actual* operating systems that many people used. An incredible number of academics studied schedulers (because that was easy to study on toy systems) & increasingly many had no idea how *actual* operating systems worked (e.g., in *real* operating systems the majority of code was in drivers, a key fact not visible to most academics). When Linux grew in capability in the *real* world (and to some extent this was true of the *BSDs as well), academics could once again study real systems. (Yes, I'm aware that QNX is a microkernel system, but there are reasons such systems are rare.) In short: Simple models for teaching purposes do have their place. But for serious academic work, there's nothing like a *real* thing. In the math context, the "real" things is proofs of the actual math statements you care about, including the statement and handling of special cases. Once you have a database of the "real" definitions and proofs, you can use various pedagogical approaches to learn about it... and the student can have confidence that they are learning about something "real". (Well, as "real" as things get in math. We can have the realism/nominalism argument another time :-). ) We've already had at least one high school student submit many set.mm proofs. So it's clearly possible to learn from "the real thing". --- David A. Wheeler -- 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/E1ivZS9-0001ew-Eq%40rmmprod07.runbox.
