From: csuh@math.ucla.edu (Chan-Ho Suh)
Subject: Re: Sorry, just a little revenge.
Date: 31 Aug 2001 16:29:56 -0700
Newsgroups: sci.math
Summary: Pointer to automated proof-checker projects

daryl@cogentex.com (Daryl McCullough) wrote in message news:<9mo3800oil@drn.newsguy.com>...

> One idea for addressing the critics (although this would require
> a lot of extra work) is to try to find an automated proof-checker,
> such as Cornell's Nu-Prl system, or the University of Texas'
> Boyer-Moore theorem prover, or Odyssey Research Associates'
> Penelope theorem prover, etc. If you can formalize your proof
> in a rigorous enough way to push it through an automated
> theorem-prover, then you know that you will have plugged
> every last gap in your reasoning.

That's a good one.  You realize, Daryl, that most people don't bother
with this route and actually *learn* what a proof is by studying some
mathematics for at least several years.  Oh wait, sorry Daryl, I just
realized that what you're getting at is that an automated
proof-checker is the only thing James can resort to, having
demonstrated a sad lack of willingness to study math.