How Close Are Computers to Automating Mathematical Reasoning? | Mathematics - Quanta Magazine

Stephen Ornes, science writer in Nashville, Tennessee says, AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine.

Illustration of a robot and a human furiously doing math next to each other
Photo: Maria Nguyen for Quanta Magazine

In the 1970s, the late mathematician Paul Cohen, the only person to ever win a Fields Medal for work in mathematical logic, reportedly made a sweeping prediction that continues to excite and irritate mathematicians — that “at some unspecified future time, mathematicians would be replaced by computers.” Cohen, legendary for his daring methods in set theory, predicted that all of mathematics could be automated, including the writing of proofs.

A proof is a step-by-step logical argument that verifies the truth of a conjecture, or a mathematical proposition. (Once it’s proved, a conjecture becomes a theorem.) It both establishes the validity of a statement and explains why it’s true. A proof is strange, though. It’s abstract and untethered to material experience. “They’re this crazy contact between an imaginary, nonphysical world and biologically evolved creatures,” said the cognitive scientist Simon DeDeo of Carnegie Mellon University, who studies mathematical certainty by analyzing the structure of proofs. “We did not evolve to do this.”

Computers are useful for big calculations, but proofs require something different...

Useful Machines Mathematicians, logicians and philosophers have long argued over what part of creating proofs is fundamentally human, and debates about mechanized mathematics continue today, especially in the deep valleys connecting computer science and pure mathematics.

For computer scientists, theorem provers are not controversial. They offer a rigorous way to verify that a program works, and arguments about intuition and creativity are less important than finding an efficient way to solve a problem. At the Massachusetts Institute of Technology, for example, the computer scientist Adam Chlipala has designed theorem-proving tools that generate cryptographic algorithms — traditionally written by humans — to safeguard internet transactions. Already, his group’s code is used for the majority of the communication on Google’s Chrome browser.
Read more... 

Recommended Reading

 The Prime Number Conspiracy
The Biggest Ideas in Math from Quanta

The Prime Number Conspiracy: The Biggest Ideas in Math from Quanta (The MIT Press) by Thomas Lin, founding editor-in-chief of Quanta. 

Source: Quanta Magazine