[Haskell-cafe] ANN: theoremquest-0.0.0

[Luke Palmer]

On Mon, Feb 28, 2011 at 7:59 AM, Tom Hawkins <tomahawkins at gmail.com> wrote:
> 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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>