tag:blogger.com,1999:blog-3722233.post6079621552130924717..comments2024-11-14T17:42:16.782-06:00Comments on Computational Complexity: When is it worth the time and effort to verify a proof FORMALLY?Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-3722233.post-5141897028236732142024-02-29T14:25:21.906-06:002024-02-29T14:25:21.906-06:00Somewhat relevant to #6 is:
https://siliconreckon...Somewhat relevant to #6 is:<br /><br />https://siliconreckoner.substack.com/p/mechanical-understanding-of-proof<br /><br />This is more about what it means to be a proof, i.e., that understanding a proof is a lot more than just formalizing each step, than the details of proof formalization.<br /><br />I'd guess that just because a verifier says that a particular proof is correct, it wouldn't mean that mathematicians stop looking for better proofs, i.e. proofs that say something deeper about the mathematics involved in the subject of the statement being proved.<br /><br />(Think Langlands Program here.)<br /><br />An obvious example is FLT, whose proof involves translating the statement of the problem into a previously thought unrelated area of mathematics, grinding the resulting problem in that area of mathematics, and then translating back into the original form.<br /><br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-15659908756179679832024-02-28T14:55:37.817-06:002024-02-28T14:55:37.817-06:00Coq got its name from the first 3 letters of one o...Coq got its name from the first 3 letters of one of the authors of the original paper. John Cherniavskynoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-445123634691959392024-02-27T11:33:56.576-06:002024-02-27T11:33:56.576-06:00Terry Tao gave a great talk on machine-assisted pr...Terry Tao gave a great talk on machine-assisted proofs at the Joint Math Meetings last month. See: https://www.youtube.com/watch?v=AayZuuDDKP0<br /><br />He describes the whole process as taking roughly 3 weeks for the Marton-polynomial-Freiman-Rusza conjecture resolution involving many individuals, including entering a chunk of the core math background. That effort made it much easier to subsequently improve a constant (from 12 to 11), close some small gaps in how they had stated things, and also identified a simpler intermediate property involving a smaller hammer for part of the proof (since the large hammer they had used would have been a lot more work in Lean) that seems likely to be useful elsewhere.<br /><br />He suggests that while LLMs are wholly unreliable in coming up with sound arguments themselves right now, using them to help with converting things to Lean is already useful.<br /><br />LLMs may also be useful in converting Lean arguments into readable math proofs.<br /><br />Obviously, these big theorems are worth spending the time now - it just requires the theorem to be sufficiently attractive for the community to take part. (My current favorite to have this done would be last year's bounds for 3-term arithmetic progressions of Kelley-Meka with simplifications, for example.) The implication is that as the body of math already in Lean grows, the extra effort is going to get smaller quite soon. <br />Paul Beamehttps://www.cs.washington.edu/people/faculty/beamenoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-25318935513620826482024-02-26T20:31:24.500-06:002024-02-26T20:31:24.500-06:00The end goal should be that all mathematical resul...The end goal should be that all mathematical results, historical and current, and their proofs are formalized (or, the result shown not to have been proved.)Paul F. Dietzhttps://www.blogger.com/profile/11277406923777545793noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-86315930400298201732024-02-26T18:31:55.988-06:002024-02-26T18:31:55.988-06:00> The Coq proof assistant (see here). This was ...> The Coq proof assistant (see here). This was used to verify the proof of<br />> the four-color theorem, see here.<br /><br />Considering<br /><br />http://blog.computationalcomplexity.org/2021/08/do-four-colors-suffice.html<br /><br />one might wonder what exactly they proved. Looking at<br /><br />https://www.ams.org/notices/200811/tx081101382p.pdf<br /><br />we find<br /><br />"Definition 4. A point is a corner of a map if and only if it belongs to the closures of at least three regions.<br /><br />"The definition of 'corner' allows for contiguous points, to allow for boundaries with accumulation points, such as the curve sin 1/x."<br /><br />I guess they can make any definitions they want to, but that isn't how I would define "corner". David Marcushttps://www.blogger.com/profile/07084520656051241766noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-65941803022684584722024-02-25T18:52:01.309-06:002024-02-25T18:52:01.309-06:00Also Coq is being renamed to Rocq (short for Rocqu...Also Coq is being renamed to Rocq (short for Rocquencourt) because (according to https://github.com/coq/coq/wiki/Alternative-names) its previous name led to women being harassed with dick jokes and leaving the project.D. Eppsteinhttps://www.blogger.com/profile/11923501729858669855noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-24747124288927981072024-02-25T18:46:54.195-06:002024-02-25T18:46:54.195-06:00Isn't this really just the same judgement we m...Isn't this really just the same judgement we make all the time as to whether a proof should add more detail? We balance the amount it would add to our convinction the proof was correct with the effort and other costs.<br /><br />But the price for formal verification is still absurdly high.TruePathhttps://www.blogger.com/profile/00124043164362758796noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-10604168905174792532024-02-25T14:55:00.706-06:002024-02-25T14:55:00.706-06:00Before posting I did many google searches to find ...Before posting I did many google searches to find out if they are related but could not find anything. They are both still alive so I could email or call them, though that seems nosy. Hopefully one of them will see this post!Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-11017824292494303292024-02-25T14:25:31.794-06:002024-02-25T14:25:31.794-06:00Actually Wikipedia biographies often do discuss ma...Actually Wikipedia biographies often do discuss mathematical blood relatives, when they can be properly sourced. For instance the articles on the three Kuperbergs all mention each other. If you can find a publication describing a relation between Alfred Hales and Thomas Hales, please let me know.D. Eppsteinhttps://www.blogger.com/profile/11923501729858669855noreply@blogger.com