A propos of the discussion on computer proofs, let me add a small footnote.
The "Kiss Precise" or "4-Circles Theorem" concerns 4 circles each tangent to the other 3. Its explicit statement occurs 1st in Descartes, but it is implicit in earlier work and has been rediscovered several times since, notably by Solly the Nobel Prize-winning chemist who announced it in verse in "Nature" (June 20, 1936) and gave it the name "Kiss Precise".
Let Ci be te curvature of the ith circle. Then the theorem states:
It is now a simple matter to prove this by computer means.
If the four centres are all joined, 4 triangles result, of which the largest has an area equal to the sum of the other 3.
Use Heron's formula to express this fact and then clear the resulting equation of square roots. This gives a 16th degree polynomial, and this may be factored to give (after a little human interpretation) the result.
This proof was first implemented by my former colleague Colin McIntosh using MAPLE. Even back then (1991) the computer time was under 3 minutes. Nowadays it wopuld be negligible.
> > >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: firstname.lastname@example.org > > 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. > > John Conway > > ----------------------------------------------------------------------------- > > 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. > > > Antreas >