Before my fall I launched a PIP (Perpetual Impossible Project). PIPs are long-range risky undertakings that cannot be finished. PIPs contradict and subvert the very notion of tightly controlled corporate style projects: hence their manifest appeal to recusants like myself.

I won’t go into details about my particular PIP. Let’s just say it captures every delusional notion I have ever entertained. Part of my project involved installing a few Proof Assistants. Proof assistants are programs that verify formal mathematical proofs. There are many proof assistant programs available. These programs are not mathematical magic bullets. They don’t prove theorems and they don’t make the job of “theorem proving” easier. To use a programming analogy: a traditional proof is like pseudo code while a formal proof is like an assembly language program. If you have ever written a nontrivial assembly language program you have some idea of the sheer effort required to produce a formal proof.

So, if formal proof only makes mathematics more difficult, why bother? This is like asking, so if implementing pseudo code only makes programming more difficult, why bother?