AI Is Here for Mathematics, Too

By: Kyle Xu

In a museum in Los Angeles is a portrait of the ancient Greek mathematician Euclid, dated from the 17th century.

Euclid’s words were the beginning of mathematical argumentation and reasoning. “Euclid famously starts with ‘definitions’ that are almost poetic,” said Jeremy Avigad, a logician at Carnegie Mellon University. “He then built the mathematics of the time on top of that, proving things in such a way that each successive step ‘clearly follows’ from previous ones, using the basic notions, definitions and prior theorems.”

However, since modern times, mathematicians have given up on the ways of Euclid. Instead, they have decided to use formal systems, which are precise symbolic representations. But this drastic change has allowed computers to understand mathematics – and now mathematicians are facing a new force: artificial intelligence.

“I am not opposed to thoughtful and deliberate use of technology to support our human understanding. But I strongly believe that mindfulness about the way we use it is essential.” said Akshay Venkatesh, a mathematician at the Institute for Advanced Study in Princeton.

These days, electronics fill everyday life. Our computers would match or exceed the problem-solving skills of the best human mathematicians within a decade of development, as predicted by Christian Szegedy in 2019. Perhaps even by 2026.

Mathematicians have responded to these disruptions without concern. Michael Harris of Columbia University is troubled by the interloping paths between the goals of mathematicians and tech industries.

Williamson, of the University of Sydney, has encouraged computer scientists and mathematicians to be more involved. “Given how likely we all are to be profoundly affected within the next five years,” Dr. Williamson said, “Deep learning has not roused as much discussion as might have been expected.”

One math gadget is an interactive theorem prover. A mathematician translates a proof into code, and then a program corrects the reasoning. But the proof assistant also has weaknesses: the program often says that it cannot understand the steps entered by the mathematician, so some may call it a “proof whiner.”

Yuhuai “Tony” Wu, a scientist formerly at Google now with a start-up in the Bay Area, has a goal to “solve mathematics.” Dr. Wu explored large language models that might help with math at Google.

Ultimately, said Dr. Wu, he dreamt of an “automated mathematician” that has “the capability of solving a mathematical theorem all by itself.”