May 8th, 2006

beartato phd

(no subject)

I've been reading "MacLane's Categories for the Working Mathematician" today because I was trying to find out how the proof of the Coherence Theorem for strict monoidal categories goes, and holy crap is there a lot of stuff in that book that makes so much more sense now. Freakin' everything is a monoid object in a suitable monoidal category. Categories themselves? Monoid objects in <O-Graph, ×O, id>. Monads? Monoid objects in <CC, ∘, id>. Rings? Monoid objects in <Ab, ⊗, Z>. And if it's not a monoid object, it's the action of one. Modules are actions of rings, suitable group actions are torsors, monad actions are T-algebras, which themselves include the remainder of the usual zoo of algebraic structures like semigroups, groups, etc.

This is a nice page full of HTML entities for math symbols: http://en.wikipedia.org/wiki/Mathematical_HTML
beartato phd

(no subject)

Freek Wiedijk has some interesting pages on the web. Here is a comparison of various theorem provers; the litmus test is proving the irrationality of the square root of 2. Here are some other miscellaneous notes about automated reasoning and verification.

The thing about root 2 being irrational also mentions an extremely "visual" proof of it. Imagine towards a contradiction that somebody gives you a big square of side length B, and two congruent little squares of side length L, and claims that the sum of the areas of the little equals the area of the big, and that B and L are integers. This would mean of course that root 2 is B/L. Now stare at this diagram:
        B
/----------------\
+-----+----------+
|.....|::::::::::|
|.....|::::::::::|
+-----+----+:::::|
|:::::|####|:::::|
|:::::|####|:::::|
|:::::+----+-----+
|::::::::::|.....|
|::::::::::|.....|
+----------+-----+
\---------/
     L

If we put one of the little squares in the lower left corner of the big, and one in the upper right, they overlap a bit. (Otherwise, each would be at most 1/4 the area of big, and that couldn't work, because 1/4 + 1/4 < 1!) Indeed, if the sum of their two areas is going to sum to big, then the amount that they overlap (the ### region) has to exactly fill in the area not filled by the littles (the ... area). But both of the ... regions are also little squares (though it's not apparent from the bad ASCII art, sorry), both the same size, (namely, B - L) and their areas sum to the ###, a square of size L. So we have obtained smaller, yet still integer-sided squares, that satisfy the same property that our original ones did. We can repeat this property endlessly, creating arbitrary small positive integers, a contradiction.