Artificial intelligence is entering the field of mathematics. Are mathematicians ready to welcome it?

Among the collections of the Getty Museum in Los Angeles is a portrait of the 17th-century ancient Greek mathematician Euclid: he is ragged, unkempt, with his hands covered in dirt, holding up his geometry work "Elements".

For more than two thousand years, Euclid's work has served as a model for mathematical argument and reasoning.

“Euclid, as we all know, started with an almost poetic [definition],” said Jeremy Avig, a logician at Carnegie Mellon University. “And then he built on top of that the mathematics of his day, using basic concepts, definitions, and a priori theorems to prove things in such a way that each step [clearly follows] from the previous step.”

Dr. Avigad said there had been complaints that some of Euclid's "obvious" steps were not obvious, but the system still worked.

But by the 20th century, mathematicians were no longer willing to base mathematics on this intuitive geometric foundation. Instead, they developed formal systems - precise symbolic representations, rules. Eventually, this formalization allowed mathematics to be translated into computer code.

In 1976, the four-color theorem—which states that four colors are enough to fill a map so that no two adjacent areas have the same color—became the first major theorem to be proved computationally brute force.

Now, mathematicians are grappling with the forces of change:

In 2019, Chrisan Szegedy, a computer scientist who formerly worked at Google and is now working at a startup in the San Francisco Bay Area, predicted that computer systems would match or surpass the problem-solving abilities of the best human mathematicians within a decade. Last year he revised that target date to 2026.

Akshay Venkatesh, a mathematician at Princeton’s Institute for Advanced Study and winner of the 2018 Fields Medal, isn’t currently interested in using AI, but he’s keen to talk about it. “I want my students to realize that their field is going to change a lot,” he said in an interview last year. He added more recently: “I’m not against thoughtful and intentional use of technology to support our human understanding. But I firmly believe that it’s critical to be mindful of how we use it.”

In February, Dr. Avigad attended a workshop on “machine-assisted proofs” at the Institute for Pure and Applied Mathematics at the University of California, Los Angeles. The gathering attracted an atypical mix of mathematicians and computer scientists. “It felt important,” said Rence Tao, a mathematician at the university, a 2006 Fields Medal winner, and a key organizer of the workshop.

Only in recent years, Dr. Tao noted, have mathematicians begun to worry about the potential threats of artificial intelligence, both to mathematical aesthetics and to themselves. Prominent community members are now raising these questions and exploring potential “taboo-breaking,” he said. One striking workshop participant sat in the front row: a trapezoidal box called the “Raiser” that uttered a mechanical whisper and raised a hand whenever an online participant asked a question. “If it’s cute and non-threatening, it helps,” Dr. Tao said.

Bringing "Proof of the Complainers"

These days, there’s no shortage of gadgets to optimize our lives — eating, sleeping, exercising. “We like to attach things to ourselves to make it easier to get things done,” said Jdan Ellenberg, a mathematician at the University of Wisconsin-Madison, during a break in the symposium. AI devices might have the same effect on math, he added. “Obviously, the question is what machines can do for us, not what they will do to us.”

One mathematical gadget is called a proof assistant, or interactive theorem prover. (“Automation” was an early incarnation in the 1960s.) Mathematicians translate proofs step by step into code; a software program then checks that the reasoning is correct. The verifications accumulate in a library, a dynamic canonical reference that others can consult. Dr. Avigad, director of the Hoskinson Center for Formal Mathematics (funded by the cryptocurrency entrepreneur Charles Hoskinson), said that this formalization laid the foundation for today’s mathematics, “just as Euclid’s attempt to codify and organize mathematics laid the foundation for the mathematics of his time.”

Recently, the open source proof assistance system Lean has received a lot of attention. Developed by Leonardo de Moura, a computer scientist now working at Microsoft, Lean uses automated reasoning and is powered by so-called old-fashioned AI (GOFAI), i.e., symbolic AI inspired by logic. So far, the Lean community has verified an interesting theorem about flipping a sphere, a key theorem in the scheme to unify mathematical fields, and other strategies.

