A friend who has some nice programming skills has been working with me on a search engine for set.mm. We'd really appreciate any feedback if anyone is willing to check out the first draft which we've done, do you like it? Is it useful? Can you find theorems you look for? You can click on your name to see your author page too :)
https://metamathsearch.herokuapp.com/ Sometimes the page sleeps and so if you get 404 maybe try going to the link again some seconds later. There's a lot we can do to take it further if it's a good direction to go in. One of the main things is tuning the search to produce more relevant results. For example if you input metamath script it could be setup so that can be only compared to theorem statements and things to make it easier to track down theorems. We wondered about having discouraged theorems be marked in a special way and maybe having an advanced search feature where you can choose what to compare your input against (theorem name, comment, proof etc). Anyway all feedback welcome. There are also some hosting issues to sort out if this engine is appreciated and we'd like to have it around long term. It's fine for the next couple of weeks. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1b76111a-f2db-472c-9453-16ab04738e4a%40googlegroups.com.
