Jason (jcreed) wrote,

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:

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.
Tags: formal systems, math, root 2, web

  • (no subject)

    Had a good bunch of discussions with Sean and Alyssa at work. Supposed to be stupid hot this weekend when we were planning to do the final cleanup of…

  • (no subject)

    Started moving some stuff into the new place in Astoria! Basically just books, but pretty much all our books made it there. Made a Zipcar reservation…

  • (no subject)

    Got lease signed! Movin' to Astoria imminently, I guess. Restaurant situation seems incredibly good over there.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded