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