Re: A call to automated proof verification systems

From: Herman Jurjus (h.jurjus_at_hetnet.nl)
Date: 06/14/04 

Date: Mon, 14 Jun 2004 18:02:31 +0200

"Booted Cat" <coolspeech@hotmail.com> wrote in message news:7a8ba0c2.0406140746.77677bad@posting.google.com...
> Dear All,
>
> Like all of you, I have been surprised at the frequent and promising
> proof claims of major math open problems these days: Twin Prime
> conjecture, Riemann's hypothesis, and Poincare's conjecture. The math
> society has never been so fast-phasing before, probably thanks to the
> availability of high-performance computers and the assistance from
> decent math software programs, and the productivity boost in general
> caused by modern operating systems and office suites. While all these
> computing powers have been saving a researcher's life by making it
> much easier to maintain large-scale problem-solving process and
> presenting papers of over 100 pages, researchers are probably facing a
> new problem in this information age: how to verify a proof claim
> efficiently?
>
> The above three said examples of claimed proofs are still under human
> verification (the oldest of them has taken more than 2 years). Reality
> has shown that human verification on very long claimed proofs can be
> very laborious, time-consuming, erroneous and fruitless.
>
> During my just-finished supper in a restaurant I got an inspiration of
> an automated proof verification system. The basic idea is simply
> letting proof claimers write their proofs in a formal language which
> can be machine-verified.

Have you done a google search for 'proof checker'?
Or how about this:
 http://www.cee.hw.ac.uk/~fairouz/automath2002/

> This will eliminate all kinds of problems
> discussed above.

>From the fact that these things exist since 35 years,
one might perhaps conclude differently. :-)

Cheers,
Herman Jurjus

Relevant Pages