Just for personal interest, I am not (yet) professionally involved in it. My question is about the state of arts in digitalization of mathematics and to what extent it is possible and reasonable.
There are different levels of digitalizations:
- OCR scan all historical mathematical texts
- organize metadata of references and authors (e.g. as graphs)
- extract mathematical objects (like theorems, definitions, etc)
- extract proofs and ideas
- formalize mathematics such that it can be completely checked by theorem provers
The main effort I found is https://imkt.org/
Steps 3/4 and 5 may be of independent interest and should be understood more parallel than chronological. Point 5 is more interesting in having (error-free) formalized math. It should also be allowed to choose different foundations of mathematics and the possibility to switch in between them. Point 3/4 is more interesting for a researcher that wants all references for a definition, a theorem, a keyword. It would be a wonderful source for doing data analysis of mathematical knowledge (historical, social, semantical, etc). In contrast to 5 it can contain errors and speculations. The main interest is in identifying and referencing mathematical objects over all the produced texts in history of math.
My question is:
The goal of https://imkt.org/ is huge but when looking at its first projects it looks (sry) a little bit disappointing. The main focus (also of other literature that I scanned through) lies on connecting the existing databases and languages, i.e. of theorem provers, computer algebra systems (and maybe wikis). I understand that different applications in math demand different systems (e.g. integer series http://oeis.org/ should also be part of it?) Can or shouldn't there be one system that contains everything that can be accessed (and is stored not just referenced!) through the same system? Are my dreams of such a system over the top?
One of the largest issues is the copyright of the big publishers. More and more is going in direction open math. Until then it is unclear to what extent a library can be complete (gaps are somehow missing the point of this system).
The other issue is the efficiency in producing the content extraction and to advance it by advertising the advantages of such a library to mathematicians such that it will move itself at some point.
There have been many efforts in the past that were abandoned again or here for years (like Mizar) but far from being known and used in daily mathematics.