Not long ago, computers started solving mathematical proofs—a fact that surprised Sir Andrew Wiles. But to Wiles, who won the Silver Plaque of the IMU (1998) and the 2016 Abel Prize, the achievements of machines underscore the role that humanness plays in mathematics.

A few years ago, Wiles, who is currently a Royal Society Research Professor at Oxford, learned from one of his students that not only could computers help solve math problems—they could also discover new proofs. “I was very impressed,” Wiles said. That student was Manjul Bhargava, who went on to win the Fields Medal in 2014. It was an approach he hadn’t really considered before. “I haven’t used computers very much, except to get an idea of calculations.”

The experience made him think more deeply about the uniquely human way that mathematicians work. Because the field builds on a specialized language and history, “we make human jumps all the time,” Wiles said. Logical arguments written out in 2016 may look quite unfamiliar to mathematicians of the future. Similarly, it can be difficult for humans to understand the logic of machines.

“A machine might be able to solve a problem that a machine can understand—but we want something that humans can understand,” Wiles said. Take, for example, the Kepler conjecture, which a computer helped solve by way of an intricate proof by exhaustion. “It’s not something you can read and check as a human mind,” Wiles said. “It would be more satisfying for humans if we could find a proof that we could really see.”

That doesn’t make computer-assisted mathematics any less valid or valuable, of course. “I’m all for computers helping us get there,” Wiles said. Rather, he described interesting differences between the logic of people and machines. Computers can process large and complex masses of data; mathematicians often prefer simple formulations. Mathematicians also speak of elegance and beauty—parameters that would be very hard to define for a computer.

“I think computers, if they were to develop mathematics themselves, would not be worried about smallness and elegance,” Wiles pointed out. They might generate proofs that contain thousands or millions of steps. “Why would they worry how long it is?”

Wiles pointed out that mathematicians sometimes succeed precisely because they’re not very much like machines. In moments of difficulty, he often walks away from his work to clear his head—literally, since much of his thinking takes place in the streets and gardens of Oxford. “Somehow, your subconscious is making connections,” he said. Paradoxically, forgetfulness can become an asset. “You need a slightly bad memory, because you need to forget the way you approached it the previous time.”

Then again, the differences between people and machines might also highlight the opportunity for teamwork. It’s said that opposites attract. Perhaps humans and computers are still learning how to complement each other.

If you would like stream Sir Andrew Wiles‘ lecture at the 4th HLF, you can do that here or watch it on YouTube.

Do you know how big the embedded image

http://scilogs.spektrum.de/hlf/files/HLF2016_Tuesday003_cf-.jpg

is?

7,358.56 KB (7,535,169 bytes)

5,760px × 3,840px

Today, computers can not think and therefore they can not develop mathematics. Andrew Wiles sentence

addresses therefore not a problem of computers but a problem of humans using computers as tools. There are certainly mathematicians which are pleased by computer aided proof engines – even if the resulting proofs are not understandable for humans. Furthermore, their is no guarantee that all interesting problems (interesting for humans) can be proved by short and beautiful proofs. This is the situation for mathematics.

On the other hand, automatically verified proofs might be useful anyway. Even if they are not easily understandable. Because proofs can also be used for verification of software programs and for verification of hardware designs.

In the long run, electronic proof assistents will be used more and more anyway. And because proofs are also for human eyes, future proof assistents will have built in proof simplifiers and they will have built in criteria for “beautiful” proofs. Because today humans decide what computers should do. Computers are a long way from the ability to decide such things by themselves.