You're right --- I was confusing the two things. [Often happens, these days.] WFL On 3/19/12, Henry Baker <hbaker1@pipeline.com> wrote:
[Proof checking is more analogous to checking that each move in a chess game is legal, rather than in playing chess, per se. Checking legality of moves is simple & mechanical; deciding which of the legal moves to make is the really hard part.]
Proof _checking_ is a purely mechanical, almost linear complexity (in the length of the proof) problem (depending upon the representation). _Finding_ a proof is the hard part, and can be multiply- (?) exponential in the length of the proof.
If you have no lemmas to rely upon, the length of the proof can be quite long, just as a program without subroutines can be quite long. So lemmas are somewhat analogous to subroutines in programming.
The reason why human proofs may not be so trivial to check is that we rely on thousands or tens of thousands of trivial lemmas and also leave out lots of intermediate steps that need to be filled in by intelligence.
Proving programs correct is often extremely tedious, because of the large number of completely trivial steps that need to be spelled out. Every loop requires an induction proof. Of course, in any non-trivial program, there are usually a few key steps that require real insight to prove.
At 02:32 PM 3/18/2012, Mike Speciner wrote:
I've always felt that the real problem with automatic proof systems is proving that what is being proved (presumably a machine-understandable specification) is equivalent to what you actually want to prove (presumably a natural language description). Perhaps this is less of a problem for mathematical theorems than it is for programs?
--ms
On 3/18/2012 1:46 AM, Henry Baker wrote:
I've been told that Java (not Javascript) routinely "proves" that new modules can't overrun their boundaries when the modules are loaded.
I've also been told that Microsoft is routinely checking many/most of its device drivers to have certain properties. Microsoft is apparently a fan of "model checking", which is a certain restricted type of theorem proving.
I've also been told that there are several types of operating systems that have been proven "secure" -- whatever that means.
I've been told that Intel has routinely been checking their floating point implementations ever since the infamous Pentium bug incident.
The only thing holding "Wikiproofia" back right now is a small, dedicated "open source" project to focus on this for a good 5-10 years to develop the basic core system and a good library of "lemmas" to cover many of the more obvious things that need to be proven.
"Artificial Intelligence" isn't needed right this second; that would only be required if you didn't want to have to explain every last detail to the proof checker; but many of the details would already be handled by a large enough library of already proven lemmas.
At 07:47 PM 3/17/2012, Fred lunnon wrote:
On 3/18/12, Marc LeBrun<mlb@well.com> wrote:
="Henry Baker"<hbaker1@pipeline.com> mechanically _check_ submitted proofs I agree this is a good idea, but have wondered how far off the dream is. ... Is Wikiproofia's first customer release date inevitably post-singularity? There are certainly plenty of projects aimed in this direction --- just search on "automated theorem proving". But I think they're unrealistic, for much the same reasons Marc advanced.
If you can't solve the problem, look for an easier one instead. In this case, the easier problem is automatic verification that a computer program implements its specification. Here the universe is extremely circumscribed, and well documented. When we've got that question satisfactorily answered, then it might be time to look seriously at automated theorem proving.
I have a vague memory of some bigwig in the UK MoD --- or maybe it was the USA DoD --- announcing grandiosely in public that in future all defence contracts would include a clause demanding that any software be proved correct. That was some time in the 1970's. When we'd all stopped laughing, we said --- quietly, of course --- don't hold your breath!
But after all the ballyhoo has been deflated, and the journalists and politicians have departed to look for other mirages to chase, things do eventually come quietly to pass in a lab somewhere out of the spotlight.
In the end, Deep Blue defeated Kasparov ...
Fred Lunnon
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun