Mathematics is hard, even for artificial intelligence (AI). So, when Google DeepMind’s AlphaProof and AlphaGeometry2 achieved the impressive feat of solving 4 out of 6 problems at the International Math Olympiad (IMO), mathematicians began revisiting an old question: can AI do mathematical research? Terence Tao, a professor of mathematics at the University of California, Los Angeles, predicts “In the future, I could imagine a big theorem being proven by a combination of 20 people and a bunch of AIs each proving little things.”
To mathematicians, the idea of dozens of people working on a research project, let alone with AI, is quite foreign. Most published research in mathematics is done in groups of 2 to 4 people. So, why are mathematicians so isolated? And what does AI have to do with collaboration in mathematics?
The breakthrough of computer assistance in mathematics was made in 1976 as an integral part of the Appel and Haken proof of the Four-Color Theorem. In layman’s terms, the theorem states the following: at least 4 colors are required to color a map such that any two adjacent regions are colored differently. Anyone with 4 colored pencils and a map can observe this fact. Yet, it is surprisingly difficult to prove. In fact, there is no human proof of the Four-Color Theorem.
Although mathematicians were skeptical at first, they soon accepted that, like the Four-Color Theorem, there are proofs which require computer assistance. Some ambitious few decided to push this new approach even further to determine if a mathematical proof could be done completely by a computer.
The short answer is yes: although very few proofs can be done this way. Softwares such as Coq, and in particular Lean, are among the most well-known proof assistants and used often as standards for formal proofs. In fact, as recently as 2021, Lean was used to verify a very difficult theorem of Peter Scholze, the 2018 field medalist. In principle, mathematicians translate their work into code which they then ask proof assistants like Lean to check it. Conceptually, Lean compares mathematicians’ codes with its own library: a database of basic axioms and mathematical statements. It acts like a translator checking whether the mathematicians’ sentences are grammatically correct. However, this human-machine interaction is inherently limited. For starters, the libraries of proof assistants are dependent on the mathematicians that work on them. Hence, they are limited by the expertise of their contributors.
Not only can AI be used for proof assistance, but it can also help develop meaningful partnerships between mathematicians, as mathematicians tend to work in smaller groups within their expertises. Since mathematics is a vast field, with its foundations thousands of years old, interactions between hyper specialized research groups can be limited which makes communication difficult.
Integrating AI with proof assistants, which are accessible online worldwide, subsides this problem. Instead of having to know everything required for a project, groups of specialized mathematicians can contribute to a larger problem by tackling smaller pieces of it. Such collaboration is only possible when the work of other mathematicians has been checked by proof assistants. In addition, questions that would require addressing colleagues can now be answered by AI, especially when it has access to an already established and rigorous library. Essentially, the process of doing mathematics can be subdivided into smaller and more accessible tasks.
In reality, such a project is rare while remaining a pipe dream for many. As of now, mathematicians know how to incorporate AI into their research but at a limited capacity. However, with the fast changing landscape of AI, mathematicians may soon be able to incorporate their new assistant into their every work. In combination with proof assistants, the mathematician-AI interaction has the potential to foster meaningful collaborations and expand the boundaries of discovery in a field that is thousands of years old.
“In combination with proof assistants, the mathematician-AI interaction has the potential to foster meaningful collaborations and expand the boundaries of discovery in a field that is thousands of years old.”
