You redefine "forgot" to make it falsiable, but also neglect that you need to refute that some "forgotten" work didn't contribute to new work down the line.

How can we hope to quantity the expenditure on math we've collectively forgotten? It's unknowable by definition. The only reasonable thing to do is to determine the value added after the expense paid. Even in a world where calculus is the only thing that we took away from the math of 1700s my guess is that this is still an economically beneficial calculation.

The real issue is we'll never know. The rich are willing to risk it all on charismatic CEO psychopaths but not on humans.

Perhaps you can ask Claude to explain it to you.

LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our complete garbage, spec and all, and say it's a proof of something.

It's not shocking at all that the people who seem to get any benefit out of LLMs in the proof assistant space are the ones who could have just don't it themselves anyway.