Metamath html revamped
I’ve been doing a lot of mathy things recently, and one of them has been playing with Metamath, which is step by step formalizing a whole bunch of mathematics. You can see what real numbers really are, how recursion and induction can be defined using only basic set theory, what a function really is, and a million other neat things. It has proofs for all of its theorems that can be verified by a very simple program, or by hand if you like. It’s just a whole bunch of substituting A for B and matching.
The only problem with it is that it’s kind of low-level. It’s hard to follow the proofs and even sometimes the definitions. Now, on the one hand, it’s probably good to become more fluent in formal mathematical language if you want to learn a lot of math. But on the other hand, part of the difficulty I was encountering was entirely avoidable, due to not including enough information about the proof when it’s displayed. In particular, to know what substitution is being made at any given point, you have to open the theorem being used at that step, and then go back to the proof. If the theorem is quite large, you might have to go back and forth quite a bit to get it in your head enough to understand what’s going on. And further, for very long equations, it can be completely impossible to do this in your head.
So I made it all happen on the screen, right there in front of you. Proofs still aren’t easy to follow, but they’re quite a bit easier than they were. Perhaps as easy as they’re going to get with Metamath. We’ll see if I get any better at reading them now. (By the way, this is done along with shrinking the site quite a bit by having it all done in javascript.)
Unfortunately, I don’t currently replicate all of the features of the Metamath site, since that would be hard and kind of boring. So you need to really start here, and then type in http://pdf23ds.net/projects/Metamath/theory-name.htm when you have a theorem whose proof you want to follow.
I invite your comments.
March 13th, 2009 at 15:35
It is a great idea to show the substitutions and it really improves readability of short proofs. For longer ones however I have a trouble figuring out what happens when I click on that magnifying glass. When the glass is yellow I clicking on it hides some lines. When it is white and I click on it sometimes I see more lines of proof, sometimes less. What is the rule here? What is the “semantics” of clicking on the magnifying glass when it is white?
It took me some time to notice that magnifying glass. I kept looking only because I knew something must be here to click. It would be helpful if you put some small “click on the [magnifying glass symbol] to see substitutions” or something like that.
Also, typically when I look at a theorem I expect hypotheses, assertion and the proof. Here I can see only the hypotheses and the proof. I guess the assertion is kind of redundant for Metamath, since it is in the last line of the proof. However, it would be better to shows it just like the original Metamath presentation does.
March 13th, 2009 at 16:40
Clicking on a non-highlighted magnifying glass will show all of its hypotheses and hide the hypotheses’ children. So if a hypothesis has child hypotheses that are expanded, they will be hidden. I have it do this because otherwise you’d extra lines between the hypotheses of the highlighted step that put them further away from each other and make it hard to read the substitutions being applied.
Thanks for the feedback.