Towards Automated Verification of Math

Given the proliferation of computers in so many aspects of our lives, it has always surprised me that verification of submitted math research is not yet totally automated. In practice, requirements like the conferral of doctoral degrees or the referral process for arXiv are still used today in order to judge whether a proposed research contribution is valid or not. This is despite the fact that the subject of math itself is supposed to be only dependent upon formal logic for validity. The idea of automating the verification of math is not a new one, and since the twentieth century there have been some interesting proposals and thoughts towards making it happen.

In this post, I discuss a point that can give us insight into some of the difficulties involved in fully automating verification, as well as what the future can hold.

The Informal Communication of Formal Reasoning

While math itself is formal, the way math is communicated amongst humans is informal.

There are various reasons that can help partially explain this. One such reason is that actually writing out each of the basic steps of a proof would be unbearably painstaking and time-consuming, especially for many of the standard proofs. Furthermore, humans view some steps as requiring greater leaps of faith to come up with, and other steps as more directly derivable from known information. Thus, mathematicians commonly skip the steps in proofs which they think are more “direct,” and they expect readers to fill in those details. But this requires informal judgment of what is direct and what is not. (A proxy may be some sort of “logical distance metric” that is computed based on say the minimum number of logical rule applications needed to go from the current to the next step, but this proxy may not reflect informal understanding of directness, especially when mathematicians use phrases such as “similarly.”) For computers, the resulting candidates for proofs would just not be complete, and therefore not fully verifiable.

Another reason involves the reuse of the same symbols and notation for different mathematical concepts — for instance, fraction notation can be reused in a totally different way to represent a derivative, as . Humans may use informal contextual understanding to resolve such ambiguities. And there are even further ambiguities in mathematical terminology — for example, we use the word “algebra” to refer to a subject and to a specific concept in the subject. Such situations also require some informal understanding to resolve.

Beyond ambiguous language, listing out all the conditions required for a theorem may often be painstaking. For instance, when we state the commutative property of addition as , we understand that and are elements of a “known universe of discourse.” For example, in a pre-college algebra class they could be real numbers, while in an abstract algebra class they could be elements of an abelian group. We informally understand some of the conditions required for our statements to be true, and even our inclusion of quantifiers like “for all” implicitly involves an assumption that the quantification is over a “universe” whose identity may be informally known. (In fact, in an equation like the one above, we might omit saying “for all,” leaving the quantifier implicitly assumed.)

All of this can help explain why computers may have some difficulties with verifying math, as it is commonly presented in research communications. In general, informal expectations can lead to challenges when they are meant to be implemented with logically precise programs. It therefore may not be too surprising that more involved techniques such as machine learning have been proposed for helping computers out — in fact, machine learning seems to be a prime candidate for getting computers to achieve informally defined tasks.

There are some exciting projects out there that take steps towards this goal. Many of them define specification languages for proof verification, and sometimes they also include some automated theorem proving functionality. Today, they are used essentially as interactive proof assistants to help mathematicians. Some of the ones I have heard about (and am loosely following) are Metamath, the Microsoft Lean prover, and the Xena project. With more development and advances in this area, hopefully we can get to a point where we can achieve more complete verification of math research as it is typically communicated.

The Future of Math Research

I’m excited for a future in which anyone can submit a paper and contribute to mathematical knowledge, independently of anything except whether the math checks out. As computers get better at filling in the details, more and more people may be able to contribute more quickly, regardless of their official or formal background. Since computer-based verification will never have false positives, such a system that is more open and democratized can eventually become the judge of validity of mathematical knowledge, helping move the field a major step closer towards the very goal of unbiased logic that defines the subject of math. And ultimately, math research can progress at a faster and faster rate, as humanity continues to push the frontier on what can be achieved with logical reasoning.