Seems like one of those Lindy effect things. The longer proofs have been part of math, the longer you should expect them to stay there. This is why you can dismiss a new fashion as a fad, but once it's been around for a while you should acknowledge its staying power.
Science, including mathematics always produce Black Swans. While it's possible to speculate about little incremental progress in known unknown, it's totally impossible to predict anything about unknown unknown. New branches of mathematics, maybe even whole new sciences, just like computer science came into existence only after a computer was invented.
Imagine if, back when we thought the sun revolves around the earth, some great king wanted to better understand astronomy. So he established a National Science Foundation to pump out hundreds of trillions of dollars to scientists to study astronomy and better understand it. What would be the result? The result would be ever more sophisticated treatises on geocentrism, with ever more complicated gymnastics to explain observations based on flawed models. It would actually make it harder to challenge geocentrism, because there would be so much more financial momentum behind geocentrism.
This is historically doubtful. The most famous anti-heliocentric researcher, Galileo, was a professor at the University of Padua. This university relied on the Church at least as much as a modern US university relies on the NSF. Furthermore the Church had vastly more power over publication than any institution in any free country today. Yet, the truth still shone through. If Renaissance Italian research funding had been greater, we would have gotten more empty treatises on heliocentrism, but also more chances at a Galileo.
John Horgan loves making these wild assertions even though he is not a trained scientist or mathematician. He once even published a book called the End of Science. In that book, Horgan said that scientists were no longer going to come up with revolutionary scientific theories like relativity and the theory of evolution. Safe to say, this guy has a reputation of writing edgy and provocative things with very little basis in reality.
John was a professor of mine, so I'll defend him a bit here :). To be clear, he's certainly a contrarian, and has a fairly pessimistic take on modern scientific progress.
I pushed back in class quite a bit about his 'End of Science' claims, and we disagreed frequently - but his actual claims are usually not as strong as they're made out to be. He simply doesn't see the same sort of practical gains being made from scientific research that we were making in the 19th and early 20th century.
If we look at the research being produced by obviously impressive scientific endeavors like LHC - I think you can see his point. We're obviously gaining knowledge, and negative results are still valuable, but we're investing more and more to make incremental progress in many fields and the actual research is becoming less and less accessible to the average person.
Anyway, it's not my job to defend John's work (he's more than capable of responding to critics) but I always found him to be interesting, patient and encouraging to his students. His class was one of my favorites and even if I disagree with his claims overall I don't think they deserve to be dismissed so readily.
I think everyone can agree that late 19th century up to the first half of the 20th century was an unusual time with many scientific breakthroughs. Science is moving much slower now, but it's still much faster than in the time before that.
The limits of a single man knowledge and understanding are perfectly real and discussion on how to overcome them is very important. I'm not a Steve Wolfram fan, but his answer in the article is much deeper than others.
As for pure proofs, they died in 14th century actually where scholastics were able to prove anything. Since Bacon and Newton experimental evidence was required to confirm the validity of the knowledge.
>Till the point when computers will create thousands of proofs a man will have trouble to understand.
I'm skeptical this will ever happen. If we create a computer X that comes up with such proofs, and we create X in such a way that we fully trust X's truthfulness, then we can trivially understand every theorem X asserts: the explanation for every such theorem is, "The theorem is asserted by X."
To put it another way, suppose I have an algorithm A which I know churns out true theorems with proofs. Suppose I run A for awhile and it churns out a theorem with a gigantic proof. The fact that the proof is gigantic is totally irrelevant. I can completely ignore said proof and accept the theorem because I know that A outputs true theorems. That knowledge itself obsoletes the very proofs A churns out.
Thank you for the link, very exciting research. I definitely agree that there are separate activities to formulate the theorem and to prove already described one. The former requires some kind of creation and imagination and might not be automated soon, the latter is probably just a directed search like AlphaGo and can be automated in a near future.
But the implementation of such automated prover means that proofs will die since human will only propose the theorems and machine will prove them maybe in some huge computation. That might be more effective overall and will probably open some new knowledge areas but at the same time humans gonna loose the need and ability to prove the statements.
