The theorem the SA article is talking about - CFSG, the Classification of Finite Simple Groups - is somewhat special in that respect. Lots of things in math fall out of fashion and get forgotten, often whole subfields. CFSG is different because the theorem itself is so basic and important that it's not likely to be forgotten in any foreseeable future. But its proof is so long and complicated that it's not even clear that there's one person who understands all of it, and the heap of details is not organised well enough for someone to just study it from books/articles without the help of people who lived through proving it back in the 70ies.
Suppose there just isn't enough interest in the younger generation of mathematicians to study the proof, even if the old guard are able to organize it better before they retire. Then we may reach a situation in which CFSG will still be used as a proved theorem and not a conjecture - because it's so powerful and important in many fields of math - but its proof will be lost to collective memory. I'm not sure, but I think that state of affairs might be without precedent.
(Here's a quote from Gian-Carlo Rota's _Indiscrete Thoughts_ on forgotten and rediscovered math:
"The history of mathematics is replete with injustice. There is a tendency
to exhibit toward the past a forgetful, oversimplifying, hero-worshiping
attitude that we have come to identify with mass behavior. Great
advances in science are pinned on a few extraordinary white-maned
individuals. [...]
One consequence of this sociological law is that whenever a
forgotten branch of mathematics comes back into fashion after a period
of neglect only the main outlines of the theory are remembered, those
you would find in the works of the Great Men. The bulk of the theory
is likely to be rediscovered from scratch by smart young
mathematicians who have realized that their future careers depend on publishing
research papers rather than on rummaging through dusty old journals.
In all mathematics, it would be hard to find a more blatant instance
of this regrettable state of affairs than the theory of symmetric
functions. Each generation rediscovers them and presents them in the latest
jargon. Today it is if-theory, yesterday it was categories and functors,
and the day before, group representations. Behind these and several
other attractive theories stands one immutable source: the ordinary,
crude definition of the symmetric functions and the identities they
satisfy.")
I really wish people would explain why they downvoted me on hackernews. Its not that I really care about the points its that I want to know what I did wrong. Like if I accidentally offended someone or it just wasn't an interesting comment or observation or that it is completely wrong statement.
Your response is excellent anatoly and I appreciate it.
However, having a Coq proof does not mean someone human understand the proof, and the software can evolve in incompatible versions unable to recheck the proof.
I agree. To some extent new generations invent notations that subsume existing ideas, but I don'tthink they are claiming to reinvent symmetric functions.
Suppose there just isn't enough interest in the younger generation of mathematicians to study the proof, even if the old guard are able to organize it better before they retire. Then we may reach a situation in which CFSG will still be used as a proved theorem and not a conjecture - because it's so powerful and important in many fields of math - but its proof will be lost to collective memory. I'm not sure, but I think that state of affairs might be without precedent.
(Here's a quote from Gian-Carlo Rota's _Indiscrete Thoughts_ on forgotten and rediscovered math:
"The history of mathematics is replete with injustice. There is a tendency to exhibit toward the past a forgetful, oversimplifying, hero-worshiping attitude that we have come to identify with mass behavior. Great advances in science are pinned on a few extraordinary white-maned individuals. [...]
One consequence of this sociological law is that whenever a forgotten branch of mathematics comes back into fashion after a period of neglect only the main outlines of the theory are remembered, those you would find in the works of the Great Men. The bulk of the theory is likely to be rediscovered from scratch by smart young mathematicians who have realized that their future careers depend on publishing research papers rather than on rummaging through dusty old journals.
In all mathematics, it would be hard to find a more blatant instance of this regrettable state of affairs than the theory of symmetric functions. Each generation rediscovers them and presents them in the latest jargon. Today it is if-theory, yesterday it was categories and functors, and the day before, group representations. Behind these and several other attractive theories stands one immutable source: the ordinary, crude definition of the symmetric functions and the identities they satisfy.")