I was just browsing some of the material at MathWorld, following James' earlier post. I was reading about some classic unsolved problems and some classic solved problems. The Kepler Conjecture really caught my attention:

In 1611, Kepler proposed that close packing (either cubic or hexagonal close packing, both of which have maximum densities of ~74.048%) is the densest possible sphere packing, and this assertion is known as the Kepler conjecture. Finding the densest (not necessarily periodic) packing of spheres is known as the Kepler problem... Soon thereafter, Hales (1997a) published a detailed plan describing how the Kepler conjecture might be proved using a significantly different approach from earlier attempts and making extensive use of computer calculations. Hales subsequently completed a full proof, which appears in a series of papers totaling more than 250 pages (Cipra 1998) The proof relies extensively on methods from the theory of global optimization, linear programming, and interval arithmetic. The computer files containing the computer code and data files for combinatorics, interval arithmetic, and linear programs require more than 3 gigabytes of space for storage.

I'm fascinated by the emergence of computer proofs in mathematics since the 50's. A lot of mathematicians have found this unsettling: something is proved by appeal to a machine -- to the results of an algorithm. The proof is not (and cannot be) fully contained in the mind of any mathematician. It is produced by a computational oracle. As an engineer, the computational approach doesn't bother me too much. I appreciate the beauty of a rigorous, elegant mathematical proof. But a result is a result.