5 ms·
My first thought when I read this title was that there should be a site like Hoogle for mathematical proofs, where one could search by type signature for existi
by mneary 12y ago
My first thought when I read this title was that there should be a site like Hoogle for mathematical proofs, where one could search by type signature for existing proofs. I'm not sure if people often think of proofs in terms of their type signature, but by Curry-Howard it would be doable.
- infruset 12y agoThis is a complicated problem. I know some Coq developers are trying to build a search tool, but the problem is there are many ways to state a theorem and you want to not only find statements that exactly correspond to your request, but also those that are convertible to it. And there it gets ugly.
- cottonseed 12y agoYou can do this in Coq with the vernacular command Search and its variants.
- cscurmudgeon 12y agoMay be tangential, but take a look at the Mizar project [1]. It has a huge repository of around 50k machine verified non-trivial theorems in human readable syntax (e.g. Gödel's completeness theorem for first-order logic). Also check out the journal Formalized Mathematics [2]. The idea is that every major new theorem in a paper has a machine verified proof attached. [1] http://mizar.uwb.edu.pl http://mizar.uwb.edu.pl [2] http://mizar.uwb.edu.pl/fm/ http://mizar.uwb.edu.pl/fm/