…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…
Q: 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?
Terence Tao: 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. 5 is kind of a maximum [number of collaborators], usually.
Q: With the advent of automated proof checkers, how is this changing?
T. Tao: 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.
Q: German mathematician and Fields Medalist Peter Scholze collaborated in a Lean project—even though he told me he doesn’t know much about computers.
T T: 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.
Q: 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?
T: 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.
Q: So it’s not a question of computing power?
T: 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.
[No, it is—that is what a compute bottleneck looks like! With enough compute, they would not be doing most of this, like organizing gangs of humans to swarm a proof, or trying to build up big standard libraries, or worrying about “user friendliness”—but simply letting the theorem provers prove everything.]