A.I. is Advancing in Mathematics

By: Jeffrey Wu

For over 2,000 years, Euclid's work constituted the foundation of mathematical argumentation and reasoning: a method of proving theorems in which each step logically follows the preceding step. Mathematicians, exhausted by the twentieth century, devised new symbolic representations that could be readily converted to computer code, using technology and artificial intelligence to check coherence or brute-force solutions.

In 1976, the four-color theorem, which states that four colors are sufficient to be able to color every region on any map such that no two adjacent regions are the same color, was the first major theorem to be proved by computational brute force. Since then, numerous new advancements have occurred. A.I. chatbots are now scoring higher than the average 16-year-old on school math tests. Christian Szegedy, a former computer scientist at Google and now at San Francisco Bay Area, predicts that by 2026, a computer system will match or exceed the problem-solving ability of the top human mathematicians.

“It feels consequential,” says mathematician Terrance Tao teaching at UCLA, winner of a Fields Medal in 2006. He continued, saying that only in the last few years have mathematicians been concerned about A.I.'s capabilities, either fearing the ruined aesthetics of mathematics or worrying that they will lose their jobs, while others are experimenting and exploring its potential.

Proof assistant Lean, a software program used to check whether each step in a proof is correct, has assisted in verifying a theorem concerning a sphere being turned inside out and the formalization of a liquid real vector space theorem.

Heather Macbeth, a mathematician at Fordham University, has incorporated Lean into her courses, providing lecture notes as well as the translated code. Students were required to submit their solutions both in Lean and written or typed form. “It gave them confidence,” Dr. Macbeth said, because they received instant line-by-line feedback on when the proof was finished.

With A.I. already this powerful, it's no wonder that people want to improve it. Yuhuai “Tony” Wu, a computer scientist who previously worked at Google and is currently working with a start-up in the Bay Area, has envisioned an “automated mathematician” that has “the capability of solving a mathematical theorem all by itself.”

Source:

https://www.crunchbase.com/person/christian-szegedy

https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html