14
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ A relevant project is Paulson's ALEXANDRIA (you can also check it at his web site) $\endgroup$
    – Pedro Sánchez Terraf
    Commented Aug 12, 2019 at 12:08
  • $\begingroup$ @PedroSánchezTerraf I have seen the website of ALEXANDRIA. The principle contains analyze mathematics but I did not see any results related to analyze mathematics. All the papers are just proving theorems. Could you give me some help about how did this project try to analyze mathematics? $\endgroup$
    – ZhangLiao
    Commented Aug 13, 2019 at 8:48
  • $\begingroup$ I'm sorry, I don't know the details on how they plan to do that. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Aug 14, 2019 at 12:00

2 Answers 2

Reset to default
11
$\begingroup$

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:

  • MathWebSearch, a content-based search engine for mathematical formulae
  • OpenMath, standards for representing the semantics of mathematical objects and communicating them between software systems
  • The MMT Language System for representation of mathematical knowledge

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.

Improve this answer
$\endgroup$
4
  • 3
    $\begingroup$ "whether two theorems "state the same thing" is a very hard computational problem" -> see When are two proofs of the same theorem really different proofs $\endgroup$
    – Ben Burns
    Commented Aug 12, 2019 at 16:08
  • $\begingroup$ @BenBurns: What are you referring to? Tom's answer? I know about that... $\endgroup$
    – Andrej Bauer
    Commented Aug 12, 2019 at 22:21
  • $\begingroup$ Sorry @AndrejBauer I should have added some context. I was assuming you're aware of the content in the linked answer since you left some comments there. I wasn't really commenting on the content of your answer, just trying to leave a footnote here for other people (like me) not as acquainted with the topic: for anyone interested in further reading on the problem of theorem equivalence, see the many different answers to the question I linked. $\endgroup$
    – Ben Burns
    Commented Aug 13, 2019 at 11:57
  • $\begingroup$ Thanks for the link! $\endgroup$
    – Andrej Bauer
    Commented Aug 13, 2019 at 12:15
4
$\begingroup$

Of course a hard part is to know whether two similar-looking lemmas are really related, and even more whether two superficially very different statements might have a short proof of their equivalence. This ITP (Interactive Theorem Proving) paper looks promising:

Learning-assisted theorem proving with millions of lemmas

Cezary Kaliszyk and Josef Urban https://doi.org/10.1016/j.jsc.2014.09.032

Improve this answer
$\endgroup$
1
  • 3
    $\begingroup$ I remember trying to figure out how to encode in Coq (in a programmatically verifiable way, not just as a comment) that two theorems are identical (this is the only way to provide two proofs for one theorem). Still no clue how to do that. $\endgroup$
    – darij grinberg
    Commented Aug 12, 2019 at 8:07

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .