6 ms·
> That's not my site. You brought the figure as an argument, so I assumed that was your argument? If not, what was your argument then? I see a (super)exponenti
by freehorse 9d ago
> That's not my site.
You brought the figure as an argument, so I assumed that was your argument? If not, what was your argument then? I see a (super)exponential fit, but I don't see why that's better than a logarithmic fit on these axes (which would imply linearity). For covid we know well about infection disease dynamics. We do not have good models for AI because we do not have prior experience. Even the data points here are obviously noisy (why is sol that higher than fable, which does not seem to reflect how people consider these models?).
> At what point did you predict the following? [...] explosion of AI-generated proofs [...]
My question is, who is gonna pause the questions that AI is gonna solve? Who is gonna decide which research directions are interesting to pursue? Who is gonna take a proof technique and generalise it into a theory and a new mathematical field and structures and associated questions? Who is gonna decide which such generalisations are interesting to pursue?
So there are 3 scenarios I see possible as to who will lead the research directions/questions:
1. Humans. If so, I don't see the explosion as a big issue, because the bottleneck for progress on mathematics is gonna stay on the human side and rhythms. There is gonna be an acceleration in getting new proofs faster, but a big part of mathematicians' job is not to write proofs but, essentially, pose interesting questions.
2. AI. The only way that I see this explosion as "human mathematicians losing control" is if AI can itself generate new questions and somehow dictate which paths are interesting. That would mean that AI has developed a "taste", which is not clear that this happens or will happen soon.
3. Nobody really. There is also the other option, that nobody does, and somehow the biggest part of theoretical mathematics stagnates and/or becomes a more superficial endeavour. Accompanied by associated budget cuts this scenario does not seem too unrealistic either.
Verifying solutions itself is the "easy" part when talking about automating proof generation, a proof will either be verified in lean or not be trusted. Lean will continue expanding to include more and more mathematics, and that's it. It will become more and more common to ask for lean verification at journal submission, depending on the field and how much it has been formalised in lean. The real question imo is "who is gonna understand the math produced and set new research directions".
- 0xDEAFBEAD 8d ago>I see a (super)exponential fit, but I don't see why that's better than a logarithmic fit on these axes (which would imply linearity). A linear fit on a logarithmic y-axis implies exponential growth. I myself don't have a strong view on ordinary exponential vs super-exponential for that graph. COVID was only ordinary exponential, so super-exponential is not needed for the COVID analogy to be valid. My point about mathematics was not about humans "losing control" of math. It was simply to ask if this was an outcome which you predicted.
- freehorse 8d ago> A linear fit on a logarithmic y-axis implies exponential growth. The fit on the graph is exponential, which makes it exp(exp(x)) growth. But it is not clear why it should be that, or linear, or logarithmic, which is what I meant. Covid was exponential growth because the rate of infection (assuming a large enough population) is proportional to the current number of actively infected people. What is the analogy here? Is there a similarly widely accepted theory for why the models will improve exponentially rather than linearly? I am not sure recursive self-improvement is that clear to be going on, for instance. I told you which outcomes I talk about. Even in a scenario where models improve exponentially, you still cannot have exponential growth in the long run in the same way that you cannot have that in the covid19 case either: you saturate the population. In the covid case a significant amount of the population has gotten infected so there are less people to infect, in the math case the problems to solve are gonna run out. Then, the bottleneck is how to pose new problems/set new directions of research, which was already not an easy problem to solve. The growth of covid was actually a logistic function, not an exponential one.