I'm currently returning to Toronto from a summit on the future of...

I tried to find a title that wasn't too bombastic:
What's clear is that we are at the start of a massive explosion of mathematical outputs; for example, below is the number of combinatorics papers posted per week to arXiv since late 2021. Other areas show a similar, but not quite dramatic, rise. I imagine a time series of tweets about math results would look similar.
Of course this work might have value to the people announcing it (credit, PR, etc.).
Right now we try to incentivize the production of high quality science by rewarding people who produce papers, prove theorems and resolve conjectures, etc. But these outputs are now mispriced, and incentivizing them is not obviously optimal for the production of high quality science. What happens if we continue to do so in the next years?
I think if we do, the dominant strategy for career success (at least in the medium term) is playing the slot machine for conjectures. In fact one does not even have to choose the conjectures--you can just ask codex to pick them and resolve them and check the work. If you care about producing correct papers you can produce multiple short papers per day this way (and people who are doing so); if you don't care about correctness you can produce far more (and people are doing this too).
What's the value-add? The cost of the tokens? Certainly not the expertise developed--there is none. No one, not even the author, is reading much of this work. Mathematicians are no longer connected to the underlying mathematics. Even human verification is arguably less valuable as the models become more reliable.
I've recently been told by multiple colleagues that they are unwilling to discuss work in progress for this reason.
Nonetheless there are some bright spots. Autoformalization becomes cheap and effective. Many gaps or errors in the literature are discovered and repaired.
Much hay has been made of the necessity of human judgment here, to check that statements and definitions are formalized correctly. I am skeptical of this--I see no reason the models will not be able to do this effectively.
On the other hand, we are already starting to see cases (e.g. the two examples in the slide below) where formalizations differ from the English text they are formalizing in ways that may not be obvious to the readers. Again mathematicians are becoming disconnected from mathematics--while they might be able to trust the *statements* in past work, it is harder to trust the *ideas*. Informalization helps with this a bit but it is costly and time-consuming.
Despite this, the profession still incentivizes the production of papers. Models start to fulfill all the functions human mathematicians do now: theory-building, conjecturing, resolving conjectures, iterating, etc. Human mathematicians are doing "lab science" with agents, perhaps directing compute to questions they find interesting.
Who is engaging with this work? How are we training the next generation? It's not clear to me that our current institutions, if they do not adapt to this new regime, continue to produce high-quality mathematicians. Indeed it seems to me that our existing incentive structures will start to reward people who *do not* engage deeply with the mathematics, or, arguably, care about it at all.















