Check out http://www.zachtronicsindustries.com/. Those games take the essence of what makes programming fun and turn it into a game. Spacechem is not free but the other games are. They do get fiendishly difficult though.

The slider where you can select what scores should be shown as full, abbreviated or hidden has a little bug/typo. The score track goes 5 4 3 2 2 0 -1 making me wonder what happens with comments with a score of 1.

There are two good examples of this. A lot of people don't believe that 0.999999... (infinite repetition) is equal to
1. Even if you prove it to them they remain convinced that there is a similar argument showing that they are unequal. Another example is the monty hall problem which is famous for even tricking many mathematicians.

Actually there is. The reason why a comma is used as a decimal separator in some places is the following. The decimal separator is more important
that the thousands separator, a misplaced thousands separator doesn't matter since it has no effect on the value. Now a speck of ink is more easily mistaken for a dot than a comma. It would be bad to mistake a speck of ink for a decimal separator.

Some people have argued that because the dot is more important for sentence structure it should also be used for the more important decimal separator. However this isn't a very strong argument since there is no reason to use grammar rules for the notation of numbers.

That said, personally I use a dot since I need the comma to separate lists of numbers (e.g. 1.2, 1.3, 1.4 ) and the comma notation for lists is almost
universal.

This is just plain wrong. Even the ancient greeks knew that the earth was spherical. This has been the dominant scientific position for a long time. The wikipedia article on it is quite good flat earth.

No, in general formalizing a proof does not require a lot of computer power. Usually it takes a lot of man power instead. Most current proof assitants are actually proof verifiers. The user has to break down the proof to elementary steps that the program can verify.

Now sometimes a computer is used to verify a lot of cases by brute force computation. Often this is not done in an actual proof assistant but within a computer algebra package. But this is also met with a sceptical eye.

The four colour theorem is perhaps one of the most famous formalized theorems. It was orginally proven by a large computation. But noone could really verify this. Recentely (2004) it was formalized completely in the proof assistant Coq (actually a custom extension). This formalized proof did require a lot of computer time allthough just on a normal computer, not a supercomputer.