MetaMath Search Engine

Jon P

unread,

Jun 22, 2019, 10:21:41 AM6/22/19

to Metamath

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.

David A. Wheeler

unread,

Jun 22, 2019, 11:14:05 AM6/22/19

to Jon P, Metamath

On June 22, 2019 10:21:41 AM EDT, Jon P <drjonp...@gmail.com> wrote:
>
>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

Cool! I have one immediate feedback, you need to add web fonts. On firefox on android, and probably many others, symbols like turnstile don't show up. And that is a problem.

The good news is that doing this is essy. You might check out how metamath.org does it. You just have to note it in the html (or css) header and put the web font on your site. (Do not just load it from an external site using your html, because that enables unauthorized tracking. It is much better to host your web fonts yourself.)

--- David A.Wheeler

David A. Wheeler

unread,

Jun 22, 2019, 11:18:15 AM6/22/19

to Jon P, Metamath

I like the idea, but I think you might want to improve how you sort for likelihood. I searched on 2+2 and did not get an exact match in first few dozen teturns. I think more exact matches should show before less exact ones.
--- David A.Wheeler

Jon P

unread,

Jun 22, 2019, 11:55:43 AM6/22/19

to Metamath

Hi David, thanks for the response :)

Re results we are using ElasticSearch and so we should have a good amount of leeway to optimise the results. I guess the best result for 2+2 is 2p2e4. We're still experimenting with how much to search the comments and theorem names and how much to search the assertions. There may need to be some way for people to specify they are searching the assertions, such as using |- maybe.

Re fonts we are a little confused (we don't have so much frontend experience). Is this the font you mean that could be hosted? https://github.com/alif-type/xits On Metamath.org it seems to call that font at the beginning however it also seems to be commented out which is a little confusing.

Giovanni Mascellani

unread,

Jun 22, 2019, 1:15:56 PM6/22/19

to metamath

Hi,

Il 22/06/19 16:21, Jon P ha scritto:

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

The idea is undoubtedly wonderful (and demand for Metamath searching
tools is definitely less than offer, for the time being), however, like
DAW, I also find that results are not what I would expect from the query.

Also, a fantastic thing to have would be a matching that know how
Metamath work, and for example is able to replace variables, or match
subtrees of formulae. Of course that would be much more work than just
throw the Metamath database into a stock searching engine. Or maybe not,
I have no idea.

But please do not interpret my remarks as discouraging: it is very nice
to have someone working on this and I am sure that with some work this
can become a very valuable tool.

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

signature.asc

David A. Wheeler

unread,

Jun 22, 2019, 2:42:11 PM6/22/19

to metamath, Metamath

On Sat, 22 Jun 2019 08:55:43 -0700 (PDT), Jon P <drjonp...@gmail.com> wrote:
> Re results we are using ElasticSearch and so we should have a good amount
> of leeway to optimise the results. I guess the best result for 2+2 is
> 2p2e4. We're still experimenting with how much to search the comments and
> theorem names and how much to search the assertions. There may need to be
> some way for people to specify they are searching the assertions, such as
> using |- maybe.

Sounds reasonable. I think if a conclusion matches exactly it should rank high,
but tweaking sort results is complicated :-).

> Re fonts we are a little confused (we don't have so much frontend
> experience). Is this the font you mean that could be hosted?
> https://github.com/alif-type/xits On Metamath.org it seems to call that
> font at the beginning however it also seems to be commented out which is a
> little confusing.

I suggest looking here for an example:
http://us.metamath.org/mpeuni/2p2e4.html

The key is this in the style:
@font-face {
font-family: XITSMath-Regular;
src: url(xits-math.woff);
}
.math { font-family: XITSMath-Regular }

Of course, now you need the file xits-math.woff at
that directory. You can get a copy from the Metamath site.

More details here:
https://developer.mozilla.org/en-US/docs/Web/CSS/@font-face

I suggest testing with Firefox; Firefox is pickier about font locations
(for security), so if it works with Firefox it'll work with anything.

Setting up the fonts takes a few minutes, but it'll mean that
the text will work almost everywhere.

I just noticed that we *only* specify a url source in Metamath.
We might want to add a local(...) to the src options, so that
people who already have XITSMath-Regular installed will just use that.
It's a minor optimization, but it'd be nice for first-timers with
poor bandwidth. I'll have to track that down later.

