24
$\begingroup$

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:

  1. OCR scan all historical mathematical texts
  2. organize metadata of references and authors (e.g. as graphs)
  3. extract mathematical objects (like theorems, definitions, etc)
  4. extract proofs and ideas
  5. 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.

Improve this question
$\endgroup$
9
  • 5
    $\begingroup$ You might look at the IMU and their efforts on WDML. Part of the idea is to archive sites like MathOverflow which show the (relatively informalized) development of mathematics in this century. Gerhard "Says 'Informalized' Is A Word" Paseman, 2020.07.15. $\endgroup$
    – Gerhard Paseman
    Commented Jul 15, 2020 at 17:43
  • 3
    $\begingroup$ There is slow progress towards point 5 (see various libraries that have grown around systems like Coq and Mizar), but at the moment nothing too high can grow on this field since most proof languages are too unstable and don't feel like "the right thing" (so any work done now will probably have to be painstakingly adapted in 10 years if not earlier). Most of the time, these libraries are written by humans, typically inspired by existing literature but in no way just straightforwardly translating it. Maybe AI could do this in 20 years, but even that's far from a given. $\endgroup$
    – darij grinberg
    Commented Jul 15, 2020 at 20:18
  • 2
    $\begingroup$ I'm not sure whether I understand point 3 correctly: If I get it right, you would like to have a database which contains theorems, definitions, etc., and which links to articles books, etc, where they are used. I am, however, under the impression that this idea underestimates the diversity of mathematical literature, even within very specific sub-areas: For instance: What precisely is the statement of Banach's fixed point theorem? What is "the" Perron-Frobenius theorem in matrix analysis? What does the existence and uniqueness theorem for ODEs say? And these are only rather mild examples... $\endgroup$
    – Jochen Glueck
    Commented Jul 16, 2020 at 0:18
  • 1
    $\begingroup$ "Same theorem" is much more of a problem than you think. Let me point out one particularly problematic situation. The foundations of algebraic geometry were completely redone in the 1960s by Grothedieck and others, to the extent that modern algebraic geometers find it very hard to read the standard text of Hodge and Pedoe from the 1950s. A much broader class of objects was introduced, and the objects previously studied were redefined in a different way. (continued) $\endgroup$
    – Alexander Woo
    Commented Jul 17, 2020 at 2:20
  • 1
    $\begingroup$ Some old theorems generalized to (at least some of) the new class of objects by doing the 'obvious' translation to the new language; some generalized but required genuinely new proofs; some remained true only for the 'classical' objects (redefined). In which cases do we have the "same theorem"? $\endgroup$
    – Alexander Woo
    Commented Jul 17, 2020 at 2:21

3 Answers 3

Reset to default
25
$\begingroup$

None of your five levels of digitalization are at all within reach. Let's take just the first one. As you say, copyright is a huge obstacle. Consider what happened when the same idea was attempted by Google (resulting in Google Books), as explained wonderfully in this article in the Atlantic. Larry Page (as in, PageRank) set up a tremendous effort to get books from libraries and scan them en masse with OCR technology to make them searchable.

After doing this for some time, publishers filed suit against Google. Google hired a massive legal team because it cared so much about creating such a library. Google managed to bring the publishers onboard with the idea, pointing out that it would allow publishers to sell out-of-print works. Unfortunately, this raised another issue, like a sad game of whack-a-mole, and the Department of Justice got involved to prevent Google from having a de-facto monopoly on out-of-print books. In the end, the Judge prevented the settlement that Google and the publishing companies had agreed to.

The same things would happen in the math world. The point is: you have a bunch of authors who died a long time ago and can't give consent to update their old publishing contracts. You have publishers who won't let go of content unless they can profit on it. And you don't have any organization large enough to be the central clearing house to connect customers who want to read these works with the places they can view and buy them. The problem only gets harder every year, because we produce more and more mathematics all the time (and OCR for math is not great, throwing a wrench into your third idea). My opinion: if Google couldn't pull together a global library, despite all the effort they put into this problem, there's no hope for the rest of us.

Improve this answer
$\endgroup$
10
  • 6
    $\begingroup$ So end run around the old system: publish newly created mathematics (and synopses and surveys of older math) under a free-to-distribute license. Just because it was done the old-fashioned way does not mean it has to stay that way. Gerhard "Get Rid Of Tradition,... Tradition!" Paseman, 2020.07.15. $\endgroup$
    – Gerhard Paseman
    Commented Jul 15, 2020 at 19:08
  • 23
    $\begingroup$ De-facto, Library Genesis is the library everyone uses these days as a first source for mathematics books; physical libraries are consulted as a last resort, for the rare books that are not (yet) on Library Genesis. But there is a huge gap between having a scan and having a readable "true PDF" or TeX file. MathPix is a promising OCR tool for mathematical formulas, but it has its limits, and typesetting can be very diverse. (Not to mention that lots of scans aren't good enough to leave OCR to machines.) $\endgroup$
    – darij grinberg
    Commented Jul 15, 2020 at 20:23
  • 8
    $\begingroup$ @darijgrinberg, I'm not sure that LibGen is the preferred resource over library books for everyone. A, uh, friend of mine definitely consults it whenever needed to stock an electronic library (say, for books to take along on travel), but, pre-pandemic, I would almost always go to the physical library to get a book (not an article). It's just too hard to browse, properly to bookmark, to compare side-by-side, etc. in an electronic reference; the electronic reading experience remains sub-par for me. $\endgroup$
    – LSpice
    Commented Jul 15, 2020 at 23:18
  • 5
    $\begingroup$ @erz Many books cross-reference themselves across hundreds of pages constantly. There's a reason books are books, and not sequences of articles. $\endgroup$
    – Kevin Carlson
    Commented Jul 16, 2020 at 4:11
  • 4
    $\begingroup$ @darijgrinberg, I definitely have nothing against those who prefer e-books, and am glad that they're there when I need them (like in the US now—I'm definitely not going in our library, even when it opens). I just don't agree that it's everyone's first choice. $\endgroup$
    – LSpice
    Commented Jul 16, 2020 at 21:11
