Slashdot Mirror
Learn The Language Of Math
N. Megill writes "While mathematics is not "closed source" in the same way that some
computer operating systems are, it can take years of hard work to
acquire the background needed to understand advanced abstract
mathematical proofs. This is because they are usually presented at a
very high level that hides most of the detail, often making them beyond
the grasp of a non-mathematician (even a very smart one such as a
computer programmer). The Metamath
project breaks down mathematical proofs into the finest possible level
of detail and builds mathematics from the ground up. Like Linux From Scratch, it can appeal
to those who like seeing things built up from first principles.
Metamath does not claim to teach you mathematics, just as reading the
kernel source code does not teach you how to use Linux, but there can be
a certain satisfaction in just knowing it is there."
I disagree, strongly. Mathematical proof comes down to three things: knowing definitions, the ability to think laterally, and a compositional style which is both terse and precise. This was driven into my skull by constant repetition by my advisor at University, while I was working on my maths degree. Learn the definitions. Memorise them! That's ninety percent of the work. The remaining ten percent can be split evenly by the acquisition of precise compositional style and by the ability to recognise the application of definitions -- this being the lateral thinking I mentioned above.
Claiming that writing and understanding mathematical proofs is hard is absurd. It's fantastically easy to write and understand proofs. The difficulty lies in making the lateral cognitive leap from some postulate to a theory dealing with the postulate. The style required to write proofs can be taught quickly, likely in a matter of hours. Learning the definitions can take a lifetime -- if this MetaMath project provides a bottom-up breakdown of mathematical axioms, theories, laws, and maxims, then it serves as a valuable aid. I know that such a tome, electronic or not, would be irreplaceable in my collection... not to mention replacing a shelf full of bright yellow maths texts.
MCH/VO S* W- N+++++ PEC+++ D(s++/r) A a+>+++ C* G++(++++) Q+ 666 Y
Oh, come on. Is it possible that once, maybe just this once, it doesn't really make sense to try and pin the Open Source Medal on this to make it even more 133t and k3w1? But hey, while you're at it, you should probably mention that you can use mathematics on Linux, too, and that it runs perfectly on both Gnome and KDE, no less! And I heard that ESR uses it, like, every day!
That aside, the concept of "open vs. closed" applies to mathematics about as much as it applies to C++. Mathematics is a tool. There is nothing that says that the inventor of a revolutionary mathematical equation must then make her knowledge available to the world. She would be just as free to form a company that charges insanely high consulting fees to process data using her secret formula as she could post it on her webpage for all the world to use freely.
While it's true that the vast majority of all mathematical knowledge is freely available to anyone who cares to look at it, that doesn't make the concepts of "open source" and "closed source" applicable to mathematics itself.
Obliteracy: Words with explosions
As a full-time mathematician I'm half-pleased to see the existence of this project, but I'm not really very thrilled with it. It's the big concepts that attract me to maths, the ideas and the big picture, not the nitty-gritty of putting together lots of little logical steps. So as a matter of taste, I don't think that Metamath presents a very appealing view of maths, and I suspect that some people will be actively put off maths by this. If not then fine, but this is my personal feeling.
Another reservation I have about this is its concentration on axiomatic set theory. This is a subject which tends to draw a lot of attention from the non-mathematics community, in popular science books and so on. In fact it's quite far out of the mainstream of mathematics (a sociological observation rather than a value judgement). I think that the importance of set theory as a "foundation" and "universal language" for mathematics has been far overstated.
This point of view on set theory is actually increasingly prevalent among the theoretical computer science community - at least, the part of it that I come into contact with. There are various structures from mathematical logic that are far more applicable to computer science than sets are: for instance, the lambda-calculus and categories. Metamath is very reductionist in its approach: it takes the smallest building blocks and shows in minute detail how they can be put together to obtain familiar objects. In contrast, the more popular modern approach is to try and describe things from the top down, e.g. one might look for abstract mathematical structures which resemble the collection of datatypes in a particular programming language.
So it's kind of nice to see this here, but it's not the face of mathematics I'd choose to present.
Ok, for what it is worth, I have two maths degrees, and am working on my third (ph.d). I am afraid either you (likely) or your advisors are sorely mistaken.
If writing and understanding mathematical proofs is so easy, why are there entire graduate courses dedicated to one or two proofs?
Some mathematics is very easy to understand. Some mathematics requires years of background to understand.
After all, much of what mathematics is really about is building abstractions on top of each other. Our only hope of obtaining deep understanding of some maths is to build powerful enough abstractions. This power has a price, and it can take years of study to understand them properly.
Understanding proofs once you have the correct framework is often easy. Creating that framework, especially if it is new work, can be very difficult. Of course it is easy when you have someone to hold your hand through the whole thing, but that is pedagogy, not mathematics. "lateral cognitive leap" doesn't mean much, except the employment of currently vougue buzz: "lateral thinking". mathematics involves many approaches, you may call some of them 'lateral' if you wish -- but it isn't a notable useful characterization...
Replying to various comments here:
I don't see where it was suggested Metamath is for newbies, or for newbies to understand math. There are several ways in which something like Metamath can provide value to non-mathematicians. For one thing, they can use it to see that there are links from a theorem all the way down, even if they do not study all those links and comprehend them as a whole.
Some posters have commented that Metamath doesn't make math understandable. That isn't its purpose. You can make something completely verifiable without making it understandable -- and that is the only way to work with the largest structures. A demonstration that a large office building will not fall down depends upon ensuring that each structural component does its job, and a single person might actually check each and every component and thus know the building will not fall down, but that person could still end up not understanding the building as a whole.
While I would not recommend somebody learn C++ by studying the compiler's generated assembly language, I would recommend that an experienced expert in C++ learn more, from time to time, by experiencing the compiler's generated assembly language. I know that studying generated assembly code has occasionally provided a useful insight into the high-level langugage specification. Similarly, studying the details is a useful occasional part of a professional mathematician's experience.
Metamath can (or will be able to) answer questions that are difficult to answer otherwise -- What axioms does (a proof of) such-and-such a theorem use? Do we know of a proof that does not use a certain axiom?
Today's proofs are subject to errors. Occasionally an error slips by an author and the referees. Eventually, papers may be submitted with links to Metaware-verified proofs, essentially eliminating the possibility of error.
Further in the future, databases like Metaware will aid the construction of proofs by supplying already-proven lemmas, so the author does not have to expend time proving something already published or reviewing publications to find it.
Maple and Mathematica are useful tools for some mathematicians, but they are flawed because they have gaps. They sometimes offer deductions that are false, because they make unwarranted assumptions about domains or absences of singularities, or whatnot. E.g., some software engineer may have poured a table of integrals into the software but neglected to make Mathematica prove a table entry is applicable to a particular user's situation before applying the entry. We need something like Metamath that is complete to serve in those times when mathematical proof is desired.
While nobody travels every road that is connected to our highway system, a key characteristic of the system that makes it useful is that it is connected. Thus each user finds a route to their destination, even though they don't understand where every road leads to or comes from.
"Learn the definitions. Memorise them! That's ninety percent of the work."
Get a grip on yourself!! I too have a math degree, and if you spent 90% of your time memorizing definitions, I am not surprized you have difficulties seeing how they relate to their uses. Mathemetics does require solid knoledge of its foundations, yes, but that does not mean memorization, it means understanding, and there's quite a bit of difference between the two. Writing proofs is not "easy." (t is fun, however) Otherwise you would not have entire courses devoted to teaching how to do proofs (and yes, dear, i am talking about graduate level courses.). Writing proofs isn't a matter of knowing the mathematical shorthand. And a single theorem's proof can contain within it innovations whence spin of entire field of study. Learn the history of mathematics, and you will see this. Look at the many popular unproven theorems, "fantastically easy"?!?!?! How many hundreds of years were spent on the 5th Postulate? Math is proofs!