Mathematics is traditionally a solitary science. In 1986 Andrew Wiles withdrew to his study for seven years to prove Fermat’s theorem. The resulting proofs are often difficult for colleagues to understand, and some are still controversial today. But in recent years ever larger areas of mathematics have been so strictly broken down into their individual components (“formalized”) that proofs can be checked and verified by computers.
Terence Tao of the University of California, Los Angeles, is convinced that these methods open up completely new possibilities for cooperation in mathematics. And if the latest advances in artificial intelligence are added to this, completely new ways of working could be established in the field in the coming years. With the help of computers, big, unsolved problems could come closer to being solved. Tao laid out his views on what is to come in an interview with Spektrum der Wissenschaft, Scientific American’sGerman-language sister publication.
[An edited transcript of the interview follows.]
On supporting science journalism
If you’re enjoying this article, consider supporting our award-winning journalism by subscribing. By purchasing a subscription you are helping to ensure the future of impactful stories about the discoveries and ideas shaping our world today.
In one of your talks at the Joint Mathematics Meetings in San Francisco, you seemed to suggest that mathematicians don’t trust each other. What did you mean by that?
I mean, we do, but you have to know somebody personally. It’s hard to collaborate with people who you’ve never met unless you can check their work line by line. Five is kind of a maximum [number of collaborators], usually.
With the advent of automated proof checkers, how is this changing?
Now you can really collaborate with hundreds of people that you’ve never met before. And you don’t need to trust them, because they upload code and the Lean compiler verifies it. You can do much larger-scale mathematics than we do normally. When I formalized our most recent results with what is called the Polynomial Freiman-Ruzsa (PFR) conjecture, [I was working with] more than 20 people. We had broken up the proof in lots of little steps, and each person contributed a proof to one of these little steps. And I didn’t need to check line by line that the contributions were correct. I just needed to sort of manage the whole thing and make sure everything was going in the right direction. It was a different way of doing mathematics, a more modern way.
German mathematician and Fields Medalist Peter Scholze collaborated in a Lean project—even though he told me he doesn’t know much about computers.
With these formalization projects, not everyone needs to be a programmer. Some people can just focus on the mathematical direction; you’re just splitting up a big mathematical task into lots of smaller pieces. And then there are people who specialize in turning those smaller pieces into formal proofs. We don’t need everybody to be a programmer; we just need some people to be programmers. It’s a division of labor.
I heard about machine-assisted proofs 20 years ago, when it was a very theoretical field. Everybody thought you have to start from square one—formalize the axioms and then do basic geometry or algebra—and to get to higher mathematics was beyond people’s imagination. What has changed that made formal mathematics practical?
One thing that changed is the development of standard math libraries. Lean, in particular, has this massive project called mathlib. All the basic theorems of undergraduate mathematics, such as calculus and topology, and so forth, have one by one been put in this library. So people have already put in the work to get from the axioms to a reasonably high level. And the dream is to actually get [the libraries] to a graduate level of education. Then it will be much easier to formalize new fields [of mathematics]. There are also better ways to search because if you want to prove something, you have to be able to find the things that it already has confirmed to be true. So also the development of really smart search engines has been a major new development.
So it’s not a question of computing power?
No, once we had formalized the whole PFR project, it only took like half an hour to compile it to verify. That’s not the bottleneck—it’s getting the humans to use it, the usability, the user friendliness. There’s now a large community of thousands of people, and there’s a very active online forum to discuss how to make the language better.
Is Lean the state of the art, or are there competing systems?
Lean is probably the most active community. For single-author projects, maybe there are some other languages that are slightly better, but Lean is easier to pick up in general. And it has a very nice library and a nice community. It may eventually be replaced by an alternative, but right now it is the dominant formal language.
When you gave a talk about a different mathematical project, someone asked you if you wanted to formalize it, and you basically said that it takes too long.
I could formalize it, but it would take a month of my time. Right now I think we’re not yet at the point where we routinely formalize everything. You have to pick and choose. You only want to formalize things that actually do something for you, such as teach you to work in Lean, or if other people really care about whether this result is correct or not. But the technology is going to get better. So I think the smarter thing to do in many cases is just to wait until it’s easier. Instead of taking 10 times as long to formalize it, it takes two times as long as the conventional way.
You even talked about getting that factor down to less than one.
With AI, there’s a real potential of doing that. I think in the future, instead of typing up our proofs, we would explain them to some GPT. And the GPT will try to formalize it in Lean as you go along. If everything checks out, the GPT will [essentially] say, “Here’s your paper in LaTeX; here’s your Lean proof. If you like, I can press this button and submit it to a journal for you.” It could be a wonderful assistant in the future.
So far, the idea for the proof still has to come from the human mathematician, doesn’t it?
Yes, the fastest way to formalize is to first find the human proof. Humans come up with the ideas, the first draft of the proof. Then you convert it to a formal proof. In the future, maybe things will proceed differently. There could be collaborative projects where we don’t know how to prove the whole thing. But people have ideas on how to prove little pieces, and they formalize that and try to put them together. In the future, I could imagine a big theorem being proven by a combination of 20 people and a bunch of AIs each proving little things. And over time, they will get connected, and you can create some wonderful thing. That will be great. It’ll be many years before that’s even possible. The technology is not there yet, partly because formalization is so painful right now.
I have talked to people that try to use large language models or similar machine-learning technologies to create new proofs. Some have said that in three years mathematics will be “solved” in the same sense that chess is solved—that machines will be better than any human at finding proofs.
I think in three years AI will become useful for mathematicians. It will be a great co-pilot. You’re trying to prove a theorem, and there’s one step that you think is true, but you can’t quite see how it’s true. And you can say, “AI, can you do this stuff for me?” And it may say, “I think I can prove this.” I don’t think mathematics will become solved. If there was another major breakthrough in AI, it’s possible, but I would say that in three years you will see notable progress, and it will become more and more manageable to actually use AI. And even if AI can do the type of mathematics we do now, it means that we will just move to a to a higher type of mathematics. So right now, for example, we prove things one at a time. It’s like individual craftsmen making a wooden doll or something. You take one doll and you very carefully paint everything, and so forth, and then you take another one. The way we do mathematics hasn’t changed that much. But in every other type of discipline, we have mass production. And so with AI, we can start proving hundreds of theorems or thousands of theorems at a time. And human mathematicians will direct the AIs to do various things. So I think the way we do mathematics will change, but their time frame is maybe a little bit aggressive.
I interviewed Peter Scholze when he won the Fields Medal in 2018. I asked him, How many people understand what you’re doing? And he said there were about 10 people.
With formalization projects, what we’ve noticed is that you can collaborate with people who don’t understand the entire mathematics of the entire project, but they understand one tiny little piece. It’s like any modern device. No single person can build a computer on their own, mine all the metals and refine them, and then create the hardware and the software. We have all these specialists, and we have a big logistics supply chain, and eventually we can create a smartphone or whatever. Right now, in a mathematical collaboration, everyone has to know pretty much all the mathematics, and that is a stumbling block, as [Scholze] mentioned. But with these formalizations, it is possible to compartmentalize and contribute to a project only knowing a piece of it. I think also we should start formalizing textbooks. If a textbook is formalized, you can create these very interactive textbooks, where you could describe the proof of a result in a very high-level sense, assuming lots of knowledge. But if there are steps that you don’t understand, you can expand them and go into details—all the way down the axioms if you want to. No one does this right now for textbooks because it’s too much work. But if you’re already formalizing it, the computer can create these interactive textbooks for you. It will make it easier for a mathematician in one field to start contributing to another because you can precisely specify subtasks of a big task that don’t require understanding everything.
A mathematical proof is not just about checking off that something is correct. A proof is also about understanding something, right? There are beautiful proofs, and there are ugly proofs that are very technical. A good proof gives you a higher understanding of the matter. So if we delegate that to machines, will we still be able to understand what they have found out?
What mathematicians are doing is that we’re exploring the space of what is true and what is false and why things are true. And the way we do it is through proofs. Everyone knows that when it’s true, we have to go try and prove it or disprove it. And that takes a lot of time. It’s tedious. But in the future, maybe we will just ask an AI, “Is this true or not?” And we can explore the space much more efficiently, and we can try to focus on what we actually care about. The AI will help us a lot by accelerating this process. We will still be driving, at least for now. Maybe in 50 years things will be different. But in the near term, AI will automate the boring, trivial stuff first.
Will AI help us solve the big, unanswered problems in mathematics?
If you want to prove an unsolved conjecture, one of the first things you need to do is to break it up into smaller pieces, each of which has a better chance of being proven. But you will often break up a problem into harder problems. It’s very easy to transform a problem into one that’s harder than into one that’s simpler. And AI has not demonstrated any ability to be any better than humans in this regard.
By breaking down a problem and exploring it, you learn a lot of new things on the way, too. Fermat’s Last Theorem, for example, was a simple conjecture about natural numbers, but the math that was developed to prove it isn’t necessarily about natural numbers anymore. So tackling a proof is much more than just proving this one instance.
Let’s say an AI supplies an incomprehensible, ugly proof. Then you can work with it, and you can analyze it. Suppose this proof uses 10 hypotheses to get one conclusion—if I delete one hypothesis, does the proof still work? That’s a science that doesn’t really exist yet because we don’t have so many AI-generated proofs, but I think there will be a new type of mathematician that will take AI-generated mathematics and make it more comprehensible. Like, we have theoretical and experimental science. There are lots of things that we discover empirically, but then we do more experiments, and we discover laws of nature. We don’t do that right now in mathematics. But I think there’ll be an industry of people trying to extract insight from AI proofs that initially don’t have any insight.
So instead of this being the end of mathematics, would it be a bright future for mathematics?
I think there’ll be different ways of doing mathematics that just don’t exist right now. I can see project manager mathematicians who can organize very complicated projects—they don’t understand all the mathematics, but they can break things up into smaller pieces and delegate them to other people, and they have good people skills. Then there are specialists who work in subfields. There are people who are good at trying to train AI on specific types of mathematics, and then there are people who can convert the AI proofs into something human-readable. It will become much more like the way almost any other modern industry works. Like, in journalism, not everyone has the same set of skills. You have editors, you have journalists, and you have businesspeople, and so forth—we’ll have similar things in mathematics eventually.
The math we do is the math that matches our brain, isn’t it? And if at some point AI is so much smarter, it might go into regions that we have problems wrapping our mind around.
Mathematics is already bigger than any one human mind. Mathematicians routinely rely on results that other people have proven. They kind of know why it’s true, they have some intuition, but they can’t break it up all the way down to the axioms. But they know where to look, or maybe they know someone who can. We already have lots of theorems that are only verified by a computer, where some massive computer calculation has checked a million cases. You could verify it by hand, but no one has the time to do it, and it’s not worth it. So I think we will adapt. It is not necessary for one person to check everything. Getting computers to do the checking for us, that’s fine by me.
At the forefront of math, there’s a lot happening that pulls together things from seemingly unrelated fields, and from my naive understanding, an AI that knows all of these fields could give you a hint and say, “Why don’t you look there? That might help you solve your problem.”
It’s a very exciting potential use of AI to create connections or at least point out possible connections. Right now it has a very lousy success rate. It might give you 10 suggestions of which one is interesting and nine are rubbish. It’s actually almost worse than random. But this could change in the future.
What are the problems that stand in the way of training a mathematical AI?
Part of the problem is that it doesn’t have enough data to train on. There are published papers online that you can train it on. But I think a lot of the intuition is not captured in the printed papers in journals but in conversations with mathematicians, in lectures and in the way we advise students. Sometimes I joke that what we need to do is to get GPT to go take a standard graduate education, sit in graduate classes, ask questions like a student and learn like humans learn mathematics.
The published version of a proof is always condensed. And even if you take all the math that has been published in the history of mankind, it’s still small compared to what these models are trained on.
And people only publish the success stories. The data that are really precious are from when someone tries something, and it doesn’t quite work, but they know how to fix it. But they only publish the successful thing, not the process.
Maybe you should register efforts to prove something, like in medical studies. The researchers would register it, and then they would have to publish it even if it didn’t work out.
We don’t have that culture. Maybe in the future formalization will become very efficient, and you might be able to formalize things in real time. And maybe if you want to use some fancy AI Lean of 2040 on a research project and you want to get funding to use this fancy AI, you have to agree that your process of trying things and failing is recorded. And then that could be used to train future AIs. Or maybe some other group is working on a similar problem, and they can see, “oh, this other group tried the same thing, but they failed,” so that you don’t have to waste time making exactly the same mistakes.
Are mathematicians wasting a lot of time?
Oh, very much so. So much knowledge is somehow trapped in the head of individual mathematicians. And only a tiny fraction is made explicit. But the more we formalize, the more of our implicit knowledge becomes explicit. So there’ll be unexpected benefits from that.
This article originally appeared in Spektrum der Wissenschaft and was reproduced with permission.