Machine-Assisted Proof

Source: Terence Tao, Notices of the AMS · 2025-01

Introduction. Mathematicians have relied upon computers (human, mechanical, or electronic) and machines to assist them in their research for centuries (or even millennia, if one considers early calculating tools such as the abacus). For instance, ever since the early logarithm tables of Napier and others, mathematicians have known the value of constructing large data sets of mathematical objects to perform computations and to make conjectures. Legendre and Gauss used extensive tables of prime numbers compiled by human computers to conjecture what is now known as the Prime Number Theorem; a century and a half later, Birch and Swinnerton-Dyer similarly used early electronic computers to generate enough data on elliptic curves over finite fields to propose their own celebrated conjecture on these objects. And many readers have undoubtedly taken advantage of one of the broadest mathematical data sets of all, the Online Encyclopedia of Integer Sequences, which has generated numerous conjectures and unexpected connections between different areas of mathematics, and serves as a valuable mathematical search engine for researchers looking for literature on a mathematical object which they do not know the name of, but which they can associate with a sequence of integers. In the 21st century, such large databases also serve as crucial training data for machine learning algorithms, which promise to automate, or at least greatly facilitate, the process of generating conjectures and connections in mathematics. Besides data generation, another venerable use of computers has been in scientific computation, which is heavily used nowadays to numerically solve differential equations and dynamical systems, or to compute the statistics of large matrices or linear operators. An early example of such computation arose in the 1920s, when Hendrik Lorentz assembled a team of human computers to model the fluid flow around the Afsluitdijk—a major dam then under construction in the Netherlands; among other things, this calculation was notable for pioneering the now-standard device of floating point arithmetic. But modern computer algebra systems (e.g., Magma, SAGE- Math, Mathematica, Maple, etc.), as well as more generalpurpose programming languages, can go well beyond traditional “number-crunching;” they are now routinely used to perform symbolic computations in algebra, analysis, geometry, number theory, and many other branches of mathematics. Some forms of scientific computation are famously unreliable due to roundoff errors and instabilities, but one can often replace these methods with more rigorous substitutes (for instance, replacing floating point arithmetic with interval arithmetic), possibly at the expense of increased runtime or memory usage. Relatives of computer algebra systems are satisfiability (SAT) solvers and satisfiability modulo theories (SMT) solvers, which can perform complex logical deductions of conclusions from certain restricted sets of hypotheses, and generate proof certificates for each such deduction. Of course, satisfiability is an NP-complete problem, so these solvers do not scale past a certain point. Here is a typical example of a result proved using a SAT solver:

• Machine learning algorithms can be used to discover new mathematical relationships, or generate potential examples or counterexamples for mathematical problems. • Formal proof assistants can be used to verify proofs (as well as the output of large language models), allow truly large-scale mathematical collaborations, and help build data sets to train the aforementioned machine learning algorithms. • Large language models such as ChatGPT can (potentially) be used to make other tools easier and faster to use; they can also suggest proof strategies or related work, and even generate (simple) proofs directly.

Each of these types of tools has already found niche applications in different areas of mathematics, but what I find particularly intriguing is the possibility of combining these tools together, with one tool counteracting the weaknesses of another. For instance, formal proof assistants and computer algebra packages could filter out the nownotorious tendency of large language models to “hallucinate” plausible-looking nonsense, while conversely these models could help automate the more tedious aspects of proof formalization, as well as provide a natural language interface to run complex symbolic or machine learning algorithms. Many of these combinations are still only at the proof-of-concept stage of development, and it will take time for the technology to mature into a truly useful and reliable tool for mathematicians.

Method. 1. Proof Assistants The mere fact that a computation was performed using a computer does not, of course, automatically guarantee it is correct. The computation could incur numerical errors, such as those caused by replacing continuous variables or equations with discrete approximations. Bugs can be inadvertently introduced into the code, or the input data may itself contain inaccuracies. Even the compiler that the computer uses to run the code could be flawed. Finally, even if the code executes perfectly, the expression that is correctly computed by the code may not be the expression that one actually wanted for the mathematical argument. Early computer-assisted proofs experienced many of these issues. For instance, the original proof of the fourcolor theorem [AH89] by Appel and Haken in 1976 revolved around a list of 1834 graphs that needed to obey two properties, called “reducibility” and “unavoidability.” Reducibility could be checked by feeding each graph one at a time into a custom-written piece of software; but unavoidability required a tedious calculation comprising hundreds of pages of microfiche—verified by hand through the heroic efforts of Haken’s daughter Dorothea Blostein—which ended up containing multiple (fixable) errors. In 1994, Robertson, Sanders, Seymour, and Thomas [RSST96] attempted to make the computational component of the Appel–Haken proof fully verifiable by computer, but ended up instead producing a simpler argument (involving just 633 graphs, and an easier procedure to verify unavoidability) that could be verified much more efficiently by computer code written in any number of standard programming languages. Proof assistants take this formalization one step further, being a special type of computer language that is designed not to perform purely computational tasks, but to verify the correctness of the conclusion of a logical or mathematical argument. Roughly speaking, each step in a mathematical proof corresponds to a number of lines of code in this language, and the overall code only compiles if the proof is valid. Modern proof assistants, such as Coq, Isabelle, or Lean, intentionally try to mimic the language and structure of mathematical writing, although they are often substantially fussier in many respects. As a simple example, in order to interpret a mathematical expression such as ab, a formal proof assistant may require one to specify precisely the “type” of the underlying variables a, b(e.g., natural numbers, real numbers, complex numbers), in order to determine which exponentiation operation is being used (which is particularly important for expressions such as 00, which have slightly different interpretations under different notions of exponentiation). Much effort has been placed into developing automated tools and extensive libraries of mathematical results to manage these low-level aspects of a formal proof, but in practice the “obvious” parts of a mathematical argument can often take longer to formalize than the “important” parts of the argument. To give just one example: given three sets A1, A2, A3, a mathematician might work with the Cartesian products (A1 ×A2)×A3, A1 ×(A2 ×A3), and ∏i∈{1,2,3} Aiinterchangeably, since they are “obviously” the “same” object; but in most formalizations of mathematics, these products are not actually identical, and a formal version of the argument may need to invest some portion of the proof establishing suitable equivalences between such spaces, and ensuring that statements involving one version of this product continue to hold for the other. For this and other reasons, the task of converting a proof written by a human mathematician—even a very careful one—to a formal proof that compiles in a formal proof assistant is quite time consuming, although the process has gradually become more efficient over time. The aforementioned four-color theorem was formalized in Coq by Werner and Gonthier in 2005 [Gon08]. The infamous Kepler conjecture on the densest packing of R3 by unit balls was proven by Hales and Ferguson in 1998 [Hal05] in a very complicated (and computer-assisted) proof.

