On Mon, Feb 28, 2011 at 7:59 AM, Tom Hawkins
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?
I think this is an interesting project. This kind of thing has been on my mind recently. I haven't necessarily been thinking about how to "publicize" theorem proving, but I have been thinking about how to use computers to coordinate the efforts of mathematicians (including mere hobbyists like me). While our goals are not identical, they are certainly related. I was set on creating my own language for a while that would facilitate this, because I'm that kind of hubristic fellow. But I realized that it would probably be a better tactic to use an existing, more popular system, since I can leverage the existing work of others for a basis, and others already know their way around this system. It's easier to get critical mass starting from a few hundred than from one. But what I miss when using these proof assistants, and what I have my eyes on, is a way to Search ALL The Theorems. In current proof assistants, developments are still distributed in "packages" -- and a particular development might have already proved a very useful lemma that wasn't the main result, and if I'm doing something only barely related I will probably not find that package and have to prove that lemma again. I hope that a *good* theorem search engine would bump the level at which I do computer-assisted mathematics to nearly the level I do math in my head (conceptual, not technical). That may be a pipe dream. A theorem search engine I would consider "good" would have to solve a few technical problems: a big one is recognizing isomorphisms -- two people declared isomorphic structures and then proved some different results about them. We would like to be able to search for results about one and find results about the other. This is probably assisted by a user who proves the isomorphism between the two structures -- inferring isomorphisms automatically is probably too much to hope for. And then there's the issue of the highly overloaded word "isomorphism" -- there is no single definition, and results can be interchangeable in different ways appropriate in different contexts with different subtleties. Suffice to say I think your project is cool and I have my eye on it. Have you thought about searching? Luke
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe