>I'm not sure if you would consider that a major result, but the inexistence >of a projective plane of order 10 was proved using a computer. I don't know >of any other proof. I think that also a tiny part of the classification of >the finite simple groups depends on computing, namely the existence of some >of the sporadic groups was established only by using a computer.
I seem to recall that a famous problem in Logic has been (recently?) proved with computers. (I will try to find information and come back). Also, I recall that a Conway's student tried once to construct the r. 65537-gon using a computer.
I located Conway's posting, so let him tell us the story:
Subject: Re: 17 sides From: John Conway <conway@math.Princeton.EDU> Date: Tue, 4 Nov 1997 12:26:51 -0500 (EST) To: email@example.com
On Tue, 28 Oct 1997, Bradley Brock wrote:
> > How could Gauss find the length of the 17-side polygon side??? > > On a related note: > I remember that one of my friends in grad school > showed John Conway the output from a little > Mathematica program that gave the sides of > the 257-gon. > > Brad
Forgive me for not replying to this before now. It obviously refers to John Steinke, who was a graduate student here some time ago, and is a bit misleading. What happened was that I proposed to him the problem of finding a publishable construction for the 65537-gon, and suggested various methods, and he did the 257-gon as a baby-example.
You are probably aware of the fact that Hermes worked for many years on finding a construction for the 65537-gon. I don't really believe the legend, that this was because his teacher told him to "go away and don't bother me again until you've found how to construct a regular 65537-gon!", but many years ago I did see in Gottingen a cardboard box that was said to contain Hermes's work on the problem.
However, I can hardly believe that he really got anywhere, because the size of the problem is much bigger than one might suppose. I did work out, though, a way of phrasing the solution that could probably fit into 20 closely-written pages, and could definitely be found nowadays by computer. However, I think Steinke lost interest in the problem and I never tried to persuade anyone else to do it.
It's obvious from the start that there's a "solution" in the form of a set of 16 quadratic equations, the coefficients of each being functions of the roots of the previous ones. The trouble is that those functions get pretty complicated, and it would take a very large book to write them all down in that form. Let for instance a,A ; b,B; c,C be the roots of the first three. Then the general element of the field they generate is a linear combination with rational coefficients of the 8 numbers
abc, abC, aBc, aBC, Abc, AbC, ABc, ABC
and so to specify the (two) coefficients of the next equation is to give a list of 16 rational numbers (which we can actually make be integers). In a similar way, to specify the coefficients of the 14th equation we'll need 2^14 = 16384 integers.
My proposed form of the solution involves going about half-way, to about the 8th equation, in this manner, thereby setting up names for all elements of the subfield of degree 256. Then one works from the other end, working out the quadratic saisfied by a particular 65537th root of unity over the next field down, and so on. Let's call it Z - then this equation is t^2 - (Z + Z^-1)t + 1 = 0, and so we invent a name, Y, for Z + Z^-1. In the same way, we invent names for the coefficients of the quadratic defining Y, and so on. By the time we get half-way, we'll've define Z, Z^-1, Y, ... in terms of about 512 numbers in the degree 256 subfield. So the solution reduces to writing out the length 256 names of each of these 512 numbers.
I would very much like to see this calculation done, since there might well be some patterns that would enable one to write down the answer more simply than the way sketched above.
Additionally, let me quote the first sentence of the last paragraph of Duane W. DeTemple's paper [1, p. 107]:
<q> 4. Remarks on the Construction of the Regular 65537-gon. We have already observed that g = 3 is a primitive root of p = 65537. The sum, product, and relative order of period pairs must then be computed (one feels sorry for the computerless Hermes!). </q>
1. Duane W. DeTemple: Carlyle Circles and the Lemoine Simplicity. The Americn Mathematical Monthly 98(1991) 97 - 108.
Note: DDeT refers to several regular heptakaidecagon constructions, but not to that one (Lebesgue's) I posted earlier.