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'?