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

You are correct. I confused myself by confounding the complexity of the proof with the complexity of finding the proof _given the size of the original problem_. Even for decidable theories like real closed fields, the proofs could be quite long. I seem to recall that if you have a series of alternating quantifiers in the original problem statement, the shortest proof might be exponential (?) in the number of alternations. Of course, once a theory is complex enough so that it can talk about Turing machines with a certain amount of tape, you can diagonalize over all such machines with shorter amounts of tape, and you can in this way force proofs to be as long as you wish. At 12:04 PM 3/19/2012, Gareth McCaughan wrote:

On Monday 19 March 2012 01:58:59 Henry Baker wrote:

...

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.

Clearly not multiply-exponential, given that proof checking is of approximately linear complexity. All you have to do is enumerate all possible proofs (there are singly-exponentially many) and check them one by one.

-- g