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."

Comments

Not my cup of tea

[Spling]

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.