[Haskell-cafe] ANN: theoremquest-0.0.0

[Tom Hawkins]

> 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).

Theorem search is one of my main motivations for a multi-player,
centralized database architecture.  With two people plugging away at
different problems, I have to imagine occasionally they develop lemmas
that could benefit each other.  Of course the search could be
googlish, where one would enter a desired proposition and it would
return a handful of matching candidates.  It could also be automated.
For example, each theorem submitted to the database could be checked
if, a) any assumptions of the theorem are already proven, and b) any
other theorem call it out as an assumption.  Then these reductions
would be perform automatically.  The greater the ability of the search
to bridge the gap between dissimilar conclusions and assumptions, the
greater the automation.

Thanks for your interest.  Let me know if you have any suggestions or guidance.

-Tom