Conference rusure::math

    i was wandering what what have happened has computers were available
    to the kinds of Newton, Euler, Gauss, etc..

    the reason i was asking, is while reading their biography , and looking
    at some of the long hand calculations they had to do, and how many
    hours that must have taken, i asked, what if say Gauss had MAPLE at his
    hands! what more would he have done ?
    
    i guess the question is whether computers can help you discover original
    theories, or they can only help you implement them/verifies them ?

    has any computer program discovered anything new in math?

    i recall reading time ago something about a theorem proving program that 
    found a new proof to a geometrical theory that was different from the known
    proofs...

    /nasser

>    i was wandering what what have happened has computers were available
>    to the kinds of Newton, Euler, Gauss, etc..
        
        I have this image of Gauss discovering the law of
        quadratic reciprocity by seeing it in a comment in the
        MAPLE source code. ;-)  Computers could have helped them
        a lot, but I'm sure many of the symbolic packages use or
        exploit discoveries/theorems of the people you mentioned.
        (This doesn't address the questions you asked later.)
        
        Dan

    Yes, a theorem prover for geometry was put through an exercise of
    proving theorems in The Elements.  It found a proof for one of the
    early theorems which was apparently previously undiscovered and which
    was one step shorter than the shortest known proof (which was
    Euclid's).

    Also, Doug Lenart wrote a program, called AM, which was a theorem
    inventor rather than a theorem prover.  It was based on heuristics for
    defining what was "interesting".  After much tuning up its heuristics
    it rediscovered much of mathematics through the mid 19th century, but
    got hung up looking for interesting consequences of Goldbach's
    Conjecture.  It did find one interesting theorem which was initially
    announced as previously undiscovered, but it turned out to be in
    Ramanujan's notebooks (where else?) (the theorem was about numbers which
    were the opposite of primes: AM defined a prime number as a number
    which had a minimum number of positive divisors, specifically 2, this
    theorem concerned numbers with a maximum number of positive divisors).

    Other than that, I don't think that you could say that any computer
    program has discovered anything new in math, but computer programs can
    be used to help mathematicians explore mathematical concepts.  The
    properties of the Mandelbrot set comes to mind, as well as the
    discovery of the proof of the 4-color conjecture.  Experimental math
    (where the experiments are performed with the aid of a computer) is now
    a widely recognized, if still somewhat controversial, area of
    mathematics.

				    Topher

RE: .3 (me)

    As Dan D'Eramo I typoed the man's name.  It is Doug Lenat not Doug
    Lenart.

						Topher

    
    I believe that the 4 color theorem was finally proven with the aid of a
    computer.  
    
       /jim
    

    now, is the 4-color problem is the one which claims that 4 colors
    are sufficient to color any map such that no two regions in map
    with adjacent boundaries have same colors?
    right? (a map can be transformed into a graph etc..)

    i read something about the 4-color theorem proving loong time ago, 
    i recall it was verified, not proofed by brute force searching some 700 
    or so possible set up (i think they classified all the possible
    geometrical position one can get with a planner graph, and that what it
    came down to , or something like that..iam not sure..)
    
    any way, the program was able to try all different combinations and
    showed that 4 colors were sufficient for all these cases it tried..

    but that is not a proof? i mean it is not a constructive proof, (like
    there is one for the 5-color problem, i think) .
    
    plus what if there was an error in the program? who can proof that the
    program that "proofed" the 4-color problem was correct itself? 
    plus what if they have missed a case in their search? (ok, this one
    i assume they are sure off..)

    by the way, did not the 4-color problem had some implications on 
    design of multi-level electronics boards (stacked up?) and optimal
    connections between all the components from every board to another?

    or something like this, iam not clear on this, but i think this problem
    had some practical implication in the area of electronics design and
    how many layers can be used etc..

/nasser

    i looked this up at home, found i have a little book called
    "the four-color problem" assaults and conquest, by thomas l. Saaty and
    Paul c. Kainen, a dover book.

    from the book, the 4cc conjecture says "that 4 colors are sufficient
    to color any map drawn in the plan or on a sphere so that no 2 regions
    with common boundary lines are colored with same color"

    from the introduction:
    "one of the transforming features of modern mathematics is the use of
    the digital computer. it is ironic but fitting that the 4cc now appears
    to have been solved by Wolfgang hanken and Kenneth Appel at the univ.
    of
    Illinois who used a well-orchestrated approach that involved, among
    other things, 10^10 separate operations on high speed computer to
    prove a finitistic form of the conjecture.
    however, the issue remains clouded because of the staggering length of
    the calculations (1200 hours in total) and because of the elaborate
    arguments needed to understand how the machine computations solve the
    problem. such a length program (both computer instructions and
    mathematical reasoning) certainly requires careful verification which
    may be years away."

    me>the main idea of the proof is reducibility in maps, they describe
    what that means, they also give the general flow chart of the
    Appel-Hanken proof (algorithm) on page 75.

    /nasser

    Re .3:
    
    That chestnut about the geometric theorem prover is often misreported. 
    The program found a proof the authors were unfamiliar with, but it was
    ancient nonetheless.  I think it involved proving two sides (or angles)
    of a triangle with two equal angles (or sides) were equal.  The authors
    knew they could drop a perpendicular to the third side, marking the
    intersection D, and show that ABD was congruent to ACD.  The program
    instead simply stated that ABC was congruent to ACB.  If this wasn't
    known to Euclid, it is still very old.
    
    
    				-- edp

re .6
    
>    plus what if there was an error in the program? who can proof that the
>    program that "proofed" the 4-color problem was correct itself? 
>    plus what if they have missed a case in their search? (ok, this one
>    i assume they are sure off..)
    
    Just because a 'conventional' proof is written out does not mean it is
    correct either? Missing a case in a search is much the same as missing
    a case in any proof. The proof is faulty. The longer the program/proof,
    the more difficult it is for someone to go through it and be *sure*
    that it is correct.
    
    By the way, when worrying about computer proofs don't forget to check
    the correctness of the compiler and (possibly) the operating system.

    
>>>>    By the way, when worrying about computer proofs don't forget to check
>>>>    the correctness of the compiler and (possibly) the operating system.
    
    And of course you must verify that the hardware correctly executes the
    instruction set !
    
    In the case of the 4-color problem, I think there has now been a
    fairly short non-computer proof.
    
    Andrew

    ... and check that the printer actually prints the proper symbols for
    the codes it receives.  I remember a case where the system line printer
    randomly substituted 1's for 2's.  The condition was only detected when
    someone mistakenly ran the same program with the same data two days in
    a row.
    
    /rab

    I don't believe that a non-computer proof has been found.  But I do
    believe that the computer part of the proof has been recreated
    independently of the original program and been found correct.  I would
    judge that that puts it in roughly the same category of reliability as
    most large conventional proofs -- maybe a bit better.  My understanding
    is that as a program, its not too complex -- and for a check, some of
    the trickier parts (the part which causes the prover to give up on a
    specific case after a while and generate a new case(s) covering the
    same territory) can be skipped completely.

				    Topher

    ok, a new thing about history of math.
    
    did you know that L'Hospital was a student of Bernoulli (john), and that 
    L'Hospital paid Bernoulli a regular salary, and in return, Bernoulli 
    agreed to teach L'Hospital about the calculus and any new discoveries 
    Bernoulli might come up with, and the agreement was that L'Hospital can do 
    anything he wished with them, then L'Hospital went and published a book 
    under his name as the first differential calculus book, and this text is 
    best known for what we now call L'Hospital rule for evaluating undetermined 
    forms !

    all this time, we say L'Hospital rule, while it was actually discovered
    by Bernoulli !

    this should be a lesson for all of you out there, be carfull what you
    sign for, and always read the small print :-)
    
    /Nasser

