Source: Felix Breuer blog, Feb 2012
The number of new results per year is increasing
The number of mathematical articles – and theorems! – published each year has increased dramatically in the last decades. To give you just one piece of evidence, here is a graph of the number of new research articles entered in the Zentralblatt MATH index each year. This figure is taken from Bernd Wegner’s article in the June 2011 newsletter of the European Mathematical Society.
There are roughly 100,000 mathematical articles on the Zentralblatt index that have been published in 2010. One hundred thousand articles, of which the majority contain (supposedly) new results. I’d go so far as to say that most mathematicians cannot read and properly digest more than 100 articles per year. (For me personally, the number is certainly lower than that.)
This means that most mathematicians cannot even make use of 0.1% of the new results published each year.
This must have at least one of the following two consequences. In my opinion, it has both.
Mathematical research is becoming more and more specific.
both trends, increasing specialization and increasing redundance, have the same effect:
Mathematical research is becoming increasingly irrelevant.
Formalizing mathematics. In my opinion, formalizing mathematics is the single one most important thing that needs to happen if we want mathematics to scale. With “formalizing mathematics” I mean a huge process that includes all of the following.
- The development of the languages and tools necessary to make the formalization of mathematical definitions, theorems and proofs feasible for the average mathematician.
- This will have to go hand in hand with the development of automatic proof systems that can automatically “fill in the gaps” present in any research article.
- The creation of an infrastructure that allows formal mathematical articles to be shared and discovered across different proof systems and formal mathematical languages.
- And, finally, the formalization of (almost) all of mathematics.
Here is why I think the project of formalizing mathematics is crucial. We, as humans, cannot cope with the sheer quantity of mathematical output that is going to be produced in the 21st century. So we have to teach computers how to discover theorems for us that are relevant for the questions we are interested in. Otherwise, the work of most mathematicians will disappear into obscurity faster than anyone can be comfortable with.
Comment posted for the source:
no mature mathematician actually believes that “theorem proving is what mathematical research is all about”, rather they all recognize that it’s all about ideas, discovering them but also reinventing them, combine them in new ways, etc.