On 28 February 2011 17:59, Jesper Louis Andersen <jesper.louis.andersen@gmail.com> wrote:

Many "normal" puzzle games fit into the NP-complete class as well, so
it would look as if human beings like the challenge of trying to solve
hard problems. Theorem proving is simply yet another beast in the zoo,
underpinning the other games.

Cale Gibbard once argued that programming is essentially a form of theorem proving. And people love programming as a hobby, so I can see that taken to its "logical conclusion" (groan) of actually solving proofs. Could there be a ProofOverflow? Tee, just joking. I think.