Computer Aided Proofs

The economist has a nice article on what it means to prove something. It talks about the proof of the Kepler conjecture being accepted into the Annals of Mathematics and what this means for the future of mathematics. The conjecture basically states that if you pack spheres into a box the same way oranges are stacked at a shop, then no other arrangement of spheres would be able to occupy more space. (without squishing the spheres of course!!) More formally it states,

(Kepler Conjecture) No packing of balls of the same radius in three dimensions has density greater than the face-centered cubic packing.

It seems very intuitive that the “shop method” is the optimal way of stacking oranges to take up the most space, however, proving this statement is another matter altogether. The history of this conjecture is very fascinating however it has recently been “solved” by Thomas C. Hales. The only problem is that the “proof” uses a computer program to solve about 100,000 linear programming problems and required 250 pages of notes and 3 gigabytes of data. The Annals of Mathematics agreed to publish the result if a series of 12 referees agreed that the proof was correct. After 4 years Gabor Fejes Tóth, the chief referee, returned a report stating that he was 99% certain of the correctness of the proof, but that the team had been unable to completely certify the proof. However, the annals has decided to publish the theoretical aspects of the proof and mention that they have not verified the computational aspects of the proof.

One Response to “Computer Aided Proofs”

  1. Administrator Says:

    Gentle reader Hemanshu, from his little village in Champaign, points out the
    PCP theorem which can be used to detect false statements with as high a probability that you like (less than 1 ofcourse). These are also used to in primality testing, to check whether a number is highly likely to be prime before using it in an encryption scheme.

Leave a Reply