Re: Motivation #1

• Mail folder: QED
• Next message: victor yodaiken: "Re: How many false theorems are there?"
• Previous message: LYBRHED@delphi.com: "From idea to project."

Message-id: <9307022257.AA27610@gemini.cs.cornell.edu>
To: qed@mcs.anl.gov
Subject: Re: Motivation #1 
In-Reply-To: <LYBRHED@delphi.com>'s message of "Fri, 02 Jul 93 02:13:20 EDT."
             <01H01TNJWG0I8ZFOWH@delphi.com> 
Date: Fri, 02 Jul 93 18:57:53 -0400
From: Wilfred Chen <chen@cs.cornell.edu>
Sender: qed-owner
Precedence: bulk

Lyle Burkhead wrote:

  Objection 10.  The Manifesto begins by promising to solve a problem which 
  either does not exist, or can't be solved.  
  
  1. The problem doesn't exist.
  
  ...

  2.  The problem exists but can't be solved.
  
  There is a sense in which there is a problem of "too much mathematics."  
  There is an enormous amount of mathematics which is undeniably important, 
  and which is inaccessible to me, because it would take a thousand years 
  to read it.  But this is an ineluctable fact.  It's not a problem that 
  could be solved.  QED could not possibly change the situation.  Nothing 
  can change it.  One man can't absorb all the mathematics produced by 
  hundreds.
  
  If you take the collected works of Abel, Riemann, Poincare, Goedel, Thom, 
  and two or three hundred other mathematicians whose work is at least 
  sometimes on more or less the same level, and enter all that mathematics 
  into a proof checker, it would still take many lifetimes to read it all.  
  In fact it would take longer to read mathematics through a QED terminal 
  than it would take to read it in printed form.  (I envision a QED 
  terminal as something resembling an ORION terminal.)

If reading is the only thing we want to make use of QED.

One of the advantage a teacher has over a book is that you can ask
questions that either aren't answered explicitly in the book or you
can't find it in the book easily.  A successful QED system would be
somewhere in the middle between a book and a teacher: being able to
answer some questions that are obvious consequences of what's in the
book.  There really is no limit to how much we could want from such a
knowledge representation system.  Furthermore, even a very poor
machine approximation to human intelligence is appealing, because it
is very much easier to duplicate.
  
  3.  The "problem" can be mitigated, but not with QED.
  
  To the extent that there is a problem of "too much math," the only way to 
  mitigate it is to increase one's reading speed.  QED goes in the wrong 
  direction.  If the target is to increase my reading speed, you don't want 
  to force me to resolve informal statements into all their nitty gritty 
  logical and set theoretic details.  That would be like forcing me to read 
  program listings in assembly language.  It would slow me down.  
  
  To increase my reading speed, what you want to do is present mathematics 
  on a computer screen in such a way that I can take in more of it at a 
  glance, and see relationships quickly that I would otherwise have to 
  discover with great labor.  Better yet, you want to present mathematics 
  on the screen in such a way that it trains my imagination, so that 
  eventually I can learn to see vector fields the way Riemann saw them, 
  without the aid of a computer, and maybe even learn to see everything 
  from the center, as he did.  

Why limit to the screen?  Surely there are limitations to the visual
system.  While we are at it (not exacly a QED topic) perhaps abstract
mathematical objects can be presented by feeding it directly to some
kind of brain implant, or, perhaps easier, some kind of direct
stimulation of the retina with light beams.  We'd probably have to be
trained from an early age to handle these.

Wilfred Chen