July 4, 2023. Artificial intelligence is invading math! That is the theme of Siobhan Robert’s report in The New York Times, “A.I. is Coming for Mathematics, Too”; physicist Peter Woit’s comments on “Not Even Wrong”; and mathematician Michael Harris’s ongoing agonizing on “Silicon Reckoner.” I recently wrote about this trend in Scientific American. Below is a free, updated version of that column. – John Horgan

Pure mathematics fascinates me, precisely because it is so inaccessible. I envision it as a remote, chilly, perilous realm, like Antarctica’s Sentinel Range. The hardy souls who scale the heights of mathematics seem superhuman.

I once asked André Weil, a legendary climber of mathematical peaks, if it bothered him that few people knew of, and fewer still understood, his accomplishments. He seemed puzzled by the question. No, he replied, “that makes it more exciting.” In his autobiography, Weil says his work transports him into “a state of lucid exaltation in which one thought succeeds another as if miraculously.”

Perhaps because I romanticize mathematicians, I’m troubled by the thought that machines might replace them. I broached this possibility in “The Death of Proof,” published three decades ago in Scientific American. In response to the growing complexity of mathematics, I reported, mathematicians were becoming increasingly reliant on computers. I asked, “Will the great mathematicians of the next century be made of silicon?”

Mathematicians are still giving me grief about that article, even as the trends I described have grown stronger. Anthony Bordg, for example, worries that his field could face a “replication crisis” like that plaguing scientific research. Mathematicians, Bordg notes in The Mathematical Intelligencer, sometimes accept a proof not because they have checked it, step by step, but because they trust the proof’s methods and author.

Given the “increasing difficulty in checking the correctness of mathematical arguments,” Bordg says, old-fashioned peer review may no longer be sufficient. Prominent mathematicians have published “proofs” so novel and elaborate that even specialists in the relevant mathematics can’t verify them. Take a 2012 proof in which Shinichi Mochizuki claims to have proved the ABC conjecture, a problem in number theory. Over the past decade, mathematicians have organized conferences to determine whether Mochizuki’s proof is true—in vain. Some accept it, others don’t. [See update below.]

Bordg suggests that computerized “proof assistants” will help validate proofs. Researchers at Microsoft have already invented an “interactive theorem prover” called Lean that can check proofs and even propose improvements—much as word-processing programs check our prose for errors and finish sentences for us. Lean is linked to a database of established results. New mathematical work must be laboriously translated into a language that Lean recognizes. But souped up with artificial intelligence, programs such as Lean could eventually “discover new mathematics and find new solutions to old problems,” according to a report in Quanta Magazine.

Some mathematicians welcome the “digitization” of mathematics, which would facilitate computer verification and make mathematics more trustworthy. Others, such as Michael Harris, are ambivalent. Advances in computer-aided mathematics, Harris says, raise a profound question: What is the purpose of mathematics? Harris sees mathematics as “a free, creative activity” that, like art, is pursued for its own sake, for the sheer joy of discovery and insight.

Harris isn’t opposed to the mechanization of mathematics per se. In a recent article, Harris points out that mathematicians have used mechanical devices, such as the abacus, for millennia. And mathematicians, after all, invented the computer.

But Harris worries that tools such as Lean will encourage a “stunted vision” of mathematics as an economic commodity or product rather than “a way of being human.” After all, funders of mathematical research like Google and the National Security Agency value mathematics primarily for its applications. As Harris puts it, mathematics is “indispensable for engineering, technology, record keeping, and any activity that involves predicting the future.”

We value science for its applications, too. Sentimental science writing, including mine, implies that science’s purpose is insight into nature. In the modern era, however, science’s primary goal is power. Science helps us manipulate nature for various ends: to extend our lives, to enrich and entertain us, to boost the economy, to defeat our enemies. Modern physics, to most of us, is unintelligible, but who cares when physics gives us smartphones and hydrogen bombs?

Physicists often adopt a utilitarian mindset, exemplified by the slogan “Shut up and calculate!” That is what professors supposedly tell students baffled by quantum mechanics. The message is that students should apply quantum formulas—for example, by building quantum computers—without worrying about their meaning. Stephen Hawking and Martin Rees have predicted that artificial intelligence will play an increasing role in physics. Wouldn’t it be funny if a quantum AI finds the long-sought unified theory of physics, but not even brilliant string theorist Edward Witten understands it?

The mechanization of knowledge brings to mind the Chinese room experiment. In this famous philosophical argument, questions written in Chinese are fed to a man in a room. Although the man doesn’t understand Chinese, he has a manual that tells him how to respond to one string of Chinese characters with another string, which represents an appropriate answer to the question. In this way, the man in the room mimics understanding of Chinese.

Philosopher John Searle intended the Chinese room experiment as a critique of the claim that machines can think. Searle likens computers to the man in the room, mindlessly processing symbols without knowing what they mean. The more mathematicians and scientists rely on machines for doing their work, the more they resemble the man in the Chinese room.

When I raised the specter of artificial mathematicians a few years ago, Scott Aaronson, whose work spans computer science, mathematics and physics, chided me. “It’s conceivable that someday,” Aaronson said, “computers will replace humans at all aspects of mathematical research—but it’s also conceivable that, by the time they can do that, they’ll be able to replace humans at music and science journalism and everything else!” At the time, I took Aaronson’s remark as a joke, but now, post-ChatGPT, it seems like a prophesy.

By the way, the question asked by my headline “Should Machines Replace Mathematicians?” is arguably beside the point, because it implies that mathematicians have a choice. A better question is whether machines can replace mathematicians. Although I’m skeptical of some claims made for artificial intelligence, it seems pretty clear that machines are already replacing human mathematicians, just as they have replaced human bank tellers, travel agents and cashiers. Mathematicians’ wishes, such as their desire to pursue truth purely for its own sake, so they can feel the “lucid exaltation” described by André Weil, are moot.

In the future, mathematics might resemble not a remote mountain range but a factory in which robots assemble cars. A few human technicians roam the factory floor, making sure the robots are working properly, but the robots do all the heavy lifting. Meanwhile, the already rich, powerful humans who own the factories keep getting richer and more powerful.

Update, July 7, 2023: Peter Woit reports that two mathematicians have proven that Mochizuki’s proof is flawed.

Further Reading:

See my columns on how AI execs resemble the mobsters in “The Sopranos”; on “conservation of ignorance”; and on the link between math and “ultimate truth.”