You can say that American society made OpenAI and Anthropic possible. No other current society would have. Suddenly, formalisation of math is becoming cheap. That's not a problem, that's the goal, and it is here much earlier than expected. That's not antisocial. That is scientific progress.
You're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon (https://mathstodon.xyz/@tao/117207856734787448)
In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts to solve these problems tend to spur further development of the field through the efforts to solve such problems, and then to digest any partial or complete solutions that emerge for further insights. Prematurely solving the problem by purely AI-powered methods - particularly without full transparency into the solution process - can contaminate this process to the point where it actually becomes a net negative for the progress of mathematics as a whole.
Yes. But that is a problem for pure mathematics, not for society. I think that pure mathematics is over. At the same time, applied mathematics will probably subsume most of pure mathematics. Fermat's theorem now is applied mathematics! It will be used to improve implementations of proof assistants for a long time.
Yes, it has been. And in the form of applied mathematics it will continue to be. It is not so much that pure mathematics disappears, but that in the future there will be just mathematics, and of course it is applied. You would be surprised what kind of mathematics appears when you actually try to formalise your applications properly. It pretty much includes everything that is thought of as pure mathematics today, and much more.
