<div>First, a picky but pertinent point: Fermat's Last Theorem wasn't done by machine. It was Andrew Wiles, at Princeton. The story is that he broke up a major work into Least Publishable Units, and set to work on FLT in secret, submitting a LPU once in awhile so his colleagues woudn't be suspicious. Then after announcing the result at the Newton Institute in England, wrinkles were discovered, and there was a couple years of intense labor, speculation, and unprecedended (for us) media coverage. The final work is two huge book-sized papers which would prerequire a couple years of Arithmetic Algebraic Geometry to be able to read, that is, few of us other than AAGeometers will ever be able to read it.
</div>
<div> </div>
<div>Yet this daunting thing was produced by humans, not machine. It's still virtually intractable.</div>
<div> </div>
<div>The Classification of Finite Simple Groups project is a modern legend. The finished result is in **thousands** of papers published by hundreds of algebarists, and last I heard some bits were still being combed over but it's generally accepted as a Done Deal (there is a new project to try and simplify it). The largest of the "Sporadic" Finite Simple Groups is the Monster; it's order has factors of all the primes, 2, 3, 5, up to 31. consecutively, then with 5 more prime factors skipping a bit among 37 through 67. The total order is too big a number to describe meaningfully in casual email (the exponent of 2 is a double-digit number, for starters).
</div>
<div> </div>
<div>We don't need computers to do this kind of harrowing work; computers just make it easier :-)</div>
<div> </div>
<div>For centuries (since Euler) there was an open problem, The Four Color Map Theorem (or Conjecture). How many colors do you need to color a map so that countries that share a border (longer than a single point) have different colors? The answer is 4. Cartographers knew this for millenia; they could color maps that way, and it matters alot to printers. But Euler himself could not prove it. He did classify all graphs (maps reduce to graphs; an edge between nodes is a border between countries) into a short list of special cases that would be sufficient to prove the theorem. Unfortunately many of those special cases were so huge that nobody could color them by hand. It took a computer, and this was done in the late 70's, at Northwestern I think, when Robert and I were students, and maybe we both attended that talk at Duke. 
</div>
<div> </div>
<div>That result brought Robert's concern out in the open: do we believe a proof that is too long for us to personally verify ourselves?  With Wiles and the group classification thing and some other such work, we've realized that machines aren't required. It is a practical impossibility for me to verify Wiles' work; in principle, maybe I could in, say, a decade. To verify the 4 color theorem would take me centuries. But really that's just a matter of degree.
</div>
<div> </div>
<div>What came out of the soul-searching is that we believe the process that generated the result (which may involve code, hardware, peer-review, reproducible measurements....) instead of the pile of generated paper. I can read the source code at Northwestern, verify that, read over Euler's list, verify that,. and then know that the correct algorithm applied to the correct material will give a correct result.; Then I could run it on my own machine to check hardware did not affect the result.
</div>
<div> </div>
<div>It made a lot of us very uncomfortable, but we left behind the day when everyone could read everything for himself, sometime between Guttenburg and Leibnitz's Monadology. </div>
<div> </div>
<div>Peter</div>
<div><br><br> </div>
<div><span class="gmail_quote">On 3/22/07, <b class="gmail_sendername">Robert G. Brown</b> <<a href="mailto:rgb@phy.duke.edu">rgb@phy.duke.edu</a>> wrote:</span>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">On Thu, 22 Mar 2007, Peter St. John wrote:<br><br>> Well to me that's the point. My brain is too small for 500Kx500K matrices
<br>> over a ring of 22 degree polynomials, too. So we throw a 16-node computer at<br>> it and crush it under the hobnailed jack-boots of Higher Mathematics.<br>> I wish I know more about the SAGE (machine) that hosts the SAGE (software)
<br>> that was used for this, but apparently <a href="http://washington.edu">washington.edu</a>'s web server can't<br>> handle the CNN exposure as well as their number cruncher can crunch numbers.<br>> They are still down.
<br><br>In the case of E8, using a computer is probably necessary, although one<br>would require a wetware interface to make the slightest bit of "sense"<br>out of the results anyway.<br><br>I do find this trend depressing, though.  Fermat's lost theorem proven
<br>using computing -- nothing elegant, just crush it underfoot, as you say.<br>E8.  Next we'll hear that the Goldbach Conjecture is finally proven by<br>virtue of solving 10^17 specific cases and exploiting a proof that once
<br>you have all of those cases proven you can iterate the result to<br>infinity somehow, or we'll hear of the Riemann Hypothesis being solved<br>this way -- nothing elegant, nothing that is (actually) of any USE.  We
<br>all know that these are true anyway, at least as well as we know that<br>the theory of gravitation is true.  In neither case can they be proven<br>(yet, in the case of the math, never in the case of gravity), in both<br>
cases they are known beyond any reasonable doubt via induction (see<br>Polya's lovely books on induction and mathematical reasoning).  Proving<br>these things by computer adds nothing to this -- in addition to the near
<br>impossibility of actually judging the computational results (deep bugs<br>remaining a ubiquitous possibility in ALL complex computer code) which<br>always leaves a sliver of doubt even then, that doubt (expressed as<br>
Jaynesian/Bayesian "degree of belief" on an information<br>theoretic/entropic basis) is already so small that it hardly changes on<br>a log scale from having done an exhaustive computation.<br><br>In the SPECIFIC case of E8 that isn't quite true.  Since string theory
<br>as a theory of everything (TOE) may be covered by E8, and since string<br>theory is reportedly insanely complex and so big that exploring it to<br>find the RIGHT decomposition into whatever \times SU(whatever) by hand
<br>might take lifetimes, it is barely possible that being able to enumerate<br>it even electronically will permit a systematic search to be performed<br>that can eliminate huge blocks of the possibilities and home in on what
<br>we can at least HOPE is a small set of decompositions.  Ideally a<br>single, unique decomposition.<br><br>That would actually be pretty cool.  For the first time in pretty much<br>forever, we'd have an actual CANDIDATE TOE, and yet another important
<br>step in "the end of physics" will have occurred.  (And note well the<br>quotes, please -- I'm not suggesting that physics research will come<br>close to ending with a TOE, only that it will finally have a firm known
<br>basic foundation.<br><br>   rgb<br><br>> Peter<br>><br>><br>> On 3/22/07, Robert G. Brown <<a href="mailto:rgb@phy.duke.edu">rgb@phy.duke.edu</a>> wrote:<br>>><br>>> On Wed, 21 Mar 2007, Peter St. John wrote:
<br>>><br>>> > Times have sure changed; with Wiles and Fermat's Last Theorm in<br>>> newspapers<br>>> > for over a year, then "A Beautiful Mind" from Hollywood; it's almost not
<br>>> > surprising that the solution of a difficult math problem is mentioned at<br>>> > CNN.com.<br>>> ><br>>> > The Exceptional Lie Group E8 computation just got done (some info at<br>
>> > <a href="http://www.aimath.org/E8/computerdetails.html">http://www.aimath.org/E8/computerdetails.html</a> about the details of the<br>>> > computation itself). Reference to the system SAGE is a bit ambiguous;
<br>>> it's<br>>> > the name of a symbolic mathematics package and apparently also a 16-node<br>>> > system at the same University of Washington. Natually I was curious<br>>> about<br>>> > the computer, but ironically, it seems that while they can handle a
<br>>> matrix<br>>> > with half a million rows and colums each (and each entry is a polynomial<br>>> of<br>>> > degree up to 22, with 7 digit coeficients), their departmental web<br>>> server
<br>>> > can't handle the load of all of CNN's readership browsing at once :-)<br>>> ><br>>> > The group E8 itself, together with some explanation of the recent news,<br>>> is<br>>> > in wiki, 
<a href="http://en.wikipedia.org/wiki/E8_%28mathematics%29">http://en.wikipedia.org/wiki/E8_%28mathematics%29</a><br>>> ><br>>> > Dr Brown might explain better than I could how sometimes the best way to<br>
>> > understand a thing is to break it down into simple groups of symmetries.<br>>><br>>> Don't you be puttin' that off on me now.  I get off of that particular<br>>> bus somewhere around the SU(N) stop, with rare excursions over into
<br>>> point groups on the other side of the tracks.  Unitary, yes.<br>>> Orthogonal, why not.  SL(2,C) even.  Strictly UNexceptional.<br>>><br>>> > Apparently, one of the funky things about E8 is that the "easiest way to
<br>>> > understand it" is itself.<br>>><br>>> Yeah, and like I have a brain that can manage ~500,000x500,000<br>>> complicated polynomial objects.  Thanks, I think... but not.<br>>><br>
>>    rgb<br>>><br>>> ><br>>> > Peter<br>>> ><br>>><br>>> --<br>>> Robert G. Brown                        <a href="http://www.phy.duke.edu/~rgb/">http://www.phy.duke.edu/~rgb/
</a><br>>> Duke University Dept. of Physics, Box 90305<br>>> Durham, N.C. 27708-0305<br>>> Phone: 1-919-660-2567  Fax: 919-660-2525     <a href="mailto:email:rgb@phy.duke.edu">email:rgb@phy.duke.edu</a><br>
>><br>>><br>>><br>><br><br>--<br>Robert G. Brown                        <a href="http://www.phy.duke.edu/~rgb/">http://www.phy.duke.edu/~rgb/</a><br>Duke University Dept. of Physics, Box 90305<br>Durham, 
N.C. 27708-0305<br>Phone: 1-919-660-2567  Fax: 919-660-2525     <a href="mailto:email:rgb@phy.duke.edu">email:rgb@phy.duke.edu</a><br><br><br></blockquote></div><br>