soft question - Why is it so difficult to write complete (computer verifiable) proofs?

The problem of putting an existing mathematical proof through a theorem prover ("formalising a proof") breaks down into 3 inter-dependent stages (with an element of recursion between the stages). With the current state of the art, all three of these stages are agonising. This gets more difficult the larger the proof is.

The first stage is to re-express the proof in a sufficiently detailed, rigorous and coherent symbolic form (or "formalisable" form). Traditional mathematical proofs often switch between different underlying formalisms, and often without any mention that this is happening. Also, sometimes pictorial arguments may be used without any explicit symbolic justification. And there will typically be fairly big, unjustified steps (e.g. "it obviously follows that ...") that may be obvious to the expert in the field, but not immediately obvious to someone fairly new to the subject. All of this needs to be re-expressed. This stage is fundamentally difficult and software cannot really help much. I expect that over time this will become a little easier as people become more experienced. At the moment there are very few people in the world capable of doing this stage effectively for large proofs (perhaps just John Harrison, Tom Hales and Georges Gonthier).

The second stage is to fill in the gaps in the theorem prover's library for theory referenced in the formalisable proof. This involves giving definitions and proving properties in the theorem prover. Ideally the theory referenced will all fit together in a way that helps formalise the proof, and sometimes it will be necessary to come up with alternative formalisms of existing parts of the theorem prover's library. This is a very skilled job, but this stage will eventually become easier as bigger and better library support is built up for the theorem prover being used.

The third stage is to actually translate the formalisable proof into a script accepted by the theorem prover. Currently, this is also a very difficult stage. It will typically take several months to become adept at controlling a theorem prover, and even then some of the steps in the formalisable proof may be agonisingly difficult to achieve. A page of formalisable proof may take weeks to actually formalise. This stage, in my opinion, should be quick and easy for mathematicians, but it will take a small revolution in theorem prover usability to bring this about. I am currently working on this.