By: Alex Tang

Two thousand years ago, the Greek mathematician Euclid wrote the treatise Elements, which is the best example of mathematical proof and reasoning from its time. Elements was based on geometric intuition. Yet, by the 20th century, mathematicians wanted a new system other than intuitive geometry, so they developed formal systems which could be translated into computer code. In 1976, the four-color theorem, which states that four colors are sufficient to fill a region without any parts of the same color touching, was the first major theorem that was proven using computational brute force.

Now, the next thing to change mathematics is artificial intelligence.

In 2019, Christian Szegedy, a computer scientist formerly at Google and now at a start-up in the Bay Area, predicted that a computer system would match or exceed the problem-solving ability of the best human mathematicians within a decade. Last year he revised the target date to 2026.

In the modern world, there are many tools and gadgets we can use to enhance our lives, whether it is in sleep, fitness, health, or other areas. “It’s very clear that the question is, ‘What can machines do for us,’ not, ‘What will machines do to us,’” Jordan Ellenberg, a mathematician at the University of Wisconsin-Madison, said.

One of the earliest gadgets to advance mathematics was the proof assistant. To use a proof assistant, a mathematician would input a proof as code into a program to be verified. The verifications would be stored in a library that others could look at. A proof assistant called Lean, developed at Microsoft by computer scientist Leonardo de Moura, has made some very interesting revelations, including one about turning a sphere inside out. However, a proof assistant also has drawbacks. Proof assistants often complain that they do not understand the proof, giving it the name “proof whiner.”

Another tool uses brute force to search for a particular item within a large data set. In 2016, Dr. Marijn Heule, a computer scientist at Carnegie Mellon University and an Amazon scholar, and his associates produced a 200 terabyte file as a proof for a math problem. In Dr. Heule’s view, this approach is needed “to solve problems that are beyond what humans can do.”

Some mathematicians have voiced concerns about AI. Michael Harris, from Columbia University, is troubled by the potentially conflicting goals and values of research mathematics and the tech and defense industries.

Geordie Williamson, from the University of Sydney, has urged mathematicians and computer scientists to be more involved in conversations. “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.”

Sources: