Just a brief note about the results produced by looking up a tag on the query page. If the tag you’re looking up points to a lemma, proposition, theorem, remark, example, exercise, situation, or definition, then the search will also return the latex code of the corresponding environment. Here is are two examples to see what it looks like. Enjoy!

Of course eventually we’ll want to render the latex directly (I prefer not do this until there is a good way to render diagrams coded with the xypic package). But in some sense seeing the latex source is better: it tells you the latex label for the result, and it allows you to copy and edit the latex source directly and email me your improvement. It would be trivial to have the page also print the proof (in case the tag points to a lemma, proposition, or theorem). Let me know if you think this is a good idea.