# Theorem generators and Theory Generators

val@netcom.com (Dewey Val Schorre)
Date: Fri, 23 Apr 93 09:12:25 -0700
From: val@netcom.com (Dewey Val Schorre)
Message-id: <9304231612.AA06019@netcom4.netcom.com>
To: qed@mcs.anl.gov
Subject: Theorem generators and Theory Generators
Sender: qed-owner
Precedence: bulk

Once QED gets going, we will need not only proof checkers and theorem
provers, but also "theorem generators" and "theory generators". A
theorem generator will work with an existing theory of QED and
generate interesting theorems that are not yet present. A theory
generator will scan the QED data base and generate "little theories"
that could have been used for proofs in existing theories.
Notice the three levels of programs:
Proof Checkers -- Always succeeds
Theorem Provers -- May loop forever but the criterion
for success is objective
Theorem and Theory Generators -- May loop forever and the
criterion
for success can only be subjective
This leads to a new form of Turing's test for artificial intelligence.
When a paper is submitted to a journal, was it written by a human
mathematician or by one of QED's theorem or theory generators?
Val