I have been wanting to gain a better understanding of interactive
theorem proving for some time. And I've often wondered: Can theorem
proving be made into a user-friendly game that could attract mass
appeal?
No.
I'd wage money on it. -- Colin Adams Preston, Lancashire, ENGLAND () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments