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