A Case for AI-Assisted Math
Table of Contents
Recently there have been several major advances in the area of AI for math. In particular, OpenAI has disproved one of the longest-standing conjectures in discrete geometry – the unit distance conjecture. This is probably the most major result that AI has ever produced. The previous AI resolution of Erdős problem 1196 on primitive sets was also notable for containing original ideas. Even more recently, there have been attempts to combine LLMs with the power of proof assistants to solve Erdős problems, which resolved 9 smaller Erdős problems. For me, these were both exciting and grim news. It seems to me a lot of my mathematician friends feel similarly; the dominating sentiment among us right now is one of panic and existential dread. Having recently participated in a workshop at CRM on applying AI to number theory research and talked with some engineers working on applying AI to math from Axiom and DeepMind, I have some new thoughts I want to share about AI-assisted math.
Are we Cooked?
I believe it is highly unlikely that mathematicians will be replaced by AI, although I cannot completely rule out the possibility. I will give my reasons, but first I want to play the devil’s advocate against a few common arguments in favor of my position.
- “AI can only do problem solving: it cannot do theory building, propose high-quality conjectures or deep programs, or develop mature mathematical taste”: In my opinion, in the not too distant future, we will see AI become exceedingly good at building theories, proposing conjectures, and so on, and it is completely conceivable that it would be much better at them than solving problems. The strengths of AI systems lie precisely at finding and discovering deep intricate patterns. The only problem is people haven’t found out how to apply them to the data type of “math knowledge”. This is a similar situation before diffusion models were applied to generating images. The core brain mechanism for theory building and conjecture proposing is not something very different from what AI systems do. Although some theories, programs, and research tastes in math are motivated by practical need from engineering and other sciences, it seems to me in pure math those things are born from the struggle with hard problems, which is something that is conceivably an emergent behavior from AI. I think it is possible that AI systems could develop its own tastes, theories, conjectures, and so on, which might even influence ours.
- “AI hallucinates and makes mistakes so they will never be trusted”: This is precisely what people are trying to solve right now using proof assistants. It's not hard to imagine an iterative process where an AI improves on itself using feedback from proof assistants, where reliable results are formalized and checked and unreliable results that do not pass the check are discarded. In fact, what human mathematicians do is very similar to this process. We think of a vague idea, try to play with it and verify it more formally, through which we often discover it is wrong, and repeat the process again. After repeating this process many times, we gradually realize what is correct and how to prove it. The hallucinations are not a bug, but a feature -- they allow for more creativity and more generalization, instead of regurgitating similar ideas.
- “Math is the most difficult intellectual activity, so if AI could replace mathematicians, then so could it replace all other human intellectual activities, which is unthinkable”: This is in some sense similar to Moravec’s paradox: what is hard for humans is very different from what is hard for AI. AI has the unique advantage that it is superhuman in patience, and has immense breadth of knowledge. In fact, so far the biggest progress AI has made on open problems are the ones whose solutions require a wide range of expertise and very technical and laborious calculations, which is difficult for human experts who usually only specialize in a few areas and have limited energy. If AI integration with proof assistants becomes mature, then math is one of the only kinds of data where correctness checking can be automated, and synthetic data can be generated cheaply. What I'm getting at is humans and AI excel in different things. What may be a very difficult problem for us may be a low-hanging fruit for AI, and vice versa.
That said, why do I still believe mathematicians will not be replaced? My reasoning relies on the following syllogism.
- Major Premise: there will always be the desire to discover and understand deeper mathematics. Over the centuries, math has strayed further and further away from material reality, but humans continue to pursue math notwithstanding. To know more and understand more deeply is a fundamental human desire, and there is an infinite amount of math to discover. I have faith that this desire will not be extinguished by AI (on the contrary, AI empowers us to explore questions that previously might have been too technical or inaccessible). That being said, my real worry is sociopolitical: that the powers that be, who do not share this desire, might withhold funding for mathematical research (which is already pathetically low) under the pretext of AI, in which case it is the humans who are culpable, not AIs. In this regard, we are in the same boat with the other sciences.
- Minor Premise: a good human mathematician + a machine will produce deeper math than machine alone. To me, math is not solely the activity of theorem proving, but understanding things more deeply, which is not as clearly defined a task as theorem proving. What counts as understanding? I think this is almost a philosophical question, and one that is dependent on what we might discover in the future. The nature of mathematical understanding is evolving as we discover new math. In this regard, it is hard to imagine AI reaching this on its own. On the other hand, as we are learning to use AI, we and the future generations of mathematicians are training to do math on a higher level of abstraction. Perhaps in the future, we will see the use of AI as something as natural as the use of calculators. When we’ve completely harnessed its power, who knows, maybe we could be able to produce results that are much deeper than we thought we could.
- Conclusion: there will always be a need for human mathematicians.
However, it is almost certain now that the nature of what a human mathematician does is undergoing revolutionary change. It is hard to speculate what doing math would feel like in the future. For me personally, the question I care deeply about is: is it still going to be an enjoyable, meaningful activity for me (and more generally human mathematicians)?
The Future of Math Research and Academia
I am loath to be one of those so-called “futurists”, but I feel compelled to do so, given how fast technological iteration has been changing my life. The precariousness of the current global political climate has also caused me some anxiety. Therefore, I’ve spent time to really think about what the future might look like for me. Here is what I theorize would change about the research paradigm and sociology in math academia in the following decade. Admittedly, I am not a sociologist, so take it with a grain of salt.
- Academic Competition: The kind of mathematicians who will thrive in the future will probably be a different kind than the ones who used to. In particular, I think mathematicians who excel at technical strength will likely be at a disadvantage, and those who might not be very technically skilled but are very creative and intuitive will have an advantage. AI is superhuman in patience – it fears no technicality and is willing to carry out sophisticated calculations, and trial and error its way through an enormous amount of proof ideas. Inequality of computing resources will also affect academic competition, and in the future math academia will perhaps be more like biology and physics, where some labs could afford expensive apparatus and some could not. It is also a question whether there will be industry positions for using AI to tackle math, which would obviously have superior compute resources. Needless to say, in the future, to excel in math academia, one needs to master the use of AI, and really train to think with AI and perhaps also train to think on a “higher level” with the help of AI.
- Problem Solving vs. Theory Building: I will make the bold claim here that we will see a convergence between problem solving and theory building, and also see more interaction between distinct fields of math. AI will empower mathematicians to explore into different areas and styles of math, even ones they weren’t used to previously.
- Research Workflow, Collaboration, and Peer Review: I would imagine the workflow of mathematicians will become more and more similar to that of a programmer: collaborations on a large scale with a shared “codebase”, or in this case maybe “mathbase”, which is probably some large database of formalized math in proof assistants such as Lean. It would be very cool to have a complete database of all hitherto math knowledge in a single database, one that can only be created with help from autoformalization AIs. The peer review process will likely be sped up as autoformalization AIs become stronger, and will increasingly be about the value of the work instead of the correctness.
- Undergraduate and Graduate Education: This is hardest to speculate; one obvious change is more emphasis on proctored exams (which I am not really fond of). Generally speaking, I think AI is good for education in that it provides decent exposition of advanced topics, saves me time digging through obscure references, and helps me calculate examples and provide intuition. In general, it makes a lot of knowledge much more accessible. The undergraduate mathematicians right now will benefit from this, and for them graduate school will probably be even more competitive than it already is, as everyone is learning more and more at a younger age.
Why do we exist? What is the meaning of life? This line of questioning led me to my pursuit of math. I believe the search for truth is one of the most meaningful things in life, and it does not seem to me that AI will take that away. On the contrary, I’m excited to live through such a revolution in math while in grad school. Math has undergone paradigm shifts every century, and each time it turns out there is more math out there, and more things to discover. This is why I am still, generally speaking, optimistic about AI in math.