Mathematics and AI

Mathematical research (including research in algorithms and complexity theory and other areas of theoretical computer science) is being shaken up by developments in generative AI. Here are some writings on the topic that I particularly like:

The recent rush by some mathematicians to feed so many of our problems into generative AI models is leading to an odd situation where humans are currently becoming line-checking referees for machines. This way of working is likely to lead to decreased human understanding in the long run. It is easy to line-check a proof without really understanding the essence of it, and the essence is what is important. As a side note, this way of working also takes the joy out of mathematics -- line-checking is one of the least enjoyable parts of being a mathematician -- the best part is working together to solve problems.

The combination of the new availability of AI tools and the existing culture in mathematics causes a particular problem for young researchers. Traditionally, PhD supervisors find "somewhat easy" problems for PhD students. The student works on these problems (with the supervisor) -- learning along the way. It takes a long time because there is a lot to learn. After that, the student's track record of "problems solved" is the credential that leads to postdoctoral research positions (and to permanent positions). With the availability of AI tools it is increasingly difficult to find suitable "somewhat easy" problems (a problem that can be solved by a new PhD student may well be solvable using high-end AI models). More generally, it seems that the track record of problems solved is going to be a bad metric for judging mathematicians in the future, at least in the near future -- I agree with Tao that the best solution for the mathematical community may be to put more emphasis on exposition and much more emphasis on high-level understanding.

I am somewhat encouraged by current work on formalising mathematics (checking proofs using Lean, or other theorem provers). Since mathematics is cumulative, it is important to keep the literature from being cluttered with incorrect proofs. However, the increasing volume of AI-generated proofs is a real problem - not all of these are correct and the community can't keep up with checking them. Work on auto-formalisation is therefore relevant. Two caveats: (1) Formalisation cannot completely solve the problem - humans would still need to verify that the problems are correctly translated into Lean, and also that all of the Mathlib libraries that get used in the proofs are correct. (2) Formalisation is not enough. The ultimate purpose of maths is not just to produce solutions to problems - it is to produce understanding. Formal proofs do not really do this. In fact, they are particularly difficult to read because they miss essential intuitive explanation.

Going beyond mathematics, I am a little bit worried about the impact on society of the cognitive outsourcing that seems to be occurring. In any case, I think it is time for the maths community (including Theoretical CS) to step back and think about our objectives. AI is a useful tool, which is clearly here to stay. We need to think about the culture and working practices of our field in order to figure out how to use it wisely.

I plan to update this page as frequently as I can -- feel free to send me your ideas and thoughts.