The article talks about the Four Color Theorem, which is usually presented as "Any map can be colored in four colors". I suspect that an automated proof of the Four Color Theorem dos not prove that statement as stated. I suspect it rather proves some complicated and ugly statement about graphs. It would be nice if these upcoming proof systems would provide a way to start with a simple statement like "Any map can be colored in four colors" or something recognizably similar, and go through the steps of defining what that means so that the original statement is proved as opposed to some contorted mathese restatement that questionably represents the original idea. ----- Original Message ----- From: "Schroeppel, Richard" <rschroe@sandia.gov> To: "'math-fun'" <math-fun@mailman.xmission.com> Sent: Wednesday, November 19, 2008 2:45 PM Subject: [math-fun] automated proof checking
The December Notices of the AMS has four articles about automated checking of mathematical proofs. Taken together, they assert that the tools are nearly ready for prime time. Download & startup details are included for the adventurous. Julie Rehmeyer (Math Trek/Science News) has an introductory article at http://www.sciencenews.org/view/generic/id/38623/title/ Math_Trek__How_to_(really)_trust_a_mathematical_proof that includes pointers to the AMS articles.
The articles make a plausible case that most individual math results could be verified with merely an unreasonable dedication (i.e., less than an impossible effort). The corollary is that (eventually) unverified results should not be submitted for review. There's lip service to the notion that math is more than (definition,theorem,proof)*, but not much more. One of the articles is about the proof of the Four Color Theorem -- the effort of formalization, and new mathematics developed along the way. The article demotes diagrams to second class objects, with character strings and syntax trees being "real". :-! There's serious work underway on things like checking the classification of simple groups and the Odd Order Theorem. The Prime Number Theorem has been verified both ways (the Erdos-Selberg elementary proof, and the Riemann Zeta Function based proof). This uses a considerable base of results about integrals and complex analytic functions. There's even some attention given to making systems that are somewhat usable, and working with theorems and proofs that are sort of readable.
This seems to be progress, at the level of being able to (someday soon) check our results. The downside is that these folks have a hammer, and non-nails don't exist.
Rich
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
-------------------------------------------------------------------------------- No virus found in this incoming message. Checked by AVG - http://www.avg.com Version: 8.0.175 / Virus Database: 270.9.9/1802 - Release Date: 11/20/2008 7:28 PM