--- David A. Wheeler

P.S., here it is in a larger context:

<STYLE TYPE="text/css">

</STYLE>
<STYLE TYPE="text/css">

</STYLE>

Glauco

unread,

Jun 22, 2019, 7:51:12 PM6/22/19

to Metamath

It really looks a promising new tool for metamath addicted :-)

A couple of remarks:

- I have to input '-cn->' to find -cn-> related theorems

- if I input

limCC '-cn->'

the search engine works in AND (cool!) but the top few results don't contain limCC (I have to scroll down a bit to find theorems containing both constants; but those theorems are actually relevant!)

If you are going to tweak it a bit, and maybe add the advanced search feature you mention, it's definitely going to be a tool I will use a lot.

Glauco

p.s.

I use regular expression search with labels a lot, you may consider adding it to the "advanced search" mode; for instance

lemul\w*

finds a lot of useful theorems focused on <_ and x.

Tony

unread,

Jun 24, 2019, 4:58:10 AM6/24/19

to Metamath

I searched for "∃z z=y". Nothing relevant was found.

Norman Megill

unread,

Jun 24, 2019, 9:31:10 PM6/24/19

to Metamath

Nice work!

Thanks for fixing "MetaMath" -> "Metamath". :) (The former sometimes gets confused w/ Chaitin's book.)

I agree w/ David that the XITS web fonts would look nicer, and it would also match the main site..

One problem with infinite scrolling is if there are many matches, it can be frustrating to have to press "end" over and over, not knowing how many are left, until it finally gets to the bottom. Unless you're just casually sampling the theorems, It is often important in Metamath to see all of the matches to determine the one you need.

Suggestion: Can the number of matches found be shown at the top of the page? Perhaps have a sequence number next to each match so you know how many you've loaded and how many are left? Could there be a button or hot key that will load all matches?

Norm

Jon P

unread,

Jun 28, 2019, 10:34:28 AM6/28/19

to meta...@googlegroups.com

https://metamathsearch.herokuapp.com/

Thanks for all the feedback. We've been working a way on tweaking the search results. We're working on optimising the search results right now, and we've uploaded the latest batch of improvements. Searching the comment text is pretty good and the theorem names are easy to match (you can try searching theorem names to see if it gets it right). Trying to match the mm code is harder, it's difficult to work out how to get it to understand enough about the sort of thing you are inputting to get useful results.

Have a go with the new version if you are interested, try putting mm searches in quotes, that seems to help things match pretty well. If you want to tweak the search yourself you can, you can right click on the page, save the source and then edit this section

bool: {

should: {

multi_match: {

// type: "best_fields",

query: query,

// default_operator: "AND",

fields: [

"name^4",

// "usage",

"source^2",

"proof^2",

// "statementNumber",

"comment^2",

"contributor",

// "date",

"statement^10",

"hypotheses^2",

// "optionalHypotheses",

// "requiredVariables",

// "allowedVariables",

// "containedVariables",

// "disjointPairs",

"html.comment^2",

"html.comment.metamath^2",

// "html.syntaxHints",

// "html.axioms",

// "html.dependencies",

// "html.usage",

"html.hypotheses^2",

"html.statement^2",

"html.proof^2",

],

boost: 100,

}

},

to change the weight given to different parts of the search.

To get a really good search we may need to index everything differently however that might be too far for us at the moment. I think it's working decently now so would be interested if people use it at all when actually trying to prove something.

Norm re fonts and total results return those things seem pretty doable, we just haven't got round to them yet :)

We've hosted the search on a free trial for another week or so, if anyone thinks it's going to be useful to you then we can talk about how to get it hosted more permanently.

Alexander van der Vekens

unread,

Jun 28, 2019, 11:12:15 AM6/28/19

to Metamath

I just tried the new version looking for "cramer". Unfortunately, only the first 5 results contain the string "cramer", but the following neither contain that sting exactly, nor something similar (or what is similar to "cramer" in the entry for theorem "imp"?).

On opening the "strange looking" entries, however, I guess why it is found: the theorem imp, for example, is used in the proofs of theorems cramerimplem1 cramerimplem2 cramer !

Maybe the search criteria and the sources of the search should be described at the top of the page, so that it is clear for everybody why certain results are shown.

Reply all

Reply to author

Forward