tag:blogger.com,1999:blog-3722233.post114157277198344037..comments2024-09-13T12:03:08.730-05:00Comments on Computational Complexity: Computer-Assisted ProofsLance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger13125tag:blogger.com,1999:blog-3722233.post-1141856230703684532006-03-08T16:17:00.000-06:002006-03-08T16:17:00.000-06:00So the section of a proof which has been gone over...<I>So the section of a proof which has been gone over by a compiler, which has had tons of runtime checking done, and probably has some test code to boot, must on top of that have a formal proof, while the part which is simply hand-checked by extremely error-prone humans is given a free ride?</I><BR/><BR/>This makes perfect sense. While the probability of "errors" in the compilation and such may be less than of a human verifying a mathematical proof, the standards being applied to the code are typically drastically lower than that applied to a rigorous proof. By the same reasoning you apply to programs, a proof should be considered correct if 1. its English grammar and mathematical notation all parse correctly, and 2. its logic follows correctly on some number of "test" instances.<BR/><BR/>For a real proof, we need more than that, both in the less formal English description and in the explicit computer code. We need not just a general good idea for why it ought to work -- there are plenty of proofs that "ought to work" but that yield false conclusions.<BR/><BR/>- DavidAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141712815822977382006-03-07T00:26:00.000-06:002006-03-07T00:26:00.000-06:00At least Hayes' program did not use randomized Mon...At least Hayes' program did not use randomized Monte Carlo subroutines. Although it would have been fun to watch the discussion if that was the case...Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141662803158127072006-03-06T10:33:00.000-06:002006-03-06T10:33:00.000-06:00============A similar point, made pedantically als...============<BR/>A similar point, made pedantically also by Robertson, Sanders, Seymour and Thomas [as quoted in Calude, Cristian S., Calude, Elena, and Marcus, Solomon. 2001. Passages of Proof. http://arXiv.org/abs/math. HO/ 0305213], about the reliability of their 1996 computer-generated proof of 4CT, can be seen as besieged sophistry: <BR/><BR/>"However, an argument can be made that our 'proof' is not a proof in the traditional sense, because it contains steps that can never be verified by humans. In particular, we have not proved the correctness of the compiler we compiled our programs on, nor have we proved the infallibility of the hardware we ran our programs on. These have to be taken on faith, and are conceivably a source of error."<BR/><BR/>Although one may doubt whether their program is logically sound, there is no essential reason why such soundness cannot be established theoretically by competent computer scientists.<BR/><BR/>Presumably, the referees included some such scientists, and, so, were able to conclude that the salient features underlying Hales' proof could be expressed, and verified, in an appropriate axiomatic mathematical language, before being expressed in '40,000 lines of custom computer code'.<BR/><BR/>Since every step of a formal proof sequence in such languages is either an axiom, or an immediate consequence of any two preceding elements of the sequence, each step can be effectively verified mechanistically by identifying the concerned axiom, or two preceding elements of the sequence that are known to be theorems, of which it is a consequence. <BR/><BR/>So long as each step is verified as logically sound, such a procedure need not be time bound, nor limited to the conceptual ability of any one individual to grasp, or even verify, the correctness of the entire proof.<BR/><BR/>Thus, there is no sensible reason to doubt the output, even though the relation between a logically effective method and a mechanistic computation is, indeed, one of faith. <BR/><BR/>It is conceivable that an appropriately designed, and maintained, machine continuously calculating the digits of Pi may start outputting an unending series of zero's, perhaps for as long as a zillion years. Our belief that it will eventually output a digit other than zero comes about because of our faith that the machine is faithfully translating our theoretical calculations concerning the digits of Pi into a physical language of mechanical I/O devices; hence we believe, as an article of faith, and despite the physical evidence, that the series of zeros will not be unending.<BR/><BR/>So, finally, what we should place our faith in is our ability to intuitively "see" the soundness of our axiomatic assertions, and theses, at the lowest, and not, as some believe, at a sufficiently sophisticated, level of understanding. This, of course, is the distinguishing feature of, for instance, Dedekind's formulation of the Peano axioms, or - as any high-school student can testify - Euclid's axioms for geometry; except the parallel postulate, these axioms are obvious to all, even if their consequences are not.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141661370298634052006-03-06T10:09:00.000-06:002006-03-06T10:09:00.000-06:00any proof using computer verification should have ...<I>any proof using computer verification should have a formal proof of the correctness of the code</I><BR/><BR/>So the section of a proof which has been gone over by a compiler, which has had tons of runtime checking done, and probably has some test code to boot, must on top of that have a formal proof, while the part which is simply hand-checked by extremely error-prone humans is given a free ride? Forgive me for finding this as absurd double standard, but I find the idea that human-checked mathematical proofs contain fewer errors than human-reviewed code contains bugs to be quite laughable.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141644070206419992006-03-06T05:21:00.000-06:002006-03-06T05:21:00.000-06:00Hales definitely tries to address the reservations...Hales definitely tries to address the reservations cited above, see<BR/><A HREF="http://www.math.pitt.edu/~thales/flyspeck/" REL="nofollow"><BR/>http://www.math.pitt.edu/~thales/flyspeck/</A>Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141643109988622542006-03-06T05:05:00.000-06:002006-03-06T05:05:00.000-06:00-- how many proofs published in annals of mathemat...-- how many proofs published in annals of mathematics have later been found to be wrong?<BR/><BR/>Wrong question. How many proofs in AofM have been found to contain an error? LOTS!<BR/><BR/>How many have turned out to be ultimately wrong? Few.<BR/><BR/>The probability of the code having a bug is certainly > 1%, but who knows what percentage of those are minor fixable things and which ones would actually make the proof fall.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141610559207252302006-03-05T20:02:00.000-06:002006-03-05T20:02:00.000-06:00if you twist up a chaine,it will take exactly that...if you twist up a chaine,it will take exactly that many turn to straitin itAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141601089425030282006-03-05T17:24:00.000-06:002006-03-05T17:24:00.000-06:00I remember Robin Thomas giving a lecture about the...I remember Robin Thomas giving a lecture about their simplified proof of the 4-color theorem. What I took from it was that authors need to publish the proof in a computer checkable format, and then multiple referees should write an independent theorem checker to verify the results.<BR/><BR/>As long as computer assisted proofs are open sourced and indepedantly verifiable I have no problem with them. That is why I am always leery of confrence papers where authors give their latest and greatest timings without publishing the source code of their implementation.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141592018816170272006-03-05T14:53:00.000-06:002006-03-05T14:53:00.000-06:00how many proofs published in annals of mathematics...how many proofs published in annals of mathematics have later been found to be wrong?<BR/><BR/>i agree with all the comments about the odds of 40000 lines of computer code not containing a bug being much higher than 1%Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141591112974779902006-03-05T14:38:00.000-06:002006-03-05T14:38:00.000-06:00Imagine the verifier has a very hard to find bug.A...Imagine the verifier has a very hard to find bug.<BR/>As usual someone finds it.<BR/><BR/>1 - If he is honest he publishes his knowledge.<BR/>2 -If he is not honest he gains world fame by proving a famous conjecture from ...Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141584239963152402006-03-05T12:43:00.000-06:002006-03-05T12:43:00.000-06:00For those who haven't seen it before, there was re...For those who haven't seen it before, there was recently a <A HREF="http://www.inria.fr/actualites/2005/theoreme4couleurs.en.html" REL="nofollow">completely computer-checked proof of the four-color theorem</A>, using the Coq proof assistant. The proof can be checked using a proof checking program that is not specialized to the theorem statement at all. The proof also has considerable "computational" content, which is supported nicely by features of Coq's logic that make it easy to mix "computational" and "mathematical" reasoning in proofs.<BR/><BR/>I bring this up in case there are nay-sayers in the audience who don't believe that it is feasible today to check formal proofs with large computational content with today's tools. :-)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141580948127080252006-03-05T11:49:00.000-06:002006-03-05T11:49:00.000-06:0040,000 lines of atrocities such as Duff's deviceC'...<I>40,000 lines of atrocities such as Duff's device</I><BR/><BR/>C'mon, Duff's device isn't an atrocity; it's a well known idiom.<BR/><BR/>(That said, I'd be somewhat surprised to see any use for it here, and if it's being used where a compiler would already know to unroll, then it actually is an atrocity.)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1141579364386989762006-03-05T11:22:00.000-06:002006-03-05T11:22:00.000-06:00I have more faith in a computer properly executing...<I>I have more faith in a computer properly executing its code more than a mathematician verifying a proof.</I><BR/><BR/>But I have more faith in a mathematician verifying a proof than I do in mathematician with no training in software engineering writing 40,000 lines of code without a bug. I don't actually know whether Hales is a good software engineer or not, but there are far more people out there who think they know how to program than there are good programmers.<BR/><BR/><I>So any proof using computer verification should have a formal proof of the correctness of the code.</I><BR/><BR/>But one usually does not prove the correctness of code. Rather, one proves the correctness of an algorithm, and nobody implements an algorithm in 40,000 lines without a bug. Most mathematicians (and probably many computer scientists) are probably not aware of the field of software safety and formal methods for requirements specification and analysis.<BR/><BR/>"Proof by programming" is a perfectly valid technique, but the programming needs to be done by someone with training in software engineering, rather than a self-taught hacker using 40,000 lines of atrocities such as <A HREF="http://en.wikipedia.org/wiki/Duff's_device" REL="nofollow">Duff's device</A>.Anonymousnoreply@blogger.com