Comment by steinwinde
13 hours ago
I would like to ask a question to you as a math professor: I think we all agree we do not know what the discipline will look like in ten years. But doesn't the rapid surge in mathematical proofs and methods imply that - at least for the coming years - there will be more, not less, work for mathematics?
Consider the "Jacobian conjecture counterexample": the work doesn't simply end once Terence Tao explains the computer-generated proof to a wider specialist audience.
1. I assume that the counterexample will give rise to a host of new questions, each of which will in turn need to be resolved. In the long run, the process of formulating questions might also be automated by AI - but likely not within the next few years to such an extent the growth of knowledge results in a decline in relevant questions.
2. Mathematicians will have a great deal to do in terms of meaningfully formalizing results within Mathlib - and hopefully Isabelle/HOL and other systems as well. From what I have read, the way current AI formalizes theorems makes them unsuitable for these libraries. I envision this as an undertaking not unlike the development of the Linux kernel. Throughout this formalization process, there should always be a human who has actually grasped the reasoning to ensure the AI hasn't simply exploited a flaw of the system.
3. Physics, chemistry, and many other sciences are currently benefiting from AI to a lesser extent. I anticipate significant changes at the interface between mathematics and other sciences as the body of mathematical knowledge expands dramatically. I cannot imagine this resulting in anything other than an increased workload, at least for the next few years.
Isn't it likely that mathematicians' workloads will initially rise rather than fall, provided they are willing to accept a shift in the nature of their tasks?
In practice, mathematicians' workloads have been a function of their work ethic, motivation, and competing demands on their time. There's no big-picture question of "how much math there is to do now"; the amount of remaining math to discover has long been presumed to be, for all intents and purposes, infinite. (Similar questions are relevant on a much smaller scale -- for example in case of someone who has specialized in a narrow specialty which goes dead.)
Your (1) is most certainly true.
As for your (2), most mathematicians I know have at most a passing interest in formalization, Mathlib, and Lean. My understanding, which is admittedly quite superficial, is that AI is actually getting quite good at translating human-readable mathematics. I could be mistaken about this, but even if there is a lot of human work to do, it sounds like a lot of anal-retentive oversight of work you didn't do yourself -- the sort of task that academics love to complain about!
Perhaps human interest in Lean will grow, but I don't anticipate it occupying the attention of more than a small slice of the community.
Your (3) is an interesting question. I work on the theoretical rather than applied side, but what you describe might very well be true for applied mathematicians.
Applied mathematician here.
Where I see models having a huge impact is in simulation code development.
One blocker for years now has been the adoption of GPUs. LLMs can fairly successfully and very quickly port to GPU and suggest/implement useful optimisations. Once it's verified, a code can go from anywhere between 2x to 1000x faster (mainly because CPU codes are so poorly optimised). Some science can reach much greater problem sizes, while some can run the same problems in hours rather than months and both can be revolutionary. Even more than that, LLMs seem to be finding fundamental performance bugs in both open and closed source core libraries so there's a bit of a whole-ecosystem uplift.
Can't comment on the more theoretical, less computational applied maths impacts!