Jason (jcreed) wrote,
Jason
jcreed

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.
Tags: formal systems, math, root 2, web
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 7 comments