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?