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

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

2010-05-11T09:10:40Z

For example I have read that is agony to give a complete proof of the Jordan curve theorem. Since all statements are meant to be justified by the postulates, where does the difficulty lie?

Answer by Charles Stewart for Why is it so difficult to write complete (computer verifiable) proofs?

2010-05-11T11:23:54Z

Well, it was agony to come up with the original Jordan curve theorem...

Informal proofs make a lot of gestures at expert knowledge to avoid spelling out the mechanics of the less interesting steps in a proof. Sometimes this can be collapsed in a similar way in a formal proof, through "tactics" that gesture to the machine verifier how to fill in the gap, but more often than not, this is impossible.

In particular, informal proofs often move fluidly between different ways of representing a phenomenon, which often requires verbose specification of a translation in a formal proof description language. Natural language is much more fluid.

I heard Henk Barendregt talk of formal proofs being around six times as long as informal proofs. Harvey Friedman has claimed that ZF set theory with definitions and partial functions does better; I don't recall his estimate; see my answer in to the Is there a formal notion... question.

Answer by mathy for Why is it so difficult to write complete (computer verifiable) proofs?

2010-05-11T19:53:30Z

There was a special issue of AMS Notices on formal proof in 2008, which discusses some of the difficulties with formal proofs in passing. Freek Wiedijk (who wrote one of the Notices articles) has plenty of good resources on his home page.

In general, one shouldn't underestimate pragmatic difficulties with the current technology of proof assistants, especially with respect to usability. As of today, formal proofs look more like computer code than actual mathematics.

What makes this issue even worse is that many proof assistants in common use are "procedural" proof assistants. A proof in a procedural proof assistant is a linear list of proof "tactics" which manipulate the proof state directly, with no express reference to intermediate goals or hypotheses. These linear scripts are unreadable unless replayed step-by-step in the proof assistant. (They're also extremely brittle, since a slight improvement in the proof tactics themselves can change the expected proof state and make the proof script almost useless.)

More modern proof assistants use declarative proof style, which does not have these problems and reads more like an informal proof.

Of course, one other issue is that each proof assistant brings its own logical foundations, syntax and special tactics: results are generally unportable between different systems, and each system may be more tailored to some branches of mathematics than others.

On the upside, proof formalization can be playful and even addictive: the ability to "interact" with the proof state and get immediate confirmation of successful steps makes for an engaging activity akin to solving a puzzle.

Answer by Mark Adams for Why is it so difficult to write complete (computer verifiable) proofs?

2011-01-11T18:25:01Z

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.

Answer by Russell O'Connor for Why is it so difficult to write complete (computer verifiable) proofs?

2011-02-20T00:08:56Z

There are probably many reasons for the difficulty, but there might be one particularly difficult problem: Mathematicians may be using meta-induction instead of induction leading to erroneous proofs.

Bundy et al. in "What is a proof?" claims that S. Baker in "Aspects of the constructive omega rule within automated deduction" claims that often when mathematicians claim to do induction they actually do meta-induction. This means that instead of proving $\forall n. P(n)$, they instead end up proving $\forall n:{\mathbb N}. Provable(P(term(n))$ (i.e. $P(0), P(1), \ldots$). This result is, in general, weaker that the result $\forall n. P(n)$ that they claim to be proving. The paper proofs are so informal that it is hard to tell that this is what they are doing, and this coupled with the fact that the theorems they are claiming to prove are actually true (and provable), means that this subtle error goes unnoticed. This leave formalizers with the difficult task of providing an actual inductive proof.

Thanks to schropp for pointing this out. Sorry for stealing your Mathoverflow karma.