Proof of the proof is in the coding

An interesting dilemma has arisen in the past ten years in mathematics and it has to do with the nature of mathematical proofs. The idea of a proof was made explicit by Euclid about 300 BC -- a set of logical steps, each depending on the others and open for review. This has been the standard for mathematical proofs for 2000 years.

But propositions that require so many calculations or comparisons that they could never be completed by hand have lately been attacked using computers. The dilemma is that the soundness of the proof depends on the computer doing all these calculations without mistake -- no bugs, no hidden errors in computation or memory or output -- but this is impossible to "audit" because of its complexity.

A recent example is the proof that the most efficient way to stack oranges or canonballs or any spheres is in a pyramid (or honeycomb -- the same thing). The problem has been around since the late 1500's and the solution was proposed by Kepler. Finally, a mathematical proof has been offered but it uses computing to make the many tedious calculations that are necessary to support the proof. After a year of trying to "audit" the work, the initial reviewers of the proof gave up.

The Annals of Mathematics decided to publish only the mathematical part of the proof -- a computer science journal will publish the computational portion.

The integration of mathematical logic and computational power will continue to be used to attack difficult propositions and the challenge of verifying the results may require ... computers?