Why is it so hard to translate some proves into machine-readable form?

Question

I have just read a topic on mathoverflow about man vs. machine in mathematics. The topic was inspired by the recent victory of Alpha Go over the World Go Champion, Lee Sedol. It reminded me of an article I read (possibly on American Mathematical Monthly) about translating Jordan Curve Theorem into machine-checkable form.

I would love to hear about why is it so hard, generally, to translate a proof of some theorem so that a machine can check it. What is fundamentally different between, says, the Four Color Theorem and Jordan Curve Theorem that makes it a lot harder for machine to deal with the later?

EDIT: I have found a wonderful related link Why is it hard to prove Jordan Curve Theorem in the case of Koch snowflake.

Answer 1

Another example is Gonthier's recent proof of Feit–Thompson theorem. It would be too long to answer your question in detail, but this link (in French) COQ ET CARACTÈRES, Preuve formelle du théorème de Feit et Thompson, contains several relevant references.

In particular, A Special Issue on Formal Proof of the Notices of the AMS gathers four articles:

Formal Proof by Thomas Hales

Formal Proof--The Four-Color Theorem by Georges Gonthier

Formal Proof--Theory and Practice by John Harrison

Formal Proof--Getting Started by Freek Wiedijk

Answer 2

It's not so much harder as much more tedious. In a formal proof (one readable by a computer program), each step in solving an equation must be made explicit. You cannot assume, for example, that the reader (a computer in this case) knows that addition on the real numbers is commutative. You cannot even say, by the commutativity of addition, such and such. You must explicitly cite some previously proven theorem of the form $$\forall x: \forall y:[x\in \mathbb{R} \land y \in \mathbb{R} \implies x+y=y+x]$$ Then you must specify an expression for both bound variables $x$ any $y$. Then you must prove each expression is indeed a real number. Then you must apply the detachment rule. (Leaving out some details!) Then you must explicitly select the expressions in the original formula for which you want to make the substitution. Whew!

What is normally simply "known" and applied almost subconciously by an experienced human reader to fill in the gaps is a multi-step process in a formal proof. The upside, of course, is that you can be virtually certain that no errors have been made. For practical purposes, there would be no real need for any further verification by a human expert.