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?
$\begingroup$
$\endgroup$
7
-
8$\begingroup$ Well, reading a proof is a human activity. Why is it so hard to get computers to do other human activities? Writing music. Driving a car. Etc. Maybe this is a question for StackOverflow? $\endgroup$– Gerald EdgarCommented May 11, 2010 at 13:57
-
15$\begingroup$ @Gerald I don't think the question is about getting machines to discover the proofs. It's about getting humans to write proofs that can be mechanically checked. The whole point of a proof is that it's a deduction where each step is supposed to be 'obvious'. This is a very different situation from writing music, say. $\endgroup$– Dan PiponiCommented May 11, 2010 at 14:23
-
3$\begingroup$ @Negative I could give a rough description of the kinds of things that get complicated when trying to formalise proofs. But if you want a really good answer I suggest picking up a proof assistant. You'll very quickly get a feel for what makes formal proofs much harder than human readable ones. $\endgroup$– Dan PiponiCommented May 11, 2010 at 14:49
-
3$\begingroup$ @sigfpe: I said reading proofs is human activity. That is what we are talking about. $\endgroup$– Gerald EdgarCommented May 11, 2010 at 15:39
-
3$\begingroup$ Gerald, there are various hard human activities that computers do easily $\endgroup$– Gil KalaiCommented Feb 28, 2011 at 8:03
|
Show 2 more comments
4 Answers
$\begingroup$
$\endgroup$
1
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.
-
$\begingroup$ It's probably useful to note that these three stages are very interdependent, and say, finding a number of hard to prove steps in stage three may revise the definitions and basic facts of stage 2, or a need for clarification in stage 1, which in turn, will have to cascade down the whole proof. $\endgroup$– codyCommented May 31, 2016 at 0:38
$\begingroup$
$\endgroup$
13
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.
answered Feb 20, 2011 at 0:08
-
4$\begingroup$ Qiaochu, he is talking about the difference between proving $\forall n\, P(n)$ and proving separately that each $P(n)$ holds, by proving by induction that each $P(n)$ is provable. The difference is whether on invokes the induction principle inside the theory or (usually inappropriately) in the meta-theory. But Russell, is there much evidence that this mistake occurs often, as you say? I would think it is comparatively rare. (Note also: Jack Silver has suggested that this error might be a source of inconsistency in mathematics.) $\endgroup$ Commented Feb 20, 2011 at 1:23
-
5$\begingroup$ It would be interesting to see an example of such an incorrect proof, and preferably an example in which it takes more than a linguistic change to fix the proof. $\endgroup$ Commented Feb 20, 2011 at 2:08
-
10$\begingroup$ @Dan Ramras, @darij grinberg: an example is the proof of the axiom of choice for finite families of nonempty sets. The proof you might naturally think of involves listing the finite family $(X_i : i< n)$, picking one element $z_i$ from each $X_i$, and then forming the set $\{(X_i, z_i) : i < n\}$. But this doesn't give a proof in ZFC of the single sentence which states that every finite family has a choice function. In general the "finite" family might really be infinite in the metatheory, in which case it would not be possible to write down a single term defining the choice function. (ctd) $\endgroup$ Commented Feb 28, 2011 at 16:34
-
9$\begingroup$ (ctd) The proof that actually works in ZFC uses the induction principle for the natural numbers, constructing the choice function inductively (recursively). Any proof of this principle that avoids induction by writing down a single term for the choice function is going to be limited to families that are finite in the metatheory rather than families that are finite in the object theory. So the proof we might naturally think of only proves a certain infinite axiom scheme, with one instance for each meta-finite $n$. $\endgroup$ Commented Feb 28, 2011 at 16:37
-
7$\begingroup$ A similar thing happens in formalizing this proof that there are infinitely many prime numbers: "Suppose all the prime numbers are less than $n$. Consider $n!+1$, which is congruent to $1$ modulo every number less than $n$. This must have some prime factor, which must be larger than $n$." Now how do you know that $n!+1$ is a number? If you answered "just write down every number from $1$ to $n$ and multiply them" then you are assuming that $n$ is meta-finite. To formalize the proof you have to use an inductive definition of $n!+1$ to prove it exists, which is harder than it might naively seem. $\endgroup$ Commented Feb 28, 2011 at 16:47
$\begingroup$
$\endgroup$
3
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.
-
2$\begingroup$ * As of today, formal proofs look more like computer code than actual mathematics.*... well, that's because formal proofs are computer code (Curry-Howard, Gentzen) and have been since the 1930's. I'd reckon they will continue to be for quite some time. :) Isn't this sort of like saying that it's unfortunate that decision procedures are so much like programs? $\endgroup$– AdamCommented Jan 11, 2011 at 18:35
-
$\begingroup$ More modern proof assistants use declarative proof style... I'm not so sure about the "modern" part distinguishing declarative from imperative proof assistants. Also, I've yet to see a declarative proof assistant with a small "trusted core" (as small as CiC or ZFC, say) which has caught on. It seems that most of the declarative assistants which make a significant advance in ease-of-use (over tactical assistants) tend to be based on rather mushy foundational arrangements. $\endgroup$– AdamCommented Jan 11, 2011 at 18:38
-
1$\begingroup$ “These linear scripts are unreadable unless replayed step-by-step in the proof assistant.” +1. Elementary tactics killed readability in Coq. Not to mention that you must learn dozens (hundreds?) little tactics. Lambda-calculus is shorter. However, advanced tactics, like “ring”, are useful. $\endgroup$– beroalCommented Jul 21, 2012 at 18:35
$\begingroup$
$\endgroup$
2
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.
-
2$\begingroup$ The estimate of six times as long seems quite optimistic. For JCT in particular, see mizar.uwb.edu.pl/jordan: "Recently, we work on proofs of lemmas left to complete the whole proof. 74 articles devoted to this theorem have been collected so far, which makes about 10% of the Mizar Mathematical Library. However, some of the articles contain suplementary theory, only indirectly relevant to the proof." $\endgroup$ Commented May 11, 2010 at 12:35
-
1$\begingroup$ @Pete: I think you are right. But a couple of caveats: Barendregt was speaking informally in a Q&A, and he was talking of systems with tactics, which Mizar doesn't have. And what baseline informal proof of the JCT should we be considering for our comparison? It's easy not to compare like with like here. $\endgroup$ Commented May 11, 2010 at 13:35