Math Pattern Language

There is a common perception that MathIsHard. The idea here is that whether or not this is true, math can be made more accessible if we explain, not just the meaning of its symbology and results, but the way mathematicians go about constructing it. The common forms of the culture of mathematics.

There are excellent books on this, of course. But none that I know of use the PatternForm that has proved so useful in software and physical architecture. Since, after 3 years of undergrad pure math + a couple decades dabbling + 1 intensive but highly unorthodox multi-year mathematical exploration I am at best a math dope, and at worst a math illiterate, I won't presume to specify what patterns should be in a MathPatternLanguage. I trust someone here will.

Good idea. Some people will say it's already done, and point to e.g. Polya, but I think your idea could be taken in some interesting different directions. For instance, Diagonalization is a major pattern in math that we discussed earlier today, and it is a branch of another major pattern, PigeonholePrinciple?, all of which are counting arguments. Then there's what one book called Bypasses, which is to take something into a different space temporarily, making certain things much easier (TAT^-1), for instance, taking something to the Fourier domain, multiplying, and coming back out of the Fourier domain is an efficient way to do, well, zillions of things, such as convolution and filtering. The general idea is definitely a pattern with applications all over the place.

It's worth mentioning that CategoryTheory is, in fact, a PatternLanguage, created by generalizing, abstracting, and unifying things that are done in all areas of math, resulting in THINGS with ARROWS drawn between them, which turns out to cover an inconceivable amount of ground. Morphisms are a basic pattern. -- Doug

I've touched on CategoryTheory but I believe I have something different in mind. Thinking of a pattern as a trusted solution to a common problem, I'd hope to see patterns like:

My thought is that, just as OOAD once was, the language of math is inaccessible because of its granularity and grain. If we had a GOF book for math, not to mention a UMLish diagrammatic format for proofs, maybe we'd find that MathIsEasy.

[[Well, in terms of concrete suggestions, I would suggest we go somewhat the other way, and design a totally formal language in which completely formal, totally rigourous, proofs are given, accompanied by a dynamic browser that shows only the top level of such proofs, with a great deal of psychologically motivated syntactic sugar in which the pure logical form is still easily accessible, and can be queried for more detail wherever something is not obvious to the reader. This may not work, but I think this is one very important direction that should be tried. This is one aspect of the so called "Qed project", which has more or less lain dormant for years now. I intend to do some work in this direction myself when I get the chance by starting with HOL-Light and attempting to add a simple proof browsing mechanism. Some folks are planning to augment DrScheme with something they call DrHol? which has some aspects like this.]]

It's a perfectly reasonable thing to do, but one must take great care to note which goals would and would not be achieved. Rigorous, formal proofs are obviously important in math. They are also formally and rigorously equivalent to string rewriting, e.g. via semi-Thue grammars (automated proof systems such as the famous Boyer-Moore prover are formally equivalent to such). Is string rewriting therefore what mathematicians do? Mostly no; mostly mathematics is about insightful thinking, something which is not present at all in the string rewriting.

So if you want something oriented purely towards proofs, that's one thing, but you should be very clear that such a thing inherently would not address assisting people to learn mathematical thought. Personally, I think that all of the historic emphasis on proofs is simply because it can be taught, whereas no one has a clue how to teach thinking, so everyone just hopes that learning to prove will lead to learning to think, and in a tiny number of cases, that does in fact happen. -- Doug

[[You can think all you want, but what you are thinking about in mathematics is how to find proofs. And note that a large part of the talk above was about reading mathematics not doing it (in the sense of finding proofs on one's own). As for what "such a thing" would not be able to do, you simply assert that. I disagree. You can wait around and see how much advance is made in this area in the future. And the Boyer Moore prover has none (or very little, at the most) of the things I was talking about in it, has an awkward logic, and was not even designed for the kind of thing I am talking about. Something like Mizar is a lot closer in its concern for a natural logic and a readable interface, but it's interface is not at all dynamic]]

What??? Now that's getting really weird. Proofs are important to show that thinking is correct. Proofs without thinking, without understanding, actually are not important. Thus proofs are not the point of math, they are merely essential, which is different.

Also, as has often been noted in the mathematical literature, most proof published in refereed math journals is closer to proof sketch than to truly rigorous proof. That's always been true, because that's the most effective way to communicate to other mathematicians. It's also a bit error prone, which annoyed the hell out of Bourbaki, so they tried to improve that, but it's still a matter of degree. Almost the only time a truly 100% complete and rigorous proof is done is in fact when a software prover is used, since it can't skip "obvious" steps.

And as for Mizar vs Boyer Moore or whatever, that utterly misses my point: all such things are formally equivalent to semi-Thue grammars. Research mathematicians, however, have gone on the record any number of times, quite angrily denying that all they do is string rewriting. -- Doug

[[No they aren't. Geez. But as for what you actually tried to say, all mathematical theories are also recursively isomorphic to the Halting Problem. Big deal. That point is totally irrelevant in this context. As for what will happen with how formal proof systems end up aiding understanding when developed with that goal in mind, you will have to wait to see what people actually working on this achieve]]

No no, that is far from my point, although that paraphrases the semi-Thue part, yes. The point is about formal math, which is just string manipulation (or TuringEquivalent or whatever you like), versus mathematical thinking, which is not any of those things. We understand the one, but not the other. Cognitive science is still a young field. We don't know quite what thought is, let alone mathematical thought, and yet we'd like to teach mathematical thinking. The lack of understanding is a barrier.

P.s. re: your "geez" -- I guess you are not aware that those mathematicians were responding to people who said in all seriousness that all mathematical thought is just string rewriting.

The comment about not skipping obvious steps reminded me of a story. A mathematics student is doing an exam, and try as he might, he cannot prove a particular theorem. He tries solving from both ends of the problem, and all looks good to start with, but he cannot 'join' the two sides of the logical steps together. Eventually he gives up and writes out the two parts of the proof, putting 'which is trivially' in between them. When the student gets his paper back it is graded A, with a C grade scrubbed out. In the middle of his proof is written, "At first I wasn't sure that this step was trivial, but then I realised it was."

See also: CategoryMath, MathPatterns

EditText of this page (last edited April 1, 2006) or FindPage with title or text search