Discussion. Furthermore, the models are often opaque, in the sense that it is difficult to extract from the model a human-understandable explanation of why the model made a particular prediction, or to understand the model’s behavior in general. As such, these tools would appear at first glance to be unsuited for research mathematics, where one desires both rigorous proof and intuitive understanding of the arguments. Nevertheless, there have been recent promising use cases of a suitably chosen machine learning tool to produce, or at least suggest, new rigorous mathematics, particularly when combined with other, more reliable techniques that can validate the output of these tools. For instance, a fundamental problem in the mathematical theory of fluid equations such as the Euler or Navier–Stokes equations is to be able to rigorously demonstrate finite time blowup of solutions uin finite time from smooth initial data. The most notorious instance of this concerns the incompressible Navier–Stokes equations in three dimensions, the resolution of which is one of the (unsolved) Millennium Prize problems; this still remains out of reach, but recent progress has been made on other fluid equations, such as the Boussinesq equations in two dimensions (a simplified model for the incompressible Euler equations in three dimensions). One route to establishing such a singularity lies in constructing a self-similar blowup solution u, which is described by a lower-dimensional function Uthat solves a simpler PDE. A closed-form solution for this PDE does not seem to be available; but if one can produce a sufficiently high-quality approximate solution ̃U to this PDE (which approximately obeys certain boundary conditions), it can be possible to then rigorously demonstrate an exact solution Uby an application of perturbation theory (such as those based around fixed point theorems). Traditionally, one would use numerical PDE methods to try to produce these approximate solutions ̃U, for instance by discretizing the PDE into a difference equation, but it can be computationally expensive to use such methods to obtain solutions with the desired level of accuracy. An alternate approach was proposed in 2019 by Wang, Lai, G ́omez-Serrano, and Buckmaster [WLGSB23], who used a Physics Informed Neural Network (PINN) trained to generate functions ̃Uthat minimized a suitable loss function measuring the extent to which the desired PDE and boundary conditions are being approximately obeyed. As these functions ̃Uare generated through a neural network rather than a discretized version of the equation, they can be faster to generate, and potentially less susceptible to numerical instabilities. As it turned out, a contemporaneous work by Chen and Hou [CH22] was able to establish finite time blowup for this equation using more traditional numerical methods; however, the machine learning paradigm shows great potential as a complementary approach components of the data may be easily discoverable by machine learning algorithms in one data representation, but nearly impossible to find in another. While some fields of mathematics are beginning to compile large databases of useful objects (e.g., knots, graphs, or elliptic curves), there are still many important classes of more vaguely defined mathematical concepts that have not been systematically placed into a form usable for machine learning.

Conclusion. 5. Further Reading The subject of machine-assisted proof is quite diffuse, distributed across various areas of mathematics, computer science, and even engineering; while each individual subfield has plenty of activity, it is only recently that efforts have been made to build a more unified community bringing together all of the topics listed here. As such, currently there are few places where one can find holistic surveys of these rapidly developing modalities of mathematics. One starting point is the proceedings [Kor23] of a June 2023 National Academies workshop on “AI to Assist Mathematical Reasoning” (which the author was a co-organizer of); as one of the outcomes of that workshop, Talia Ringer led an effort to compile AI for mathematics resources, the results of which may be found at https://docs.google.com/document/d /1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0. For instance, in that document is a link to the “Natural Number Game” that is an accessible and interactive way to get acquainted with the Lean proof assistant language. Many of the examples discussed here were also drawn from a February 2023 IPAM workshop on “Machine assisted proof” (which the author also co-organized), whose talks may be found online. We thank the anonymous referee for corrections and suggestions.