Computers and Proof
Formal proof is an interesting process, and a rising dilemma for mathematicians. The big issue: Should we accept computer-augmented proofs?
Concerns first arose in 1976 when Appel and Haken used a computer (exhaustion techniques) to prove the four color theorem. It involved thousands of lines of computer code and took over 1200 hours to run. As humans could not replicate or check the 400-page proof, many felt it was "questionable" until Georges Gonthier gave a formal proof in 2005.
And recently, Hales used a computer to prove Kepler's conjecture about sphere-packing. It only involved 300 pages and 40,000 lines of computer code. A team of mathematicians tried to validate the proof over several years and "will not be able to certify it in the future, because they have run out of energy to devote to the problem."
Would you accept a computer's proof? How would you validate it? Reminds me of the student's attempt to use an exhaustive list to prove that the number of primes is infinite...not sure they are done yet...with or without a computer!