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."
This is like saying the best way for newbies to understand a C++ program is for them to decompile it and look at the assembly!
There is no way to short-circut the "years of hard work" involved in understanding higher-level mathematics. I know it's the holy grail of CS geeks everywhere to streamline the hard work of understanding proofs, but mathematical decompilation is not the answer.
Slashdot 's editors are dickheads
There are times when being able to see everything all at once isn't the best way of learning something. If I lay out out complete blueprints for the space shuttle, you're not going to have that much better an understanding of it (unless, of course, you've already know how to deal with situations like that).
... that the amount of times you mention open source and Linux in a Slashdot submission is directly proportional to the likelihood that the story will be accepted.
I wonder if it is anything like Metamoderation for Mathemeticians
Math Trolling: x+y=z*troll if x=fp
You say you want a revolution....
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
Wonderful to see one are where folks are making it possible for those interested to actually trace stuff back to its roots.
>The difficulty lies in making the lateral cognitive leap from some postulate to a theory dealing with the postulate.
Thank you. This is exactly the problem I had in school for math and what I see alot of people having difficulty with in many areas.
The surprise isn't how often we make bad choices; the surprise is how seldom they defeat us.
Learn the definitions. Memorise them! That's ninety percent of the work.
Anything 90% of which is memorizing definitions is unlikely to be interesting. Or useful, come to think of it.
Kaa
Kaa
Kaa's Law: In any sufficiently large group of people most are idiots.
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
Proofs and "mathematical rigor" are ridiculously overused in teaching.
This is a ridiculous extension of the current misconception that mathematical simplicity and conceptual simplicity go hand in hand, when the opposite is true.
Imagine if children were taught arithmetic by route of logistics... only a handful of geniuses would be able to make change! Yet go to university and you'll see professors trying to build understanding the way they would build proofs: introduce axioms, show higher relationships that emerge from these axioms, later introduce tricks of the trade for practical , and then, maybe, once (or rather, if!) the student shows a good understanding, talk about applications. You have to take it on faith that years of painful, boring proofs will lead to interesting and useful ideas.
It's sheer idiocy, and terrifically destructive of promising young minds. Not only does it drive people away from math, it encourages absurd semi-religious attitudes that math somehow has independent existence that we are discovering, rather than being a language invented by man to describe the universe around us.
Possibly my favorite book is "Mathematician's Delight", which shows the correct method of teaching math: explain applications first (to build interest), practical method second, and then, maybe, if the student shows understanding and interest, talk about proofs that the math works.
---
Doesn't BigBlue do something like this?
At least ChessMaster8000 does and its pretty good.
The surprise isn't how often we make bad choices; the surprise is how seldom they defeat us.
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...
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
After an amount of time, one forgets what it is like to be a newbie. To linux, complex mathematics, even to life. This can only be overcome by spending time refreshing your memory by hanging out with users (user-testing), elementary math students, and children.
One example I have to relate occurred in my freshman calc class a number of years back. The professor had grown accustomed to spending his day discussing high-level mathematical proofs with his colleagues, and forgot what it is like to not know everything, and still be learning. Our assignment was to calculate the volume of a 3-dimensional curved object whose primary shape was a triangle.
When it came time to figure out the area of the triangle, he went through a 20 minute proof in front of the class which involved something like 8 different variables. Afterwards, I stood up and volunteered the formula I learned in high school, 1/2 (base x height). The professor was so shocked that I came up with the same answer in 2 lines of algebra, that he was unable to complete the rest of the calculus computation.
I'm no genius, but was there really any reason to try losing his students when the triangle wasn't the base of his lesson plan?
- passion
Formal mathematical proofs are usually only useful to mathematicians. For most people it suffices to tell them that the theory is true and has been proved to be so. I don't think it's going to help people to slog through abstract mathematics at unprecedented levels of detail. I think the public would be much better served with concise regular English descriptions of mathematical concepts and perhaps the how and why of certain mathematical proofs. Techies need math, they don't need to try to be mathematicians.
I took Engineering Physics in university so I'm no stranger to advanced math. I know the fundamental theories they're breaking things down to, but this is still some hard stuff to understand. For instance:
If the goal is to really make this stuff understandable I think they need to provide some much more basic examples in the style of: If you have 3 apples and I give you 2 more apples, how many apples do you have?
I think for the above axiom an equivalent would be:
j: it is raining
y: the ground is wet
c: there are puddles on the ground
If it is raining then if the ground is wet there are puddles on the ground.
If the above is true then:
If it's true that if it is raining then the ground is wet, it's true that if it's raining then there are puddles on the ground.
This basically says: if whenever the ground is wet there are puddles, and whenever it rains the ground is wet, then whenever it rains the ground will be wet and there will be puddles.
Then again, it is a Monday.
Ah, the call of the "pure" mathematician: "You want to apply this stuff? To hell with you, philistine!"
True pure mathematicians, unconcerned with application, are insane. They don't recognize mathematics as derived from real-world observation, they are just happy little computers, playing with meaningless symbols to solve meaningless puzzles, upset when you point out that there is no such thing as a self-evident truth to make an axiom of.
Practical applications may not be their motivation, but it's the justification for their pay, and the origin of their field. We, the economic animals that value utility enough to put food on the table, shouldn't defer to their irrationality.
The one advantage of using these economically insane individuals is, of course, that they come cheap. But while it makes sense to take advantage of them, we must be careful not to let them spread their insanity with their products.
For mathematicians, give me a Donald Knuth any day, who mixes practical work and theory in his life, for the improvement of both, and is eager to change notations and rules to make them easier to work with and learn and into a better reflection of reality. He has, and spreads, a healthy appreciation of useful math, not a degenerate disdain for "applied" (sullied, tainted) math.
---
Weren't these the guys that were getting sued by Wolfram Research (makers of Mathematica)?
Need Free Juniper/NetScreen Support? JuniperForum
I think the worst problem with the way mathematics is taught (either from a teacher, or a book) is the lack of visualization. Indeed, there's an almost religious commitment to rigidity and formalism, when a lot of time, all we need is a little insight, and thenall the symbols will make sense.
Take abstract algebra for instance. It's really arcane and odd; What makes a group? Closure, Associativity, Identity, and Inverses. Most people believe that these things cannot be visualized, and so go on and on with really abstract lines like (AB)C=A(BC), eA=Ae=e, A(-A)=e, etc., etc.,. But these things *CAN* be easily visualized, it just takes the slightest bit of creativity. It's easy to teach these things with pictures, where you're just interfacing with people's intuitive understanding, rather than trying to go through a difficult semantics/symbol layer.
I've taught young kids how to identify groups (think abelian); It's really not a problem, provided you have their attention.
If I need to know the proof of something, I go look it up somewhere that I know will have the right level of abstraction, and depend on me to know the real basics. This may involve looking up one or two subreferences, but they too will be more loosely stated. I don't need links to formal theorems that 2+2=4, thanks.
Where I see this having some applicability (and presumably the source of Wolfram Research's ire, cited above) is with machine understanding. To the extent that it is possible to make a machine "understand" higher mathematics through this sort of reductionism, an archive like this could be rather useful. I am pessimistic about this approach, though. Did anyone notice that there are no nontrivial results in the archive not pertaining to logic/set theory? That's because of the absolutely daunting amount of work in creating such a characterization.
I tremble at the thought of seeing, say, Wiles' proof of the Fermat conjecture in a form like this. No human mind could hold it all. So what use is this, really, to humans?
Has this book's copyright ever expired, and if so, did some unconstitutional law make it de-expire? The three volumes' dates of publication are 1910, 1912 and 1913.
Are there any jobs going that would require me to learn and apply this ?
For some people jobs aren't the motivational force in their life, I know it's hard to believe, but some people value knowledge and intellectual exploration over the pursuit of money.
That being said. Yes having a strong grounding in math does help with programming. Maybe no company would require you to learn and apply it (though I would run to a company that was more about research flavored things like this if I could), but it could make you a better programmer.
You summed it up nicely yourself. It does look like fun.
I'm the big fish in the big pond bitch.
From the site (to be precise, http://users.shore.net/~ndm/java/mmexplorer/mmset. html):
This is a particularly bad way of displaying mathematical formulae, because the meaning of the text depends in a very messy way on the layout (i.e., what font it is in). It shouldn't be the case that just looking at a formula in a different font renders it completely meaningless.
The pleasant way to use mathematical symbols online is using Unicode. The unicode character set, which is supported by all common web browsers including Netscape 4, contains all the symbols a mathematician could want (indeed, arguably, all the symbols anyone could want), such as GREEK SMALL LETTER PHI, RIGHTWARDS ARROW, DIAMOND OPERATOR, LEFT NORMAL FACTOR SEMIDIRECT PRODUCT etc..
If a browser doesn't have a particular symbol, the user will see a mark that shows that a character is missing. What they won't see is characters which are semantically different, like "R" instead of RIGHTWARDS ARROW. If the user saves the page as a text file, the maths symbols will still be present and retain their meaning.
For more complicated mathematical expressions, the way to go is MathML. However, since most browsers other than Mozilla can't support this yet, though you may be able to get plug-ins. Nevertheless, anything has to be better than encoding semantic information through font choice.
perl -e 'fork||print for split//,"hahahaha"'
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.
Programmers are not automatically smarter than
non-programmers. Programmers can often be thick
as two short planks.
Speaking as someone trained as a physicist and
working as a programmer, it's a real mistake to
underestimate those from the diametrically
opposite disciplines.
K.
-
-- Proud descendant of semi-nomadic cattle-herders.
"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!
The point was that if they aren't concerned with utility, it doesn't matter to them whether the problems they solve allow nuclear reactors to be designed, have no apparent use, or improve network communications - it's just another meaningless, but interesting, puzzle. While they shouldn't necessarily be concerned with applications themselves, they should be making their solutions as easy to absorb as possible for those who will make practical use of it.
To me, "you should pay me because someone will probably come up with a use for what I do, even if I don't know what" is a lot more acceptable attitude than "you should pay me because I am doing something that I appreciate aesthetically, despite the fact that you don't understand it and thus can't appreciate it, because of your bad taste and low intelligence."
I agree that every branch of math that solves new problems (no matter how abstract) is likely to have applications, but that doesn't excuse hostility to application-centered minds, which I see implicit in the structure of educational materials. Applied math isn't naturally as hard as they make it, by teaching it through proofs.
They are producing new math, which is good, but they are obfuscating it and the old math (into forms suited to the purposes of researchers, not students or practical users), which is bad. We should take care to only allow the good out, and thus maximize their utility, because they don't care to do it themselves.
---
This is like saying the best way for newbies to understand a C++ program is for them to decompile it and look at the assembly!
The choice of title for this story, "Learn The Language Of Math," was unfortunate and was the Slashdot editor's, not mine. Indeed I say "Metamath does not claim to teach you mathematics, just as reading the kernel source code does not teach you how to use Linux" which directly contradicts the title.
Metamath is definitely not for everyone and is no substitute for the normal way one normally learns mathematics. It is meant to amuse you, amaze you, and possibly enlighten you in its own special way. I thought it would be of interest to Slashdot readers. Come on now, wasn't it?
People interested in formalization and verification of math should also check out Mizar, which has vaguely similar goals but (IMO) requires a higher degree of mathematical maturity to be able to follow its proofs. It tries to mimic mathematical proofs they way they are normally published, whereas Metamath is more like a machine language showing you every nitpicking detail. On the other hand Mizar has many contributors and its scope is much broader. Mizar is a language intended for real mathematicians, not armchair ones.
I see a lot of overlapping work with Symbolic Computation Group's Maple.
There really is little overlap. Maple and Mathematica have no concept of mathematical proof. They are tools that help you generate mathematical results, but they do not verify them rigorously -- you are at the mercy of whoever wrote the specific modules being used, and there have been some glaring bugs in the past. A "bug" is impossible with the Metamath scheme, unless you state your starting axioms incorrectly. And they are limited. For example they cannot derive existence results that depend on, say, the Axiom of Choice.
Congrats... We've been spammed. Instead of mentioning money to get our attention, "Linux" was the repeated hook. Gee Norm, If you're going to pull the wool over the Slashdot community's eyes, the least you can do is post anonymously.
I made no attempt to hide the fact it is (mostly) my project. I put my name as the author of the story and my name is on the web site. Is there a rule that says one can't discuss one's own work? It should be considered on its own merits, perhaps more suspiciously than usual since I am the author. I certainly derive no financial benefit from my site. I mean, is it really worse than the stories that tell you how to hack a ball-point pen?
As for Linux being the hook, I think the kernel source code analogy is a good one, to suggest specifically that Metamath is not the best way to learn math (contrary to the story's unfortunate title). Instead it is like exposing what is under the hood, very analogous to seeing the source code for a program that otherwise is like a black box.
MetaMath people, how about putting some smegging commentry and discriptions on the proofs. Plus why not have each symbol hyperlink to its definition. Its in hypertext so why not use.
I attempted to put a meaningful comment in each of the 3000+ theorems, with cross-references to textbook theorems and exercises whenever I could find them. The textbooks should be the real source if you really want to learn at a high level, and the Metamath proof a supplement in case you get stuck. Metamath is not intended to be a stand-alone teaching tool, although a few people seem to have attempted to use it as such. As far as commenting the proof steps, they are unimportant other than to demonstrate how the theorem was arrived at; by drilling down you can convince yourself to any degree of satisfaction. As far as symbols, there is a "syntax hints" underneath each proof that explains them.
The pleasant way to use mathematical symbols online is using Unicode.
Thanks, I will consider this. A few years ago when I started this Unicode was not supported by most browsers.
--Norm Megill
--
"May the forces of evil become confused on the way to your house"
--
"May the forces of evil become confused on the way to your house"
-George Carlin
Alright then, I assume you know the definitions of continuity, limit/cluster points, compactness, and the statement of the Heine-Borel theorem. Prove the Heine-Borel theorem for me without reference to texts. I'll give you a hint -- there's not a great deal of "lateral thinking" involved, just use the stuff I've already mentioned (unless you want to drop down to set theory first...).
Maybe you're so super-smart that you'll get this "easy" proof straight away. It took me two weeks, and was anything but easy. It was gratifying, though. =-)
-Paul Komarek
"After all, much of what mathematics is really about is building abstractions on top of each other."
I will have to disagree with that point. Mathematics isn't about building abstraction on top of abstraction, but finding the simplest abstraction posible for a given concept. Any single topic in mathematics is worth a semester to study, but if you spent a whole semester studying one proof it must not have been that elegant.
bash-2.04$
bash-2.04$
bash-2.04$yes "Don't you hate dialup connections?"| write USERNAME
I don't mean to speak for the creators of Metamath, but I think the coolness of their project has little or nothing to do with pedagogy.
-Paul Komarek
- It would allow you to really check your new earth-shattering proof. No more working on one for years, presenting it to the world to great acclaim, and withdrawing it a year later because somebody finds that tiny flaw (as has happened to one of the Ferma's proofs). Instead, just feed in your result to the database, hit "verify", and presto! a clear yes/no answer (and a pointer to the problem step in the proof if its a "no"). Keep in mind *verifying* a proof is trivial work for a computer - it is coming up with one which takes genius.
- It would also make it easier for you to construct new proofs. The computer would be able to automate much of the "dirty work" involved. Yes, math is an art but even in the most inspired proof you have to laboriously construct proof steps which are "obvious", boring, and vital (for ensuring the proof does indeed work). A computer would be able to fill these in for you, using a not-that-bright theorem prover. Everyone doubting the usefulness of this should ask grad math students about the assignments they get from their professors - physicists too, coming to think of it
- You could also use spare CPU cycles globally to look for proofs for interesting theorems - something along the lines of the seti@home project. Brute force *does* work, if you have enough of it... and, of course, it would give the AI people a wonderful playground for trying out their stuff. This is a much tougher problem then chess - but a much more useful one to solve.
Of course, it would be a whale of a project. It would take some serious commitment from math departments... So the best way is to start with some specific sub-field of math, which the Metamath people have done. Moaning that this isn't "all math" yet, or that it isn't "the most important part of math", is silly. You have to start somewhere. Their web site states they are already expanding the project to other fields.