Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question

closed as off topic by Asaf Karagila, Hans Lundmark, Rasmus, Zev Chonoles Dec 20 '11 at 13:10

Questions on Mathematics Stack Exchange are expected to relate to math within the scope defined by the community. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about reopening questions here.If this question can be reworded to fit the rules in the help center, please edit the question.

    
Zentralblatt and Math Reviews have evolved in the direction you envisage (aside from the set theory part!). –  André Nicolas Dec 20 '11 at 4:56
2  
I think this is not the place for this question, voted to close. –  Asaf Karagila Dec 20 '11 at 7:02
    
automated-theorem-proving seems to me to be the closest tag we have to formalized mathematics. Feel free to retag if you think we have a better one. –  Martin Sleziak Dec 20 '11 at 7:35
add comment

2 Answers

up vote 5 down vote accepted

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.

share|improve this answer
add comment

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.

share|improve this answer
1  
I know it wouldn't work with all results (equivalent statements). However, although one can write equivalent statements for the same result (not the complete proof, just the statement of the theorem), I thought the odds would be good that two researches would write them in the same way. But I have no experience with writing such statements, so I guess that's why I wasn't discouraged. Thanks for your comment. –  anon Dec 20 '11 at 4:31
add comment

Not the answer you're looking for? Browse other questions tagged or ask your own question.