As for computers proving stuff, perhaps there are some examples where computers
have DISPROVED statements of the form:

	There is no set of numbers such that...

Perhaps such statements have been disproven by computers that have found
large numbers satisfying the requisite property.  For example:

	There are no composite numbers of the form 2^(2^p-...

something like that where no one knew if it was really true until someone's
computer program factored some huge number of that form.

Any examples of this ?

/Eric

> Perhaps such statements have been disproven by computers that have found
> large numbers satisfying the requisite property.  For example:
>
>	There are no composite numbers of the form 2^(2^p-...
    
    Sure.  The generalized version of FLT (sorry, I don't have the proper
    conjecture name) that stated you needed N terms of X_i^N to add up to
    a perfect Nth power.  (Can't find two cubes that sum to a cube but CAN
    find three, etc.)
    
    Computers were used to find four 5th powers that sum to a 5th power,
    the first known counterexample.  The terms were on the order of 6 digits.
    
      John

Does anyone know a more complete reference for a book called
(I think) "Mathematics made difficult"? , probably out of print?

It's hilarious.

Does anyone know a good URL where I can start to search
for such a thing? 

Hank

Article 51253 of sci.math:
Path: nntpd2.cxo.dec.com!pa.dec.com!decwrl!spool.mu.edu!darwin.sura.net!mojo.eng.umd.edu!delliott
From: [email protected] (David L. Elliott)
Newsgroups: sci.math
Subject: "Mathematics Made Difficult"
Date: Sat, 21 Aug 93 15:18:42 GMT+7:00
Organization: Project GLUE, University of Maryland, College Park
Lines: 31
Message-ID: <[email protected]>
NNTP-Posting-Host: newra.src.umd.edu
Summary: Available again
Keywords: Mathematics Humor

About "Mathematics Made Difficult"--
A year or two ago somebody (J. Baez?) mentioned this very rare book of
mathematical humor ... in fact, it's intended for mathematicians only...

"Just as the fractured leg confused the Zen disciple, it is hoped that
this book may help to confuse some uninitiated reader and put him on
the road to... mathematical satori."

The part about the marriage customs of brackets [ ] ( ) { } is notable...
"in France, one encounters  [  [ "  and almost every part of mathematics
is touched on wittily, with weird puns too.

By chance I encountered its author. He has the copyright (it was
originally published 1971 by Wolfe Publishing Ltd., London) and issues it
spiral-bound from:   
ERGO Publications
Box 550114, Birmingham, Alabama 35255-0114     Phone 205-933-0879
... send a check for $12.75 (includes postage)
made out to Carl E. Linderholm.

The book has been reviewed in MR, mentioned in Halmos' autobiography and
by Knuth.

David L. Elliott
Disclaimer: I have nothing to gain from this except sharing a rarity.

-- 
David L. Elliott                                       [email protected]
Institute for Systems Research/ A.V. Williams Building
University of Maryland/ College Park, MD 20742

Thank you! Mr. Linderholm has moved, but a friend of mine
followed redirections and spoke to his mum, who said he'd
be back on Monday. I'll post the latest gen next week.

H.

My chum has come up with the following...

Righto. The news

Send your cheque to the following address.

        ERGO,
        2908 Hewitt Ave.
        Silver Spring.
        Maryland 20906.

The cost is $12.75 per copy for ground shipping anywhere in the
world. Carl suggests that you send the sterling equivalent based on
the spot price from a recent copy of the Financial Times. I think he's
done this before.