Idea: Resource to avoid publishing something someone else published

Question

Researchers often prove theorems but they don't know whether somebody else already published the same result.

One strategy is to read papers on the topic or search keywords, however it would take way too long to read all the papers on one's subject and some of them might not even be accessible (e.g., one might need to buy a journal in a foreign country).

So it would be great if there is one resource which indexes papers with their results. The results would have to be written in an universal language. Many results in Math and CS can be reduced to set theory, so the results could be stated as a formal sentence of set theory. If such resource exists, a researcher would simply need to state their result formally in a specified language and he would quickly find whether someone else already published their result.

Does something like this exist? If not, I think that's surprising.

Answer 1

The was QED project, which seems to have died, but Mizar project seems to continue in the same spirit.

IIRC the main goal was an attempt to formalize the whole mathematical knowledge in the form such that the proof can be computer-checked. It is really an ambitious goal, but if you have a look at Mizar page and JFM, the number of theorems and proofs which have been formalized seems impressive to me.

But the possibility of searching for results and proofs was also discussed, I will quote from this document. It was linked from the Wikipedia article. (I think I have seen discussion of possibility of such searches elsewhere, maybe at sci.math.)

The discussion following the talk centered on the problem of retrieving information from a database. Since most information is currently stored in the form of text files it is difficult to organize the data in such a way that they are amenable to "semantic" queries as opposed to a purely textual search

---

I don't think this answers your question satisfactorily (and I hope somebody will be able to add more about this project or similar projects) but at least this shows what has been done in similar direction. In case you're interested in formalizing proofs of theorems, I believe that the paper Formal Proof—Getting Started by Freek Wiedijk might be interesting for you.

You can also have a look into references and external links in Wikipedia article on QED project.

The book F. Wiedijk (ed.), The Seventeen Provers of the World, foreword by Dana S. Scott, Springer LNAI 3600, 2006, might be of interest, too. Google books link and Springer link.

Answer 2

On the offchance that you aren't joking, here are two reasons why this idea is a non-starter. One, any halfway complicated result in mathematics would take hundreds of pages to express as a formal sentence of set theory. Two, the correspondence between results in Mathematics and formal sentences in set theory is one-many. Two very different looking sentences in set theory could represent exactly the same mathematical result. So it wouldn't be enough to search the literature for your sentence; you'd have to search for sentences equivalent to your sentence, and that's pretty much impossible.