Many mathematicians predict that one of the most important mathematical stories in the 21st century will be the changing role of computers in assisting mathematicians in proving theorems, or even in proving theorems themselves. UCLA professor Terence Tao highlighted some of the history and potential future of machine-assisted mathematics at the 40th anniversary symposium for MSRI/SLMath held in April 2023.

The four-color theorem, which states that four colors suffice to color the regions of any map so that no two adjacent regions have the same color, is one of the most famous examples of computer-assisted proof. In 1976, Kenneth Appel and Wolfgang Haken reduced the proof of the theorem to verifying some key properties of 1834 different graph configurations. Electronic computers and a human computer (Haken’s daughter Dorothea Blostein) then did that verification, one case at a time. The four-color theorem’s association with computer assistance doesn’t stop there; in 1996, another group of researchers improved and streamlined the cases to 633 that could be checked solely by electronic computers. In 2005, the proof succumbed to a different notion of computer assistance: Benjamin Werner and Georges Gonthier used the proof assistant Coq to create a completely computer-verified proof of the theorem.

Human "computers" at work for NASA's Jet Propulsion Laboratory.  Credit:  NASA/JPL-CalTech

Formal proof assistants such as Coq are a little different from computer programs that evaluate equations or verify properties for a large number of inputs. Proof assistants rely on computer coding of logical statements and inference. These programs can evaluate theorems that are input and, in the case of the most modern programs, even generate their own logically consistent proofs. Some mathematicians advocate using these formal proof assistants to verify results in all areas, noting that published mathematics, even in prestigious peer-reviewed journals, is still prone to human error.

In recent years, another facet has emerged in computer assistance in mathematics: neural networks. ChatGPT has become famous (or infamous) in the broader culture as it continues to grow better and better at producing reasonable images or text in response to prompts about all sorts of different topics. But similar neural networks, which are fed examples and eventually learn to create outputs similar to those examples, have found uses in mathematics already. For example, neural networks trained on various knots and their invariants have produced some intriguing links between properties of knots that were not already known to be related. Because neural networks are somewhat opaque — they respond to inputs but cannot explain why they gave a particular response — those relationships are still being probed by human mathematicians. This preliminary work illustrates the potential for computers to assist human mathematicians by suggesting new avenues of inquiry.

Computer-assisted mathematics comes with its own challenges. On the technical side, proof assistants require a great deal of groundwork before they are able to assist with cutting-edge mathematics. When celebrated German mathematician Peter Scholze wanted to use the proof assistant Lean to verify one of his proofs, he discovered that the foundations of his research field had not yet been coded into Lean, so several preliminary pieces had to be added before work could proceed on the main theorem. Philosophically, theorems such as the four-color theorem, whose only known proofs rely on heavy-duty computation, force mathematicians to confront questions about the purpose of mathematics. A proof that relies on a computer crunching through hundreds or thousands of examples strikes many mathematicians as logically sound but intellectually unsatisfying. Is there some overarching reason why the theorem is true beyond brute force case-by-case analysis? Mathematicians are still wrestling with the importance of human understanding to their work, and they will continue to do so as computers assume new roles in mathematics.