Mathematicians don’t need to worry about AI taking over their jobs just yet
You don’t need a human brain to do maths — even artificial intelligence can write airtight proofs of mathematical theorems.
An AI created by a team at Google has proven more than 1200 mathematical theorems. Mathematicians already knew proofs for these particular theorems, but eventually the AI could start working on more difficult problems.
One of the core pillars of maths is the concept of proof. It is an argument based on known statements, assumptions, or rules, that a certain mathematical statement, such as a theorem, is true.
To train their AI, the Google team started with a database of more than 10,000 human-written mathematical proofs, along with the reasoning behind each step known as a tactic. Tactics could include using a known property about numbers, such as the fact that multiplying x by y is the same as multiplying y by x, or applying the chain rule.
Then, they tested the AI on 3225 theorems it hadn’t seen before and it successfully proved 1253 of them. Those that it couldn’t prove were because it had only 41 tactics at its disposal.
To prove each theorem, the AI split them into smaller and smaller components using the list of tactics. Eventually each of the smaller components could be proven with a single tactic, thus proving the larger theorem.
“Most of the proofs we used are relatively short, so they don’t require a lot of long complicated reasoning, but this is a start,” says Christian Szegedy at Google. “Where we want to get to is a system that can prove all the theorems that humans can prove, and maybe even more.”
Tackling harder problems
While this particular algorithm is focused on linear algebra and complex calculus, changing its training set could allow it to do any sort of mathematics, says Szgedy. For now, the AI’s main application is filling in the details of long and arduous proofs with extreme precision.
Mathematicians often make intellectual jumps in their proofs without spelling out the exact tactics used to get from one step to the next, and provers like this could walk through the intermediate work automatically, without requiring a human mathematician to fill in each exact tactic used.
“You get the maximum of precision and correctness all really spelled out, but you don’t have to do the work of filling in the details,” says Jeremy Avigad at Carnegie Mellon University in Pennsylvania. “Maybe offloading some things that we used to do by hand frees us up for looking for new concepts and asking new questions.”
AIs like this could one day even solve maths problems we don’t know how to solve or that are too long and complicated. But that will take a much larger training set, more tactics, and a simpler way to plug the theorems into the computer. “That’s far away, but I think it could happen in our lifetime,” says Szgedy.
“Pretty much anything that you can state and try to prove mathematically, you can put into this system,” says Avigad. “You can distill just about all of mathematics down to very basic rules and assumptions, and these systems implement those rules and assumptions.”
All of this happens in a matter of seconds per proof and the only source of error is the translation of the theorem into formal language the computer can understand. Szegedy says that the team is now working on the problem of automatic translation so that it’s easier for mathematicians to interact with the system.
For more such insights, log into www.international-maths-challenge.com.
*Credit for article given to Leah Crane*