But the proof assistant has its drawbacks: It often complains that it doesn’t understand the definitions, axioms, or reasoning steps that the mathematician has typed, earning it the nickname “the proof complainer.” All these complaints can make research cumbersome. But the same functionality—providing line-by-line feedback—also makes the system useful for teaching, says Heather Macbeth, a mathematician at Fordham University in Durham, Massachusetts.

This spring, Dr. Macbeth designed a "bilingual" course: She translated each problem on the blackboard into Lean code in the class notes, and students submitted solutions to homework problems in both Lean and prose. "This gave them confidence," Dr. Macbeth said, because they got instant feedback on when the proof was complete and whether each step in the process was right or wrong.

After attending the workshop, Emily Riehl, a mathematician at Johns Hopkins University, used an experimental proof assistant program to formalize a proof she had previously published with a co-author. At the end of one verification, she said, “I really understood the proof very, very deeply, much more deeply than I had ever understood it before. I thought about it so clearly that I could explain it to a very dumb computer.”

Brute force reasoning—but is it mathematics?

Another automated reasoning tool used by Marijn Heule, a computer scientist at Carnegie Mellon University and an Amazon scholar, is what he calls “brute reasoning.” He says that you simply use carefully designed coding to say which “exotic object” you want to find, and a supercomputer will churn through the search space and determine whether the entity exists.

Just before the seminar, Dr. Heule and one of his Ph.D. students, Bernardo Ercaseaux, finally came up with a solution to a long-standing 50 TB file problem. However, the file bears little comparison to the result Dr. Heule and his collaborators arrived at in 2016: “200 TB mathematical proof is the largest ever,” a headline in the journal Nature announced. The article went on to ask whether solving problems with these tools really counts as mathematics. In Dr. Heule’s view, such methods are necessary “to solve problems that humans cannot solve.”

Another group of tools uses machine learning, which can synthesize large amounts of data and patterns, but is not good at logical, step-by-step reasoning. Google's DeepMind has designed machine learning to solve problems such as protein folding (AlphaFold) and chess winning (AlphaZero). In a 2021 Nature paper, a team described their work as "advancing mathematics by guiding human intuition through artificial intelligence."

Yuhuai "Tony" Wu, a former Google computer scientist and now a startup in the Bay Area, outlined a more ambitious goal for machine learning: "solving math problems." At Google, Dr. Wu explored how large language models that support chatbots could help with math. The model the team used was trained on internet data and then fine-tuned using large, math-rich datasets such as online archives of math and science papers. The specialized chatbot, called Minerva, "is very good at mimicking humans" when asked to solve math problems in everyday English, Dr. Wu said at the seminar. The model scored better than the average 16-year-old student on a high school math test.

Ultimately, Dr Wu said, he envisions an “automated mathematician” with “the ability to solve mathematical theorems on its own”.

Mathematics as a touchstone

Mathematicians have paid varying degrees of attention to these disturbances.

Michael Harris of Columbia University expressed doubts in his “Silicon Reckoner” substack. He was troubled by the potentially conflicting goals and values ​​between studying mathematics and national defense.

Dr Harris lamented the lack of discussion about the larger impact of AI on mathematical research, particularly “compared to the very active conversation going on”, which is “pretty much everywhere except mathematics”.

DeepMind collaborator Geordie Williamson of the University of Sydney spoke at NAS. Gathering and encouraging mathematicians and computer scientists to engage more in such conversations. At the Los Angeles workshop, he began his talk with a quote adapted from George Orwell's 1945 essay "You and the Atom Bomb." "It didn't generate as much discussion as expected, given that all of us are likely to be profoundly affected in the next five years," Dr. Williamson said.

Dr. Williamson believes that mathematics is the touchstone of what machine learning can or cannot do. Reasoning is the essence of mathematical processes and the key unsolved problem in machine learning.

Early in his work with DeepMind, the team found a simple one that predicted “a mathematical quantity that I care about very much,” and it did so with “ridiculous accuracy,” Dr. Williamson told me in an interview. Dr. Williamson struggled to understand why — which would form the basis of a theorem — but couldn’t. No one at DeepMind could. Like the ancient geometer Euclid, the neural network had somehow intuitively discerned mathematical truths, but the logical “why” was far from obvious.

A prominent theme at the Los Angeles workshop was how to combine intuition and logic. If AI can do both, everything will be solved.