From andrews@math.psu.edu Thu Mar 7 14:13:20 1996
Received: from leibniz.math.psu.edu (root@[146.186.130.2]) by euclid.math.temple.edu (8.6.12/8.6.12) with ESMTP id OAA18494 for ; Thu, 7 Mar 1996 14:13:19 -0500
Posted-Date: Thu, 7 Mar 1996 14:13:19 -0500
Received-Date: Thu, 7 Mar 1996 14:13:19 -0500
Received: from hemlock.math.psu.edu (andrews@hemlock.math.psu.edu [146.186.130.80]) by leibniz.math.psu.edu (8.6.12/8.6.9) with ESMTP id OAA07276; Thu, 7 Mar 1996 14:13:15 -0500
From: George E Andrews
Received: (andrews@localhost) by hemlock.math.psu.edu (8.6.12/8.6.9) id OAA17810; Thu, 7 Mar 1996 14:13:14 -0500
Date: Thu, 7 Mar 1996 14:13:14 -0500
Message-Id: <199603071913.OAA17810@hemlock.math.psu.edu>
To: zeilberg@euclid.math.temple.edu
Subject: Re: Opinion 10 of DZ
Cc: andrews@leibniz.math.psu.edu
Status: RO
Dear Doron,
Your point is not quite as powerful as you seem to think. I should
have granted that once anyone gets to the stage in mathematical insight where
an algorithm will verify what happens next, then a computer is a viable (albeit
less than insightful) option.
What you must do to convince me that your strong AI beliefs are really
onto something, is to explain to me how the computer would generate the
Dilcher-Borwein-Borwein paper given only the input of Roy North's observation.
If you are given the statement of their Theorem 1, then Shalosh, MAPLE and
approximately one jillion analysts know how to do the proof. No one gave them
the Chauvenet Prize just for carrying out Euler-MacLaurin summation.
Let me turn to an example closer to my life which makes my point better.
Euler obeserved that if we denote by c(n) the central entry in the trinomial
table:
1
1 1 1
1 2 3 2 1
1 3 6 7 6 3 1
1 4 10 16 19 16 10 4 1
1 5 15 30 45 52 45 30 15 5 1
. . . . . . . . . .
. . . . . . . . . .
then for a long time 3*c(n-1)-c(n) is equal to F(n)(F(n)+1),
where F(n) is the n-th Fibonacci number. Euler was perplexed by why this
was true for many cases but eventually failed. I wrote a paper to explain
the phenomenon and the initial discussion of Euler's problem eventually led
to (among other things) the splitting of the Rogers-Ramanujan functions into
even and odd parts, etc.
My point is that once one knows what is going on (for Euler's observation
there are two representations of a homogeneous fourth order recurrence) the
actual proof may well be routine. I do not believe, however, that (purely from
what is said above) the machine will get any farther than Euler in
explaining this phenomenon.
I look forward to hearing your further thoughts.
Sincerely,
George
From andrews@math.psu.edu Thu Mar 7 15:25:51 1996
Received: from leibniz.math.psu.edu (root@leibniz.math.psu.edu [146.186.130.2]) by euclid.math.temple.edu (8.6.12/8.6.12) with ESMTP id PAA19710 for ; Thu, 7 Mar 1996 15:25:51 -0500
Posted-Date: Thu, 7 Mar 1996 15:25:51 -0500
Received-Date: Thu, 7 Mar 1996 15:25:51 -0500
Received: from hemlock.math.psu.edu (andrews@hemlock.math.psu.edu [146.186.130.80]) by leibniz.math.psu.edu (8.6.12/8.6.9) with ESMTP id PAA08153; Thu, 7 Mar 1996 15:25:45 -0500
From: George E Andrews
Received: (andrews@localhost) by hemlock.math.psu.edu (8.6.12/8.6.9) id PAA17900; Thu, 7 Mar 1996 15:25:44 -0500
Date: Thu, 7 Mar 1996 15:25:44 -0500
Message-Id: <199603072025.PAA17900@hemlock.math.psu.edu>
To: zeilberg@euclid.math.temple.edu
Subject: Re: Opinion 10 of DZ
Cc: andrews@leibniz.math.psu.edu
Status: RO
Dear Doron,
My point is NOT that BBD are rigorous and MAPLE isn't. My point is that
once Theorem 1 is discovered, the proof is fairly routine. In other words,
once BBD had the "AHA!" moment the rest was verification. Your sermons (which
do not coincide with your behavior) suggest a world in which the insight from
proof would never be sought, and we would basically be kept around as pets for
the computers. How can you possibly deduce the following paragraph from the
fact that some clever mathematician has put the algorithm for determining
the first few terms of an Euler-MacLaurin expansion in MAPLE.
"So instead of wasting our time proving things (or playing chess), let's
dedicate our time to programming the computer to prove things.
Myself, I find programming just as fun, and intellectually rewarding
and challenging, as proving (or playing chess). So let's take
pride, for some time, in our programming skills. Soon, of course,
computers will also beat us there, and once they learn how to
program, the race would be lost, since they would be able to
teach themselves how to program to program.
Then we would be able to wean ourselves of our competitive spirit,
and do proofs (or programs) just for fun, like working out, or
doing crossword puzzles."
Give me a break! You don't really believe this. You didn't work as hard
as you did on the ASM conjecture believing this did you? The WZ algorithms
are beautiful and amazing achievements. Why dimish the accomplishment by
suggesting that they provide evidence for belief that eventually no one will
have to do mathematics except for sport?
Sincerely,
George
From jborwein@cecm.sfu.ca Thu Mar 7 12:21:36 1996
Received: from cecm.sfu.ca (banzai.cecm.sfu.ca [142.58.12.67]) by euclid.math.temple.edu (8.6.12/8.6.12) with ESMTP id MAA16426 for ; Thu, 7 Mar 1996 12:21:34 -0500
Posted-Date: Thu, 7 Mar 1996 12:21:34 -0500
Received-Date: Thu, 7 Mar 1996 12:21:34 -0500
Received: by cecm.sfu.ca (940816.SGI.8.6.9/940406.SGI)
id JAA10611; Thu, 7 Mar 1996 09:21:33 -0800
From: jborwein@cecm.sfu.ca (Jonathan Borwein)
Message-Id: <199603071721.JAA10611@cecm.sfu.ca>
Subject: Re: Opinion 10 of DZry
To: zeilberg@euclid.math.temple.edu
Date: Thu, 7 Mar 1996 09:21:32 -0800 (PST)
Cc: pborwein@cecm.sfu.ca (Peter Borwein)
In-Reply-To: <9603071655.AA08562@ralbag.math.temple.edu> from "zeilberg@euclid.math.temple.edu" at Mar 7, 96 11:55:29 am
X-Mailer: ELM [version 2.4 PL22]
Content-Type: text
Content-Length: 1219
Status: RO
> In George Andrews's rejoinder ,`The death of proof? semi-rigorous
> mathematics? you've got to be kidding', (Math. Intell. 16(4) (Fall 1994),
> 16-18), to my semi-rigorous manifesto (Notices of the AMS, Oct. 1993,
> reprinted ibid., 11-14), he brings an example of a result that was
> found by computer (that the partial sum of Gregory's series, 4 arctan(1),
> taken at 500000 gives most of the digits of Pi to very high accuracy),
> but that required humans of the caliber of Borwein, Borwein, and Dilcher
> (Amer. Math. Monthly 96(1989), 681-687) to prove and explai.
>
> This paper, winner of the Chauvenet prize, used by Andrews to proclaim
> Human Chauvinism(sic!), could have (essentially) been done by Maple,
> in one line, in less than a second of CPU time. This was pointed out to
> me today by Gert Almkvist
> (in an E-mail message whose main point was something else). The line
> is:
>
> asympt(simplify( (sum(4*(-1)^(j-1)/(2*j-1),j=1..n/2)-Pi)/(-1)^(n/2+1)),n,11);
Doron: I tend to agree with you; but this is beside the point.
Indeed,
it is EXACTLY what we DID IN 1988 once we realized the phenomenon existed
^^^^^^^^
It is that step you still don't account for.
Jon
From kuperberg-greg@MATH.YALE.EDU Thu Mar 7 12:22:54 1996
Received: from PASCAL.MATH.YALE.EDU (MATH-GW.CS.YALE.EDU [128.36.0.22]) by euclid.math.temple.edu (8.6.12/8.6.12) with SMTP id MAA16446 for ; Thu, 7 Mar 1996 12:22:53 -0500
Posted-Date: Thu, 7 Mar 1996 12:22:53 -0500
Received-Date: Thu, 7 Mar 1996 12:22:53 -0500
Received: by PASCAL.MATH.YALE.EDU; Thu, 7 Mar 1996 12:16:23 -0500
Date: Thu, 7 Mar 1996 12:16:23 -0500
From: Greg Kuperberg
Message-Id: <199603071716.AA26122@PASCAL.MATH.YALE.EDU>
To: zeilberg@euclid.math.temple.edu
Subject: Re: Opinion 10 of DZ
Status: RO
>Soon, of course,
>computers will also beat us there, and once they learn how to
>program, the race would be lost, since they would be able to
>teach themselves how to program to program.
>Then we would be able to wean ourselves of our competitive spirit,
>and do proofs (or programs) just for fun, like working out, or
>doing crossword puzzles.
Yes, but how would we justify to the computers that they should
keep us as pets?
Greg
From foda@maths.mu.OZ.AU Fri Mar 8 02:34:06 1996
Received: from mundoe.maths.mu.OZ.AU (mundoe.maths.mu.OZ.AU [128.250.35.32]) by euclid.math.temple.edu (8.6.12/8.6.12) with ESMTP id CAA29791 for ; Fri, 8 Mar 1996 02:32:31 -0500
Posted-Date: Fri, 8 Mar 1996 02:32:31 -0500
Received-Date: Fri, 8 Mar 1996 02:32:31 -0500
Received: from mundoe.maths.mu.OZ.AU by mundoe.maths.mu.OZ.AU with SMTP (8.7.1)
id SAA29120; Fri, 8 Mar 1996 18:32:22 +1100 (EST)
Message-Id: <199603080732.29120@mundoe.maths.mu.OZ.AU>
To: zeilberg@euclid.math.temple.edu
Subject: Re: Opinion 10 of DZ
In-reply-to: Your message of Thu, 07 Mar 96 11:55:29 -0500.
<9603071655.AA08562@ralbag.math.temple.edu>
Date: Fri, 08 Mar 96 18:32:22 +1100
From: Omar Foda
Status: RO
Dear Doron,
> So instead of wasting our time proving things (or playing chess),
> let's dedicate our time to programming the computer to prove things.
Naively speaking, teaching computers how to prove theorems, must
be regarded as an endeavour exercised at a plane that transcends
that of proving things directly.
In a certain sense, you need to develop 'meta-proofs' that transcend
the 'proofs' that you are aiming at, and that only subsequently descend,
or specialize, to them.
I wonder if I am making sense.
At any rate, what I wish to say is that I do not really see
a contradiction between what you are saying, and what someone like
Andrews is saying.
To my mind, you are really talking about two different ways of
doing things.
If there seems to be a conflict, then that is only the case at the level
of strategy: 'which way to proceed? proving theorems, or meta-theorems'.
However, since we are all in that most previliged of all situations of
basially working for the fun of it, one can comfortably say 'to each his
own'!
With best regards,
Omar.
PS Please don't tell my grant providers I ever said I am working
to have fun.
PPS Anthony Joseph says that 'Combinatorics with algebra is like
sex without love'. Does that imply that 'Algebra without combinatorics
is like love without sex'?