AI Will Become Mathematicians’ ‘Co-Pilot’

Scientific American

Fields Medalist Terence Tao explains how proof checkers and AI programs are dramatically changing mathematics.

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 WissenschaftScientific American’sGerman-language sister publication.

[An edited transcript of the interview follows.]

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.

Read More