Nicholas Thompson wrote:Marcus G. Daniels wrote: In some abstract sense, I think you can say a mathematical proof is always an algorithm. (reading the Nick/Owen offline, I see I might be in perfect opposition to Owen on this?)To me, the word algorithm suggests an emphasis on clarity and economy of effort, whereas a proof emphasizes the fact a conclusion in correct, and why. But a problem can be cast either way. Some are pretty simple (degenerate unto ridiculous?) algorithms... like a proof by example. Inductive proofs are more obviously what we think of as "algorithms". Exhaustive proofs are the most common proofs to be implemented as an algorithm (executed by human or computer). As a practical matter, plenty of algorithms have been written to *generate and test* complex logic statements, supporting the pursuit of a proof. The Four Color problem is the most well known example of a computer-assisted-proof and its correctness remains a question among many Mathematicians, but I think most Algorithmaticians (???) and Computer Geeks would believe that they can infer the accuracy of the results of the algorithms by inspecting the algorithms that generate and test the very large number of examples this particular proof requires. I believe that one of our own (Jack Horner) has written his own formal logic program to test the writings of Thomas Aquinas and has, in fact, found many of Aquinas' threads of logic to be lacking. At the risk of getting Jack in to the food fights here, I think some of the folks here would find his work in this area entertaining. http://en.wikipedia.org/wiki/Automated_theorem_prover Alas, none of this is Applied Complexity... (or is it?) - Steve PS. I am writing these long-winded missives while watching our new Laser Scanner extract millions of surface points from various test objects . Each scan takes 2-10 minutes. Just enough time to get all philosophical about matters mathematical/computational/algorithmic. I will be handing the scanner off to more practical people than I soon, and will therefore give the list a break from these ponderings. |
============================================================ FRIAM Applied Complexity Group listserv Meets Fridays 9a-11:30 at cafe at St. John's College lectures, archives, unsubscribe, maps at http://www.friam.org
