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? And if so, could a population of gamers collectively solve interesting and relevant mathematical problems? To try to answer these questions -- and to gain some experience myself with theorem proving -- I started a project called TheoremQuest [1]. TheoremQuest intends to be a multi-player game system, where the game server receives requests by clients, such as theorem queries and inference rule applications. The TheoremQuest server validates deductions, compares them with existing theorems in the database, then returns results. TheoremQuest's deductive system borrows that of John Harrison's HOL Light [2]. There are 2 Hackage packages: theoremquest [3] is a library that declares types for terms, inference rules, and client-server transactions, used by both server and clients; and theoremquest-client [4] is an example client (tq). All the code, including the server-side, is hosted at github [5]. Currently the client-server interface is working, but little else. The library has defined most of the core inference rules, but has none of the basic types or axioms. And the "tq" client is nothing at all like a game; at this point it is just a command line tool to test the server. Currently "tq" can ping the server, create a new user, apply inference rules, and print out theorems. Here's how "tq" can prove "x |- x": $ tq newuser tomahawkins tomahawkins@gmail.com Ack $ export THEOREMQUEST_USER=tomahawkins $ tq infer 'ASSUME (Var (Variable "x" Bool))' Id 1 $ tq theorem 1 assumptions: Var (Variable "x" Bool) conclusion: Var (Variable "x" Bool) I'd love to have help with this project, if anyone's interested. I'm still grappling with the logical core, but I think the real challenge will be creating game clients that are both capable and yet intuitive enough to appeal to the general population. If the masses can play Sudoku, shouldn't they be capable of interactive theorem proving? -Tom [1] http://theoremquest.org [2] http://www.cl.cam.ac.uk/~jrh13/hol-light/ [3] http://hackage.haskell.org/package/theoremquest [4] http://hackage.haskell.org/package/theoremquest-client [5] http://github.com/tomahawkins/theoremquest