tag:blogger.com,1999:blog-3722233.post2938497816995715919..comments2022-08-09T23:53:51.029-05:00Comments on Computational Complexity: Computer Assisted Proofs- still controversial?Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-3722233.post-27856462881028991962013-05-03T04:42:45.293-05:002013-05-03T04:42:45.293-05:00As a student in the 1970's I was teached that ...As a student in the 1970's I was teached that proof - computer or man driven - will forever be striked by the 'Godel theorem' malediction.. In other words: I always lie.. is true !Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-17989556267291128022013-05-02T15:32:04.707-05:002013-05-02T15:32:04.707-05:00hi LF great post thx much for the tip on the NYT a...hi LF great post thx much for the tip on the NYT article. its great you take a sensible view on this subj but its easy to see how the mathematicians are upset about this subject. theres some really exciting stuff happening over in timothy gowers blog on this subject, really urge CS types to check it out, some major cross pollination opportunities going on.<br /><br />have been tracking this subj for many,many yrs. planning on putting up a way cool post with zillions of great links on the subj. if some who read this drop by my blog, drop me a comment & Ill write it up sooner rather than later. [can track exactly who does this by the referrer stats, wink]<br /><br />in the meantime my blog has several links on the home page on the subject.<br /><br />this also fits into what is called "empirical/experimental math" which is seeing some slow increase in spread/acceptance.<br /><br />4color proof-- one of the greats of the 20th century if you ask me!<br />thx again for the great post/topic! hope to read more on the subj in future!<br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-53601458092846734932013-05-02T09:51:31.496-05:002013-05-02T09:51:31.496-05:00There was a year-long program this year at the IAS...There was a year-long program this year at the IAS on something called homotopy type theory, which is an extension of the logic used in Coq and makes it possible to talk directly about homotopy theory and higher category theory. This makes computer-assisted proofs in these areas *much* more feasible. This spring, we did computer-assisted proofs of some basic theorems in homotopy theory, like calculating some homotopy groups of spheres. These proofs are less like Kepler or four-color, where the proof assistant is helping handle the massive number of cases, and more like the recent computer-assisted proof of the Feit-Thompson odd-order theorem, which is more traditional math that just happens to be done on a computer. In the homotopy theory specifically, it's definitely the case that we are getting new insights out of the perspective on homotopy theory provided by type theory, and the process of doing the proofs in a proof assistant. Dan Licatahttps://www.blogger.com/profile/05419342217317164459noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-654051068587270392013-05-01T13:33:55.710-05:002013-05-01T13:33:55.710-05:00I believe and hope that mechanized proofs will be ...I believe and hope that mechanized proofs will be common in math and computer science in the future. Proof assistants such as Isabell and Coq increase the trust in the results and can sometimes help to organize and develop the proof. (Like programming on paper vs. programming with a computer.)<br /><br />Are proof assistants still controversial? Absolutely. Some friends of mine are mathematicians and they are very skeptical about proof assistants. Some are claiming that formalizing proofs with them is just a waste of time since you don't get any insights. Others are claiming that it is impossible to use these tools. Another colleague who is a logician does not trust Coq because he does not understand its meta theory.<br /><br />All this reminds me of the arguments that people make against new programming languages. I think that the reasons why people make such arguments are similar: They are scared by new things that they don't understand immediately and that might change the way they work.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-40850925970919954372013-05-01T10:35:07.747-05:002013-05-01T10:35:07.747-05:00Cute!
I fixed the typo.
Actually VERY LOG might ...Cute!<br /><br />I fixed the typo.<br /><br />Actually VERY LOG might mean log(log) or log^*.<br /><br />bad idea for a blog post: what would VERY log mean? or VERY followed<br />by a function. VERY square. VERY polynomial. GASARCHhttps://www.blogger.com/profile/06134382469361359081noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-54067711367993029592013-05-01T08:59:44.151-05:002013-05-01T08:59:44.151-05:00"there have to be some statements that have v..."there have to be some statements that have very log proofs" -- so f(n) = O(log(n))! Neat! :)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-82070291831724313132013-05-01T05:39:31.479-05:002013-05-01T05:39:31.479-05:00I believe that one day formal proofs in Coq/Isabel...I believe that one day formal proofs in Coq/Isabella will be the norm and not the exceptions. You will see conference committee saying: Proofs should be 10 pages of human readable abstract + comments together with the Coq proof (with a limit of 10Gb). It will play the role that latex will play in todays submission.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-35148720306161208652013-04-30T21:13:21.172-05:002013-04-30T21:13:21.172-05:00Thomas Hale is working with a team on a fully form...Thomas Hale is working with a team on a fully formalized proof of Kepler Conj., in the proof assistant HOL Light:<br /><br />http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet<br /><br />As I (sketchily) understand it, there is no hope or intention of getting a 'simple' proof in the usual sense; in fact there is going to be significantly more case analysis and numerical work than in the original proof, because computation is cheap and this will make the proof's superstructure more manageable.Anonymousnoreply@blogger.com