11
$\begingroup$

On my opinion, 2-5 are non-realistic (and hardly needed), while 1 is indeed desirable and important. To be sure, a substantial progress was made in the recent years towards 1. But it still remains a remote goal.

David White mentioned the main obstacle: the existing shameful copyright system. But there are several other obstacles. The number of math periodicals is really enormous, many were owned by universities and various societies in the past, and there is no real will to digitalize all these obscure publications. There are many old publications of various societies in most European countries which are still not digitalized. Big companies probably see no perspective of profit in this (and they are probably right), and volunteers have more important things to do.

As I understand copyright does not apply to 18-19 centuries math journals. Still, there is little interest in their digitalization. Few big journals which still continue, digitalized the old issues (and claim copyright for this digitalization). But no one seems to be interested in those journals which do not continue.

In many cases, even when a digitalization is available, the quality is too poor to read or print, or search. The old volumes of Comptes rendus are available, but try to find anything in them. Sometimes they show you "digitalized" pages on the screen but do not allow to download the pdf file of the article. So you are supposed to print a large paper one page at a time, if allowed to print at all.

The result is easy to predict: with the current demise of the usual libraries, most this mathematics will be simply lost. And no realistic remedy is visible. Well, this is not the first time that such thing happens: by various estimates about 90% of Hellenistic mathematics and science were lost. (And practically 100% of Greek pre-Hellenistic).

Of course one can argue that "the most important" works are preserved. For example Euclid is preserved but all his predecessors are not. Perhaps there is some truth in this. (Imagine that of all 20 century mathematics only Bourbaki is preserved:-)

Improve this answer
$\endgroup$
12
  • 6
    $\begingroup$ I”m not sure I agree on your 18-19 centuries assessment. Most everything to 1850 or 1900 is scanned and available in archives like numdam, gallica, hathitrust, biodiversity, archive.org that seem safe even if Google books were to shut down. After 1950 or so is another matter with, anyway, a much reduced signal/noise. $\endgroup$
    – Francois Ziegler
    Commented Jul 15, 2020 at 21:12
  • 4
    $\begingroup$ Most German "provincial" journals (which have names beginning with Sitzungsberichte, Abhandlungen, etc. are not digitalized, even the famous one published in Gottingen). And this is only one example. The famous Russian journal Doklady of the Academy is not digitalized. We only have translations for few years when it was translated. $\endgroup$
    – Alexandre Eremenko
    Commented Jul 15, 2020 at 21:58
  • 4
    $\begingroup$ (1), (2), (3), (4),... $\endgroup$
    – Francois Ziegler
    Commented Jul 15, 2020 at 23:08
  • 2
    $\begingroup$ You say Doklady is not digitized. It is available for the period 1957-1995 at mathnet.ru/php/… $\endgroup$
    – KConrad
    Commented Jul 16, 2020 at 2:11
  • 2
    $\begingroup$ @erz: I can give you one reason: reading old mathematics is difficult and requires highest qualification. People who have it prefer to spend their time more productively: by proving their own theorems:-) $\endgroup$
    – Alexandre Eremenko
    Commented Jul 16, 2020 at 3:40
3
$\begingroup$

There's a lot of work lately on formalizing large parts of classical mathematics using proof assistants, see for example the Lean prover and the accompanying library mathlib. You can see an overview of what has been formalized here; it includes a lot of classical abstract algebra and real analysis, although there's also a lot of undergraduate math they haven't formalized yet which they list here. If you think that's all "trivial", there's ongoing work to formalize the proof of the independence of the continuum hypothesis, the proof that it's possible to evert the sphere, etc.

An interesting facet of this project is that all the proofs are kept under a version control system and you can see the entire history of every proof. It's common for the initial proof of some result to be very long and verbose, only for people to find ways to shorten it or make it more elegant later -- for example, von Neumann's proof of the Radon-Nikodym theorem. Where before you might have had to trace through the citations of loads of historical papers that your library might not even have, now you can see exactly how this process played out by just doing git blame.

Improve this answer
$\endgroup$

You must log in to answer this question.

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