Is Math the Next AI Frontier? A Conversation with Terence Tao
With interest growing in using AI for formal theorem proving, there is real momentum for the field of AI and mathematical research. As Tom Kalil, CEO of Renaissance Philanthropy, notes, “Progress in AI for Math can lead to the discovery of new fundamental theorems, strengthen hardware and software security, and improve the reasoning capabilities of AI models.”
To explore where the field is headed and what’s possible when AI meets formalization, Tom spoke with Terence Tao, Fields Medalist and Professor of Mathematics at the University of California, Los Angeles. They discuss the promise of collaborative math at scale, the role of philanthropy, and the practical and cultural challenges still ahead.
Check out highlights from their conversation in the following video, and read the full transcript* below.
Tom: Terry, I'd love to hear what applications of AI to fundamental math you're most excited about.
Terence: Formalization is extremely tedious and time-consuming, and there's a lot of scope for automation to improve this. I think that will be a true revolution in our subject. The dream is, of course, that AI will help us actually propose new conjectures and new ideas to solve math problems. It can also work to fill in small steps, such as doing a small computation for running small codes and relations, for example. I use AI all the time to plot various functions, which I would not have taken the time to do previously. So, this is already happening, and I think it will become much more widespread.
Similarly, my dream is that people will do math by having conversations with AI systems, which will handle a lot of the drudge work. The key problem right now is that [AI systems] make lots of mistakes, and they don't have the capability to recover from these mistakes. So, the integration of formalization will be key to keeping them on track. We’ll also need to adapt our workflows to make sure that we are not just trusting AI blindly, but that we're using it to open our own intuition and research.
Overall, yes, there's a lot of potential, and there are exciting experiments right now.
Tom: What are some other major bottlenecks that are associated with integrating AI into formalization? What are some potential research directions for addressing these challenges?
Terence: There are many issues. For example, we have cultural issues. Many of us still use blackboards and chalk, so there will be some cultural resistance to moving towards a more distributed computer-assisted model.
I think there is also a trust problem with AI. The current models are very unreliable. There was initial excitement around two, three years ago when everyone started playing with these models, but people have slowly gotten burned a few too many times. So, we need to find ways to really integrate with formal verification and similar tools, just to keep these models on track. And, we need ways to independently verify outputs. This means having both computer tools, but also training humans on how to swap out mistakes. If we had ways to make AI more trustworthy, more reliable, that would definitely be useful.
I think another bottleneck is that the most popular AI is, of course, proprietary, expensive AI, which you can't run locally. You can’t train these models on your own data. I think having more lightweight models is important. You don’t need the most advanced AI all the time. Just being able to do auto-complete, say, Lean code, [to] just fill in one or two lines at a time, is useful. It's a fairly mundane use of AI technology, but so useful. It doesn’t have to be the flashiest, latest technology to deliver the biggest productivity.
Tom: Shifting gears a little bit to the AI for Math Fund. We really benefited from having you as an advisor. Could you comment on the quality of the proposals that we received?
Terence: I was very impressed by the breadth and the depth of the proposals. The response from the community to this particular call was excellent. I think it really filled a gap. You know, these types of directions are so new that traditional funding agencies are just beginning to react. These projects often fall through the cracks. They’re not quite math, they’re not science, and they’re not quite infrastructure. They are some combination of all three.
Public funding agencies certainly haven't done nothing. They've tried some experiments. However, I think a lot of people were bottlenecked by not having funding.
Tom: On that note, what advice would you give philanthropists who are excited about the potential of AI and math and want to support projects like this?
Terence: Well, I'm very glad that there is a lot of interest. I think there's a broad range of projects to support. One method is to support big, multi-million-dollar projects, but we also need a lot of microgrants.
For example, one thing we need is community building. We have a bunch of mathematicians who already have tenure and who have some free time to devote to these projects. However, at the post-doc and graduate student level, there are a lot of young people who need stable careers. They need publications. Having support for students and post-docs to spend some time on these projects would be very useful, I think. At least in the near term, the model would probably be for many of these post-docs to continue spending a large fraction of their time on more traditional mathematics, but also have some funding for formalization projects. I think that could be quite crucial. It’s not the flashiest thing, but it builds the ecosystem.
Tom: What can Renaissance Philanthropy and other philanthropists do that is more related to field building, community building, and education?
Terence: Things like networking events create spaces where people can discuss these projects. There are various things to try, some of which may not be all that expensive, but just require some support.
I think a lot of this subject is going to be community-driven, more so than traditional math research projects, where there is a senior faculty member or expert in the field to drive us a bit forward. We actually don't have that many senior experts in formalization yet, you know. The field is just too new. So this will be a much more 21ist-century-type of field.
For example, in formalization there are a lot of contributions coming from the broader community: people in computer science, people in the tech industry, high school students, and then just members of the general public. They may not have the training to coordinate a large traditional research project with a principal investigator, but they can contribute to a large distributed project.
Tom: Many people are interested in fundamental math as an end in itself, but I think there's also interest among some philanthropists in accelerating progress in math because it is the language of science. Do you have any thoughts on the role that philanthropy could play not only at this intersection of AI and math, but also at this intersection of AI, math, and science?
Terence: That's an exciting long-term prospect. Math is unique in that we have this really reliable way to check our answers compared to science. Formal verification works really well for math problems. In the sciences, there’s going to be some transfer, ideally once we figure out how to keep AI honest with a useful form of replication—particularly in the physical sciences where we know how to simulate very well. For example, if you're going to solve a physics or engineering problem, you can run some simulations or use a CAD [Computer-Aided Design]—and that is somewhat analogous to formal verification in math. So, for instance, people are now using AI to accelerate their chip design, with the AI proposing new circuits for chips and then “verifying” them in a CAD.
The life sciences are more challenging. In the longer term, there will definitely be a lot of interaction. I think in the near term, what is missing is more interdisciplinary interaction. Mathematicians still only work with mathematicians. Physicists only work with physicists, and so on. So, I think the emerging interface between AI, math, and science is still a bit too new to launch really big projects. It's premature to create a Physicslib (on the same scale as Mathlib), for instance. One day, maybe.
I think, at some point, there just has to be some serendipitous meeting between computer scientists, physical scientists, mathematicians, you know? Then some exciting proof of concept will emerge.
Tom: I know you’ve talked about verification. Obviously, in the context of math, you can do automated theorem proving, but are there systems that allow for rapid experimental verification too? For instance, in computational fluid dynamics, could you imagine a kind of self-driving lab that provides faster feedback?
Terence: I could see that. I already use AI tools to help me code very simple computations, which I just wouldn't do before. It does enable a certain amount of experimental mathematics, which is still a very tiny fraction of current mathematical activity.
We need people with the right vision and imagination. Mathematics is entering an era of scale, where you can actually crowdsource big research projects that you would not think of doing if it were just you and your graduate students. But we have so few working examples of that scale that it’s hard to predict what is going to happen. I just started one or two projects like this, trying to prove thousands of millions of mistakes at the same time. I think once we get the culture of having these large-scale math projects, alongside more traditional projects with one or two people, that will create a demand for these platforms where a lot of people can contribute. So, it’s an area of experimentation right now.
Tom: Well, you know, one of the things that I find really interesting and important about philanthropy is its flexibility. That’s why I've been excited to launch Renaissance Philanthropy. We can get the research community to think about a broader way of doing things.
For example, I serve as the chair of Convergent Research, which has been supporting focused research organizations (FROs). These are time-bound research nonprofits with a CEO. So, they have a community of purpose, associated with a well-run startup, but because they're philanthropically funded, they have the ability to work on things that are difficult to monetize. Now that the model exists, we've got more people saying, ‘I've identified this bottleneck to progress in my field, which I might be able to address if there were an FRO working on this problem.’
If we had greater structural diversity in how we fund and organize math research, we may be able to take better advantage of new tools. Do you have any thoughts on that?
Terence: The other sciences have been able to invent new paradigms. So far, this hasn’t happened as much in mathematics, but it's on the cusp. So, it's exciting. As you say, we’re going to need new, more diverse funding structures. There will be new types of mathematicians in the future who are very good at organizing large projects. That's not a skill that we've been able to find much use for traditionally. Mathematicians–we’re famously a bunch of cats. We do our own thing. But now, we can also work at a massive scale, and this opens up all kinds of things that we could not do before.
Renaissance Philanthropy is committed to driving innovation at the intersection of AI and mathematics through partnerships with XTX Markets on initiatives such as the AI for Math Fund, which Terence Tao supported as an advisor, and programmatic support for Mathlib.
*This transcript has been lightly edited for grammar and syntax.