By Alexander Cox, Australian National University
During my Vacation Research Scholarship, I have been using an Interactive Theorem Prover (ITP). In this post I will explain what this is and why it is useful.
A theorem prover (TP), otherwise known as a proof assistant, is software designed to validate mathematical proofs. You ‘teach’ the TP the relevant maths and then try to prove some mathematical results which should follow.
Once you have an informal handwritten proof, it is relatively easy to convince another mathematician that it is a correct proof, so long as they understand the relevant mathematics. The same is not necessarily true when trying to convince a TP. In contrast with informal proofs communicated between mathematicians, where small details are often skimmed over and sometimes mistakes are unknowingly made, TPs are designed so that proofs cannot be verified unless every step, however small, is justified.
This means that while it may take considerable time to teach your TP the relevant mathematics, once this is done you have a powerful tool. They can give you a guarantee that a proof is correct or show you where an informal proof is incorrect. The correctness of verified proofs only depends on the theorem prover itself and specification of the problem being correct.
In many cases, a TP can do proofs for you, and TPs which focus on this are called automated theorem provers (ATP). Unfortunately, much of mathematics is undecidable, meaning there are problems which an ATP can neither prove nor refute. In some of these cases ITPs can be used because they combine automation with human guidance and intuition.
In an ITP a proof is mostly developed by the human user, who specifies each step to take. These steps are carried out by the TP, some of which are composed of many smaller steps which are commonly used together and do not require human guidance.
One major mathematical proof to be formally verified in an ITP is the proof of the Four Colour Theorem, a problem which was stated in 1852, but had no complete proof until it was formally verified in 2005 (Gonthier, 2008). The theorem roughly states that only four colours are needed to colour any flat map without any two bordering regions being the same colour. Several partial proofs were produced, but all either made large jumps in reasoning, or relied on unverified computer programs. Using an ITP finally gave a proof which could be trusted.
Another area of application of ITPs is verifying software. Most software is only tested for correctness with some sample inputs, but this cannot give you a guarantee of correctness. ITPs can be used to prove a program matches its specification, and thus has no bugs (unless the specification does). This is increasingly important for programs we place a high level of trust in because we want these to be as safe as possible (Filliâtre, 2011).
If you would like to learn more about theorem provers the following article provides an interesting overview (Avigad & Harrison, 2014).
Avigad, J. & Harrison, J., 2014. Formally verified mathematics. Communications of The ACM, 57(4), pp. 66-75.
Filliâtre, J.-C., 2011. Deductive software verification. International Journal on Software Tools for Technology Transfer, 13(5), pp. 397-403.
Gonthier, G., 2008. Formal Proof—The Four-Color Theorem. Notices of the AMS, 55(11), pp. 1382–1393.
Alexander Cox was a recipient of a 2018/19 AMSI Vacation Research Scholarship.