A friend of mine from grad school recently suggested a really good idea for a webtool on his blog (it’s a personal blog, so I won’t link there, but he can identify himself in comments if the urge strikes): one should be able to search for theorems based on hypotheses and/or conclusions. So that if you wanted to prove a representation was indecomposible, you could search for theorems where that was the conclusion.

Of course, such a thing would only be functional if it could produce this automatically, which would be a tricky business. On the other hand, computers aren’t as stupid as they sometimes seem. If they can do machine translation, they should be able to do this (eventually). Any Googlers out there looking for something to do in their 20% time?

### Like this:

Like Loading...

*Related*

I think that the part of this that’s within reach without a difficult software idea is to isolate statements of theorems for keywording. Also, if a theorem is restated many times, you could use a clustering algorithm in the space of sequences of words to find a “most standard” statement of the result. A clustering algorithm could also be useful to partition the set of statements of theorems into approximately distinct theorems.

Forget blogs, I want mathscinet to do this! For that matter, wouldn’t it be great if math papers were written in WEB (or some variant), so that running LaTeX on a file gave you the .dvi, and running some other program on the same file gave you a formal statement of the main theorems e.g. in HOL light. Plus I’d also like a pony.

Danny, could you elaborate a little? I think anything called “WEB” is officially ungoogleable.

Ah, I spoke too soon. Wikipedia to the rescue again: http://en.wikipedia.org/wiki/WEB

Of course ideally we would have formal versions of the proofs too.

I thought about this, too.

My first idea was to start slowly, writing macros for LaTeX which generate unique identifiers for theorems, definitions and proofs, so that you can quote some statement and link directly to it (not just to the entire document). of course, this involves some kind of online math library, too.

there are some wiki-based approaches out there – does anyone of you use such a thing?

I would really want to add to my LaTeX theorems some formal header which states which theorems in the WWW it does depend on.

Best Regards,

Konrad

Hmmm… you are all ignoring the reason the web grew in the first place. It was (is) ugly, it was (is) full of mangled code, misspelt words, and had enough blink tags to make a grown man cry.

Yet the learning curve was pitifully easy. Any fool could knock up a web page; learning the very basics of HTML didn’t require serious effort. Contrast with all efforts to impose a more structured, correct framework. XHTML is still only for professionals and geeks; the semantic web is still light-years away.

In mathematics, we may be fortunate in having authors who value precision. But nevertheless, if you try to impose uniformity in theorem definitions etc from on high, it will fail.

a-

Who proposed imposing uniformity from on high? And who are here is on high enough to even contemplate that? We just said it would be cool if people started using existing tools to make their math papers more accessible to searching.

Incidentally, one of the other reasons the web grew in the first place was that people produced programs smart enough to make sense of the tons of seeming haphazard data. Hopefully someone can do that in this case too.

I should clarify: I was referring to the comments referring to formal proofs/papers in WEB/inline metacomments etc. rather than the post itself.

Sure, some good citizens will take the “technically correct” path – maybe the AMS can come up with a shiny logo they can put alongside the W3C one on their webpages! But they will be completely drowned out by those that don’t.

I think it’s more important to come up with some way of reliably searching through LaTeX. When trying to search (for example) differential equations, it’s very laborious.

When I had suggested this idea, I was surprised no one had at least done a rough hack. Mathematicians label their theorems with just a few terms (Thm, Cor, Lem, etc). Those statements generally use a handful of forms (“if… then…”; TFAE; and others). Even if all they did was just sweep through math articles looking for these forms and then copy whole portions of text into “hypothesis” and “conclusion” fields, that would be a lot better than now. Sure there would be tons of inaccuracies, but it’d be a smaller pool to search through to at least get your investigations started. Google Scholar assumedly already has a list of math journals, so how hard would this rough hack be to do?

This type of thing is currently being worked in the computer science field.