Proof assistant software provide an interesting take on the process of doing mathematics. On the one hand it is tedious to make clear to literal-minded machines what might be intuitively obvious to humans. On the other hand, having your proof explicit enough to be checked by a machine is the ultimate realization of the dream of turning reasoning into calculation.
I’ve been trying to learn how to use the Isabelle proof assistant. Here is my attempt to prove the following simple proposition
In a finite group of people, some of whom are friends with some of the others there must be at least two people who have the same number of friends.
To my embarassment, I could not actually solve the puzzle when it was first posed to me. But my friend mentioned just the phrase “pigeonhole principle” and all was clear.
Getting a correct Isabelle proof took hours. Here it is.
Here is my take from the experience:
- The amount of labour required to formalize even relatively simple results is huge, at least for beginners.
- The task would have been impossible without Isabelle’s integration with high-quality automatic theorem provers. I turned to Sledgehammer again and again.
- The task would have been impossible without Isabelle’s huge library of proofs from classical mathematics. I could use readymade results about relations, functions and finite sets. However this library also makes unexpected choices. For example any natural number can be subtracted from another but the answer is “0” if the second number happens to be larger. This makes proofs a bit unnatural since “x-y” does not automatically satisfy the identities you would expect from algebra.
- Small changes in inputs can make a big difference in processing time. So trial and error is required to find efficiently checkable proofs.
- Formalizing proofs does clarify thought. I realized that there were two missing assumptions in the informal proof as I had understood it: the irreflexivity of friendship and the need to have at least two individuals.