I am reading a paper
Ittay Weiss, The QED Manifesto after Two Decades — Version 2.0, Journal of Software, 11 no. 8 (2016) pp. 803–815, doi:10.17706/jsw.11.8.803-815
The paper says
Goal 7: Organization of Knowledge. The volume of mathematical knowledge is staggering. Not only is it the entirety of mathematics that is well beyond the scope of mastery for any single person, the same can be said of each of the major areas of mathematics (e.g., topology, algebra, analysis, logic, etc.). Moreover, an overwhelming quantity of new mathematics is accumulated each year. For users of mathematics as well as for novice and expert mathematicians, navigating the ocean of results is becoming an ability that appears to require superhuman capabilities. Both QED 1.0 and QED 2.0 aim to provide invaluable tools for this purpose. The system will have tools to navigate, search, and compare results. By analyzing the interdependencies in the coding of various results the system will be able to automatically locate similar results suspected of being related (or perhaps duplicates), thus identifying areas of mathematics that are more closely related than what appears to be.
I think organizing knowledge is really important for interactive theorem proving (ITP). Especially, I want to figure out the status of comparing, analyzing the mathematics represented by ITP. But I can not find any project or paper works on comparing and analyzing mathematics represented by ITP. Could you recommend me some papers or projects related to comparing and analyzing mathematics using ITP?
Best Answer
Organization of mathematics in computerized form is a somewhat separate topic from automated and assisted theorem proving. Here are some pointers that will get you started:
A typical theme in mathematical knowledge organization is how to represent mathematical knowledge in a platform independent way, agnostic with respect to mathematical foundations (or at least translatable between foundations), and readily searchable. None of these are easy to solve. You might think, for instance, that we could all just agree on some format to represent formulas, but that is not the case. Should we use first-order logic, higher-order logic, or type theory? Which meta-level operations on formal theories should we support? Who governs the naming conventions for lemmas, theorems and definitions? And there are meta-theorems showing that figuring out whether two theorems "state the same thing" is a very hard computational problem, even just for very simple fragments of logic.
I personally think that these efforts are immensly important, but also that we should not expect them to result in a grand unification of mathematical knowledge. The accepted view of mathematical foundations is that, surely, all of mathematics can be unified as a coherent whole in a single system. However, if you put a bunch of experts on foundations of math into a room and lock them up until they have agreed on one particular mathematical formalism which will serve for expressing all of mathematics, they will die of thirst before they agree on anything. I don't think this is the fault of logicians or logic. It has something deeper to do with how multi-agent system (as computer scientists like to call collections of intelligent entities) organize knowledge.