"Quick and Dirty Refereeing?" by Madhu Sudan. Science, 29 August 2003, pages 1191-1192.
This article, written by the 2002 winner of the Nevanlinna Prize of the International Mathematical Union, discusses recent results in automated proof checking. Researchers have developed a procedure for making mathematical proofs checkable by computer. Once this procedure is carried out, a computer can check only a small portion of the proof and declare whether the proof is correct or whether, within a certain measure of probablity, the proof is erroneous. As Sudan notes, ``Mathematicians look to proofs for providing insight and intuition into [a] theorem and use it to develop their own theories.'' Therefore automated methods of proof-checking are not likely to replace traditional proofs that mathematicians use in their research. Nevertheless, the new proof-checking methods are having an impact in several areas, including solving optimization problems and, indirectly, improving error-correcting codes. They also provide insight into the question ``Does P equal NP?'', which is a major open question in mathematics and one of the Millennium Prize Problems of the Clay Mathematics Institute.
--- Allyn Jackson