On Mon, 2011-02-28 at 19:37 -0700, Luke Palmer wrote:
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.
This was attempted to some extent in the Mowgli and HELM projects: http://mowgli.cs.unibo.it/ http://helm.cs.unibo.it/ The HELM project in particular is relevant. To whit:
First of all, having a common, application independent, meta-language for mathematical proofs, similar software tools could be applied to different logical dialects, regardless of their concrete nature. This would be especially relevant for all those operations like searching, retrieving, displaying or authoring (just to mention a few of them) that are largely independent from the specific logical system.
Unfortunately the related Coq and NuPRL searchable libraries seems to be down at the moment, as all implementation effort has been switched to Matita, which uses some of the Mowgli and HELM components. Thanks, Dominic