Context

• Mail folder: QED
• Next message: Robert S. Boyer: "QED-like Efforts"
• Previous message: beeson@cats.ucsc.edu: "Re: From idea to project"

Message-id: <199308061558.AA15235@antares.mcs.anl.gov>
Date: Fri, 6 Aug 93 09:58:57 -0600
From: Randall Holmes <holmes@diamond.idbsu.edu>
To: qed@mcs.anl.gov
Subject: Context
Sender: qed-owner

A lot of what you are describing is already being done.  For instance,
I have written a theorem prover, with ultimate aims similar to what
you are discussing, and am going to test it by getting undergraduates 
to work with it in the coming semester.  This is "code in a specific
language on a specific computer".  There are several actual theorem
prover projects in existence, busily building libraries of proved 
theorems, so far as I can tell.  The official aim of these projects
(and of mine) is software verification, but this covers a lot of
nontrivial mathematics.

I'm going to go back and read your introductory messages; I'm having
some difficulty figuring out why you are discussing as hypothetical things
which already exist and have existed for some time!

The opinions expressed		|     --Sincerely,
above are not the "official"	|     M. Randall Holmes
opinions of any person		|     Math. Dept., Boise State Univ.
or institution.			|     holmes@math.idbsu.edu