A call to automated proof verification systems

From: Booted Cat (coolspeech_at_hotmail.com)
Date: 06/14/04 

Date: 14 Jun 2004 08:46:50 -0700

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. This will eliminate all kinds of problems
discussed above.

Prolog (http://en.wikipedia.org/wiki/Prolog) is a relevant point to
this idea. Given some facts and rules, Prolog use inferrence
algorithms (probably breadth-first search or depth-first search) to
judge if a statement is right. But the path of proof is
computer-enumerated rather than given by the user.

Program verification is an established area in computer science, which
may also be relevant to this topic.

Best Regards,
Yao Ziyuan, Computer Science Freshman of Fudan Univ.
http://www.babelcode.org

Relevant Pages
Loading