By Mike Sha

Mathematics is the study of symmetry, patterns, and numbers. Professional mathematicians spend most of their time thinking and proving facts about these abstract concepts. Einstein used differential geometry to formulate his theory of gravity. Machine learning researchers use differential geometry and representation theory to design effective neural networks.

At the heart of mathematics is logic and consistency; a proof in mathematics is different from “proof” or “evidence” in the sciences. Starting from a set of facts about numbers and logic (axioms) which are assumed to be true, a mathematical proof of another statement (a theorem) demonstrates that the statement is logically consistent with the axioms. Unlike science, mathematics deals in absolute truths.

To aid mathematicians in organizing their work, researchers have developed formal proof assistants, which are computer languages that can verify mathematical statements. Unlike humans, formal proof assistants do not make mistakes.

Why should we formalize proofs?

Here are two papers published in Annals of Mathematics, the premier academic journals for mathematics: one paper (Schumacher and Tsuji) claims that all moduli spaces of polarized varieties are quasi-projective, whereas the other (Kollár) gives counterexamples. Neither paper has been retracted from Annals!

One of these articles must be incorrect, but the subject matter is so abstract and specialized that it is difficult to trust the few human experts that exist to decide which one. Since we assume both are true (they are published), we assume a logically inconsistent basis in mathematics, and by assuming a false statement, we can prove anything else is true, like 2 + 2 = 5.

A proof assistant can prove one of these articles correct, and find the flaw in the other, as well as providing confidence in the results.

Theorems in mathematics are stated as “if A is true, then B is true.” If we assume a statement A that is false, we are saying “if false = true, then B is true.” This statement is always true, because false is never true, so we can never prove that B is true.

Mathematics is a house of cards, with fields like calculus and algebra built on set theory, and differential geometry built on calculus and algebra. All of the language of mathematics must first be expressed in the proof assistant before it can prove more complex facts. Because the central component of a proof assistant (the kernel) is logically consistent and provides the methods of reasoning available to the user, trusting the statements given by a proof assistant is logically equivalent to trusting only the kernel, which is short and human-verifiable. The correctness of all subsequent proofs written in the proof assistant language depends only on the correctness of the kernel. Current existing proof assistants include Microsoft Research’s Lean, the HOL family of proof assistants, and Thierry Coquand’s Coq.

Even so, proof assistants are a long way from verifying the statements at the cutting edge of mathematics. The foundations are not all yet written out in each proof assistant language, though progress is being made to complete this task³.

Unfortunately, due to Gödel’s incompleteness theorems⁴, there are mathematical statements which are unprovable, and proof assistants will not magically solve these issues.

For example, in set theory (which can be used as a foundation for mathematics), Russell’s paradox asks for the meaning of “let S be the set of all sets which do not contain themselves.” The question then is, “does S contain itself?” If S contains itself, then by definition, S is a set which does not contain itself. If S does not contain itself, then S should be contained in S, since we claimed that S contained all such sets.

Gödel’s first incompleteness theorem says that such an unprovable statement exists in any mathematical framework powerful enough to describe the natural numbers (0, 1, 2, …). Fortunately, these unprovable statements are irrelevant to the results that we can derive in many fields of mathematics.

Proving a theorem using Lean

The mathematical fact that makes proof assistants work is the Curry-Howard correspondence: if you can write a program for it, you can prove it. Here is an example of a simple theorem we can prove using Lean: squaring an even number produces an even number (Figure 2).

On the left is the actual Lean code one would write, and on the right is the current state of the proof. The state of the proof shows variables (yellow) which are our assumptions for the proof, while the sideways blue T (“right tack” or “turnstile”) shows us the goal we are trying to prove. Green text are comments, which are ignored by Lean.

Proof assistants are extremely useful for carrying out tedious algebra, and to check cases in proofs. There is current research into automating the proving of theorems using artificial intelligence, to make using such proof assistants easier to use. Notice that line 20 of the above pictured theorem was the major human input: we had to supply the proof assistant with the correct number to use to prove the goal, otherwise we would have failed.

As mathematics grows ever more complex, proof assistants can be useful tools for organizing and verifying results, avoiding situations where results directly contradict each other and cutting down on human error.

Further reading

To have some more fun with theorem proving, play the Natural Number Game (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/), developed by Kevin Buzzard and Mohammad Pedramfar at Imperial College London as an introduction to the Lean theorem prover and to mathematical induction. This is a very cool application that runs Lean in your browser!

TL:DR

• Formal proof assistants are computer languages that help eliminate human error in mathematical reasoning.

---

References

1. Schumacher, G., & Tsuji, H. (2004). Quasi-projectivity of moduli spaces of polarized varieties. Annals of Mathematics, 159(2), 597–639. https://doi.org/10.4007/annals.2004.159.597
2. Kollár, J. (2006). Non-quasi-projective moduli spaces. Annals of Mathematics, 164(3), 1077–1096. https://doi.org/10.4007/annals.2006.164.1077
3. The mathlib Community. (2020). The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. https://doi.org/10.1145/3372885.3373824
4. Dicker, R. M. (1963). K. Gödel, on formally undecidable propositions of Principia Mathematica and related systems, translated by B. Meltzer with an introduction by R. B. Braithawatte (Oliver and Boyd, 1962), VIII + 72 pp., 12s. 6d. Proceedings of the Edinburgh Mathematical Society, 13(3), 256–257. https://doi.org/10.1017/s0013091500010920